A hierarchy of temporal logics with past

DOI10.1016/0304-3975(95)00035-UzbMath0873.68068OpenAlexW1998387957WikidataQ126298498 ScholiaQ126298498MaRDI QIDQ672329

Ph Schnoebelen, François Laroussinie

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(95)00035-u

zbMATH Keywords

temporal logics

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items (23)

Axiomatization of a branching time logic with indistinguishability relations ⋮ Back from the future ⋮ Temporal Logic and Fair Discrete Systems ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ On the Hybrid Extension of CTL and CTL + ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ \textit{Once} and \textit{for all} ⋮ Interval vs. Point Temporal Logic Model Checking ⋮ About the expressive power of CTL combinators ⋮ Translations between modal logics of reactive systems ⋮ Hybrid and First-Order Complete Extensions of CaRet ⋮ Alternating-time temporal logics with linear past ⋮ Event Identifier Logic ⋮ Unnamed Item ⋮ Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions ⋮ The Complexity of CTL* + Linear Past ⋮ CaRet With Forgettable Past ⋮ On the Complexity of Branching-Time Logics ⋮ The modalized Heyting calculus: a conservative modal extension of the Intuitionistic Logic ★ ⋮ Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past ⋮ An axiomatization of PCTL* ⋮ Branching-time logics repeatedly referring to states ⋮ Specification in CTL + past for verification in CTL.

Cites Work

• Translations between modal logics of reactive systems
• The temporal logic of branching time
• Characterizing finite Kripke structures in propositional temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Decision procedures and expressiveness in the temporal logic of branching time
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• A new algebraic semantic approach and some adequate connectives for computation with temporal logic over discrete time
• Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
• Characterization of temporal property classes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A hierarchy of temporal logics with past