Game Development Reference

In-Depth Information

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 [1982], where the players are called

Automaton and Pathfinder.

The rules of the game are as follows:

A

•
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

are:

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

•

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

A

.

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

Search Nedrilad ::

Custom Search