# Farkas certificates and minimal witnesses for probabilistic reachability constraints

arXiv: https://arxiv.org/abs/1910.10636 · HTML: https://mlsanity.com/paper/1910.10636/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Oct 2019.

## Built on by (most cited first, 3 of 3)

- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [Multi-Objective Controller Synthesis with Uncertain Human Preferences](https://mlsanity.com/paper/2105.04662/) (2021)
- [Certifying Almost-Sure Reachability in Unknown MDPs](https://mlsanity.com/paper/2610.18119/) (2026)

## Abstract (arXiv)

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.