Game Development Reference
v means that u has a smaller priority than v , and Odd is the set
of nodes with an odd priority. We denote this class of structures by
In each case, when we say that winning regions of parity games are definable
in a logic L , we mean that there is is a formula ψ 0 and ψ 1 of L such that
for any structure
PG d ), ψ σ is true in exactly those nodes in
from which Player σ has a winning strategy.
4.5.1 Parity games with a bounded number of priorities
For any fixed d , the winning regions of parity games in PG d are definable by
LFP-formulae with d nested fixed-point operators. For Player 0, the formula
ψ 0 ( x ):=[ gfp R 0 x. [ lfp R 1 x. ... [ fp R d− 1 x.ϕ ( x, R 0 ,...,R d− 1 )]( x ) ... ]( x ) ,
ϕ ( x, R 0 ,...,R d− 1 ):=
(( V 0 x
P i x
y ( Exy
R i y ))
( V 1 x
P i x
y ( Exy
R i y ))) .
The fixed-point operators alternate between gfp and lfp , and hence fp =
gfp if d is odd, and fp = lfp if d is even.
Theorem 4.20 For every d ∈ N , the formula ψ 0 defines the winning region
of Player 0 in parity games with priorities 0 ,...,d− 1 .
Proof In general, LFP-formulae are hard to understand, especially if they
have many alternations between least and greatest fixed-points. However, in
this case have an elegant argument based on model-checking games to prove
that, for every parity game
=( V,V 0 ,V 1 ,P 0 ,...,P d− 1 ) and every position
= ψ 0 ( v )
Player 0 has a winning strategy for
Let G ∗ be the model-checking game for the formula ψ 0 ( v )on G and identify
Verifier with Player 0 and Falsifier with Player 1. Hence, Player 0 has a
winning strategy for G ∗ if, and only if, G| = ψ 0 ( v ).
By the construction of model-checking games, G ∗ has positions of the form
η ( u ), where u
V and η is a subformula of ψ 0 . The priority of a position
R i u is i , and when η ( u ) is not of this form, then its priority is d .
We claim that the game
G ∗ is essentially, i.e., up to elimination of stupid
moves (which would lead to a loss within one or two moves) and up to
contraction of several consecutive moves into one, the same as the original