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