Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
From MaRDI portal
Publication:1989347
DOI10.1016/j.tcs.2020.02.015zbMath1433.03049OpenAlexW3006352198MaRDI QIDQ1989347
Alexander Bolotov, Paqui Lucio, Montserrat Hermo
Publication date: 21 April 2020
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2020.02.015
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items (2)
One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A tableau-based decision procedure for CTL\(^*\)
- Rewrite rules for \(\mathrm{CTL}^\ast\)
- 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.
- One-Pass Tableaux for Computation Tree Logic
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- “Sometimes” and “not never” revisited
- Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach
- Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
- An automata-theoretic approach to branching-time model checking
- A Decision Procedure for CTL* Based on Tableaux and Automata
This page was built for publication: Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
