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

DOI10.1016/J.JCSS.2011.08.006MaRDI QIDQ439961zbMATH OpenOpenAlexFDO

Authors Orna Kupferman, Amir Pnueli, Moshe Y. Vardi

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

alternating automatadecision proceduresexpressive powerpast-time operatorstemporal logic

Mathematics Subject Classification ID

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

Recommendations

• A hierarchy of temporal logics with past
• A branching time logic with past operators
• Past is for free: on the complexity of verifying linear temporal properties with past
• Past is for free: On the complexity of verifying linear temporal properties with past
• The Complexity of CTL* + Linear Past

Cites work

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

Cited in

(23)

• An extended branching-time Ockhamist temporal logic
• Cycle detection in computation tree logic
• Specification in CTL + past for verification in CTL.
• Alternating-time temporal logics with linear past
• On weighted first-order logics with discounting
• Past is for free: on the complexity of verifying linear temporal properties with past
• Back from the future
• Expressive power of ``now and ``then operators
• A quick axiomatisation of LTL with past
• Branching-time type operators on finite pseudo-Boolean algebras
• On the Complexity of Branching-Time Logics
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• Ockhamist Computational Logic: Past-Sensitive Necessitation in CTL
• scientific article; zbMATH DE number 1471238 (Why is no real title available?)
• Interval vs. point temporal logic model checking. An expressiveness comparison
• A one-pass tree-shaped tableau for LTL+past
• Flow logic
• scientific article; zbMATH DE number 7439738 (Why is no real title available?)
• Results on alternating-time temporal logics with linear past
• Flow logic
• Semipositive LTL with an Uninterpreted Past Operator
• A hierarchy of temporal logics with past
• Reasoning about XML with temporal logics and automata

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

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