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