A Decision Procedure for CTL* Based on Tableaux and Automata

DOI10.1007/978-3-642-14203-1_28zbMath1257.03035OpenAlexW1534088363MaRDI QIDQ5747771

Oliver Friedmann, Markus Latte, Martin Lange

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_28

Mathematics Subject Classification ID

2-person games (91A05) Automata and formal grammars in connection with logical questions (03D05) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items (12)

A Tableau for Bundled Strategies ⋮ Branching Time? Pruning Time! ⋮ Logic programming approach to automata-based decision procedures ⋮ To be fair, use bundles ⋮ Branching-time logics with path relativisation ⋮ Expressiveness and succinctness of a logic of robustness ⋮ A tableau-based decision procedure for CTL\(^*\) ⋮ Unnamed Item ⋮ 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}^+\) ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ A Rooted Tableau for BCTL*

Cites Work

• Unnamed Item
• Unnamed Item
• Alternating finite automata on \(\omega\)-words
• Automata, logics, and infinite games. A guide to current research
• An axiomatization of full Computation Tree Logic
• Complementation, Disambiguation, and Determinization of Büchi Automata Unified
• Tighter Bounds for the Determinisation of Büchi Automata
• Solving Parity Games in Practice
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• The Complexity of Tree Automata and Logics of Programs
• Solving Parity Games in Big Steps
• A Sound and Complete Deductive System for CTL* Verification

This page was built for publication: A Decision Procedure for CTL* Based on Tableaux and Automata