A complete characterization of deterministic regular liveness properties

Many systems can be modeled formally by nondeterministic Buchi-automata. The complexity of model checking then essentially depends on deciding subset conditions on languages that are recognizable by these automata and that represent the system behavior and the desired properties of the system. The involved complementation process may lead to an exponential blow-up in the size of the automata. We investigate a rich subclass of properties, called deterministic regular liveness properties, for which complementation at most doubles the automaton size if the properties are represented by deterministic Buchi-automata. In this paper, we will present a decomposition theorem for this language class that entails a complete characterization of the deterministic regular liveness properties, and extend an existing incomplete result which then, too, characterizes the deterministic regular liveness properties completely. (C) 2007 Elsevier B.V. All rights reserved.