In automata theory, McNaughton's theorem refers to a theorem that asserts that the set of ω-regular languages is identical to the set of languages recognizable by deterministic Muller automata. This theorem is proven by supplying an algorithm to construct a deterministic Muller automaton for any ω-regular language and vice versa. This theorem has many important consequences. Since (non-deterministic) Büchi automata and ω-regular languages are equally expressive, the theorem implies that Büchi automata and deterministic Muller automata are equally expressive. Since complementation of deterministic Muller automata is trivial, the theorem implies that Büchi automata/ω-regular languages are closed under complementation. Original statement In McNaughton's original paper, the theorem was stated as: "An ω-event is regular if and only if it is finite-state." In modern terminology, ω-events are commonly referred to as ω-languages. Following McNaughton's definition, an ω-event is a finite-state event if there exists a deterministic Muller automaton that recognizes it. Constructing an ω-regular language from a deterministic Muller automaton One direction of the theorem can be proven by showing that any given Muller automaton recognizes an ω-regular language. Suppose A = (Q,Σ,δ,q0,F) is a deterministic Muller automaton. The union of finitely many ω-regular languages produces an ω-regular language; therefore it can be assumed without loss of generality that the Muller acceptance condition F contains exactly one set of states {q1, ... ,qn}. Let α be the regular language whose elements will take A from q0 to q1. For 1≤i≤n, let βi be a regular language whose elements take A from qi to q(i mod n)+1 without passing through any state outside of {q1, ... ,qn}. It is claimed that α(β1 ... βn)ω is the ω-regular language recognized by the Muller automaton A. It is proved as follows. Suppose w is a word accepted by A. Let ρ be the run that led to the acceptance of w. For a time instant t, let ρ(t) be the state visited by ρ at time t. We create an infinite and strictly increasing sequence of time instants t1, t2, ... such that only states in {q1, ... ,qn'} appear after time t1, and for each a and b, ρ(tna+b) = qb. Such a sequence exists because all and only the states of {q1, ... ,qn} appear in ρ infinitely often. By the above definitions of α and β's, it can be easily shown that the existence of such a sequence implies that w is