An -word is a word where positions are indexed by natural numbers. We write for the set of -words over an alphabet . To recognise languages of -words, we use Büchi automata (we will later move a monoid style).
Büchi automata. A nondeterministic Büchi automaton has the same syntax as a nondeterministic automaton over finite words (say, without -transitions), i.e. it is a tuple
where consisting of states, the input alphabet, initial states, final states, and transitions. Such an automaton accepts an -word if it admits some run which begins in an intial state and visits final states infinitely often. Call a language -regular if it is recognised by some nondeterministic Büchi automaton.
Example. The obvious question is: what about deterministic Büchi automata? As it turns out, these are too weak. Indeed, consider the set of -words over alphabet where the letter appears finitely often, this set can be described by the expression . Here is a picture of a nondeterministic Büchi automaton that recognises this language:
We claim that no deterministic Büchi automaton recognises this language. Suppose that there would be such an automaton. Run this automaton on the word . Since this word contains finitely many ‘s, it should be accepted, and therefore an accepting state should be used after reading some finite prefix . Consider now the word . Again this word should be accepted, and therefore there should be some such that an accepting state is seen after reading . Iterating this construction, we get an -word of the form
such that the automaton visits an accepting state before every , and therefore accepts, despite the word having infinitely many ‘s. Note how we crucially used determinism – by assuming that changing a suffix of the word does not change the run on a prefix.
The automaton monoid and linked pairs
Our goal is to prove that nondeterministic Büchi automata are closed under complementation, and then a form determinisation: namely nondeterministic Büchi automata are equivalent to Boolean combinations of deterministic Büchi automata. Before proving these results, we show how to associate to each nondeterministic Büchi automaton a monoid homomorphism.
The automaton homomorphism. Consider a nondeterministic Büchi automaton with states . For a finite run (i.e. a finite sequence of transitions), define the profile of the run to be the triple in such that the first coordinate is the source state, the last coordinate is the target state, and the middle coordinate says whether or not the run contains an accepting state (1 means yes). For a finite input word , define it profile
to be the set of all profiles of finite runs over this word. It is not difficult to see that the profile function is compositional, and therefore its image, call it , can be equipped with a monoid structure so that
becomes a monoid homomorphism. This monoid homomorphism is called the automaton homomorphism associated to the automaton.
Linked pairs and factorisations. Define a linked pair in the monoid to be a pair of elements such that and . This notion makes sense in any monoid, but the following notion of accepting linked pair is specific to the monoid defined above. Define a linked pair to be accepting if there are some states such that is initial and the elements , when seen as sets of triples, satisfy
If a linked pair is not accepting, then it is called rejecting.
For and , define an -factorisation of to be a factorisation
into nonempty words such that and
Note that the existence of such a factorisation implies that is a linked pair.
Büchi Linked Pair Lemma. A word is rejected if and only if it admits an -factorisation for some rejecting linked pair .
Proof. Suppose that is rejected. Apply the Ramsey theorem, yielding some -factorisation for some linked pair. Clearly this pair must be rejecting, since otherwise we could construct an accepting run for . For the converse implication, suppose that admits an -factorisation, say
for some rejecting linked pair. Define to be the position at the beginning of the word , in particular is the first position. We claim that there cannot be any accepting run on . Toward a contradiction, suppose that does admit an accepting run, call it . If is accepting, then by the pigeonhole principle one can find some such that accepting states are seen between and , and the same state, call it , is seen in positions and . This means that there is some initial state that the word admits a run of profile . In other words, we have
By the same kind of reasoning, we conclude that
and therefore the linked pair is accepting, contradicting our assumption.
Complementation of Büchi automata
As an application of the automaton homomorphism, we prove that languages recognised by nondeterministic Büchi automata are closed under complementation. This is Büchi’s original proof of the result. We will also use the same ideas to prove determinisation, which is done here.
Theorem. For every nondeterministic Büchi automaton, the complement of its language is recognised by a nondeterministic Büchi automaton.
Proof. Consider a language recognised by a nondeterministic Büchi automaton, and let be the automaton homomorphism corresponding to this automaton. By the Büchi Linked Pair Lemma, the complement of is equal to
with the union ranging over rejecting linked pairs. The above language is easily seen to be recognised by a nondeterministic Büchi automaton.