348
F. Delgrange et al.
2 Preliminaries
For a finite set Ω, let Dist(Ω ) =
μ : Ω → [0, 1] |
ω∈Ω μ(ω) = 1
be the set of
probability distributions over Ω with support supp(μ) = {ω ∈ Ω | μ(ω) > 0}. We
write R ≥0 = {|x| | x ∈ R} and R ∞ = R∪{∞} for the non-negative and extended
real numbers, respectively. 1
= 1, . . . , 1 denotes the vector of size ∈ N with
all entries 1. We just write 1 if is clear. Let pi denote the i
th entry and p · p
the dot product of p, p
∈ (R ∞ )
. p ≤ p
, p + p
, and |p| are entry-wise. For
Boolean expression cond , let [cond ] = 1 if cond is true and [cond ] = 0 otherwise.
2.1 Markov Decision Processes, Strategies, and End Components
Definition 1 (Markov decision process [36]). A Markov decision process
(MDP) is a tuple M = S, Act , P, s I with finite set of states S, initial state
s I ∈ S, finite set of actions Act , and transition function P : S × Act × S → [0, 1]
with
s ∈S P(s, α, s
) ∈ {0, 1} for all s ∈ S and α ∈ Act .
We fix an MDP M = S, Act , P, s I . Intuitively, P(s, α, s
) is the probability to
take a transition from s to s
when choosing action α. An infinite path in M is a
sequence π = s 0 α 1 s 1 α 2 · · · ∈ (S×Act )
ω with P(s i , α i+1 , s i+1 ) > 0 for all i ∈ N.
We write π[i] = s i for the (i+1)th state visited by π and define the length of π
as |π| = ∞. A finite path is a finite prefix ˆ
π = s 0 α 1 . . . α n s n of infinite path π,
where last(ˆ π) = s n ∈ S, |ˆ π| = n and ˆ
π[i] = s i for i ≤ n. The set of finite (infinite)
paths in M is denoted by Paths
M
fin (Paths
M
inf ). The enabled actions at a state
s ∈ S are given by the set Act (s) = {α ∈ Act | ∃ s
∈ S : P(s, α, s
) > 0}. We
assume Act (s) = ∅ for all s. If |Act (s)| = 1 for all s ∈ S, M is called a Markov
Chain (MC). We write M s for the MDP obtained by replacing the initial state
of M by s ∈ S. For s ∈ S and α ∈ Act , we define the set of successor states
succ(s, α) = {s
| P(s, α, s
) > 0}. For s
∈ S, the set of predecessor state-action
pairs is given by pre(s
) = {{s, α | P(s, α, s
) > 0}. For a set E ⊆ S × Act , we
define SE = {s ∈ S | ∃ α : s, α ∈ E}, Act E = {α ∈ Act | ∃ s : s, α ∈ E},
and PE(s, α, s
) = [s, α ∈ E] · [s
∈ SE] · P(s, α, s
). We say E is closed for
M if ∀ ∀s, α ∈ E : α ∈ Act (s) and succ(s, α) ⊆ SE.
Definition 2 (Sub-MDP). The sub-MDP of M, closed E ⊆ S × Act , and
s ∈ SE is given by ME, s = SE, Act E, PE, s. We also write ME for
the sub-MDP ME, s and an arbitrary state s ∈ SE.
Definition 3 (End Component). A non-empty set E ⊆ S × Act is an end
component (EC) of M if E is closed for M and for each pair of states s, s
∈ SE
there is a finite path ˆ
π ∈ Paths
ME
fin
with ˆ
π[0] = s and last(ˆ π) = s
. An EC E
is maximal, if there is no other EC E
with E E
. The set of all maximal end
components of M is MECS (M).
The maximal ECs of a Markov chain are also called bottom strongly connected
components (BSCCs). A strategy resolves nondeterminism in MDPs:
F. Delgrange et al.
2 Preliminaries
For a finite set Ω, let Dist(Ω ) =
μ : Ω → [0, 1] |
ω∈Ω μ(ω) = 1
be the set of
probability distributions over Ω with support supp(μ) = {ω ∈ Ω | μ(ω) > 0}. We
write R ≥0 = {|x| | x ∈ R} and R ∞ = R∪{∞} for the non-negative and extended
real numbers, respectively. 1
= 1, . . . , 1 denotes the vector of size ∈ N with
all entries 1. We just write 1 if is clear. Let pi denote the i
th entry and p · p
the dot product of p, p
∈ (R ∞ )
. p ≤ p
, p + p
, and |p| are entry-wise. For
Boolean expression cond , let [cond ] = 1 if cond is true and [cond ] = 0 otherwise.
2.1 Markov Decision Processes, Strategies, and End Components
Definition 1 (Markov decision process [36]). A Markov decision process
(MDP) is a tuple M = S, Act , P, s I with finite set of states S, initial state
s I ∈ S, finite set of actions Act , and transition function P : S × Act × S → [0, 1]
with
s ∈S P(s, α, s
) ∈ {0, 1} for all s ∈ S and α ∈ Act .
We fix an MDP M = S, Act , P, s I . Intuitively, P(s, α, s
) is the probability to
take a transition from s to s
when choosing action α. An infinite path in M is a
sequence π = s 0 α 1 s 1 α 2 · · · ∈ (S×Act )
ω with P(s i , α i+1 , s i+1 ) > 0 for all i ∈ N.
We write π[i] = s i for the (i+1)th state visited by π and define the length of π
as |π| = ∞. A finite path is a finite prefix ˆ
π = s 0 α 1 . . . α n s n of infinite path π,
where last(ˆ π) = s n ∈ S, |ˆ π| = n and ˆ
π[i] = s i for i ≤ n. The set of finite (infinite)
paths in M is denoted by Paths
M
fin (Paths
M
inf ). The enabled actions at a state
s ∈ S are given by the set Act (s) = {α ∈ Act | ∃ s
∈ S : P(s, α, s
) > 0}. We
assume Act (s) = ∅ for all s. If |Act (s)| = 1 for all s ∈ S, M is called a Markov
Chain (MC). We write M s for the MDP obtained by replacing the initial state
of M by s ∈ S. For s ∈ S and α ∈ Act , we define the set of successor states
succ(s, α) = {s
| P(s, α, s
) > 0}. For s
∈ S, the set of predecessor state-action
pairs is given by pre(s
) = {{s, α | P(s, α, s
) > 0}. For a set E ⊆ S × Act , we
define SE = {s ∈ S | ∃ α : s, α ∈ E}, Act E = {α ∈ Act | ∃ s : s, α ∈ E},
and PE(s, α, s
) = [s, α ∈ E] · [s
∈ SE] · P(s, α, s
). We say E is closed for
M if ∀ ∀s, α ∈ E : α ∈ Act (s) and succ(s, α) ⊆ SE.
Definition 2 (Sub-MDP). The sub-MDP of M, closed E ⊆ S × Act , and
s ∈ SE is given by ME, s = SE, Act E, PE, s. We also write ME for
the sub-MDP ME, s and an arbitrary state s ∈ SE.
Definition 3 (End Component). A non-empty set E ⊆ S × Act is an end
component (EC) of M if E is closed for M and for each pair of states s, s
∈ SE
there is a finite path ˆ
π ∈ Paths
ME
fin
with ˆ
π[0] = s and last(ˆ π) = s
. An EC E
is maximal, if there is no other EC E
with E E
. The set of all maximal end
components of M is MECS (M).
The maximal ECs of a Markov chain are also called bottom strongly connected
components (BSCCs). A strategy resolves nondeterminism in MDPs: