In the literature, I have only found a formal definition for safety properties in LTL. This, essentially, boils down to the following: every trace that violates the property has a finite prefix attesting this violation. This, indeed, works nicely for LTL, which is based on traces. What about CTL? For properties that can be equivalently expressed in LTL and in CTL, the definition safety in CTL can be given by transposing that from LTL. What about the ones that are not expressible in LTL?For instance, AG p is clearly a safety property, when p is a state predicate. What about AG EF p? If the property is violated, then there exists a finite trace ending in a state, from which no state satisfying p is reachable. Also, assuming there is a definition of safety in CTL, is there a syntactic characterisation of such properties?
Safety properties in CTL
program verification;temporal logic;linear temporal logic