Game Development Reference
In-Depth Information
q 1
( q 1 ,a,q 1 ,q + )
( q 1 ,a,q 2 ,q + )
q 2
( q 2 ,a,q 1 ,q 1 )
q 2
( q 1
,a,q + ,q 1
)
q
1
( q 1 ,b,q + ,q + )
( q + ,a,q + ,q + )
( q + ,b,q + ,q + )
Figure 2.14 The emptiness game for the example PTA. The thick arrows
define a winning strategy for Constructor
2 Spoiler chooses a direction and the game moves on to position q 0 or q 1 .
A play of this game is an infinite sequence of states and transitions. For
the winning condition only the sequence of states is relevant: The winning
condition for Constructor is the acceptance condition of
A
.
This is a parity game on a finite game graph. In the same way as for the
membership game we get the following lemma.
Lemma 2.18
is not empty iff Constructor
has a winning strategy in the emptiness game for
The language of the PTA
A
A
.
Consider the following example PTA
A
over the alphabet
{
a, b
}
with state
q 1 ,q 1 ,q 2 ,q + }
set
{
, initial state q 1 , and the following transitions and priorities:
( q 1 ,a,q 1 ,q + ) q 1 ,a,q + ,q 1 ) q + ,a,q + ,q + )
c ( q 1 )= c ( q 1 )=1
( q 1 ,a,q 2 ,q + ) q 1 ,b,q + ,q + ) q + ,b,q + ,q + )
c ( q 2 )= c ( q + )=2
( q 2 ,a,q 1 ,q 1 )
The emptiness game together with a winning strategy for Constructor
is shown in Figure 2.14. The nodes of Constructor are labelled with the
name of the state and the corresponding priority. The transitions do not
have a priority in the game because they are not considered for the winning
condition.
Since Constructor has a winning strategy we can deduce that there
is a tree that is accepted by
. Furthermore, from a positional winning
strategy one can construct a finitely generated tree that is accepted by
A
.
The idea is that the strategy of Constructor associates to each state a
A