An axiomatization of full computation tree logic
The paper deals with the logic CTL\(^*\), also called the full computation tree logic. It was introduced by Emerson and Sistla (1984) and has been mainly studied as a tool for specification and verification of complex systems in computer science and practice. The main problem regarding those applications is that of model checking (i.e., the question if a state satisfies a given formula). NEWLINENEWLINENEWLINEThe problem studied here is motivated by more classical questions of logic, it concerns validity (or satisfiability) and the relevant (Hilbert-style) axiomatization. Though the validity problem for CTL\(^*\) was known decidable, the existence of a simple, sound and complete axiomatization has been a long standing open problem -- and this is solved by the present paper. NEWLINENEWLINENEWLINEThe author uses the known axiomatization system for CTL\(^*\) with a more general semantics (i.e., the logic \(\forall\)LTFC [\textit{C. Stirling}, ``Modal and temporal logics, in: S. Abramsky et al. (eds.), Handbook of logic in computer science. Vol. 2, 477-563 (1992; Zbl 0777.68001)]), and adds an axiom (scheme) and a rule to achieve a sound and complete system for CTL\(^*\) with the standard semantics (on Kripke structures with total accessibility relation). The axiom expressess (the expected) limit closure while the main novelty is the rule -- called the Auxiliary Atoms rule. The main technical part then deals with showing completeness of the system. The author also provides an informal overview of the proof and comparison with techniques used previously for related results.
- R-generability, and definability in branching time logics
- A finite axiomatization of the set of strongly valid Ockhamist formulas
- Branching-time logic with quantification over branches: The point of view of modal logic
- Decidability for branching time
- Deciding full branching time logic
- Handbook of philosophical logic. Volume II: Extensions of classical logic
- scientific article; zbMATH DE number 747023 (Why is no real title available?)
- Non-definability of the class of complete bundled trees
- Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
- Testing and generating infinite sequences by a finite automaton
- Multi-modal CTL: completeness, complexity, and an application
- Axiomatising extended computation tree logic
- Mathematical modal logic: A view of its evolution
- Sublogics of a branching time logic of robustness
- Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
- An approach to infinitary temporal proof theory
- A compositional approach to CTL^* verification
- Propositional Q-logic
- A propositional probabilistic logic with discrete linear time for reasoning about evidence
- Intention as commitment toward time
- A propositional dynamic logic for instantial neighborhood semantics
- A survey on temporal logics for specifying and verifying real-time systems
- A propositional linear time logic with time flow isomorphic to ^2
- Quantification over sets of possible worlds in branching-time semantics
- An axiomatization of PCTL*
- A rooted tableau for \(\mathrm{BCTL}^*\)
- Decidability and expressivity of Ockhamist propositional dynamic logics
- Completeness and decidability results for CTL in constructive type theory
- Axiomatization of a branching time logic with indistinguishability relations
- Branching time? Pruning time!
- A Labeled Natural Deduction System for a Fragment of CTL *
- Verifying Time and Communication Costs of Rule-Based Reasoners
- A tableau-based decision procedure for CTL^*
- scientific article; zbMATH DE number 2015275 (Why is no real title available?)
- Information dynamics and uniform substitution
- Completeness and complexity of multi-modal CTL
- Probabilistic Temporal Logics
- Системы временной логики I: моменты, истории, деревья
- scientific article; zbMATH DE number 7407777 (Why is no real title available?)
- A complete axiomatisation for quantifier-free separation logic
- Rewrite rules for \(\mathrm{CTL}^\ast\)
- Probabilistic logics based on Riesz spaces
- A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
- Axiomatising extended computation tree logic
- From the archives of the formal methods and tools lab. Axiomatising and contextualising ACTL
- Completeness of a branching-time logic with possible choices
- Probabilistic temporal logic with countably additive semantics
- (Heterogeneous) structured specifications in logics without interpolation
- Next-time coalition logic
- Axiomatising tree-interpretable structures
- Deontic action logic, atomic Boolean algebras and fault-tolerance
- Algebraic neighbourhood logic
- Deductive verification of alternating systems
This page was built for publication: An axiomatization of full computation tree logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2758043)
