Game Development Reference
exists a move of one player that ensures the win against all moves of the
other player. In this case the game has just two rounds: The first player picks
a run on the input tree, and the second player picks a path through the run.
The first player wins if the path satisfies the acceptance condition. We will
modify this game such that the players do not choose these objects in one
step but incrementally build them. This allows us to express the acceptance
of a tree in the form
strategy for Eva
strategies for Adam ( ... ) .
Then we use determinacy of these games allowing us to express non-
acceptance of a tree as
strategy for Adam
strategies for Eva ( ... ) .
This statement is in the form of
and we show how to construct an
automaton that checks this property.
We start by defining the membership game that characterises the mem-
bership of a tree t in the language of a given PTA
=( Q, Σ ,q in , Δ , pri ).
Since one player tries to construct an accepting run and the other player
tries to show that the run is not accepting by selecting a path through the
run, we call the players Constructor and Spoiler. This game has been
proposed by Gurevich and Harrington , where the players are called
Automaton and Pathfinder.
The rules of the game are as follows:
• The game starts at the root of the tree in the initial state of A , i.e., in the
position ( q in ,ε ).
} ∗ isanode
The moves of the game from a position ( u, q ) where u
0 , 1
of t , and q is a state of
1 Constructor picks a transition ( q, a, q 0 ,q 1 ) that matches q and the
label a of t at u , i.e., a = t ( u ).
2 Spoiler chooses a direction and the game moves on to position ( u 0 ,q 0 )
or ( u 1 ,q 1 ).
A play of this game is an infinite sequence of states and transitions together
with the nodes in the tree. For the winning condition only the sequence of
states is interesting: Constructor wins if this state sequence satisfies
the acceptance condition of
The shape of this game is illustrated in Figure 2.11. The dashed lines
represent the tree nodes. For each tree node the circles represent states, i.e.,
the positions of Constructor, and the triangles transitions. The arrows