Game Development Reference
In-Depth 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 model-checking and LFP model-checking 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 first-order 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 st-order 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 non-positional strategy f in the original game
β = α 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 (non-positional) strategy for the game
has a winning strategy in the first-order 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 βT-positions 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.

Custom Search