  This paper introduces Farkas certificates for lower and upper bounds on
minimal and maximal reachability probabilities in Markov decision processes
(MDP), which we derive using an MDP-variant of Farkas' Lemma. The set of all
such certificates is shown to form a polytope whose points correspond to
witnessing subsystems of the model and the property. Using this correspondence
we can translate the problem of finding minimal witnesses to the problem of
finding vertices with a maximal number of zeros. While computing such vertices
is computationally hard in general, we derive new heuristics from our
formulations that exhibit competitive performance compared to state-of-the-art
techniques. As an argument that asymptotically better algorithms cannot be
hoped for, we show that the decision version of finding minimal witnesses is
NP-complete even for acyclic Markov chains.
