One-pass Context-based Tableaux Systems for CTL and ECTL

DOI10.4230/LIPICS.TIME.2020.14MaRDI QIDQ6060101zbMATH OpenOpenAlexFDO

Authors Alex Abuin, Alexander Bolotov, M. Hermo, P. Lucio

Publication date 2 November 2023

Full work available at URL https://dblp.uni-trier.de/db/conf/time/time2020.html#AbuinBHL20

zbMATH Keywords

branching-timeexpressivenessfairnesstemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• One-Pass Tableaux for Computation Tree Logic
• Extending fairness expressibility of ECTL^+: a tree-style one-pass tableau approach
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• A tableau-based decision procedure for CTL^*
• A faster tableau for \(\mathrm{CTL}^{\ast}\)

Cites work

• An axiomatization of ECTL
• And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• Decision procedures and expressiveness in the temporal logic of branching time
• Dual systems of tableaux and sequents for PLTL
• scientific article; zbMATH DE number 3937153 (Why is no real title available?)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• One-Pass Tableaux for Computation Tree Logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Tableau methods for modal and temporal logics
• The complexity of propositional linear temporal logics
• The temporal logic of branching time
• Towards certified model checking for PLTL using one-pass tableaux
• Using branching time temporal logic to synthesize synchronization skeletons
• “Sometimes” and “not never” revisited

Cited in

(3)

• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• One-pass and tree-shaped tableau systems for \(\mathrm{TPTL}\) and \(\mathrm{TPTL}_b+\mathrm{Past}\)
• A Tableau for Bundled CTL

This page was built for publication: One-pass Context-based Tableaux Systems for CTL and ECTL

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