Game Development Reference
InDepth Information
Hence even the problem of computing winning regions in reachability
games is
complete for LFP
via this logical notion of reduction.
4.5.3 Parity games with an unbounded number of priorities
We now show that winning regions of parity games are not definable in LFP
when the game graph may be infinite.
Theorem 4.25
are not definable in
LFP
, even
under the assumptions that the game graph is countable and the number of
priorities is finite.
Winning regions in
PG
Proof
Suppose that Win(
x
)
∈
LFP defines the winning region of Player 0
on
PG
. We use this formula to solve the modelchecking problem for LFP on
N
).
Recall that, for any
ϕ
(
x
)
=(
ω,
+
,
·
∈
LFP, we have a parity game
G
(
N
,ϕ
) such that,
for all
n
N

=
ϕ
(
n
)
⇐⇒ G
(
N
,ϕ
)

= Win(
v
n
)
(where
v
n
is the initial position associated with
ϕ
(
n
))
Further, the modelchecking game
G
(N
,ϕ
) is firstorder interpretable in N.
Hence the formula Win(
x
) is mapped, via a firstorder translation I
ϕ
,into
another LFPformula Win
ϕ
(
x
) such that
G
(
N
,ϕ
)

= Win(
v
n
)
⇐⇒
N

= Win
ϕ
(
n
)
.
Win
ϕ
(
x
) depends on
ϕ
, but does
not increase the alternation depth. Hence, on arithmetic, every formula
ϕ
(
x
)
would be equivalent to one of fixed alternation depth:
The firstorder translation Win(
x
)
→
N

=
ϕ
(
n
)
⇐⇒
N

= Win
ϕ
(
n
)
.
However, it is known that the alternation hierarchy of LFP on arithmetic
is strict.
Definability on finite graphs.
On finite game graphs, the definability
issues are different and closely related to complexity. One of the most inter
esting questions is whether the winning regions are definable in fixedpoint
logics such as LFP or the
μ
calculus.
It is not di
cult to see that the
μ
calculus is not su
cient (no matter how
one would precisely define a
μ
calculus on
). Again, this is a consequence
of the strictness of the alternation hierarchy. A
μ
calculus formula defining
PG
Search Nedrilad ::
Custom Search