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

zbMATH Keywords

decidabilitytableauxCTLfinitely bounded semantics

Mathematics Subject Classification ID

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

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)

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

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)