Farkas certificates and minimal witnesses
335
Remark 6.2. To compute minimal witnesses for Pr
max
s0 (♦ goal) ≥ λ, [77, 78]
(witnesses for Pr
min
s0 (♦ goal) ≥ λ were not considered) propose the MILP with
objective: min
(s,α)∈M σ(s, α), subject to the conditions
∀(s, α) ∈ M. z(s) ≤ 1 − σ(s, α) +
s ∈S
P(s, α, s
) · z(s
) + b(s)
(6.1)
∀s ∈ S. z(s) ≤
α∈Act(s)
σ(s, α), z(s 0 ) ≥ λ
(6.2)
where σ(s, α) are binary integer variables. It was implemented in the tool
ltlsubsys. The idea is to directly encode a scheduler in the set of equations
Az ≤ b using σ. In [77, 78] a number of additional redundant constraints are
given to guide the search. In contrast to [77, 78] we do not need to handle so-called
problematic states, as our precondition Pr
min
s (♦(goal ∨ fail)) > 0 guarantees that
no such states exist.
k-step quotient sum (QS k ) heuristics. Approximating the maximal number
of zeros in a polytope is computationally hard in general [8]. We now derive
a heuristic approach for this problem called quotient sum heuristic which is
based on iteratively solving LPs over the polytope, where the objective function
for each iteration depends on an optimal solution of the previous LP. More
precisely, we take o 1 = (1, . . . , 1) and take an optimal solution QS 1 of the LP
min o 1 · y s.t. y ∈ P
max (λ). Many entries in QS 1 may be small, but still greater
than zero. In order to push as many of the small values of QS 1 to zero, we define
a new objective function by
o 2 (i) =
1/ QS 1 (i), if QS 1 (i) > 0
C,
if QS 1 (i) = 0
(6.3)
where C is a value that is greater than any value 1/ QS 1 (i). We now take
a solution QS 2 of the new LP min o 2 · y s.t. y ∈ P
max (λ) and form the next
objective function o 3 as in (6.3). Inductively this generates a sequence of objective
functions (o k ) k≥1 and corresponding optimal solutions (QS k ) k≥1 in P
max / min (λ).
By Theorem 5.4 we can construct a witnessing subsystem with as many states as
the number of non-zero entries in QS k .
7 Experiments
In this section we evaluate our MILP formulations and heuristics on a number
of DTMC and MDP benchmarks from the Prism benchmark-suite [58, 59]. We
compare our results with the tool Comics [50], which implements heuristic
approaches to compute small subsystems for DTMCs. It has two modes: the local
search extends a given subsystem by short paths that carry much probability,
whereas the global search searches for the next most probable path from the
335
Remark 6.2. To compute minimal witnesses for Pr
max
s0 (♦ goal) ≥ λ, [77, 78]
(witnesses for Pr
min
s0 (♦ goal) ≥ λ were not considered) propose the MILP with
objective: min
(s,α)∈M σ(s, α), subject to the conditions
∀(s, α) ∈ M. z(s) ≤ 1 − σ(s, α) +
s ∈S
P(s, α, s
) · z(s
) + b(s)
(6.1)
∀s ∈ S. z(s) ≤
α∈Act(s)
σ(s, α), z(s 0 ) ≥ λ
(6.2)
where σ(s, α) are binary integer variables. It was implemented in the tool
ltlsubsys. The idea is to directly encode a scheduler in the set of equations
Az ≤ b using σ. In [77, 78] a number of additional redundant constraints are
given to guide the search. In contrast to [77, 78] we do not need to handle so-called
problematic states, as our precondition Pr
min
s (♦(goal ∨ fail)) > 0 guarantees that
no such states exist.
k-step quotient sum (QS k ) heuristics. Approximating the maximal number
of zeros in a polytope is computationally hard in general [8]. We now derive
a heuristic approach for this problem called quotient sum heuristic which is
based on iteratively solving LPs over the polytope, where the objective function
for each iteration depends on an optimal solution of the previous LP. More
precisely, we take o 1 = (1, . . . , 1) and take an optimal solution QS 1 of the LP
min o 1 · y s.t. y ∈ P
max (λ). Many entries in QS 1 may be small, but still greater
than zero. In order to push as many of the small values of QS 1 to zero, we define
a new objective function by
o 2 (i) =
1/ QS 1 (i), if QS 1 (i) > 0
C,
if QS 1 (i) = 0
(6.3)
where C is a value that is greater than any value 1/ QS 1 (i). We now take
a solution QS 2 of the new LP min o 2 · y s.t. y ∈ P
max (λ) and form the next
objective function o 3 as in (6.3). Inductively this generates a sequence of objective
functions (o k ) k≥1 and corresponding optimal solutions (QS k ) k≥1 in P
max / min (λ).
By Theorem 5.4 we can construct a witnessing subsystem with as many states as
the number of non-zero entries in QS k .
7 Experiments
In this section we evaluate our MILP formulations and heuristics on a number
of DTMC and MDP benchmarks from the Prism benchmark-suite [58, 59]. We
compare our results with the tool Comics [50], which implements heuristic
approaches to compute small subsystems for DTMCs. It has two modes: the local
search extends a given subsystem by short paths that carry much probability,
whereas the global search searches for the next most probable path from the