Safety, liveness and fairness in temporal logic

DOI10.1007/BF01211865zbMath0820.68077OpenAlexW2131064738MaRDI QIDQ1343862

A. Prasad Sistla

Publication date: 9 February 1995

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

Full work available at URL: https://doi.org/10.1007/bf01211865

zbMATH Keywords

safety propertiesliveness propertiesverification of concurrent programstemporal formula

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Spanning the spectrum from safety to liveness, Translating Testing Theories for Concurrent Systems, Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective, A brief account of runtime verification, Arbitrary arrow update logic, Exhaustive property oriented model-based testing with symbolic finite state machines, On monitoring linear temporal properties, Deciding safety and liveness in TPTL, Quantitative safety and liveness, A first-order logic characterization of safety and co-safety languages, On the limits of refinement-testing for model-checking CSP, A first-order logic characterisation of safety and co-safety languages, Linear temporal logic symbolic model checking, An abstract interpretation-based model for safety semantics, Using temporal logics to express search control knowledge for planning, On relative and probabilistic finite counterability, The complexity of counting models of linear-time temporal logic, Unnamed Item, Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations, On High-Quality Synthesis, \(\omega\)-regular languages are testable with a constant number of queries, Sensing as a Complexity Measure, Falsification of LTL Safety Properties in Hybrid Systems, Efficient data validation for geographical interlocking systems, On the refinement of liveness properties of distributed systems, From complementation to certification

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