332
F. Funke et al.
NP-complete for acyclic DTMCs, where acyclicity means that the underlying
graph with V = S and E = {(s, t) ∈ S × S | P(s, t) > 0} is acyclic (as before, we
take S = S all \{goal, fail}). This answers a conjecture of [77] in the affirmative and
also shows NP-completeness of finding minimal witnesses for Pr
min
M,s0 (♦ goal) ≥ λ.
Theorem 4.5. The witness problem is NP-complete for acyclic DTMCs.
Proof (Sketch). An NP-algorithm for the witness problem is given by guessing a
set of states of size k and verifying in polynomial time that the corresponding
subsystem satisfies Pr M ,s0 (♦ goal) ≥ λ.
For hardness, we give a reduction from the clique problem, which is among
Karp’s 21 NP-complete problems [54]. The idea is the following: Given an instance
of the clique problem with graph G = (V, E) and integer k, construct an acyclic
Markov chain M with states S = {s 0 } ∪ V ∪ E ∪ {goal, fail} and edges from each
vertex v ∈ V to all edges to which it is incident. Then the existence of a k-clique
can be reduced to the existence of a “saturated” subsystem in M with k states
in V . To check whether the subsystem is saturated, we require it to have more
probability than a certain threshold, which depends on k and |V |. Details can be
found in the full version [42].
Remark 4.6. NP-completeness of transition-minimal and size-minimal versions
of the witness problem for acyclic DTMCs follows along the same lines, where
only the sizes and thresholds for the subsystems need to be adapted.
However, DTMCs whose underlying graph is a tree permit an efficient algorithm for computing minimal witnesses (for the proof see the full version [42]).
Proposition 4.7. Minimal witnesses in tree-shaped DTMCs can be computed
in polynomial time.
Proof (Sketch). The algorithm first transforms the DTMC at hand into a binary
(tree-shaped) DTMC, and then works bottom up by storing for each state the
highest probability that can be obtained with a subsystem of size k, for all k up
to the size of the subtree.
5 Relating Farkas certificates and minimal witnesses
In this section we establish a strong connection between Farkas certificates on
the one hand and witnesses for probabilistic reachability constraints on the other
hand. We first note that the set of Farkas certificates for non-strict lower bounds
forms a polytope, i.e., a bounded polyhedron.
Lemma 5.1 (Polytopes of Farkas certificates). Let M = (S all , Act, s 0 , P)
be an MDP as in Setting 2.2 and consider A ∈ R
M×S and b ∈ R
S introduced
there. Then for every λ ∈ [0, 1] the polyhedra
P
min (λ) = {z ∈ R
S
| Az ≤ b ∧ z(s 0 ) ≥ λ}
P
max (λ) = {y ∈ R
M
| y ≥ 0 ∧ yA ≤ δ s0 ∧ yb ≥ λ}
are both polytopes, called the polytopes of Farkas certificates.
F. Funke et al.
NP-complete for acyclic DTMCs, where acyclicity means that the underlying
graph with V = S and E = {(s, t) ∈ S × S | P(s, t) > 0} is acyclic (as before, we
take S = S all \{goal, fail}). This answers a conjecture of [77] in the affirmative and
also shows NP-completeness of finding minimal witnesses for Pr
min
M,s0 (♦ goal) ≥ λ.
Theorem 4.5. The witness problem is NP-complete for acyclic DTMCs.
Proof (Sketch). An NP-algorithm for the witness problem is given by guessing a
set of states of size k and verifying in polynomial time that the corresponding
subsystem satisfies Pr M ,s0 (♦ goal) ≥ λ.
For hardness, we give a reduction from the clique problem, which is among
Karp’s 21 NP-complete problems [54]. The idea is the following: Given an instance
of the clique problem with graph G = (V, E) and integer k, construct an acyclic
Markov chain M with states S = {s 0 } ∪ V ∪ E ∪ {goal, fail} and edges from each
vertex v ∈ V to all edges to which it is incident. Then the existence of a k-clique
can be reduced to the existence of a “saturated” subsystem in M with k states
in V . To check whether the subsystem is saturated, we require it to have more
probability than a certain threshold, which depends on k and |V |. Details can be
found in the full version [42].
Remark 4.6. NP-completeness of transition-minimal and size-minimal versions
of the witness problem for acyclic DTMCs follows along the same lines, where
only the sizes and thresholds for the subsystems need to be adapted.
However, DTMCs whose underlying graph is a tree permit an efficient algorithm for computing minimal witnesses (for the proof see the full version [42]).
Proposition 4.7. Minimal witnesses in tree-shaped DTMCs can be computed
in polynomial time.
Proof (Sketch). The algorithm first transforms the DTMC at hand into a binary
(tree-shaped) DTMC, and then works bottom up by storing for each state the
highest probability that can be obtained with a subsystem of size k, for all k up
to the size of the subtree.
5 Relating Farkas certificates and minimal witnesses
In this section we establish a strong connection between Farkas certificates on
the one hand and witnesses for probabilistic reachability constraints on the other
hand. We first note that the set of Farkas certificates for non-strict lower bounds
forms a polytope, i.e., a bounded polyhedron.
Lemma 5.1 (Polytopes of Farkas certificates). Let M = (S all , Act, s 0 , P)
be an MDP as in Setting 2.2 and consider A ∈ R
M×S and b ∈ R
S introduced
there. Then for every λ ∈ [0, 1] the polyhedra
P
min (λ) = {z ∈ R
S
| Az ≤ b ∧ z(s 0 ) ≥ λ}
P
max (λ) = {y ∈ R
M
| y ≥ 0 ∧ yA ≤ δ s0 ∧ yb ≥ λ}
are both polytopes, called the polytopes of Farkas certificates.