Game Development Reference
In-Depth Information
π be the MD optimal minimising strategy which exists by Proposition 5.6.
Then
( σ,π )
v
( σ,π )
v
sup
σ∈ Σ
π∈ Π P
inf
( Reach ( T )) = sup
σ∈ Σ P
( Reach ( T ))
( σ [ v ] )
v
sup
σ∈ Σ P
( Reach ( T ))
( σ [ v ] )
v
sup
σ∈ Σ
π∈ Π MD P
inf
( Reach ( T )) .
Now assume that the '
' direction of Equality (5.7) does not hold. Then
there is some ε> 0 such that
(1) there is an ε -optimal maximising strategy σ in v ;
(2) for every σ
( σ [ v ] )
v
Π MD s.t.
Σ there is π
P
( Reach ( T ))
val ( v )
2 ε .
Π MD such
Note that condition (2) implies that for every σ
Σ there is π
( σ,π )
v
( σ,π )
v
that either P
( ¬T U v )=1,or P
( ¬T U v ) < 1 and
( σ,π )
v
P
( ¬v U T )
T U v )
val ( v )
2 ε.
( σ,π )
v
1
−P
(
¬
Now consider the strategy σ of condition (1) and a play initiated in v .
Using condition (2) repeatedly, we obtain a strategy π
Π such that
whenever a state of the form wv is visited in the play G ( σ,π )
, then either
v
( σ,π )
wv
( σ,π )
wv
P
(
¬
T U v ) = 1, or
P
(
¬
T U v ) < 1 and
( σ,π )
wv
P
(
¬
v U T )
T U v )
val ( v )
2 ε.
( σ,π )
wv
1
−P
(
¬
( σ,π )
v
From this we obtain
P
( Reach ( T ))
val ( v )
2 ε which is a contradiction.
Finally, let us consider a temporal objective P F t where the atomic
proposition t is valid exactly in the target vertices of T . The next proposi-
tion (taken from Brazdil et al. [2009a]) answers the associated determinacy
question. Again, the answer seems somewhat unexpected.
Proposition 5.9
, ( V ,V ,V ) , Prob ) be a stochastic
game with a temporal objective P F t associated to a subset of target ver-
tices T
Let G =( V,
V . Then G is not necessarily determined. However, if G is finitely
branching, then it is determined.
Proof A counterexample for the first part of Proposition 5.9 is easy to
construct. Let G u and G v be the games of Figure 5.2 and Figure 5.3, where