Game Development Reference
In-Depth Information
of the only player we have that
P v ( {w ∈ Run ( G ( τ v ,v ) | w | = ν ψ} ) .
(5.3)
For finite-state 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 (infinite-state) 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 model-checking problem
for stochastic games and formulae of probabilistic branching-time 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 branching-time objectives. As we shall
see, this difference is substantial.
|
The problems of interest
Let
be a class of turn-based 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 linear-time 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