Game Development Reference

In-Depth Information

relations
V
0
,V
1
,E,

≺

,
Odd defined in the natural way and [
v
] as the starting

vertex.

Exercise 4.5

Str(
τ
) is bisimilar to a

parity game if, and only if, its bisimulation quotient is a parity game, i.e.,

(

Prove that a structure (

G

,v
)

∈

,v
)
∼
∈PG

G

.

Theorem 4.26

be any class of parity games on finite game graphs,

such that winning positions on its bisimulation quotients are decidable in

polynomial time. Then, on

Let

C

C

, winning positions are
LFP
-definable.

Proof

, and

Player 0 wins from initial position
v
. It su
ces to construct a bisimulation-

invariant class
X
of structures (
H,u
) such that

Let Win

C

be the class of parity games (

G

,v
), such that (

G

,v
)

∈C

(1)
X
is decidable in polynomial time,

(2)
X

∩C

= Win

C

.

Indeed, by Otto's Theorem
X
is then definable by an LFP-formula
ψ
(
x
),

such that, given any parity game (

G

,v
)

∈C

we have

G,v∈
Win
C⇐⇒G,v∈ X ⇐⇒ G |
=
ψ
(
v
)
.

By assumption, there exists a polynomial time algorithm
A
which, given a

parity game (

∈C
∼
, decides whether Player 0 wins

from
v
.Itisnot

important what the algorithm returns for quotients outside

G

,v
)

G

C
∼
, as long as

it is isomorphism-invariant and halts in polynomial time. Finally, let
B
be

the algorithm which, given any finite structure in Str(
τ
), first computes its

bisimulation quotient, and then applies algorithm
A
.

Clearly
B
is a polynomial time algorithm, since bisimulation quotients

are e
ciently computable. Further the class
X
of structures accepted by

B
is invariant under bisimulation. Indeed, let

H
be two bisimilar

structures. Then their bisimulation quotients are isomorphic and are therefore

either both accepted or both rejected by
A
. Finally,
X

H

and

∩

C
= Win

C

. Indeed,

given a parity game

, then it has the same winner as its bisimulation

quotient which is therefore correctly decided by the algorithm
B
.

G

,v

∈C

Corollary 4.27

of all finite parity games, winning regions

are
LFP
-definable if, and only if, they are computable in polynomial time.

On the class

PG

For further results on the definability of winning regions in parity games,

we refer to Dawar and Gradel [2008].

Search Nedrilad ::

Custom Search