McNaughton's Theorem

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 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.

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.

One direction of the theorem can be proven by showing that any given Muller automaton recognizes an ω-regular language.

Suppose A = (Q,Σ,δ,q₀,F) is a deterministic Muller automaton. The union of finitely many ω-regular languages produces an ω-regular language, therefore it can be assumed w.l.o.g. that the Muller acceptance condition F contains exactly one set of states {q₁, ... ,q_n}. Let α be the regular language whose elements will take A from q₀ to q₁. For 1≤i≤n, let β_i be a regular language whose elements take A from q_i to q_{(i mod n)+1} without passing through any state outside of {q₁, ... ,q_n}. It is claimed that α(β₁ ... β_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 which 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 t₁, t₂, ... such that for each a and b, ρ(t_na+b) = q_b. Such a sequence exists because all the states of {q₁, ... ,q_n} 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 an element of α(β₁ ... β_n)^ω.

...
Wikipedia