Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
type: Item
instance of: scholarly article
title: Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
author: Alex Abuin
author: Alexander Bolotov
author: M. Hermo
author: P. Lucio
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2022-11-16T00:00:00Z
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7618127
zbMATH Keywords: temporal logic
zbMATH Keywords: fairness
zbMATH Keywords: branching-time
zbMATH Keywords: certified model checking
Wikidata QID: Q115188987
describes a project that uses: Dafny
describes a project that uses: TTM
MaRDI profile type: Publication
full work available at URL: j.jlamp.2022.100828
OpenAlex ID: W4307038540
cites work: One-Pass Tableaux for Computation Tree Logic
cites work: Q5322945
cites work: The temporal logic of branching time
cites work: Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
cites work: Characterizing finite Kripke structures in propositional temporal logic
cites work: Symbolic model checking: \(10^{20}\) states and beyond
cites work: Using branching time temporal logic to synthesize synchronization skeletons
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Q4385542
cites work: Decision procedures and expressiveness in the temporal logic of branching time
cites work: “Sometimes” and “not never” revisited
cites work: Tableau methods of proof for modal logics
cites work: Q3674621
cites work: Dual systems of tableaux and sequents for PLTL
cites work: From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
cites work: And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL
cites work: Tableau methods for modal and temporal logics
cites work: An axiomatization of ECTL
cites work: Q5672218
cites work: Verification from Declarative Specifications Using Logic Programming
cites work: Dafny: An Automatic Program Verifier for Functional Correctness
cites work: Q3838819
cites work: The complexity of propositional linear temporal logics
cites work: Q5560258
cites work: Q3710510
cites work: Towards certified model checking for PLTL using one-pass tableaux
DOI: 10.1016/J.JLAMP.2022.100828
description: scientific article; zbMATH DE number 7618127