Game Development Reference
InDepth Information
of the only player we have that
P
v
(
{w ∈ Run
(
G
(
τ
v
,v
)
 w 
=
ν
ψ}
)
.
(5.3)
For finitestate MDPs, condition (5.3) is equivalent to
Run
(
G
(
τ
v
,v
)
=
ν
ψ
in
τ
{P
v
(
{
w
∈

w

}
)
}
(5.4)
which is exactly the semantics proposed by Bianco and de Alfaro [1995]. For
general (infinitestate) MDPs, conditions (5.3) and (5.4) are not equivalent.
At first glance, one might be tempted to think that
v
=
ν
ψ
iff player
has a
ϕ
winning strategy in
v
. A straightforward induction on the structure
of
ϕ
reveals that '

' holds, but the opposite direction is
invalid
.Tosee
this, consider the formula
ϕ
⇒
(
P
>
0
F
a
)
(
P
>
0
F
b
) and the vertex
v
of the
≡
∨
following game, where
ν
(
u
a
)=
{
a
}
and
ν
(
u
b
)=
{
b
}
:
u
a
u
b
v
Intuitively, the formula
ϕ
says 'a state satisfying
a
is reachable, or a state
satisfying
b
is reachable'. Note that player
has a
ϕ
winning strategy in
v
(in
=
ν
P
>
0
F
a
, because
fact, every strategy of player
is
ϕ
winning). However,
v

player
♦
has a strategy which makes the vertex
u
a
unreachable. Similarly,
=
ν
ϕ
. This means that the
modelchecking
problem
for stochastic games and formulae of probabilistic branchingtime logics (i.e.,
the question of whether
v
=
ν
P
>
0
F
b
, and hence
v
v


=
ν
ϕ
)is
different
from the problem of deciding
the winner in stochastic games with branchingtime objectives. As we shall
see, this difference is substantial.

The problems of interest
Let
be a class of turnbased stochastic games and Φ a class of temporal
objectives. The most important questions about the games of
G
G
and the
objectives of Φ include the following:
(1)
Are all games of
determined for all objectives of
Φ
?
(2)
What is the type of winning strategies if they exist?
(3)
Who wins in a given vertex?
(4)
Can we compute winning strategies?
G
As we shall see in Section 5.3.2, stochastic games with temporal objectives
are
not
necessarily determined (even for lineartime objectives). This means
that 'nobody' is an eligible answer to Question (3). Since randomisation and
memory can help the players to win, Question (3) can be refined into
'Does
player
(or player
♦
) have a winning strategy of type XY in a given vertex
Search Nedrilad ::
Custom Search