An axiomatization of full Computation Tree Logic

DOI10.2307/2695091zbMath1002.03015OpenAlexW2153737593MaRDI QIDQ2758043

M. A. Reynolds

Publication date: 7 January 2003

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.666.2813

zbMATH Keywords

completenessvaliditysemanticsKripke structurestemporal logicsatisfiabilityaxiomatizationfull computation tree logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (32)

Axiomatization of a branching time logic with indistinguishability relations ⋮ Deontic action logic, atomic Boolean algebras and fault-tolerance ⋮ Branching Time? Pruning Time! ⋮ Системы временной логики I: моменты, истории, деревья ⋮ Unnamed Item ⋮ A propositional probabilistic logic with discrete linear time for reasoning about evidence ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Completeness of a branching-time logic with possible choices ⋮ A tableau-based decision procedure for CTL\(^*\) ⋮ Mathematical modal logic: A view of its evolution ⋮ A propositional linear time logic with time flow isomorphic to \(\omega^2\) ⋮ Algebraic neighbourhood logic ⋮ Information dynamics and uniform substitution ⋮ Deductive verification of alternating systems ⋮ Sublogics of a branching time logic of robustness ⋮ Intention as commitment toward time ⋮ Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ An approach to infinitary temporal proof theory ⋮ A compositional approach to CTL\(^*\) verification ⋮ A Decision Procedure for CTL* Based on Tableaux and Automata ⋮ Quantification over sets of possible worlds in branching-time semantics ⋮ A Labeled Natural Deduction System for a Fragment of CTL * ⋮ Verifying Time and Communication Costs of Rule-Based Reasoners ⋮ A Rooted Tableau for BCTL* ⋮ Decidability and Expressivity of Ockhamist Propositional Dynamic Logics ⋮ A propositional dynamic logic for instantial neighborhood semantics ⋮ An axiomatization of PCTL* ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Propositional \(\text Q\)-logic ⋮ Probabilistic Temporal Logics

Cites Work

• Unnamed Item
• Handbook of philosophical logic. Volume II: Extensions of classical logic
• A finite axiomatization of the set of strongly valid Ockhamist formulas
• Decidability for branching time
• \(R\)-generability, and definability in branching time logics
• Deciding full branching time logic
• Non-definability of the class of complete bundled trees
• Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
• Branching-time logic with quantification over branches: The point of view of modal logic
• Testing and generating infinite sequences by a finite automaton

This page was built for publication: An axiomatization of full Computation Tree Logic