Game Development Reference

In-Depth Information

bilistic model for message losses. Usually, it is assumed that each individual

message is lost independently with probability
λ>
0 in every step. A

stochastic game with lossy channels (SGLC) is obtained by splitting the

control states into two disjoint subsets that are controlled by player

and

player

, respectively. However, message losses still occur randomly.

In Baier et al. [2006], it was shown that SGLC with qualitative reach-

ability objectives are decidable. MDPs with lossy channels and various

ω
-regular objectives were examined by Baier et al. [2007]. SGLC with

Buchi objectives were studied recently by Abdulla et al. [2008].

♦

•

One-counter stochastic games.
These are stochastic games generated

by one-counter machines, i.e., finite-state automata equipped with an

unbounded counter which can store non-negative integers. The set of

control states is split into three disjoint subsets controlled by player

,

player

, or the random player, who are responsible for selecting one of

the available transitions. One-counter MDPs with various reachability

objectives were recently studied by Brazdil et al. [2010].

♦

5.2.2 Win-lose games

Another important class of zero-sum stochastic turned-based games are

win-lose games
where the objective of player is to satisfy some property

which is either valid or invalid for every play of
G
(the associated yield

assigns 1 to the plays where the property is valid, and 0 to the other plays).

An important subclass of such properties are
temporal objectives
that can

be encoded as formulae of suitable temporal logics.

Let
ϕ
be a formula which is either valid or invalid in every state of every

play of
G
. We say that a strategy
σ ∈
Σis
ϕ
-winning in
v
if for every

strategy
π ∈
Π we have that the state
v
of
G
(
σ,π
)

satisfies
ϕ
. Similarly, a

v

strategy
π

∈

Πis

¬

ϕ-winning in v
if for every
σ

∈

Σ we have that the state

v
of
G
(
σ,π
)

does
not
satisfy
ϕ
. We say that
G
(with
ϕ
)is
determined
if for

v

every
v

∈

V
either player

has a
ϕ
-winning strategy in
v
or player

♦

has a

¬

ϕ
-winning strategy in
v
.

Temporal logics can be classified as
linear-time
or
branching-time
, de-

pending on whether they 'ignore' the branching structure of transition systems

or not, respectively (see, e.g., Emerson [1991]). The syntax of these logics

is built upon a countable set
Ap
=

{

a, b, c, . . .

}

of
atomic propositions
.A

2
Ap

valuation
is a function
ν
:
V

→

which to every vertex
v
assigns the set

ν
(
v
)

Ap
of all atomic propositions that are valid in
v
. Note that
ν
can be

naturally extended to the states of a play of
G
(for every state
wv

⊆

V
∗
V

∈

Search Nedrilad ::

Custom Search