Publication Details

Shepherding Hordes of Markov Chains

ČEŠKA Milan, JANSEN Nils, JUNGES Sebastian and KATOEN Joost-Pieter. Shepherding Hordes of Markov Chains. In: Proceedings of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 11428. Praha: Springer International Publishing, 2019, pp. 172-190. ISBN 978-3-030-17464-4. Available from: https://link.springer.com/chapter/10.1007/978-3-030-17465-1_10
Czech title
Syntéza topologie v Markovovských řetězcích
Type
conference paper
Language
english
Authors
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Jansen Nils (RUN)
Junges Sebastian (RWTH Aachen University)
Katoen Joost-Pieter (RWTH)
URL
Keywords

parametric Markov chains, synthesis from specification, Markov Decision Processes, abstraction refinement

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.

Published
2019
Pages
172-190
Proceedings
Proceedings of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
11428
Conference
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Praha, CZ
ISBN
978-3-030-17464-4
Publisher
Springer International Publishing
Place
Praha, CZ
DOI
UT WoS
000681174300010
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11964,
   author = "Milan \v{C}e\v{s}ka and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen",
   title = "Shepherding Hordes of Markov Chains",
   pages = "172--190",
   booktitle = "Proceedings of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 11428,
   year = 2019,
   location = "Praha, CZ",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-17464-4",
   doi = "10.1007/978-3-030-17465-1\_10",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11964"
}
Back to top