Game Development Reference
In-Depth 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 model-checking 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 model-checking game G (N ) is first-order interpretable in N.
Hence the formula Win( x ) is mapped, via a first-order translation I ϕ ,into
another LFP-formula 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 first-order 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 fixed-point
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