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.[1] 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.
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,Σ,δ,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 .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 . 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 appear after time t1, and for each a and b, ρ(tna+b) = qb. Such a sequence exists because all and only the states of 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 α(β1 ... βn)ω.
Conversely, suppose w ∈ α(β1 ... βn)ω. Due to definition of α, there is an initial segment of w that is an element of α and thus leads A to the state q1. From there on, the run never assumes a state outside of, 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=a1a2... ∈ αβω. Let w(i,j) be the finite segment ai+1,...,aj-1aj of w. For building a Muller automaton for αβω, we introduce the following two concepts with respect to w.
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.
We have used both the concepts of "favor" and "equivalence" in Lemma 2. Now, we are going to use the lemma to construct a Muller automaton for language αβω. The proposed automaton will accept a word if and only if a time i exists such that it will satisfy the right hand side of Lemma 2. The machine below is described informally. Note that this machine will be a deterministic Muller automaton.
The machine contains p+2 deterministic finite automaton and a master controller, where p is the size of Aβ*. One of the p+2 machine can recognize αβ* and this machine gets input in every cycle. And, it communicates at any time i to the master controller whether or not w(0,i) ∈ αβ*. The rest of p+1 machines are copies of Aβ*. The master can set the Aβ* machines dormant or active. If master sets a Aβ* machine to be dormant then it remains in its initial state and oblivious to the input. If master activates a Aβ* machine then it reads the input and moves, until master makes it dormant and force it back to the initial state. Master can make a Aβ* machine active and dormant as many times as it wants. The master stores the following information about the Aβ* machines at each time instant.
Initially, the master may behave 2 different ways depending on α. If α contains empty word then only one of the Aβ* is active otherwise none of the Aβ* machines are active at the start. Later at some time i, if w(0,i) ∈ αβ* and none of Aβ* machines are in initial state then master activates one of the dormant machines and the just activated Aβ* machine start receiving input from time i+1. At some time, if two Aβ* machines reach to the same state then master makes the machine dormant that was activated later than the other. Note that the master can make the above decisions using the information it stores.
For the output, the master also have a pair of red and green lights corresponding to each Aβ* machine. If a Aβ* machine goes from active state to dormant state then corresponding red light flashes. The green light for some Aβ* machine M, which was activated at j, flashes at time i in the following two situations:
Note that the green light for M does not flash every time when a machine goes dormant due to M.
The above description of a full machine can be viewed as a large deterministic automaton. Now, it is left to define the Muller acceptance condition. In this large automaton, we define μn to be the set of states in which the green light flashes and the red light does not flash corresponding to nth Aβ* machine. Let νn be the set of states in which the red light does not flash corresponding to nth Aβ* machine. So, Muller acceptance condition F = . This finishes the construction of the desired Muller automaton. Q.E.D.
Since McNaughton's proof, many other proofs have been proposed. The following are some of them.