Game Development Reference
In-Depth Information
.
Figure 2.11 Shape of the membership game
from the circles to the triangles indicate that Constructor chooses for a
given state a possible transition, and the arrows exiting from the triangles
correspond to the choices of Spoiler who moves either to the left or to the
right into the corresponding state of the transition.
One should note here that the shape of the game reminds one of a tree but
that the game graph itself is not a tree, it is an acyclic graph. For example,
in the illustration in Figure 2.11 the leftmost circle in the bottom row can be
reached via two different paths. Hence, the existence of positional strategies
is not obvious (for game graphs that are trees all strategies are positional
because a vertex encodes the full history of the play).
With the picture from Figure 2.11 in mind it is rather easy to see that
there is a correspondence between the runs of A on t and the strategies for
Constructor:
Fixing the transition to be used at the root is the same as defining the
first move of Constructor.
Then Spoiler can only move to the left or to the right. The states at
these successors are already fixed by the transition. Defining the strategy
for Constructor at these successors is again the same as fixing the
transitions for a run, and so on.
By the definition of the winning condition and positional determinacy of
parity games we obtain the following lemma.
Lemma 2.14
) iff there is a positional winning strategy
for Constructor in the membership game.
A tree t is in T (
A