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

Search Nedrilad ::

Custom Search