Deterministic omega-regular liveness properties.
Frank Nießner, Ulrich Ultes‐Nitsche, Peter Ochsenschläger · 1997
A major drawback for the use of automated verification techniques is the complexity of verification algorithms in general. One of the sources of the algorithms' complexity is the difference between the language classes accepted by deterministic and nondeterministic Büchi-automata respectively. This difference causes the problem of complementing Büchi-automata and hence deciding subset conditions on regular !-languages to be PSPACE-complete. We investigate in this paper whether nontrivial property classes exist that can be characterized by deterministic Büchi-automata and hence be complemented rather easily. Since the class of safety properties is known to be representable deterministically, taking into account that safety properties are the closed sets in the Cantor topology, it suffices for us to identify nontrivial deterministic !-regular liveness properties.