Deterministic ω-regular liveness properties

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 inthe Cantor topology, it suffices for us to identify nontrivial deterministic ω-regular liveness properties