Game Development Reference
In-Depth Information
where u
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
G∈PG
(resp.
PG d ), ψ σ is true in exactly those nodes in
G
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
is
ψ 0 ( x ):=[ gfp R 0 x. [ lfp R 1 x. ... [ fp R d− 1 x.ϕ ( x, R 0 ,...,R d− 1 )]( x ) ... ]( x ) ,
where
ϕ ( x, R 0 ,...,R d− 1 ):=
i<d
(( 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
G
=( V,V 0 ,V 1 ,P 0 ,...,P d− 1 ) and every position
v
V ,
= ψ 0 ( v )
G|
⇐⇒
Player 0 has a winning strategy for
G
from v.
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