Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach

DOI10.4230/LIPIcs.TIME.2018.5zbMath1487.68154OpenAlexW2898734050MaRDI QIDQ5079769

Paqui Lucio, Alexander Bolotov, Montserrat Hermo

Publication date: 28 May 2022

Full work available at URL: https://doi.org/10.4230/LIPIcs.TIME.2018.5

zbMATH Keywords

fairnesstemporal logictableaubranching-timeone-pass tableau

Mathematics Subject Classification ID

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

Related Items (1)

Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)

Uses Software

• TTM
• Rabinizer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut-free sequent systems for temporal logic
• Dual systems of tableaux and sequents for PLTL
• FM 2009: Formal methods. Second world congress, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings
• Decision procedures and expressiveness in the temporal logic of branching time
• Model-based testing of reactive systems. Advanced lectures.
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• Rabinizer 2: Small Deterministic Automata for LTL ∖ GU

This page was built for publication: Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach