Safety, liveness and fairness in temporal logic

Citations Over Time

Abstract

Abstract In this paper we present syntactic characterization of temporal formulas that express various properties of interest in the verification of concurrent programs. Such a characterization helps us in choosing the right techniques for proving correctness with respect to these properties. The properties that we consider include safety properties, liveness properties and fairness properties. We also present algorithms for checking if a given temporal formula expresses any of these properties.

Related Papers

• → Alternating-time temporal logic(2002)313 cited
• Temporal and Dynamic Logic(2010)
• → Reasoning about actions in dynamic linear time temporal logic(2001)42 cited
• → Temporal Logic(1991)
• → Handling of Past and Future with Phenesthe+(2023)