CTL with finitely bounded semantics

DOI10.4230/LIPICS.TIME.2017.14MaRDI QIDQ6487463zbMATH OpenFDO

Authors Valentin Goranko, Antti Kuusisto, Raine Rönnholm

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPICS.TIME.2017.14

zbMATH Keywords

CTLdecidabilityfinitely bounded semanticstableaux

Mathematics Subject Classification ID

Temporal logic (03B44) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Alternating-time temporal logic ATL with finitely bounded semantics
• A faster tableau for \(\mathrm{CTL}^{\ast}\)
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• A tableau-based decision procedure for CTL^*
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata

Cited in

(4)

• Bounded game-theoretic semantics for modal mu-calculus
• Game-theoretic semantics for \(\mathrm{ATL}^+\) with applications to model checking
• Alternating-time temporal logic ATL with finitely bounded semantics
• Flat fragments of CTL and CTL: separating the expressive and distinguishing powers

This page was built for publication: CTL with finitely bounded semantics

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