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

and Gradel [2008]

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

bisimulation-invariant
part of Ptime. See also [Gradel et al., 2007, Section

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

Search Nedrilad ::

Custom Search