334
F. Funke et al.
6 Computing witnessing subsystems
In this section we use the results of Section 5 to derive two algorithms for the
computation of minimal witnesses for reachability constraints in MDPs. As the
problem is NP-hard, we also present a heuristic approach aimed at computing
small witnessing subsystems.
Vertex enumeration. Corollary 5.5 gives rise to the following approach of computing minimal witnessing subsystems: enumerate all vertices in the corresponding
polytope and choose one with a maximal amount of zeros. Vertex enumeration of
polytopes has been studied extensively [11, 12, 14, 21, 22, 35, 36, 40, 41, 63, 68]
and has been shown to be computationally hard [55, Corollary 2].
First experiments that we have conducted with the SageMath
2 toolkit which
supports vertex enumeration have not scaled well in the dimension, which in
our case is the number of states in the original system. Also, we found no tool
support for vertex enumeration that is able to handle sparse matrices, which is
essential for bigger benchmarks.
Mixed integer linear programming. An approach that computes minimal
witnesses to the threshold problem Pr
max
s0 (♦ goal) ≥ λ using mixed integer linear
programs (MILP) was presented in [77, 78]. Using the following lemma, we can
derive MILP formulations from our polytope formulations.
Lemma 6.1. Let P = {x | Ax ≤ b, x ≥ 0} ⊆ R
n be a polytope and K ≥ 0 be
such that for all p ∈ P and 1 ≤ i ≤ n we have p(i) ≤ K. Consider the MILP
min
1≤i≤n
σ(i) s.t. x ∈ P, x ≤ K · σ, σ(i) ∈ {0, 1}
Then a vector (σ, x) is an optimal solution of this MILP if and only if x is a
point in P with a maximal number of zeros.
For P
min
≥0 (λ) we can use Lemma 3.1 to derive that K = 1 is a viable bound.
By invoking again Corollary 5.5, this means that a solution (z, σ) of the MILP
min
s∈S
σ(s) s.t. z ∈ P
min
≥0 (λ), z ≤ σ, σ(i) ∈ {0, 1}
encodes a minimal witnessing subsystem in the integral variables σ. This MILP
was used in [77, 78] for the computation of minimal witnessing subsystems of
DTMCs .
An upper bound K as in Lemma 6.1 for P
max (λ) can be found in polynomial
time by taking the objective value of an optimal solution to the LP
max
(s,α)∈M
y(s, α) s.t. y ∈ P
max (λ)
2 http://www.sagemath.org/
F. Funke et al.
6 Computing witnessing subsystems
In this section we use the results of Section 5 to derive two algorithms for the
computation of minimal witnesses for reachability constraints in MDPs. As the
problem is NP-hard, we also present a heuristic approach aimed at computing
small witnessing subsystems.
Vertex enumeration. Corollary 5.5 gives rise to the following approach of computing minimal witnessing subsystems: enumerate all vertices in the corresponding
polytope and choose one with a maximal amount of zeros. Vertex enumeration of
polytopes has been studied extensively [11, 12, 14, 21, 22, 35, 36, 40, 41, 63, 68]
and has been shown to be computationally hard [55, Corollary 2].
First experiments that we have conducted with the SageMath
2 toolkit which
supports vertex enumeration have not scaled well in the dimension, which in
our case is the number of states in the original system. Also, we found no tool
support for vertex enumeration that is able to handle sparse matrices, which is
essential for bigger benchmarks.
Mixed integer linear programming. An approach that computes minimal
witnesses to the threshold problem Pr
max
s0 (♦ goal) ≥ λ using mixed integer linear
programs (MILP) was presented in [77, 78]. Using the following lemma, we can
derive MILP formulations from our polytope formulations.
Lemma 6.1. Let P = {x | Ax ≤ b, x ≥ 0} ⊆ R
n be a polytope and K ≥ 0 be
such that for all p ∈ P and 1 ≤ i ≤ n we have p(i) ≤ K. Consider the MILP
min
1≤i≤n
σ(i) s.t. x ∈ P, x ≤ K · σ, σ(i) ∈ {0, 1}
Then a vector (σ, x) is an optimal solution of this MILP if and only if x is a
point in P with a maximal number of zeros.
For P
min
≥0 (λ) we can use Lemma 3.1 to derive that K = 1 is a viable bound.
By invoking again Corollary 5.5, this means that a solution (z, σ) of the MILP
min
s∈S
σ(s) s.t. z ∈ P
min
≥0 (λ), z ≤ σ, σ(i) ∈ {0, 1}
encodes a minimal witnessing subsystem in the integral variables σ. This MILP
was used in [77, 78] for the computation of minimal witnessing subsystems of
DTMCs .
An upper bound K as in Lemma 6.1 for P
max (λ) can be found in polynomial
time by taking the objective value of an optimal solution to the LP
max
(s,α)∈M
y(s, α) s.t. y ∈ P
max (λ)
2 http://www.sagemath.org/