# Shepherding Hordes of Markov Chains

## TL;DR

This paper introduces a scalable approach to analyze large families of Markov chains, enabling efficient property satisfaction verification and optimization across millions of models, with applications in software engineering and probabilistic programming.

## Contribution

It combines MDP model checking and abstraction refinement to efficiently analyze large Markov chain families, improving scalability over existing methods.

## Key findings

- Handles families of millions of MCs effectively
- Outperforms existing solutions in scalability
- Applicable to software product lines and probabilistic programs

## Abstract

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.