Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

A Lattice-Theoretic Approach to Safety and Liveness

Panagiotis Manolios and Richard Trefler.
Twenty-Second ACM Symposium on Principles of Distributed Computing (PODC 2003), pages 325-333. ACM Press, July 2003. © ACM, 2003.

Abstract

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 notions in the 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 lattice-theoretic 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 w-regular string and tree languages.


Gzipped Postscript (69K) © ACM.
PDF (177K) © ACM.
Postscript (179K) © ACM.