Game Development Reference
In-Depth Information
the winning region of Player 0 on
PG
could be translated to formulae of the
PG d (for any fixed d ) with just a bounded
increase of the alternation depth. But this would mean that, for any d , the
winning regions of parity games with d priorities can be expressed by a
μ -calculus formula with a fixed alternation level, which would contradict the
strictness of the alternation hierarchy of L μ . For details, we refer to Dawar
We now turn to the least fixed-point logic LFP. Clearly, a proof that
winning regions of parity games in
usual μ -calculus on structures
are LFP-definable would imply that
parity games are solvable in polynomial time. Surprisingly, it turns out that
also the converse direction holds, despite the fact that LFP is weaker than
Ptime.
To prove this, we use a result by Otto [1999] saying that the multi-
dimensional μ -calculus, which is a fragment of LFP, captures precisely the
3.5.3] for an exposition of this result.
Winning positions in parity games are of course invariant under the usual
notion of bisimulation (e.g., as structures in
PG
PG d ). However, to apply Otto's
Theorem for parity games with an unbounded number of priorities, we have to
consider bisimulation on structures of the form
G
=( V,V 0 ,V 1 ,E,
, Odd). Let
be the vocabulary of parity games with a starting
node, and let Str( τ ) denote the class of all structures of this vocabulary. If
we have two such structures that are indeed parity games, then bisimilarity
as τ -structures coincides with the usual notion of bisimilarity in
τ =
{
V 0 ,V 1 ,E,
, Odd ,v
}
d , for
appropriate d . However, not all structures in Str( τ ) are parity games, and the
class of parity games is not closed under bisimulation. An e cient procedure
for deciding whether a structure is bisimilar to a parity game is to compute
its quotient under bisimulation and checking whether it is a parity game.
For a structure (
PG
b on
elements of G defined with respect to the binary relations E , and 1 .
That is to say is the largest relation satisfying:
G
,v )
Str( τ ) consider the bisimulation relation a
if a
b then a and b agree on the unary relations V 0 ,V 1 and Odd;
for every x
aE there is a y
bE such that x
y , and conversely;
for every x with a
x there is a y with b
y and x
y and conversely;
and finally
for every x ≺ a there is a y ≺ b such that x ∼ y , and conversely.
,v ) for the bisimulation quotient of (
We write (
G
G
,v ), i.e., the structure
whose elements are the equivalence classes in
G
with respect to
with the