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.
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.