A tableau-based decision procedure for CTL\(^*\)

DOI10.1007/s00165-011-0193-4zbMath1242.68302MaRDI QIDQ432138

M. A. Reynolds

Publication date: 3 July 2012

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-011-0193-4

zbMATH Keywords

automated reasoning; tableau; branching time; CTL\(^*\)

Mathematics Subject Classification ID

68T27: Logic in artificial intelligence

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

Related Items

Expressiveness and succinctness of a logic of robustness, A resolution calculus for the branching-time temporal logic CTL, Rewrite rules for \(\mathrm{CTL}^\ast\), Sublogics of a branching time logic of robustness, Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\), To be fair, use bundles, A Tableau for Bundled Strategies

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using branching time temporal logic to synthesize synchronization skeletons
• Proof methods for modal and intuitionistic logics
• Alternative semantics for temporal logics
• Decision procedures and expressiveness in the temporal logic of branching time
• An axiomatization of PCTL*
• An axiomatization of full Computation Tree Logic
• A Tableau for Bundled CTL
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• The Complexity of Tree Automata and Logics of Programs
• A Decision Procedure for CTL* Based on Tableaux and Automata