Game Development Reference
In-Depth Information
a
b
a, b
a
b
a, b
q 0
q 1
q 0
q 1
a
Figure 2.5 A non-deterministic Buchi automaton and a deterministic parity
automaton accepting the words containing finitely many b
( ab ) ω
. Both inputs induce the following sequence of sets of
states (the labels above the arrows correspond to the first input, the ones
below the arrows to the second one):
= ababab
···
a
a {
a
b {
a
a {
a
b {
{
q 0 }
q 0 ,q 1 }
q 0 ,q 1 }
q 0 ,q 1 }
q 0 ,q 1 }···
The first input should be accepted, and the second one should be rejected.
But since both induce the same sequence of state sets, the subset construction
does not carry enough information for determinisation, no matter which
acceptance condition we use.
The known determinisation constructions that are of optimal complexity
generalise the subset construction by keeping track of several sets that are
usually arranged in a tree. The first one was proposed by Safra in 1988. The
determinisation theorem itself was already shown by McNaughton in 1966
using a doubly exponential construction.
Theorem 2.6 (McNaughton [1966], Safra [1988]) For each non-deterministic
Buchi automaton with n states there is an equivalent deterministic parity
automaton with 2 O ( n log n ) states.
For some recent work on upper and lower bounds for the determinisation
of Buchi automata we refer the reader to Piterman [2006], Kahler and Wilke
[2008], Schewe [2009], and Colcombet and Zdanowski [2009].
The other direction of the equivalence between deterministic parity and
non-deterministic Buchi automata is left as an exercise.
Exercise 2.3 Show that each deterministic parity automaton can be trans-
formed into an equivalent non-deterministic Buchi automaton.
Hint: The Buchi automaton guesses an even priority at some point and
verifies that it occurs infinitely often and that it is the maximal priority from
this point onwards.
We call languages that can be accepted by non-deterministic Buchi au-
tomata (or equivalently by deterministic parity automata) ω -regular .