330
F. Funke et al.
Proposition 3.3. For ∈ {≥, >} and ∈ {≤, <} we have
Pr
min
s0 (♦ goal) λ ⇐⇒ ∃y ∈ R
M
≥0 . yA ≥ δ s0 ∧ yb λ
Pr
max
s0 (♦ goal) λ ⇐⇒ ∃y ∈ R
M
≥0 . yA ≤ δ s0 ∧ yb λ
Together, Corollary 3.2 and Proposition 3.3 give us all certificate conditions
of Table 1.
4 Minimal witnesses for reachability in MDPs
In this section we consider the following problem: Given an MDP M that satisfies
the property Pr
min
M,s0 (♦ goal) ≥ λ (or Pr
max
M,s0 (♦ goal) ≥ λ), find a small subsystem
M
of M that still satisfies these thresholds. Such a subsystem is a witness to
the satisfaction of the property in M. We first define subsystems and consider
different measures of size which we show to be equivalent. Then we deal with the
question of finding minimal witnessing subsystems.
Subsystems, witnesses and notions of minimality. Our definition of subsystem is essentially the same to the definition in [77, 78] that was used for
witnessing subsystems of Pr
max
M,s0 (♦ goal) λ. From now on we restrict our
attention to properties of the form Pr
min / max
M,s0
(♦ goal) λ. One can deal with
upper bounds by exchanging the roles of fail and goal and invoking the equality
Pr
min
M,s0 (♦ goal) = 1− Pr
max
M,s0 (♦ fail), which holds by the conditions of Setting 2.2.
Intuitively, a subsystem M
of M contains a subset of states of M, and
a transition of M originating in a state of M
remains unchanged in M
or
is redirected to fail (instead of explicitely redirecting to fail, sub-stochastic
distributions are used in [77, 78] with the same effect).
Definition 4.1 (Subsystem and witness). Let M = (S all , Act, s 0 , P) be an
MDP as in Setting 2.2. A subsystem M
⊆ M is an MDP M
= (S
all , Act, s 0 , P
)
with fail, goal ∈ S
all ⊆ S all , Act M (s) = Act M (s) for all s ∈ S
all , and for all
s, t ∈ S
all with t = fail and α ∈ Act we have
P
(s, α, t) > 0 =⇒ P
(s, α, t) = P(s, α, t).
We say that the states S all \S
all and the transitions (s, α, t) with P(s, α, t) > 0 and
P
(s, α, t) = 0 have been deleted in M
. A witness for Pr
min / max
M,s0
(♦ goal) λ is
a subsystem M
⊆ M such that Pr
min / max
M ,s0
(♦ goal) λ.
Remark 4.2. The condition Act M (s) = Act M (s) ensures that the probability of
a deleted transition (s, α, t) is added to (s, α, fail). This is essential for witnesses
for Pr
min
M,s0 (♦ goal) λ as one could otherwise remove entire actions causing
low probabilities and obtain greater Pr
min in M
than in M as a result. For
witnesses of Pr
max
M ,s0 (♦ goal) λ one could delete this condition, thus leading to
the notion of [77, 78].
F. Funke et al.
Proposition 3.3. For ∈ {≥, >} and ∈ {≤, <} we have
Pr
min
s0 (♦ goal) λ ⇐⇒ ∃y ∈ R
M
≥0 . yA ≥ δ s0 ∧ yb λ
Pr
max
s0 (♦ goal) λ ⇐⇒ ∃y ∈ R
M
≥0 . yA ≤ δ s0 ∧ yb λ
Together, Corollary 3.2 and Proposition 3.3 give us all certificate conditions
of Table 1.
4 Minimal witnesses for reachability in MDPs
In this section we consider the following problem: Given an MDP M that satisfies
the property Pr
min
M,s0 (♦ goal) ≥ λ (or Pr
max
M,s0 (♦ goal) ≥ λ), find a small subsystem
M
of M that still satisfies these thresholds. Such a subsystem is a witness to
the satisfaction of the property in M. We first define subsystems and consider
different measures of size which we show to be equivalent. Then we deal with the
question of finding minimal witnessing subsystems.
Subsystems, witnesses and notions of minimality. Our definition of subsystem is essentially the same to the definition in [77, 78] that was used for
witnessing subsystems of Pr
max
M,s0 (♦ goal) λ. From now on we restrict our
attention to properties of the form Pr
min / max
M,s0
(♦ goal) λ. One can deal with
upper bounds by exchanging the roles of fail and goal and invoking the equality
Pr
min
M,s0 (♦ goal) = 1− Pr
max
M,s0 (♦ fail), which holds by the conditions of Setting 2.2.
Intuitively, a subsystem M
of M contains a subset of states of M, and
a transition of M originating in a state of M
remains unchanged in M
or
is redirected to fail (instead of explicitely redirecting to fail, sub-stochastic
distributions are used in [77, 78] with the same effect).
Definition 4.1 (Subsystem and witness). Let M = (S all , Act, s 0 , P) be an
MDP as in Setting 2.2. A subsystem M
⊆ M is an MDP M
= (S
all , Act, s 0 , P
)
with fail, goal ∈ S
all ⊆ S all , Act M (s) = Act M (s) for all s ∈ S
all , and for all
s, t ∈ S
all with t = fail and α ∈ Act we have
P
(s, α, t) > 0 =⇒ P
(s, α, t) = P(s, α, t).
We say that the states S all \S
all and the transitions (s, α, t) with P(s, α, t) > 0 and
P
(s, α, t) = 0 have been deleted in M
. A witness for Pr
min / max
M,s0
(♦ goal) λ is
a subsystem M
⊆ M such that Pr
min / max
M ,s0
(♦ goal) λ.
Remark 4.2. The condition Act M (s) = Act M (s) ensures that the probability of
a deleted transition (s, α, t) is added to (s, α, fail). This is essential for witnesses
for Pr
min
M,s0 (♦ goal) λ as one could otherwise remove entire actions causing
low probabilities and obtain greater Pr
min in M
than in M as a result. For
witnesses of Pr
max
M ,s0 (♦ goal) λ one could delete this condition, thus leading to
the notion of [77, 78].