Publication Details
Shepherding Hordes of Markov Chains
parametric Markov chains, synthesis from specification, Markov Decision
Processes, abstraction refinement
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.
@inproceedings{BUT156852,
author="ČEŠKA, M. and JANSEN, N. and JUNGES, S. and KATOEN, J.",
title="Shepherding Hordes of Markov Chains",
booktitle="Proceedings of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
year="2019",
series="Lecture Notes in Computer Science",
volume="11428",
pages="172--190",
publisher="Springer International Publishing",
address="Praha",
doi="10.1007/978-3-030-17465-1\{_}10",
isbn="978-3-030-17464-4",
url="https://link.springer.com/chapter/10.1007/978-3-030-17465-1_10"
}