Game Development Reference
InDepth 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 modelche
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 IFPformulae
poses no major di
culties. Proceeding by induction on the number of nested
fixedpoint formulae, one has to combine the argument just given (applied
to the outermost fixedpoint) with the correctness proof for the LFPmodel
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 fixedpoint.
On the other hand, an infinite play in an IFPmodelchecking 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 modelchecking
games for LFPformulae.
Search Nedrilad ::
Custom Search