Game Development Reference
Figure 2.13 A single path through a coding of a positional strategy of
• Obtain C from A strat by omitting the strategy annotation in the labels.
This operation corresponds to a simple projection that removes the Γ
component of the labels. This can be seen as
guessing the strategy for Spoiler.
A strat has to check that the plays obtained by
following the thick edges (the strategy of Spoiler) do not satisfy the accep-
tance condition (the strategy is winning for Spoiler). For this task we first
focus on single paths of the tree.
We code these paths by adding to the labels on the path the next direction 0
or 1 taken by the path. In this way we obtain infinite words over Σ
Looking at Figure 2.12,
0 , 1
This is indicated in Figure 2.13, where a single path from the tree shown in
Figure 2.12 is selected.
Now we construct an ω -automaton that checks whether on such paths the
strategy is winning for Spoiler. This ω -automaton has to check whether
all plays that can be obtained by following the thick arrows (the strategy of
Spoiler) along the given path do not satisfy the acceptance condition of
We obtain this ω -automaton as follows:
Construct a non-deterministic Buchi automaton that guesses a play along
the strategy edges of Spoiler and accepts if it does satisfy the acceptance
Determinise (see Theorem 2.6) and complement this Buchi automaton, and
obtain a deterministic parity word automaton
strat that accepts those
paths of a tree on which Spoiler's strategy is winning.
strat in parallel
along all paths of the given tree by merging the transitions of
Now we can run this deterministic parity word automaton
strat for the