R. Negulescu and J. A. Brzozowski
Relative Liveness: From Intuition to Automated Verification

Research Report CS-95-32
Department of Computer Science
University of Waterloo
Waterloo, Ontario, Canada N2L 3G1
50 pp., July 1995


We point out deficiencies of previous treatments of liveness. We define a new liveness condition in two forms: one based on finite trace theory, and the other on automata. We prove the equivalence of these two definitions. We also introduce a safety condition and provide modular and hierarchical verification theorems for both safety and liveness. Finally, we present a verification algorithm for liveness.

Download this report (compressed postscript).

Go back to publications index.
Go back to Maveric home page.