McNaughton's theorem

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 without loss of generality 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 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 t₁, t₂, ... such that only states in {q₁, ... ,q_n'} appear after time t₁, and for each a and b, ρ(t_na+b) = q_b. Such a sequence exists because all and only 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)^ω.

Conversely, suppose w ∈ α(β₁ ... β_n)^ω. Due to definition of α, there is an initial segment of w that is an element of α and thus leads A to the state q₁. From there on, the run never assumes a state outside of {q₁, ... ,q_n}, due to the definitions of the β's, and all the states in the set are repeated infinitely often. Therefore, A accepts the word w.

The other direction of the theorem can be proven by showing that there exists a deterministic Muller automaton that recognizes a given ω-regular language.

The union of finitely many deterministic Muller automata can be easily constructed; therefore without loss of generality we assume that the given ω-regular language is of the form αβ^ω. Consider an ω-word w=a₁a₂... ∈ αβ^ω. Let w(i,j) be the finite segment a_i+1,...,a_j-1a_j of w. For building a Muller automaton for αβ^ω, we introduce the following two concepts with respect to w.

Favor

A time j favors time i if j > i, w(0,i) ∈ αβ*, and w(i,j) ∈ β*.

Equivalence

E(i,j,k), or i is equivalent to j as judged at time k, if i,j ≤ k, w(0,i) ∈ αβ*,w(0,j) ∈ αβ*, and for every word x in Σ*, w(i,k)x ∈ β* if and only if w(j,k)x ∈ β*. It is easy to note that if E(i,j,k) then for all k < l, E(i,j,l). In other words, if i and j are ever judged to be equivalent then they will stay equivalent thereafter. And also for the same l, l favors i if and only if l favors j. Let E(i,j) if there exists a k such that E(i,j,k).

Let p be the number of states in the minimum deterministic finite automaton A^β* to recognize language β*. Now we prove two lemmas about the above two concepts.

Lemma 1

For any time k, among the times i,j < k such that w(0,i) and w(0,j) ∈ αβ*, the number of equivalence classes induced by E(i,j,k) is bounded by p. Also the number of equivalence classes induced by E(i,j) is bounded by p.

Proof: The finite automaton A^β* is minimum; therefore it does not contain equivalent states. Let i and j be such that w(0,i) and w(0,j) ∈ αβ* and E(i,j,k). Then, words w(i,k) and w(j,k) will have to take A^β* to the same state starting from the initial state. Hence, first part of lemma is true. The second part is proved by contradiction. Let's suppose there are p+1 times i₁,...,i_p+1 such that no two of them are equivalent. For l > max(i₁,...,i_p+1), we would have, for each m and n, not E(i_m,i_n,l). Therefore there would be p+1 equivalence classes, as judged at l, contradicting the first part of the lemma.

Lemma 2

w ∈ αβ^ω if and only if there exists a time i such that there are infinitely many times equivalent to i and favoring i.

Proof: Let's suppose w ∈ αβ^ω then there exists a strictly increasing sequence of times i₀,i₁,i₂,... such that w(0,i₀) ∈ α and w(i_n,i_n+1) ∈ β. Therefore, for all n > m, w(i_m,i_n) ∈ β* and i_n favors i_m. So, all the i's are members of one of the finitely many equivalence classes (shown in Lemma 1). So, there must be an infinite subset of all i's that belongs to same class. The smallest member of this subset satisfies the right hand side of this lemma.

Conversely, suppose in w, there are infinitely many times that are equivalent to i and favoring i. From those times, we will construct a strictly increasing and infinite sequence of times i₀,i₁,i₂,... such that w(0,i₀) ∈ αβ* and w(i_n,i_n+1) ∈ β*. Therefore w would be in αβ^ω. We define this sequence by induction:

Base case: w(0,i) ∈ αβ* because i is in a equivalence class. So, we set i₀=i. We set i₁ such that i₁ favors i₀ and E(i₀,i₁). So, w(i₀,i₁) ∈ β*.

Induction step: Suppose E(i₀,i_n). So, there exists a time i' such that E(i₀,i_n,i'). We set i_n+1 such that i_n+1 > i', i_n+1 favors i₀, and E(i₀,i_n+1). So, w(i₀,i_n+1) ∈ β* and, since i_n+1 > i' we have by definition of E(i₀,i_n,i'), w(i_n,i_n+1) ∈ β*.

Since McNaughton's proof, many other proofs have been proposed. The following are some of them.

• ω-regular languages can be shown equiv-expressive to Büchi automata. Büchi automata can be shown to equiv-expressive to semi-deterministic Büchi automata. Semi-deterministic Büchi automata can be shown to be equiv-expressive to deterministic Muller automata. This proof follows the same lines as the above proof.
• Safra's construction transforms a non-deterministic Büchi automaton to a deterministic Rabin automaton.[2] This construction is known to be optimal.
• There is a purely algebraic proof[3] of McNaughton's theorem.