Game Development Reference
relations V 0 ,V 1 ,E,
, Odd defined in the natural way and [ v ] as the starting
Str( τ ) is bisimilar to a
parity game if, and only if, its bisimulation quotient is a parity game, i.e.,
Prove that a structure (
,v ) ∼ ∈PG
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
, winning positions are LFP -definable.
Player 0 wins from initial position v . It su ces to construct a bisimulation-
invariant class X of structures ( H,u ) such that
be the class of parity games (
,v ), such that (
(1) X is decidable in polynomial time,
Indeed, by Otto's Theorem X is then definable by an LFP-formula ψ ( x ),
such that, given any parity game (
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
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
C = Win
given a parity game
, then it has the same winner as its bisimulation
quotient which is therefore correctly decided by the algorithm B .
of all finite parity games, winning regions
are LFP -definable if, and only if, they are computable in polynomial time.
On the class
For further results on the definability of winning regions in parity games,
we refer to Dawar and Gradel .