Game Development Reference
. To see this, we compare playing
from a current position u
V 0 ∪
G ∗ from any position ϑ k ( u ), where ϑ k ( x ) is the subformula
[ gfp R k ... ]or[ lfp R k ... ]of ψ 0 ( x ). In
, Player 0 selects at position u
G ∗ , the play goes
from ϑ k ( u ) through the positions ϑ k +1 ( u ) ,...,ϑ d− 1 ( u ) to the inner formula
ϕ ( u, R 0 ,...,R d− 1 ).
This formula is a disjunction, so Verifier (Player 0) decides how to proceed.
But her only reasonable choice at this point is to move to the position
( V 0 u
a successor w
uE , and the play proceeds from w .In
R i y ), since with any other choice she would lose one
move later. But from there, the only reasonable move of Falsifier (Player 1)
is to go to position
P i u
y ( Euy
y ( Euy
R i y ), and it is now the turn of Player 0 to
select a successor w
R i w ). This forces Player 1 to
move to R i w from which the play proceeds to ϑ i ( w )).
Thus one move from u to w in
vE and move to ( Euw
corresponds to a sequence of moves
G ∗ from ϑ k ( u )to ϑ i ( w ), but the only genuine choice is the move from
y ( Euy
R i y )to( Euw
R i w ), i.e., the choice of a successor w
G ∗ the minimal, and hence relevant,
priority that is seen in the sequence of moves from ϑ k ( u )to ϑ i ( w ) is that of
R i w which is also i . The situation for positions u
, the position u has priority i , and in
V 1 ∩
P i is the same, except
G ∗ now goes through
that the play in
y ( Exy
R i y ) and it is Player 1 who
selects a successor w
uE and forces the play to R i w .
Hence the (reasonable) choices that have to be made by the players in
and the relevant priorities that are seen are the same as in a corresponding
. Thus, Player 0 has a winning strategy for
from v if, and only
G ∗ from position ψ 0 ( v ). But since
if, Player 0 has a winning strategy for
is the model-checking game for ψ 0 ( v )on
this is the case if, and only if,
= ψ 0 ( v ).
The formula ψ 1 defining the winning region for Player 1 is defined similarly.
Notice that the formula ψ σ has width two. An analogous construction can
be carried out in the μ -calculus. The corresponding formulae are
( V 0 ∧
X j ) .
Win d = νX 0 μX 1 νX 2 ...λX d− 1
P j ∧ ♦
X j )
( V 1 ∧
P j ∧
Corollary 4.21 The following three problems are algorithmically equivalent,
in the sense that if one of them admits a polynomial-time algorithm, then all
of them do.
(1) Computing winning regions in parity games.