On characterization of safety and liveness properties in temporal logic
Aravinda Prasad Sistla · 1985
In the verification of concurrent programs two kinds of properties are of primary importance and have been extensively investigated([3]): safety properties and liveness properties.Safety properties assert that something bad never happens while liveness properties assert that something good will eventually happen.In this paper we investigate the possibility of syntactically characterizing safety properties and liveness properties in temporal logic.A formal definition for safety properties was first given by Lamport and a slightly less restrictive definition is given in [5].We cony sider the later definition which states that a formula f in temporal logic expresses a safety property iff the following condition is satisfied: f holds on a a sequence iff every prefix of this sequence can be extended to satisfy the formula.We also consider a stronger definition of safety properties called strong safety properties.We show that the set of strong safety properties that can be expressed in propositional temporal logic are exactly those properties which are expressed by formulae built using the modality G("always"), the propositional connectives A,v and atomic propositions or their negations.