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

DOI10.1007/s00165-011-0193-4zbMath1242.68302OpenAlexW2043154866MaRDI 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 reasoningtableaubranching timeCTL\(^*\)

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (7)

A Tableau for Bundled Strategies ⋮ To be fair, use bundles ⋮ Expressiveness and succinctness of a logic of robustness ⋮ 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}^+\) ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\)

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

This page was built for publication: A tableau-based decision procedure for CTL\(^*\)