Safety, liveness and fairness in temporal logic

DOI10.1007/BF01211865zbMath0820.68077MaRDI QIDQ1343862

A. Prasad Sistla

Publication date: 9 February 1995

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

safety properties; liveness properties; verification of concurrent programs; temporal formula

Mathematics Subject Classification ID

68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

68T27: Logic in artificial intelligence

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations, On High-Quality Synthesis, Arbitrary arrow update logic, Deciding safety and liveness in TPTL, Linear temporal logic symbolic model checking, \(\omega\)-regular languages are testable with a constant number of queries, On the refinement of liveness properties of distributed systems, Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective, On the limits of refinement-testing for model-checking CSP, Using temporal logics to express search control knowledge for planning, A brief account of runtime verification, From complementation to certification, Unnamed Item, An abstract interpretation-based model for safety semantics, Translating Testing Theories for Concurrent Systems, Falsification of LTL Safety Properties in Hybrid Systems

Cites Work

• Defining liveness
• Safety without stuttering
• Recognizing safety and liveness
• Completing the temporal picture
• Modalities for model checking: Branching time logic strikes back
• Alternative semantics for temporal logics
• Can message buffers be axiomatized in linear temporal logic?
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• The complexity of propositional linear temporal logics
• Proving Liveness Properties of Concurrent Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item