Game Development Reference

In-Depth Information

two directions 0 and 1 into a single transition of a tree automaton as follows:

path

δ
(
q,
(
a, γ,
0)) =
q

δ
(
q,
(
a, γ,
1)) =
q

A

strat
:

(
q,
(
a, γ
)
,q
,q
)

A
strat
:

for all
q

∈

Q
,
a

∈

Σ, and
γ

∈

Γ.

The automaton

C

is obtained by omitting the strategy encoding:

(
q,
(
a, γ
)
,q
,q
) becomes (
q, a, q
,q
)
.

From the explanations above it follows that

C

indeed accepts the complement

language of

A

, resulting in the following theorem.

Theorem 2.16
(Rabin [1969])
For a given tree automaton one can con-

struct a tree automaton for the complement language.

The main steps of the construction described in this section are summarised

as follows:

•

Characterise acceptance in terms of winning strategies in the membership

game.

•

Positional determinacy for parity games yields: a tree
t
is not accepted iff

Spoiler has a positional winning strategy in the membership game.

•

Construct an automaton that checks if a given strategy of Spoiler is

winning. This construction is based on the determinisation of
ω
-automata.

•

Obtain the desired automaton by projection (removing the strategy anno-

tations).

This proof scheme was proposed by Gurevich and Harrington [1982] (see also

Thomas [1997]). It is a nice illustration of how determinacy of infinite games

can help to solve problems in automata theory. Note that the positional

determinacy or winning strategies are not used inside the construction

but only to prove the correctness of the construction. The main step in

the construction itself is the use of the determinisation theorem for Buchi

automata.

In Muller and Schupp [1995] a different proof is presented that only

relies on the determinacy of the membership game without making any

assumptions on the type of the strategies. From the construction one can

derive a finite memory determinacy result for game graphs that have the

shape of a membership game.

The size of the complement automaton is determined by the complexity

of the determinisation construction for word automata. If

is a PTA with

n
states and
k
priorities, then the Buchi word automaton that has to be

A

Search Nedrilad ::

Custom Search