Game Development Reference
Figure 2.12 Shape of positional strategies for Spoiler in the membership
Applying the positional determinacy for the negation of the statement, we
) iff there is a positional winning
strategy for Spoiler in the membership game.
A tree t is not in T (
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
. 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
} ∗ →
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
Now the next steps in the construction of the complement automaton
0 , 1
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
σ if σ is winning for Spoiler in the membership game for
and t .