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

Search Nedrilad ::

Custom Search