# SWITSS: Computing Small Witnessing Subsystems

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Aug 2020.

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

- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)

## Abstract (arXiv)

Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear programming. Returned subsystems can automatically be rendered graphically and are accompanied with a certificate which proves that the subsystem is indeed a witness.