Safety and Liveness in Branching Time
Panagiotis Manolios and Richard J. Trefler.
In Joseph Halpern, editor, Logic in Computer Science. LICS 2001, pages 366-374. IEEE Computer Society, June 2001. © IEEE, 2001.
We extend the Alpern and Schneider linear time characterization of safety and liveness properties to branching time, where properties are sets of trees. We define two closure operators that give rise to the following four extremal types of properties: universally safe, existentially safe, universally live, and existentially live. The distinction between universal and existential properties captures the difference between the CTL path quantifiers A (for all paths) and E (there is a path). We show that every branching time property is the intersection of an existentially safe property and an existentially live property, a universally safe property and a universally live property, and an existentially safe property and a universally live property. We also examine how our closure operators behave on linear time properties.
We then focus on sets of finitely branching trees and show that our
closure operators agree on linear time safety properties.
Furthermore, if a set of trees is given implicitly as a Rabin tree
automaton, B, we show that it is possible to compute the
Rabin automata corresponding to the closures of the language of B.
This allows us to effectively compute B-safe and
B-live such that the language of B is the
intersection of the languages of B-safe and
B-live. As above, B-safe and
B-live can be chosen so that their languages are
existentially safe and existentially live, universally safe and
universally live, or existentially safe and universally live.
Gzipped Postscript (58K)