BTL₂ and the expressive power of ECTL^+

DOI10.1016/J.IC.2005.07.006MaRDI QIDQ2500472zbMATH OpenOpenAlexFDO

Authors Alexander Rabinovich, Philippe Schnoebelen

Publication date 16 August 2006

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2005.07.006

zbMATH Keywords

expressivity of branching-time temporal logicmodel checking

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• On the Expressive Power of QLTL
• CTL^* and ECTL^* as fragments of the modal -calculus
• About the expressive power of CTL combinators
• scientific article; zbMATH DE number 139986
• scientific article; zbMATH DE number 7440178
• Flat fragments of CTL and CTL: separating the expressive and distinguishing powers
• On the expressive power of \textsc{Klaim}-based calculi
• On the expressive power of \textsc{Klaim}-based calculi

Cites work

• An application of games to the completeness problem for formalized theories
• An infinite hierarchy of temporal logics over branching time
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Counting on CTL^*: On the expressive power of monadic path logic
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Decision procedures and expressiveness in the temporal logic of branching time
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• First-order logic with two variables and unary temporal logic
• Future temporal logic needs infinitely many modalities
• scientific article; zbMATH DE number 1705163 (Why is no real title available?)
• scientific article; zbMATH DE number 3888913 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 4027441 (Why is no real title available?)
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2038753 (Why is no real title available?)
• scientific article; zbMATH DE number 1927553 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• scientific article; zbMATH DE number 2112984 (Why is no real title available?)
• scientific article; zbMATH DE number 2196601 (Why is no real title available?)
• Modalities for model checking: Branching time logic strikes back
• Model checking a path (preliminary report)
• Monadic Logic of Order over Naturals has no Finite Base
• The complexity of propositional linear temporal logics
• The complexity of propositional linear temporal logics in simple cases
• The decision problem for branching time logic
• The polynomial-time hierarchy
• The temporal logic of branching time
• “Sometimes” and “not never” revisited

Cited in

(6)

• CTL^* and ECTL^* as fragments of the modal -calculus
• scientific article; zbMATH DE number 4119616 (Why is no real title available?)
• Branching-time logics and fairness, revisited
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• A clausal resolution method for branching-time logic \(\text{ECTL}^+\)
• Arity hierarchy for temporal logics

This page was built for publication: \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)

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