Shepherding Hordes of Markov Chains
This addresses a computational bottleneck for software product lines, planning under partial observability, and probabilistic program sketching, though it is an incremental improvement using existing techniques.
The paper tackles the problem of analyzing large families of Markov chains defined over discrete parameters, which is NP-hard for questions like distinguishing members that satisfy quantitative properties or finding optimal ones. The result shows that combining MDP model checking and abstraction refinement enables handling families of millions of Markov chains with superior scalability compared to existing solutions.
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.