manolios@cc.gatech.edu
College of Computing
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.
|
Last modified: Mon Jun 21 10:58:16 EDT 2004
manolios@cc.gatech.edu |
College of Computing |