Mikołaj Bojańczyk

Büchi automata

Define the syntax of a nondeterministic Büchi automaton to be the same as that of an NFA. For this lecture it will be more convenient to use accepting transitions, i.e. the accepting set is a set of transitions, not a set of states. An infinite word is accepted by the automaton if there exists a run which begins in one of the initial states, and visits some accepting transition infinitely often.

Fact. Nondeterministic Büchi automata are more expressive than deterministic Büchi automata.

Proof. The example language is the set of words over alphabet where the letter appears finitely often.  Suppose that there is a deterministic Büchi automaton that recognises this word. Let us view the set of all possible inputs as an infinite tree, where the vertices are prefixes .  Since the automaton is deterministic, to each edge of this tree one can uniquely assign a transition of the automaton. We claim that every vertex  of this tree has an accepting transition in its subtree, this is because the word should have an accepting run. Applying that claim to vertices that end with , we construct an infinite path in the tree which has infinitely often and uses accepting transitions infinitely often.

The above fact shows that if we want to determines automata for -words, we need something more different than the Büchi condition. One solution is called the Muller condition, and is described below. Later, we will see another, equivalent, solution, which is called the parity condition.

Muller automata

The syntax of a Muller automaton is the same as for a Büchi automaton, except that the accepting set is different. Instead of being a set of transitions, the accepting set in a Muller automaton with states is a family of sets of states. A run is accepting if the set of states visited infinitely often belongs to the family . For example, if the family is

then a run is accepting if “infinitely often ” implies “infinitely often “. A convenient (and more succinct) way to describe a Muller condition is to give a propositional formula (i.e. a formula built out of variables using and ) where the variables are states, and a variable stands for “infinitely often “. The family in the example above would be represented by a formula

Deterministic Muller automata are clearly closed under complement – it suffices to replace the accepting family by , or use negation if the formula representation is used. This lecture is devoted to proving the following determinisation result.

McNaughton’s Theorem. For every nondeterministic Büchi automaton there exists an equivalent deterministic Muller automaton.

The converse of the theorem, namely that deterministic Muller automata can be transformed into equivalent nondeterministic Büchi automata is more straightforward, and shown in the exercise session. The theorem is named after McNaughton because he was the first to prove it. I think that the proof here is similar to one from this paper of Muller and Schupp.

The proof strategy is as follows. We first define a family of languages, called universal Büchi languages, and show that the McNaughton’s theorem boils down to recognising these languages. Then we show how the universal languages can be recognised by deterministic Muller automata.

The universal Büchi language

For a finite set , define a -dag to be a directed acyclic graph where the nodes are pairs and every edge is of the form

Furthermore, every edge is colored by one of two colors: “accepting” or “non accepting”. We assume that there are no parallel edges. Here is a picture of a -dag, with accepting edges being solid lines, and non-accepting edges being dashed lines.

As we will show, the essence of  McNaughton’s theorem is finding a deterministic Muller automaton which inputs a -dag and says if it contains a path with infinitely many accepting edges. In order to write such an automaton, we need to encode as -dag as an -word. This is done using an alphabet, which we denote by , where the letters look like this:

Formally speaking, a letter in is a function from to three possibilities: “no edge”, “an accepting edge”, and a “non-accepting edge”. Define the universal Büchi language over states  to be the set of words which, when treated as a -dag, contain a path that visits accepting edges infinitely often. The key to McNaughton’s theorem is the following proposition.

Proposition. For every finite  there exists a deterministic Muller automaton recognizing the universal Büchi language over states .

Before proving the proposition, let us show how it implies McNaughton’s theorem. To make this and other proofs more transparent, it will be convenient to use transducers. Define a transducer to be a deterministic finite automaton, without accepting states, where each transition is additionally labelled by a letter from some output alphabet. If the input alphabet is and the output alphabet is , then a transducer defines a function

It is easy to see that languages recognised by deterministic Muller automata are closed under inverse images of transducers, i.e. for every deterministic Muller automaton with input alphabet , and every transducer , there exists a deterministic Muller automaton which accepts a word if and only if accepts .

Proof of McNaughton’s theorem. We claim that every language recognised by a nondeterministic Büchi automaton reduces to a universal Büchi language via some transducer. Let be a nondeterministic Büchi automaton with input alphabet , states , and initial state . By simply copying the transitions of the automaton, one obtains a transducer

such that a word is accepted by if and only if contains a path with infinitely many accepting edges. By composing the transducer with the automaton from the proposition, we get a deterministic Muller automaton equivalent to .

It now remains to show the proposition, i.e. that the universal Büchi language can be recognised by a Muller automaton. The proof has two steps. The first step is stated in Lemma 1 and says that a when dealing with the universal Büchi language, one can write a deterministic transducer which replaces an arbitrary dag by an equivalent tree. Here we use the name tree for a -dag where, every non-isolated node has exactly one incoming edge, with a single exception, called the root, which is in the leftmost column and has no incoming edges. Here is a picture of such a tree, with the isolated nodes not drawn:

Lemma 1. There exists a deterministic transducer

which outputs only trees and is invariant with respect to the universal Büchi language, i.e. if the input contains a path with infinitely many accepting edges, then so does the output and vice versa.

Lemma 1 is proved here. The second step is stated in Lemma 2 and says that a deterministic Muller automaton can test if a tree contains an accepting path.

Lemma 2. There exists a deterministic Muller automaton which inputs a tree and accepts if and only if the tree contains an accepting path.

Lemma 2 is proved here. The two lemmas complete McNaughton’s theorem.