Farkas certificates and minimal witnesses
331
s 0
t
u
v
fail
goal
α
β
α
α
γ
α
γ
β
(a)
s 0
u
v
fail
goal
α
β
α
γ
α
γ
β
(b)
Fig. 1: An MDP (with omitted probabilities (a)) and a subsystem (b), where
redirected transitions are dashed.
Example 4.3. Figure 1a depicts an MDP and Figure 1b indicates the subsystem
that is obtained by deleting the state t and additionally the transition (u, α, s 0 ).
The following lemma ensures that we can use the subsystems as witnesses for
both Pr
max
M,s0 (♦ goal) λ and Pr
min
M,s0 (♦ goal) λ.
Lemma 4.4. Let M be an MDP as in Setting 2.2 and M
⊆ M. Then:
Pr
min
M ,s0 (♦ goal) ≤ Pr
min
M,s0 (♦ goal) and Pr
max
M ,s0 (♦ goal) ≤ Pr
max
M,s0 (♦ goal)
We consider the following notions of minimality for subsystems:
(1) State-minimality: |S
all | is minimal.
(2) Transition-minimality: The number of transitions, i.e. triples (s, α, t)
satisfying P
(s, α, t) > 0, is minimal;
(3) Size-minimality: The sum of states and transitions is minimal.
Depending on the situation, one notion might be more suitable than the
others. However, in the full version [42] we show that finding transition-minimal
(respectively, size-minimal) witnesses can be reduced to finding state-minimal
witnesses with a linear (respectively, quadratic) blow-up. We will therefore restrict
ourselves to state-minimality for the rest of this paper.
NP-completeness of finding minimal witnesses for DTMCs. In this
section we determine the computational complexity of the witness problem:
Given a DTMC M, a positive integer k, and a rational number λ ∈ [0, 1],
decide whether there exists a witness M
⊆ M for Pr M,s0 (♦ goal) ≥ λ with
at most k states. The corresponding problem for MDPs is known to be NPcomplete [24, 78]
1 . In this section we show that the witness problem is already
1 Although the framework in [24] considers a richer logic, the hardness proof uses only
probabilistic reachability formulas such as the ones we consider.
331
s 0
t
u
v
fail
goal
α
β
α
α
γ
α
γ
β
(a)
s 0
u
v
fail
goal
α
β
α
γ
α
γ
β
(b)
Fig. 1: An MDP (with omitted probabilities (a)) and a subsystem (b), where
redirected transitions are dashed.
Example 4.3. Figure 1a depicts an MDP and Figure 1b indicates the subsystem
that is obtained by deleting the state t and additionally the transition (u, α, s 0 ).
The following lemma ensures that we can use the subsystems as witnesses for
both Pr
max
M,s0 (♦ goal) λ and Pr
min
M,s0 (♦ goal) λ.
Lemma 4.4. Let M be an MDP as in Setting 2.2 and M
⊆ M. Then:
Pr
min
M ,s0 (♦ goal) ≤ Pr
min
M,s0 (♦ goal) and Pr
max
M ,s0 (♦ goal) ≤ Pr
max
M,s0 (♦ goal)
We consider the following notions of minimality for subsystems:
(1) State-minimality: |S
all | is minimal.
(2) Transition-minimality: The number of transitions, i.e. triples (s, α, t)
satisfying P
(s, α, t) > 0, is minimal;
(3) Size-minimality: The sum of states and transitions is minimal.
Depending on the situation, one notion might be more suitable than the
others. However, in the full version [42] we show that finding transition-minimal
(respectively, size-minimal) witnesses can be reduced to finding state-minimal
witnesses with a linear (respectively, quadratic) blow-up. We will therefore restrict
ourselves to state-minimality for the rest of this paper.
NP-completeness of finding minimal witnesses for DTMCs. In this
section we determine the computational complexity of the witness problem:
Given a DTMC M, a positive integer k, and a rational number λ ∈ [0, 1],
decide whether there exists a witness M
⊆ M for Pr M,s0 (♦ goal) ≥ λ with
at most k states. The corresponding problem for MDPs is known to be NPcomplete [24, 78]
1 . In this section we show that the witness problem is already
1 Although the framework in [24] considers a richer logic, the hardness proof uses only
probabilistic reachability formulas such as the ones we consider.