Game Development Reference

In-Depth Information

game

G

. To see this, we compare playing

G

from a current position
u

∈

V
0
∪

P
i

G
∗
from any position
ϑ
k
(
u
), where
ϑ
k
(
x
) is the subformula

[
gfp
R
k
...
]or[
lfp
R
k
...
]of
ψ
0
(
x
). In

with playing

G

, Player 0 selects at position
u

G
∗
, the play goes

from
ϑ
k
(
u
) through the positions
ϑ
k
+1
(
u
)
,...,ϑ
d−
1
(
u
) to the inner formula

ϕ
(
u, R
0
,...,R
d−
1
).

This formula is a disjunction, so Verifier (Player 0) decides how to proceed.

But her only reasonable choice at this point is to move to the position

(
V
0
u

a successor
w

∈

uE
, and the play proceeds from
w
.In

R
i
y
), since with any other choice she would lose one

move later. But from there, the only reasonable move of Falsifier (Player 1)

is to go to position

∧

P
i
u

∧∃

y
(
Euy

∧

∃

y
(
Euy

∧

R
i
y
), and it is now the turn of Player 0 to

select a successor
w

R
i
w
). This forces Player 1 to

move to
R
i
w
from which the play proceeds to
ϑ
i
(
w
)).

Thus one move from
u
to
w
in

∈

vE
and move to (
Euw

∧

G

corresponds to a sequence of moves

G
∗
from
ϑ
k
(
u
)to
ϑ
i
(
w
), but the only genuine choice is the move from

in

∃

y
(
Euy

∧

R
i
y
)to(
Euw

∧

R
i
w
), i.e., the choice of a successor
w

∈

uE
.In

G
∗
the minimal, and hence relevant,

priority that is seen in the sequence of moves from
ϑ
k
(
u
)to
ϑ
i
(
w
) is that of

R
i
w
which is also
i
. The situation for positions
u

G

, the position
u
has priority
i
, and in

∈

V
1
∩

P
i
is the same, except

G
∗
now goes through

that the play in

∀

y
(
Exy

→

R
i
y
) and it is Player 1 who

selects a successor
w

uE
and forces the play to
R
i
w
.

Hence the (reasonable) choices that have to be made by the players in

∈

G
∗

and the relevant priorities that are seen are the same as in a corresponding

play of

G

. Thus, Player 0 has a winning strategy for

G

from
v
if, and only

G
∗
from position
ψ
0
(
v
). But since

G
∗

if, Player 0 has a winning strategy for

is the model-checking game for
ψ
0
(
v
)on

G

this is the case if, and only if,

=
ψ
0
(
v
).

G|

The formula
ψ
1
defining the winning region for Player 1 is defined similarly.

Notice that the formula
ψ
σ
has width two. An analogous construction can

be carried out in the
μ
-calculus. The corresponding formulae are

d−
1

(
V
0
∧

X
j
)
.

Win
d
=
νX
0
μX
1
νX
2
...λX
d−
1

P
j
∧
♦

X
j
)

∨

(
V
1
∧

P
j
∧

j
=0

Corollary 4.21
The following three problems are algorithmically equivalent,

in the sense that if one of them admits a polynomial-time algorithm, then all

of them do.

(1) Computing winning regions in parity games.

Search Nedrilad ::

Custom Search