328
F. Funke et al.
Given a state t ∈ S, we let
Pr
max
s
(♦t) = sup
S
Pr
S
s (♦t) and Pr
min
s (♦t) = inf
S
Pr
S
s (♦t)
denote the maximal and minimal probability to reach t eventually when starting
in s and set Pr
min (♦t) = (Pr
min
s (♦t)) s∈S and Pr
max (♦t) = (Pr
max
s
(♦t)) s∈S . The
supremum and infimum is indeed attained by an MD-scheduler [13, Lemmata
10.102 and 10.113], thus justifying the superscripts.
Setting 2.2. Henceforth we will assume that M = (S all , Act, ι, P) has a unique
initial state s 0 ∈ S and two distinguished absorbing states fail and goal ∈
S all , i.e., P(goal, α, s) = 0 for all α ∈ Act and s ∈ S all with s
= goal, and
likewise for fail. Here goal represents a desirable outcome of the modeled system
and fail an outcome that is to be avoided. We use the notation S = S all \
{fail, goal}, we assume that every state s ∈ S is reachable from s 0 . We also
assume that under every scheduler fail or goal is reachable from any state, i.e.,
Pr
min
s (♦(goal ∨ fail)) > 0 for all s ∈ S. If M does not satisfy this condition from
the start, we can apply a standard preprocessing step, which is essentially given
by taking the MEC quotient of M, see [2, 3] and also [26]. While it is often
easier to verify the condition Pr
min
s (♦(goal ∨ fail)) > 0, it is in fact equivalent to
Pr
min
s (♦(goal ∨ fail)) = 1 (see the full version [42]).
Whenever suitable, we denote by M also the set of enabled state-action pairs,
i.e., M = {(s, α) ∈ S × Act | α ∈ Act(s)}. Let A ∈ R
M×S be defined by
A((s, α), t) =
1 − P(s, α, s), if s = t
−P(s, α, t),
if s = t
We denote by b = (b(s, α)) (s,α)∈M ∈ R
M with b(s, α) = P(s, α, goal) and by
δ s0 the probability distribution that assigns 1 to s 0 , and 0 to all other states.
The vectors Pr
min (♦ goal) and Pr
max (♦ goal) can be characterized using the
following linear programs. Although this characterization is well-known, we give a
proof in the full version [42] due to slight differences with the standard literature.
Proposition 2.3 (LP characterization, cf. [16, Lemma 8]). Let M be
an MDP as in Setting 2.2 and let δ ∈ R
n
>0 . Then the vectors Pr
min (♦ goal) and
Pr
max (♦ goal) are, respectively, the unique solution of the LPs
max δ · z s.t. Az ≤ b
and
min δ · z s.t. Az ≥ b.
3 Farkas certificates for reachability in MDPs
In this section we establish certificates for the following statements:
(1) All schedulers S satisfy Pr
S
s0 (♦ goal) λ (i.e., Pr
min
s0 (♦ goal) λ).
(2) Some scheduler S satisfies Pr
S
s0 (♦ goal) λ (i.e., Pr
max
s0 (♦ goal) λ).
(3) All schedulers S satisfy Pr
S
s0 (♦ goal) λ (i.e., Pr
max
s0 (♦ goal) λ).
(4) Some scheduler S satisfies Pr
S
s0 (♦ goal) λ (i.e., Pr
min
s0 (♦ goal) λ).
where ∈ {≤, <} and ∈ {≥, >}. The basis of our construction is the LP
characterization of the probabilities above and, crucially, Farkas’ Lemma.
F. Funke et al.
Given a state t ∈ S, we let
Pr
max
s
(♦t) = sup
S
Pr
S
s (♦t) and Pr
min
s (♦t) = inf
S
Pr
S
s (♦t)
denote the maximal and minimal probability to reach t eventually when starting
in s and set Pr
min (♦t) = (Pr
min
s (♦t)) s∈S and Pr
max (♦t) = (Pr
max
s
(♦t)) s∈S . The
supremum and infimum is indeed attained by an MD-scheduler [13, Lemmata
10.102 and 10.113], thus justifying the superscripts.
Setting 2.2. Henceforth we will assume that M = (S all , Act, ι, P) has a unique
initial state s 0 ∈ S and two distinguished absorbing states fail and goal ∈
S all , i.e., P(goal, α, s) = 0 for all α ∈ Act and s ∈ S all with s
= goal, and
likewise for fail. Here goal represents a desirable outcome of the modeled system
and fail an outcome that is to be avoided. We use the notation S = S all \
{fail, goal}, we assume that every state s ∈ S is reachable from s 0 . We also
assume that under every scheduler fail or goal is reachable from any state, i.e.,
Pr
min
s (♦(goal ∨ fail)) > 0 for all s ∈ S. If M does not satisfy this condition from
the start, we can apply a standard preprocessing step, which is essentially given
by taking the MEC quotient of M, see [2, 3] and also [26]. While it is often
easier to verify the condition Pr
min
s (♦(goal ∨ fail)) > 0, it is in fact equivalent to
Pr
min
s (♦(goal ∨ fail)) = 1 (see the full version [42]).
Whenever suitable, we denote by M also the set of enabled state-action pairs,
i.e., M = {(s, α) ∈ S × Act | α ∈ Act(s)}. Let A ∈ R
M×S be defined by
A((s, α), t) =
1 − P(s, α, s), if s = t
−P(s, α, t),
if s = t
We denote by b = (b(s, α)) (s,α)∈M ∈ R
M with b(s, α) = P(s, α, goal) and by
δ s0 the probability distribution that assigns 1 to s 0 , and 0 to all other states.
The vectors Pr
min (♦ goal) and Pr
max (♦ goal) can be characterized using the
following linear programs. Although this characterization is well-known, we give a
proof in the full version [42] due to slight differences with the standard literature.
Proposition 2.3 (LP characterization, cf. [16, Lemma 8]). Let M be
an MDP as in Setting 2.2 and let δ ∈ R
n
>0 . Then the vectors Pr
min (♦ goal) and
Pr
max (♦ goal) are, respectively, the unique solution of the LPs
max δ · z s.t. Az ≤ b
and
min δ · z s.t. Az ≥ b.
3 Farkas certificates for reachability in MDPs
In this section we establish certificates for the following statements:
(1) All schedulers S satisfy Pr
S
s0 (♦ goal) λ (i.e., Pr
min
s0 (♦ goal) λ).
(2) Some scheduler S satisfies Pr
S
s0 (♦ goal) λ (i.e., Pr
max
s0 (♦ goal) λ).
(3) All schedulers S satisfy Pr
S
s0 (♦ goal) λ (i.e., Pr
max
s0 (♦ goal) λ).
(4) Some scheduler S satisfies Pr
S
s0 (♦ goal) λ (i.e., Pr
min
s0 (♦ goal) λ).
where ∈ {≤, <} and ∈ {≥, >}. The basis of our construction is the LP
characterization of the probabilities above and, crucially, Farkas’ Lemma.