Game Development Reference
In-Depth Information
it has to be a final state. The definition is replaced by other mechanisms for
acceptance, similar to the winning conditions in infinite games.
An ω -automaton is of the form
=( Q, Σ ,q 0 , Δ , Acc ), where Q, Σ ,q 0 , Δ
are as for standard finite automata, i.e., Q is a finite set of states, Σ is
the input alphabet, q 0 is the initial state, and Δ
A
Q is the
transition relation. The component Acc defines the acceptance condition and
is explained below.
For an infinite word α
Q
×
Σ
×
Σ ω ,a run of
A
on α is an infinite sequence of
Q ω that starts in the initial state, ρ (0) = q 0 , and respects the
transition relation, ( ρ ( i ) ( i ) ( i + 1))
states ρ
0.
It remains to define when such a run is accepting. We are mainly interested
in two types of acceptance conditions:
Δ for all i
In a Buchi automaton Acc is given as a set F
Q of states. A run is
accepting if it contains infinitely often a state from F .
In a parity automaton Acc is given as a priority mapping pri : Q
N
.
A run is accepting if the maximal priority appearing infinitely often is
even.
Deterministic automata are defined as usual: there is at most one transition
per state and letter.
Figure 2.5 shows a non-deterministic Buchi automaton (on the left-hand
side) accepting the language of infinite words over Σ =
that contain
finitely many b . A simple argument shows that there is no deterministic
Buchi automaton for this language (Landweber [1969]):
{
a, b
}
Exercise 2.2 Show that no deterministic Buchi automaton can accept the
language of infinite words over Σ =
that contain finitely many b .
Hint: Long sequences of a would always lead such an automaton into an
accepting state. Hence, there is some n such that the infinite word ( a n b ) ω
consisting of long a -blocks separated by b would be accepted.
{
a, b
}
But it is very easy to construct a deterministic parity automaton for this
language using the priorities 0 and 1. Such an automaton is shown on the
right-hand side of Figure 2.5.
One can show that the two models of non-deterministic Buchi automata
and deterministic parity automata are in fact equivalent in expressive power.
The di cult direction is the construction of a deterministic parity automaton
from a non-deterministic Buchi automaton. The classical subset construction
that is used to determinise automata on finite words does not work as
illustrated by the following example: Consider the Buchi automaton on
the left-hand side of Figure 2.5 and the two inputs a ω
= aaaaaa
···
, and