McNaughton's Theorem
Encyclopedia
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 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.
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 w.l.o.g. 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 which led to the acceptance of w. For a time instant t, let ρ(t) is the state visited by ρ at time t. We create an infinite and strictly increasing sequence of time instants t1, t2, ... such that for each a and b, ρ(tna+b) = qb. Such a sequence exists because all 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 an element of α(β1 ... βn)ω.
Suppose w ∈ α(β1 ... βn)ω. Due to definition of α, there is an initial segment of w that is an element of α and leads A to the state q1. From there on, the run never assumes a state outside of {q1, ... ,qn}, due to the definitions of β's, and all the states in the set are repeated infinitely often. Therefore, A accepts the word w.
The union of finitely many deterministic Muller automata can be easily constructed therefore w.l.o.g. we assume that the given ω-regular language is of the form αβω. Let's suppose ω-word w=a1,a2,... ∈ αβω. Let w(i,j) be the finite segment ai+1,...,aj-1,aj of w. For building a Muller automaton for αβω, we introduce the following two concepts with respect to w.
Favor
Equivalence
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
Lemma 2
a Muller automaton for language αβω. The proposed automaton will accept a word iff 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 initial state and becomes oblivious to the input. If master activates a Aβ* machine then it keeps reading the input move, 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 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.
Lemma 3
Lemma 4
Lemma 5
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 = { S | ∃n μn ⊆ S ⊆ νn }. This finishes the construction of the desired Muller automaton. Q.E.D.
Automata theory
In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...
, McNaughton's theorem refers to a theorem that asserts that the set of ω-regular languages
Omega-regular language
The ω-regular languages are a class of ω-languages which generalize the definition of regular languages to infinite words. Büchi showed in 1962 that ω-regular languages are precisely the ones definable in a particular monadic second-order logic called S1S.- Formal definition :An...
is identical to the set of languages recognizable by deterministic Muller automata
Muller automaton
In automata theory, a Muller automaton is a type of an ω-automaton.The acceptance condition separates a Muller automomaton from other ω-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
Büchi automaton
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
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
Muller automaton
In automata theory, a Muller automaton is a type of an ω-automaton.The acceptance condition separates a Muller automomaton from other ω-automata....
. 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 {q1, ... ,qn}.
Let α be the regular language
Regular language
In theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....
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 which led to the acceptance of w. For a time instant t, let ρ(t) is the state visited by ρ at time t. We create an infinite and strictly increasing sequence of time instants t1, t2, ... such that for each a and b, ρ(tna+b) = qb. Such a sequence exists because all 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 an element of α(β1 ... βn)ω.
Suppose w ∈ α(β1 ... βn)ω. Due to definition of α, there is an initial segment of w that is an element of α and leads A to the state q1. From there on, the run never assumes a state outside of {q1, ... ,qn}, due to the definitions of β's, and all the states in the set are repeated infinitely often. Therefore, A accepts the word w.
Constructing a deterministic Muller automaton from a given ω-regular language
The other direction of the theorem can be proven by showing that there exist a Muller automaton that recognize a given ω-regular language.The union of finitely many deterministic Muller automata can be easily constructed therefore w.l.o.g. we assume that the given ω-regular language is of the form αβω. Let's suppose ω-word w=a1,a2,... ∈ αβω. Let w(i,j) be the finite segment ai+1,...,aj-1,aj 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 ∈ β* iff 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 iff 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 statesDfa minimizationIn computer science, more specifically in the branch of automata theory, DFA minimization is the task of transforming a given deterministic finite automaton into an equivalent DFA that has minimum number of states. Here, two DFAs are called equivalent if they describe the same regular language...
. 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 i1,...,ip+1 such that no two of them are equivalent. For l > max(i1,...,ip+1), we would have, for each m and n, not E(im,in,l). Therefore, there would be p+1 equivalence classes, as judged at l, contradicting the first part of the lemma.
Lemma 2
- w ∈ αβω iff 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 i0,i1,i2,... such that w(0,i0) ∈ α and w(in,in+1) ∈ β. Therefore, for all n > m, w(im,in) ∈ β* and in favors im. 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 which 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 i0,i1,i2,... such that w(0,i0) ∈ αβ* and w(in,in+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 i0=i. We set i1 such that i1 favors i0 and E(i0,i1). So, w(i0,i1) ∈ β*.
- Induction step: Lets suppose E(i0,in). So, there exists a time i' such that E(i0,in,i'). We set in+1 such that in+1 > i', in+1 favors i0, and E(i0,in+1). So, w(i0,in+1) ∈ β* and, since in+1 > i' we have by definition of E(i0,in,i'), w(in,in+1) ∈ β*.
Muller automaton construction
We have used both the concepts of "favor" and "equivalence" in lemma 2. Now, we are going to use the lemma to constructAutomata construction
In automata theory, automata construction is an important mathematical technique used to demonstrate the existence of an automaton with a certain desired property...
a Muller automaton for language αβω. The proposed automaton will accept a word iff 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 initial state and becomes oblivious to the input. If master activates a Aβ* machine then it keeps reading the input move, 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.
- Current states of Aβ* machines.
- List of the active Aβ* machines in the order of their activation time.
- For each active Aβ* machine M, the set of other active Aβ* machines that were in a accepting state at the time of activation of M. In other words, if a machine is made active at time i and some other machine was last made active at j < i and continue to be active till i then the master keeps the record whether or not i favors j. This record is dropped if the other machine goes dormant before M.
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 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:
- M is in initial state, thus E(j,i,i) and i favors j ( the initial state has to be accepting state).
- For some other active Aβ* machine M' activated at k, where j< k
Note that the green light for M does not flash every time when a machine goes dormant due to M.
Lemma 3
- If there exist a time equivalent to infinitely many times that favor it and i is the earliest such time, then a Aβ* machine M is activated at i, remained active forever (no corresponding red light flash thereafter), and flashes the green light infinitely many times.
- Proof: Let's suppose a Aβ* machine was activated at time j such that j < i and this machine goes to initial state at time i. Therefore, if any time is equivalent and favors i then the time must be in the same relation with j. This contradicts the hypothesis that i is the earliest time such that infinitely many times equivalent to i and favoring i. So at time i, no active machine can be in the initial state. Hence, the master has to activate a new Aβ* machine at time i, which is our M. This machine will never go dormant because if some other machine, which was activated at time l, makes it dormant at time k then E(l,i,k). Again, the same contradiction is implied. By construction and due to infinitely many times are equivalent to i and favor i, the green light will flash infinitely often.
Lemma 4
- Conversely, if there is a Aβ* machine M whose green light flashed infinitely often and red light only finitely often then there are infinitely many times equivalent to and favoring the last time at which M became active.
- Proof: True by construction.
Lemma 5
- w ∈ αβω iff, for some Aβ* machine, the green light flashes infinitely often and the red light flashes only finitely often.
- Proof: Due to lemma 2-4.
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 = { S | ∃n μn ⊆ S ⊆ νn }. This finishes the construction of the desired Muller automaton. Q.E.D.
Other proofs
Since McNaughton's proof, many other proofs have been proposed. The following are some of them.- ω-regular language can be shown equiv-expressive to Büchi automataBüchi automatonIn computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...
. Büchi automata can be shown to equiv-expressive to semi-deterministic Büchi automataSemi-deterministic büchi automatonIn automata theory, a semi-deterministic Büchi automaton is a special type of Büchi automaton. In such an automaton, states can be divided into two partitions such that one part forms a deterministic automaton and this part also contains all the accepting states.For every Büchi automaton, a...
. 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 Muller automaton. This construction is known to be optimal.
- There is a purely algebraic proof of McNaughton's Theorem.