Farkas certificates and minimal witnesses
339
(a) Witnesses for Pr
min
s 0 (♦ goal) ≥ λ.
(b) Witnesses for Pr
max
s 0 (♦ goal) ≥ λ.
Fig. 5: MDP benchmark: CSMA-3-2 (36,850 states)
8 Conclusion
In this paper we brought together two a priori unrelated notions in the context of
probabilistic reachability constraints: on the one hand Farkas certificates, which
are vectors satisfying certain linear inequalities that we derive using MDP-specific
variants of Farkas’ Lemma, and on the other hand witnessing subsystems, which
provide insight into which parts of the system are essential for the satisfaction of
the considered property. This connection reduces the computation of minimal
(respectively, small) witnessing subsystems to finding a Farkas certificate with a
maximal (respectively, large) number of zeros. Furthermore, it leads to a unified
notion of witnessing subsystem for Pr
max
s0 (♦ goal) ≥ λ and Pr
min
s0 (♦ goal) ≥ λ.
We showed that the decision version of computing minimal witnessing subsystems is NP-complete for acyclic DTMCs and introduced heuristics for the
computation of small witnesses based on Farkas certificates. Experiments of the
heuristics exhibited competitive results compared to the approach implemented
in Comics and showed that they scale well with the system size and threshold. As
expected, computing minimal subsystems using the derived MILP formulations
consumed significantly more time than the heuristics and often triggered timeouts.
The upper and lower bounds that were computed in the given time by the new
MILP formulation for Pr
max
s0 (♦ goal) ≥ λ were comparable to known techniques.
We have considered MDPs in which the probability to reach goal or fail is
positive under each scheduler. In future work, we plan to extend our techniques to
weaken this assumption. Exploring how vertex enumeration techniques could be
adapted to the MDP-specific form of the Farkas polytopes is another interesting
line of future work. We also plan to implement a tool for working with Farkas
certificates in practice, which encompasses their generation as well as their
independent validation.
339
(a) Witnesses for Pr
min
s 0 (♦ goal) ≥ λ.
(b) Witnesses for Pr
max
s 0 (♦ goal) ≥ λ.
Fig. 5: MDP benchmark: CSMA-3-2 (36,850 states)
8 Conclusion
In this paper we brought together two a priori unrelated notions in the context of
probabilistic reachability constraints: on the one hand Farkas certificates, which
are vectors satisfying certain linear inequalities that we derive using MDP-specific
variants of Farkas’ Lemma, and on the other hand witnessing subsystems, which
provide insight into which parts of the system are essential for the satisfaction of
the considered property. This connection reduces the computation of minimal
(respectively, small) witnessing subsystems to finding a Farkas certificate with a
maximal (respectively, large) number of zeros. Furthermore, it leads to a unified
notion of witnessing subsystem for Pr
max
s0 (♦ goal) ≥ λ and Pr
min
s0 (♦ goal) ≥ λ.
We showed that the decision version of computing minimal witnessing subsystems is NP-complete for acyclic DTMCs and introduced heuristics for the
computation of small witnesses based on Farkas certificates. Experiments of the
heuristics exhibited competitive results compared to the approach implemented
in Comics and showed that they scale well with the system size and threshold. As
expected, computing minimal subsystems using the derived MILP formulations
consumed significantly more time than the heuristics and often triggered timeouts.
The upper and lower bounds that were computed in the given time by the new
MILP formulation for Pr
max
s0 (♦ goal) ≥ λ were comparable to known techniques.
We have considered MDPs in which the probability to reach goal or fail is
positive under each scheduler. In future work, we plan to extend our techniques to
weaken this assumption. Exploring how vertex enumeration techniques could be
adapted to the MDP-specific form of the Farkas polytopes is another interesting
line of future work. We also plan to implement a tool for working with Farkas
certificates in practice, which encompasses their generation as well as their
independent validation.