Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
From MaRDI portal
Publication:2095426
DOI10.1016/j.jlamp.2022.100828OpenAlexW4307038540WikidataQ115188987 ScholiaQ115188987MaRDI QIDQ2095426
Montserrat Hermo, Alexander Bolotov, Alex Abuin, Paqui Lucio
Publication date: 16 November 2022
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2022.100828
Uses Software
Cites Work
- The temporal logic of branching time
- Dual systems of tableaux and sequents for PLTL
- Using branching time temporal logic to synthesize synchronization skeletons
- Characterizing finite Kripke structures in propositional temporal logic
- 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
- Tableau methods of proof for modal logics
- Dafny: An Automatic Program Verifier for Functional Correctness
- And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
- From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
- 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
- Verification from Declarative Specifications Using Logic Programming
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
