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

Search Nedrilad ::

Custom Search