Game Development Reference

In-Depth Information

.

Figure 2.12 Shape of positional strategies for Spoiler in the membership

game

Applying the positional determinacy for the negation of the statement, we

obtain:

Lemma 2.15

)
iff there is a positional winning

strategy for
Spoiler
in the membership game.

A tree t is not in T
(

A

The next goal is to construct an automaton that checks for a tree
t
if

there is a positional winning strategy for Spoiler in the membership game.

By Lemma 2.15 such an automaton su
ces to recognise the complement

language of

. We start by analysing positional strategies for Spoiler.

A move for Spoiler consists in choosing a direction for a given pair of

tree node and transition, as illustrated by the thick edges in Figure 2.12.

Such a positional strategy for Spoiler can be written as a mapping

A

}
∗
→

σ
:

{

0
,
1

(Δ

→{

0
,
1

}

)

that defines for each tree node how the choices of Spoiler for the different

transitions are. Let us denote the finite set Δ

of mappings from

transitions to directions 0
,
1 by Γ. Then a positional strategy for Spoiler

is simply a tree over the alphabet Γ, and hence can be processed by a tree

automaton.

Now the next steps in the construction of the complement automaton

→{

0
,
1

}

C

are the following:

•

Construct an automaton

A
strat
that reads trees of the form
t

×

σ
, i.e.,

annotated with a positional strategy for Spoiler such that

A
strat
accepts

t

×

σ
if
σ
is winning for Spoiler in the membership game for

A

and
t
.

Search Nedrilad ::

Custom Search