Game Development Reference
In-Depth Information
v isanodeof
K
, such that
K
,v
|
= ϕ if, and only if, Player 0 has a winning
strategy in
) from position ( ϕ, v ). As a consequence, an e cient
algorithm for solving parity games would also solve the model-checking
problem for L μ .
Since L μ -formulae can be seen as LFP-formulae of width two, the bounds
established in the previous section apply: The model-checking problem for
L μ is in UP
G
(
K
Co-UP, and it is a major open problem whether it can be
solved in polynomial time. For L μ -formulae of bounded alternation depths,
the associated parity games have a bounded number of priorities and can
therefore be solved in polynomial time.
Also the structure complexity can be settled easily. Since L μ is a fragment
of LFP, all properties expressible in L μ are decidable in polynomial time.
Further, there exist ψ
L μ for which the model-checking problem is Ptime-
complete. Indeed, winning regions of reachability games are definable not only
in LFP, but also in the μ -calculus. In a game G =( V,V 0 ,V 1 ,E ), Player 0 has
a winning strategy from v if, and only if, G, v
X )).
Despite this result, the μ -calculus is far away from a logic that would
capture Ptime. Since L μ is a fragment of MSO, all word languages definable
in L μ are regular languages , and of course, not all Ptime-languages are
regular.
|
= μX. (( V 0
X )
( V 1
4.5 Definability of winning regions in parity games
We have seen that the model-checking problem for the LFP and the modal
μ -calculus can be reduced to the problem of computing winning regions
in parity games. We now discuss the question of whether, and under what
conditions, winning regions of parity games are definable in LFP and the
μ -calculus.
To study questions of logical definability for parity games ( V,V 0 ,V 1 ,E, Ω)
we need to represent the games as relational structures. We distinguish
between two cases.
For fixed d , we consider parity games where the range of the priority
function Ω is in
=( V,V 0 ,V 1 ,E,P 0 ,...,P d− 1 )
where P 0 ,...,P d− 1 are pairwise disjoint unary relations such that P i is the
set of positions v with Ω( v )= i . We denote this class of structures by
{
0 ,...,d
1
}
as structures
G
PG d .
On the other hand, to consider classes of parity games with an unbounded
number of priorities , we consider them as structures
G
=( V,V 0 ,V 1 ,E,
, Odd)