A lattice-theoretic characterization of safety and liveness

The distinction between safety and liveness properties is due to Lamport who gave the following informal characterization. Safety properties assert that nothing bad ever happens while liveness properties assert that something good happens eventually. In a well-known paper Alpern and Schneider gave a topological characterization of safety and liveness for the linear time framework. Gumm has stated these nothe more abstract setting of ∨-complete Boolean algebras. Recently, we characterized safety and liveness for the branching time framework and found that neither the topological characterization nor Gumm’s characterization were general enough for our needs. We present a latticetheoretic characterization that allows us to unify previous results on safety and liveness, including the results for the linear time and branching time frameworks and for ω-regular string and tree languages. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying...

• Type: Conference
• Year: 2003
• Where: PODC
• Authors: Panagiotis Manolios, Richard J. Trefler
• Keywords: Distributed And Parallel Computing, PODC 2003, Safety, Time Frameworks, Topological Characterization