Game Development Reference
In-Depth Information
Theorem 4 .30
If
A |
= ψ ( a ) , then Verifier wins the game
G
(
A
( a )) from
position ψ ( a ) .If
A |
= ψ ( a ) , then Falsifier wins the game
G
(
A
( a )) from
position ψ ( a ) .
Proof
Suppo se first that
A |
= ψ ( a ). Then there is some ordinal α<ω such
= ϕ α ( a ). We construct a w inning strategy for Verifier in the game
that
A |
G
(
A
( a )) starting at position ψ ( a ).
From ψ ( a ) the game procee ds to ( T a
ϕ ( a )). At this position, Verifier
repeatedly chooses the node T a until this node has been visited α -times.
After that, she backtracks and moves to ϕ ( a ). By Lemma 4.29 and since
A | = ϕ α ( a ), Verifier has a strategy to win the remaining play.
Now suppose that A | = ψ ( a ). If, after αT -positions, one of the players
backtrac ks , then Falsifier has a winning strategy for the remaining game, since
A |
= ϕ α ( a ). Hence, the only possibility fo r Verifier to win the game in a finite
number of moves is to avoid positions T b where Fa ls ifier can bac kt rack. C on -
sider the formulae ϕ f , with ϕ f = false and ϕ α + f ( x )= ϕ [ T/ϕ f , T/false ]( x ).
They define the stages of [ ifp T x.ϕ [ T,false ]( x )], obtained from ψ by replac-
ing negative occurrences of T by false . If V erifier could force a finit e winning
play, with α
1 positions of the form T c and without positions T c , then
she woul d in fact have a winning strategy for the model-che c king game
G
f ( a )). Since ψ f implies ϕ α , it would follow that
= ϕ α ( a ). But this
(
A
A |
is impossible.
The extension of the proof of Theorem 4.30 to arbitrary IFP-formulae
poses no major di culties. Proceeding by induction on the number of nested
fixed-point formulae, one has to combine the argument just given (applied
to the outermost fixed-point) with the correctness proof for the LFP-model-
checking games. Notice that the essential differences between backtracking
games and parity games are in the effects of backtracking moves. Backtracking
moves impose a finiteness condition on one priority (unless it is later released
by smaller priority) and the effect of such a move remains essentially the
same in the general case as in the case of formulae with a single fixed-point.
On the other hand, an infinite play in an IFP-model-checking game is a play
in which the backtracking moves do not play a decisive role. The winner of
such a play is determined by the parity condition and the analysis of such
plays closely follows the proof that parity games are the model-checking
games for LFP-formulae.