Game Development Reference
In-Depth Information
k and we can use nodes in the game graph to represent the
d
∈{
0 ,...,n,
∞}
values of the d i .
The structure of the formulae ψ 0 defining the winning region for Player 0
in backtracking games with priorities <k is similar to the structure of the
corresponding LFP-formula for parity games. It has the form
ψ 0 ( x ):=[ gfp R 0 xd. [ lfp R 1 xd. ... [ fp R k− 1 xd.ϕ ( R, x, d )] ... ]( x,
,...
)
with k nested fixed-points, applied to a formula ϕ which is first-order, up
to the IFP-subformula defining the order of the bisimulation types. In its
various nested fixed-points the formula builds up sets of configurations
( x, d 0 ,...,d k− 1 ) such that if ( x, d 0 ,...,d k ) ∈ R Ω( x ) , then Player 0 can extend
any partial play π , ending in node x with d π ( j )= d j for all j<k ,toa
winning play.
We do not give an explicit construction here, but explain the idea. For
details, we refer to Dawar et a l. [ 20 06].
First of all the formula ϕ ( R, x, d ) states that for some i , the priority of x
is i and the tuple ( d 0 ,...,d k− 1 ) has
at all positions greater than i (which
corresponds to the fact that a node of priority i releases all backtracking
moves on higher priorities). Fu r ther, if x is a position of Player 0, then she
can win from configuration ( x, d ) if she can move to a successor y of x fr om
which she wins t he play. Winning from y means that the configuration ( y, d )
reached from ( x, d ) b y moving to y is in R Ω( y ) . Thus the formula must define
what it means for ( y, d ) to be the configuration reached from x when moving
to y .
This involves a case distinction.
If d i = , Player 0 can either do an ordinary move or, in case x ∈ B ,
a backtracking move. After an ordinary move to a successor node y of
priority j the play will have the configuration ( y, d ) which satisfies d =
( d 0 ,...,d j ,
)) and which must be in R j . After a backtracking move,
we will have, for some m
,...,
=
, a configuration ( x, d 0 ,...,d i− 1 ,m,
,...,
)
which must be in R i
In the case that d i = m ≤|G| , the formulae must express that Player 0
wins the m -step game on priority i from x . This game is won by Player 0 if
there is a successor y of x from which she wins and either the priority j of
y is less than i , i.e., all backtracking moves on priorities greater than j are
released ( d l =
for all l>j ), or the priority j of y equals i and Player 0
wins the m
1 step game from y (and all d l with l<i are left unchanged),
or the priority j of y is greater than i , in which case the play continues with
the configuration ( y, d 0 ,...,d i ,
,...,
), i.e., all active backtracking moves