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

DOI10.4230/lipics.time.2020.14zbMath1530.03068OpenAlexW3089732952MaRDI QIDQ6060101

Alexander Bolotov, Montserrat Hermo, Alex Abuin, Paqui Lucio

Publication date: 2 November 2023

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

zbMATH Keywords

fairnesstemporal logicexpressivenessbranching-time

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The temporal logic of branching time
• Dual systems of tableaux and sequents for PLTL
• Using branching time temporal logic to synthesize synchronization skeletons
• Symbolic model checking: \(10^{20}\) states and beyond
• 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
• And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
• One-Pass Tableaux for Computation Tree Logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• An axiomatization of ECTL

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