Temporal logic properties can be broadly categorized into safety and liveness properties. Informally, safety properties state that a “bad thing” never happens whereas liveness properties state that a “good thing” must eventually happen. These informal definitions are made precise in the paper Defining Liveness (Alpern, Schneider, 1985), and are also discussed in a later paper, Decomposing Properties into Safety and Liveness using Predicate Logic (Schneider, 1987). Formalizing Safety a...
