Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models

DOI10.1016/J.JLAMP.2022.100828OpenAlexW4307038540WikidataQ115188987 ScholiaQ115188987MaRDI QIDQ2095426FDOQ2095426

M. Hermo, Alexander Bolotov, Alex Abuin, P. 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

zbMATH Keywords

fairnesstemporal logicbranching-timecertified model checking

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Dafny: An Automatic Program Verifier for Functional Correctness
• Characterizing finite Kripke structures in propositional temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• The complexity of propositional linear temporal logics
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Using branching time temporal logic to synthesize synchronization skeletons
• Decision procedures and expressiveness in the temporal logic of branching time
• “Sometimes” and “not never” revisited
• The temporal logic of branching time
• Tableau methods for modal and temporal logics
• Dual systems of tableaux and sequents for PLTL
• One-Pass Tableaux for Computation Tree Logic
• Tableau methods of proof for modal logics
• Verification from Declarative Specifications Using Logic Programming
• Towards certified model checking for PLTL using one-pass tableaux
• From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
• An axiomatization of ECTL

Cited In (2)

• Preface to selected papers from 20th workshop on programming and languages (PROLE 2021)
• A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL

Uses Software

• Dafny
• TTM

This page was built for publication: Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models

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