Mikołaj Bojańczyk

As we showed in the example of “finitely many a‘s”, deterministic Büchi automata are not closed under complement. However, if we simply add complementation, i.e. we close them under Boolean combinations, then we get a (deterministic) model that is equivalent to nondeterministic Büchi automata.

McNaughton’s Theorem. For every nondeterministic Büchi automaton, its language is a Boolean combination of languages recognised by deterministic Büchi automata.

This theorem was originally proved by McNaughton. The construction below is slightly similar to the original one, and different from the more often used constructions that do not use algebra, e.g. the Safra construction or the Muller-Schupp construction. The key concept in the proof is the idea of a tail \Jj-class. 

Tail \Jj-class. For a word w \in \Sigma^\omega, we say that m \in M appears arbitrarily far if there are infinitely many positions x such that for some y (depending on x) the infix from x to y has type mIt is easy to see if m,n \in M appear arbitrarily far, then there is some k \in M that also appears arbitrarily far, and is \Jj-heavier or equivalent to both of them. Therefore there is a unique heaviest \Jj-class that contains elements which appear arbitrarily far, call this \Jj-class the tail \Jj-class of the word.

Lemma. For every \Jj-class, the set of \omega-words with this tail \Jj-class is a Boolean combination of languages recognised by deterministic Büchi automata.

Proof. For every m \in M there is a deterministic Büchi automaton which recognises words where m appears arbitrarily far. The automaton works like this: it enters an accepting state whenever it sees a word that contains m as an infix. Then it returns to the initial state, and restarts the process, and so on forever. The automaton for the tail \Jj-class is a Boolean combination of these automata. \Box

Recall that Büchi’s Linked Pair Lemma said that acceptance or rejection by a nondeterministic Büchi automaton is uniquely determined by the existence of linked pair factorisations. Therefore, McNaughton’s theorem will follow from the lemma bellow, which shows how to use deterministic automata to see if there exist linked pair factorisations.

Lemma. For every linked pair (s,e) in the monoid M the set of words which admit an (s,e)-factorisation is a Boolean combination of languages recognised by deterministic Büchi automata.

Proof. For a word w \in \Sigma^\omega, we say that the pair (s,e,e) appears arbitrarily far if there are infinitely many positions x such that for some y < z (depending on x) the prefix up to x has type s,  the infix from x to y has type e, and the infix from y to z also has type e. Using the same idea as before, one can show that the set of words where (s,e) appears arbitrarily far is a Boolean combination of languages recognised by deterministic Büchi automata. Therefore, to  complete the lemma it suffices to show that a word admits an (s,e)-factorisation if and only if (s,e,e) appears arbitrarily far, and the \Jj-class of contains e. The left-to-right implication is immediate, so let us do the right-to-left implication.

Suppose then that the tail \Jj-class of w contains e, and that (s,e,e) appears arbitrarily far to the right. Since (s,e,e) appears arbitrarily far to the right, there exists a factorisation

    \[w = w_0 w_1 w_2 \cdots \cdots\]

such that every nonempty prefix w_0 \cdots w_i has type s and every w_i has both a prefix and suffix of type e.  Since the tail \Jj-class contains e, it follows that for all but finitely many i, the type of w_i is \Jj-equivalent to e. Without loss of generality, we assume that every w_i has type that is \Jj-equivalent to e. Since this type begins with e, ends with e, and is \Jj-equivalent to e, it must be in the \Hh-class of e by the Eggbox Lemma. Furthermore, this \Hh-class, call it H, is a group, because it contains an idempotent. By grouping the decomposition, we can assume without loss of generality that there is some h \in H such that every word w_1 \cdots w_i has type h. This implies that every w_i has type that is the identity in the group, which is the idempotent e. \Box

 

Leave a Reply

Your email address will not be published. Required fields are marked *