As we showed in the example of “finitely many ‘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 -class. 

Tail -class. For a word , we say that appears arbitrarily far if there are infinitely many positions such that for some (depending on ) the infix from to has type . It is easy to see if appear arbitrarily far, then there is some that also appears arbitrarily far, and is -heavier or equivalent to both of them. Therefore there is a unique heaviest -class that contains elements which appear arbitrarily far, call this -class the tail -class of the word.

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

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

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 in the monoid the set of words which admit an -factorisation is a Boolean combination of languages recognised by deterministic Büchi automata.

Proof. For a word , we say that the pair appears arbitrarily far if there are infinitely many positions such that for some (depending on ) the prefix up to has type ,  the infix from to has type , and the infix from to also has type . Using the same idea as before, one can show that the set of words where 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 -factorisation if and only if appears arbitrarily far, and the -class of contains . The left-to-right implication is immediate, so let us do the right-to-left implication.

Suppose then that the tail -class of contains , and that appears arbitrarily far to the right. Since appears arbitrarily far to the right, there exists a factorisation

   

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