\textit{Once} and \textit{for all}

DOI10.1016/j.jcss.2011.08.006zbMath1245.03022OpenAlexW2165306422MaRDI QIDQ439961

Moshe Y. Vardi, Amir Pnueli, Orna Kupferman

Publication date: 17 August 2012

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2011.08.006

zbMATH Keywords

temporal logicexpressive powerdecision proceduresalternating automatapast-time operators

Mathematics Subject Classification ID

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

Related Items (9)

Unnamed Item ⋮ Unnamed Item ⋮ Interval vs. Point Temporal Logic Model Checking ⋮ On weighted first-order logics with discounting ⋮ Alternating-time temporal logics with linear past ⋮ Reasoning about XML with temporal logics and automata ⋮ Unnamed Item ⋮ Cycle detection in computation tree logic ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A hierarchy of temporal logics with past
• Automata-theoretic techniques for modal logics of programs
• Alternating automata on infinite trees
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Propositional dynamic logic of regular programs
• Reasoning about infinite computations
• Temporal logic in specification. Altrincham, UK, April 8-10, 1987. Proceedings
• Specification in CTL + past for verification in CTL.
• Decision procedures and expressiveness in the temporal logic of branching time
• Temporal logic can be more expressive
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
• An automata-theoretic approach to branching-time model checking
• The Complexity of CTL* + Linear Past

This page was built for publication: \textit{Once} and \textit{for all}