Game Development Reference

In-Depth Information

where
u

v
means that
u
has a smaller priority than
v
, and Odd is the set

of nodes with an odd priority. We denote this class of structures by

≺

.

In each case, when we say that winning regions of parity games are definable

in a logic
L
, we mean that there is is a formula
ψ
0
and
ψ
1
of
L
such that

for any structure

PG

G∈PG

(resp.

PG
d
),
ψ
σ
is true in exactly those nodes in

G

from which Player
σ
has a winning strategy.

4.5.1 Parity games with a bounded number of priorities

For any fixed
d
, the winning regions of parity games in
PG
d
are definable by

LFP-formulae with
d
nested fixed-point operators. For Player 0, the formula

is

ψ
0
(
x
):=[
gfp
R
0
x.
[
lfp
R
1
x. ...
[
fp
R
d−
1
x.ϕ
(
x, R
0
,...,R
d−
1
)](
x
)
...
](
x
)
,

where

ϕ
(
x, R
0
,...,R
d−
1
):=

i<d

((
V
0
x

∧

P
i
x

∧∃

y
(
Exy

∧

R
i
y
))

∨

(
V
1
x

∧

P
i
x

∧∀

y
(
Exy

→

R
i
y
)))
.

The fixed-point operators alternate between
gfp
and
lfp
, and hence
fp
=

gfp
if
d
is odd, and
fp
=
lfp
if
d
is even.

Theorem 4.20
For every d ∈
N
, the formula ψ
0
defines the winning region

of Player 0 in parity games with priorities
0
,...,d−
1
.

Proof
In general, LFP-formulae are hard to understand, especially if they

have many alternations between least and greatest fixed-points. However, in

this case have an elegant argument based on model-checking games to prove

that, for every parity game

G

=(
V,V
0
,V
1
,P
0
,...,P
d−
1
) and every position

v

∈

V
,

=
ψ
0
(
v
)

G|

⇐⇒

Player 0 has a winning strategy for

G

from
v.

Let
G
∗
be the model-checking game for the formula
ψ
0
(
v
)on
G
and identify

Verifier with Player 0 and Falsifier with Player 1. Hence, Player 0 has a

winning strategy for
G
∗
if, and only if,
G|
=
ψ
0
(
v
).

By the construction of model-checking games,
G
∗
has positions of the form

η
(
u
), where
u

V
and
η
is a subformula of
ψ
0
. The priority of a position

R
i
u
is
i
, and when
η
(
u
) is not of this form, then its priority is
d
.

We claim that the game

∈

G
∗
is essentially, i.e., up to elimination of stupid

moves (which would lead to a loss within one or two moves) and up to

contraction of several consecutive moves into one, the same as the original

Search Nedrilad ::

Custom Search