# Shepherding Hordes of Markov Chains

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

## Key facts

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

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

- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Finite-State Controllers for (Hidden-Model) POMDPs using Deep Reinforcement Learning](https://mlsanity.com/paper/2602.08734/) (2026)
- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)

## Abstract (arXiv)

This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, planning under partial observability, and sketching of probabilistic programs. Simple questions, like `does at least one family member satisfy a property?', are NP-hard. We tackle two problems: distinguish family members that satisfy a given quantitative property from those that do not, and determine a family member that satisfies the property optimally, i.e., with the highest probability or reward. We show that combining two well-known techniques, MDP model checking and abstraction refinement, mitigates the computational complexity. Experiments on a broad set of benchmarks show that in many situations, our approach is able to handle families of millions of MCs, providing superior scalability compared to existing solutions.