6. Büchi automata

Mikołaj Bojańczyk

zajęcia / courses

An $\omega$ -word is a word where positions are indexed by natural numbers. We write $\Sigma^\omega$ for the set of $\omega$ -words over an alphabet $\Sigma$ . To recognise languages of $\omega$ -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 $\epsilon$ -transitions), i.e. it is a tuple

$(Q,\Sigma,I,F,\delta) \qquad \mbox{with } I,F \subseteq Q \quad \mbox{and } \delta \subseteq Q \times \Sigma \times Q$

where $Q$ consisting of states, the input alphabet, initial states, final states, and transitions. Such an automaton accepts an $\omega$ -word if it admits some run which begins in an intial state and visits final states infinitely often. Call a language $\omega$ -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 $\omega$ -words over alphabet $\set{a,b}$ where the letter $a$ appears finitely often, this set can be described by the expression $(a+b)^*b^\omega$ . 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 $ab^\omega$ . Since this word contains finitely many $a$ ‘s, it should be accepted, and therefore an accepting state should be used after reading some finite prefix $ab^{n_1}$ . Consider now the word $ab^{n_1} a b^\omega$ . Again this word should be accepted, and therefore there should be some $n_2$ such that an accepting state is seen after reading $ab^{n_1} a b^{n_2}$ . Iterating this construction, we get an $\omega$ -word of the form

$ab^{n_1} ab^{n_2} ab^{n_3} \cdots$

such that the automaton visits an accepting state before every $a$ , and therefore accepts, despite the word having infinitely many $a$ ‘s. Note how we crucially used determinism – by assuming that changing a suffix of the word does not change the run on a prefix. $\Box$

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 $Q$ . For a finite run $\rho$ (i.e. a finite sequence of transitions), define the profile of the run to be the triple in $Q \times \set{0,1} \times Q$ 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 $w \in \Sigma^*$ , define it profile

$h(w) \subseteq Q\times \set{0,1} \times Q$

to be the set of all profiles of finite runs over this word. It is not difficult to see that the profile function $h$ is compositional, and therefore its image, call it $M$ , can be equipped with a monoid structure so that

$h : \Sigma^* \to M$

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 $M$ to be a pair of elements $s,e \in M$ such that $se = s$ and $ee=e$ . 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 $p,q \in Q$ such that $p$ is initial and the elements $s,e$ , when seen as sets of triples, satisfy

$(p,1,q) \in s \qquad \mbox{and} \qquad (q,1,q)$

If a linked pair is not accepting, then it is called rejecting.

For $s,e \in M$ and $w \in \Sigma^\omega$ , define an $(s,e)$ -factorisation of $w$ to be a factorisation

$w = w_0 w_1 w_2 \cdots$

into nonempty words such that $h(w_0)=s$ and

$h(w_i w_{i+1} \cdots w_j) = e \qquad \mbox{ for every }1 \le i \le j$

Note that the existence of such a factorisation implies that $(s,e)$ is a linked pair.

Büchi Linked Pair Lemma. A word $w \in \Sigma^\omega$ is rejected if and only if it admits an $(s,e)$ -factorisation for some rejecting linked pair $(s,e)$ .

Proof. Suppose that $w$ is rejected. Apply the Ramsey theorem, yielding some $(s,e)$ -factorisation for some linked pair. Clearly this pair must be rejecting, since otherwise we could construct an accepting run for $w$ . For the converse implication, suppose that $w$ admits an $(s,e)$ -factorisation, say

$w = w_0 w_1 w_2 \cdots$

for some rejecting linked pair. Define $x_i$ to be the position at the beginning of the word $w_i$ , in particular $x_0$ is the first position. We claim that there cannot be any accepting run on $w$ . Toward a contradiction, suppose that $w$ does admit an accepting run, call it $\rho$ . If $\rho$ is accepting, then by the pigeonhole principle one can find some $0 < i < j$ such that accepting states are seen between $x_i$ and $x_j$ , and the same state, call it $q$ , is seen in positions $x_i$ and $x_j$ . This means that there is some initial state $p$ that the word $w_0 \cdots w_{j-1}$ admits a run of profile $(p,1,q)$ . In other words, we have

$(p,1,q) \in h(w_0 \cdots w_{j-1}) = s$

By the same kind of reasoning, we conclude that

$(q,1,q) \in h(w_i \cdots w_{j-1})=e$

and therefore the linked pair $(s,e)$ is accepting, contradicting our assumption. $\Box$

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 $L \subseteq \Sigma^\omega$ recognised by a nondeterministic Büchi automaton, and let $h : \Sigma^* \to M$ be the automaton homomorphism corresponding to this automaton. By the Büchi Linked Pair Lemma, the complement of $L$ is equal to

$\bigcup_{(s,e)} h^{-1}(s) (h^{-1}(e))^\omega$

with the union ranging over rejecting linked pairs. The above language is easily seen to be recognised by a nondeterministic Büchi automaton. $\Box$

zajęcia / courses

6. Büchi automata

Leave a Reply