\textit{Once} and \textit{for all}
From MaRDI portal
Publication:439961
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
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}
