1. Determinisation of ω-automata

Mikołaj Bojańczyk

zajęcia / courses

1. Determinisation of ω-automata

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 $\set{a,b}$ where the letter $a$ 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 $\set{a,b}^*$ . 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 $v \in \set{a,b}^*$ of this tree has an accepting transition in its subtree, this is because the word $vb^\omega$ should have an accepting run. Applying that claim to vertices that end with $a$ , we construct an infinite path in the tree which has $a$ infinitely often and uses accepting transitions infinitely often. $\Box$

The above fact shows that if we want to determines automata for $\omega$ -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 $Q$ is a family $\mathcal F \subseteq \mathsf PQ$ of sets of states. A run is accepting if the set of states visited infinitely often belongs to the family $\mathcal F$ . For example, if the family is

$\mathcal F = \set{\emptyset,\set{q},\set{p,q}}$

then a run is accepting if “infinitely often $p$ ” implies “infinitely often $q$ “. 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 $\neg,\land$ and $\lor$ ) where the variables are states, and a variable $q$ stands for “infinitely often $q$ “. The family $\Ff$ in the example above would be represented by a formula

$\neg p \lor q$

Deterministic Muller automata are clearly closed under complement – it suffices to replace the accepting family by $\mathsf PQ -\mathcal F$ , 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 $Q$ , define a $Q$ -dag to be a directed acyclic graph where the nodes are pairs $Q \times \Nat$ and every edge is of the form

$(q,i) \to (p,i+1) \qquad \mbox{for some }p,q \in Q\mbox{ and }i \in \Nat.$

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 $Q$ -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 $Q$ -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 $Q$ -dag as an $\omega$ -word. This is done using an alphabet, which we denote by $[Q]$ , where the letters look like this:

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

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

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 $\Sigma$ and the output alphabet is $\Gamma$ , then a transducer defines a function

$f : \Sigma^\omega \to \Gamma^\omega.$

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 $\Aa$ with input alphabet $\Gamma$ , and every transducer $f : \Sigma^\omega \to \Gamma^\omega$ , there exists a deterministic Muller automaton which accepts a word $w \in \Sigma^\omega$ if and only if $\Aa$ accepts $f(w)$ .

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 $\Aa$ be a nondeterministic Büchi automaton with input alphabet $\Sigma$ , states $Q$ , and initial state $q$ . By simply copying the transitions of the automaton, one obtains a transducer

$\begin{align*} f : \Sigma^\omega \to [Q]^\omega \end{align*}$

such that a word $w \in A^\omega$ is accepted by $\Aa$ if and only if $f(w)$ 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 $\Aa$ . $\Box$

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 $Q$ -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

$\begin{align*} f : [Q]^\omega \to [Q]^\omega \end{align*}$

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 $w \in [Q]^\omega$ and accepts if and only if the tree contains an accepting path.

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

zajęcia / courses

1. Determinisation of ω-automata

1. Determinisation of ω-automata

Leave a Reply