One-Pass Tableaux for Computation Tree Logic

DOI10.1007/978-3-540-75560-9_5MaRDI QIDQ3498455zbMATH OpenOpenAlexFDO

Authors Pietro Abate, Rajeev Goré, Florian Widmann

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75560-9_5

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Logic in computer science (03B70)

Recommendations

• A tableau-based decision procedure for CTL^*
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• A faster tableau for \(\mathrm{CTL}^{\ast}\)
• scientific article; zbMATH DE number 1189110
• A Tableau for Bundled CTL

Cites work

• A clausal resolution method for branching-time logic \(\text{ECTL}^+\)
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• About cut elimination for logics of common knowledge
• Automata-theoretic techniques for modal logics of programs
• BDD-based decision procedures for the modal logic K ★
• Clausal temporal resolution
• Cut-free common knowledge
• Decision procedures and expressiveness in the temporal logic of branching time
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• How to optimize proof-search in modal logics
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 67500 (Why is no real title available?)
• scientific article; zbMATH DE number 1765664 (Why is no real title available?)
• Optimizing description logic subsumption
• Proceedings of the 1st international workshop on Symbolic model checking (SMC '99), as part of the 2nd federated logic conference (FLoC '99). Trento, Italy, July 6, 1999
• Temporal logic can be more expressive
• The temporal logic of branching time

Cited in

(21)

• Syntactic cut-elimination for common knowledge
• Dual systems of tableaux and sequents for PLTL
• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• Efficient SAT-based minimal model generation methods for modal logic S5
• And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
• The proof theory of common knowledge
• Invariant-free clausal temporal resolution
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• A tableau-based decision procedure for CTL^*
• A tableau calculus for first-order branching time logic
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• Syntactic cut-elimination for common knowledge
• Modal logic S5 satisfiability in answer set programming
• Extending fairness expressibility of ECTL^+: a tree-style one-pass tableau approach
• A Refined Resolution Calculus for CTL
• A resolution calculus for the branching-time temporal logic CTL
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• One-pass Context-based Tableaux Systems for CTL and ECTL
• Towards certified model checking for PLTL using one-pass tableaux
• Verified tableaux: from modal logics to modal fixpoint logics

This page was built for publication: One-Pass Tableaux for Computation Tree Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3498455)