Decomposing Properties into Safety and Liveness Using Predicate Logic

摘要

Two classes of properties are of particular interest when considering programs: safety properties and liveness properties. Informally, a safety property stipulates that 'bad things' do not happen during execution of a program and a liveness property stipulates that 'good things' do happen (eventually). Distinguishing between safety and liveness properties is useful because knowing whether a property is safety or liveness helps when deciding how to prove that the property holds for a program. A new proof is given that every property can be expressed as a conjunction of safety and liveness properties. The proof is in terms of first-order predicate logic.