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

\(\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, Falsification of LTL Safety Properties in Hybrid Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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