Game Development Reference
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
, respectively. However, message losses still occur randomly.
In Baier et al. , 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. . SGLC with
Buchi objectives were studied recently by Abdulla et al. .
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
, 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. .
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
ϕ-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 either player
has a ϕ -winning strategy in v or player
ϕ -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 ). The syntax of these logics
is built upon a countable set Ap =
a, b, c, . . .
of atomic propositions .A
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