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
.

Search Nedrilad ::

Custom Search