Game Development Reference
InDepth Information
after the play has gone through
αT
positions, then the play ends when
α
further
T
p
ositions have been visited. Falsifier h
as
won, if the last of these is
of form
T c
, and Verifier has won if it is of form
T c
.
The differences between IFP modelchecking and LFP modelchecking are
in fact best illustrated with this simple case. We claim that Verifier has a
winning strategy for the game
G
(
A
,ψ
)if
A

=
ψ
and Falsifier has a winning
strategy if
=
ψ
.
We lo
o
k at the firstorder for
m
ulae
ϕ
α
de
fining the st
ages
of
th
e induction.
Let
ϕ
0
(
a
)=
false
and
ϕ
α
+1
(
a
)=
ϕ
α
(
a
)
A

ϕ
[
T/ϕ
α
, T/ϕ
α
](
x
). On finite
∨
≡
α<ω
ϕ
α
(
a
).
The
fir
storder game
structures
ψ
(
a
)
,ϕ
α
(
a
)) ca
n
be seen as an unfolding of the game
G
(
A
,ϕ
α
(
a
)) corresponds to a unique position
G
(
A
,ψ
(
a
))
.
Every position in
G
(
A
in
,ψ
(
a
)), and conversely, for a pair (
p, β
) where
p
is a position of
G
(A
,ϕ
α
(
a
)) and
β ≤ α
is an ordinal, there is a unique associated position
p
β
of the unfolded game
G
(A
,ϕ
α
(
a
)). When a play in
G
(A
,ϕ
α
(
a
)) reaches
a position
T c
, it is regenerated to either
T c
or
ϕ
(
T,c
) and such a regener
ation move decrements the associated ordinal. T
h
e corresponding play in
G
(A
,ϕ
α
(
a
)) proceeds to position
ϕ
β
(
c
)or
ϕ
[
T/ϕ
β
, T/ϕ
β
](
c
). We can use this
correspondence to translate strategies between the two games. Noti
c
e that
the lifting of a positional strategy
f
in the unfolded game
G
(
A
,ϕ
α
(
a
)) will
G
(
A
produce a nonpositional strategy
f
∗
in the original game
,ψ
): start with
β
=
α
and, for any position
p
, let
f
∗
(
p
):=
f
(
p
β
); at regeneration moves, the
ordinal
β
is decremented.
Consider now a play in
G
(
A
,ψ
) after a backtracking mo
ve
prior to which
βT
positions have been visited, and suppose that
G
(
A
=
ϕ
β
(
a
). Then Verifier
A

,ϕ
β
(
a
)) (from position
ϕ
β
(
a
)) which translates into a (nonpositional) strategy for the game
has
a
winning strategy in the firstorder game
G
(
A
,ψ
)
with the following properties: Any play that is consistent with this strategy
will either be winning for Verifier before
βT
positions have been seen, or
the
β
th
T
position wi
ll
be negative.
Similarly, if
G
(
A
=
ϕ
β
(
a
) then Falsifier has a winning strategy for
,ϕ
β
(
a
)),
A

G
(
A
and this strategy translates into a strategy for the game
,ψ
) by which
Falsifier forces the play (after backtracking) from position
ψ
(
a
) to a positive
β
th
T
position, unless she wins before
βT
positions have been seen. We
hence have established the following fact.
G
(
A
Lemma 4.29
Suppose that a play on G
(A
,ψ
)
has been backtracked to the
initial position ψ
(
a
)
after βTpositions have been visited. Veri
fi
er has a
winning strategy for the remaining game if, and only if,
=
ϕ
β
(
a
)
.
A

From this we obtain the desired result.
Search Nedrilad ::
Custom Search