consists of all ω-words in Σω in which 1 occurs only finitely many times. A non-deterministic Büchi automaton recognizing L needs only two states q0 (the initial state) and q1. Δ consists of the triples (q0,0,q0), (q0,1,q0), (q0,0,q1) and (q1,0,q1). F = {q1}. For any input α in which 1 occurs only finitely many times, there is a run that stays in state q0 as long as there are 1s to read, and goes to state q1 afterwards. This run is successful. If there are infinitely many 1s, then there is only one possible run: the one that always stays in state q0. (Once the machine has left q0 and reached q1, it cannot return. If another 1 is read, there is no successor state.) Notice that above language cannot be recognized by a deterministic Büchi automaton, which is strictly less expressive than its non-deterministic counterpart. Expressive power of ω-automata An ω-language over a finite alphabet Σ is a set of ω-words over Σ, i.e. it is a subset of Σω. An ω-language over Σ is said to be recognized by an ω-automaton A (with the same alphabet) if it is the set of all ω-words accepted by A. The expressive power of a class of ω-automata is measured by the class of all ω-languages that can be recognized by some automaton in the class. The nondeterministic Büchi, parity, Rabin, Streett, and Muller automata, respectively, all recognize exactly the same class of ω-languages. These are known as the ω-Kleene closure of the regular languages or as the regular ω-languages. Using different proofs it can also be shown that the deterministic parity, Rabin, Streett, and Muller automata all recognize the regular ω-languages. It follows from this that the class of regular ω-languages is closed under complementation. However, the example above shows that the class of deterministic Büchi automata is strictly weaker. Conversion between ω-automata Because nondeterministic Muller, Rabin, Streett, parity, and Büchi automata are equally expressive, they can be translated to each other. Let us use the following abbreviation : for example, NB stands for nondeterministic Büchi ω-automaton, while DP stands for deterministic parity ω-automaton. Then the following holds. Clearly, any deterministic automaton can be viewed as a nondeterministic one. with no blow-up in the state space. with a polynomial blow-up in the state space, i.e., the number of states in the resulting NB is , where is the number of