Detail publikace

Shepherding Hordes of Markov Chains

ČEŠKA, M. JANSEN, N. JUNGES, S. KATOEN, J.

Originální název

Shepherding Hordes of Markov Chains

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

ČEŠKA, M.; JANSEN, N.; JUNGES, S.; KATOEN, J.

Vydáno

17. 4. 2019

Nakladatel

Springer International Publishing

Místo

Praha

ISBN

978-3-030-17464-4

Kniha

Proceedings of 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Edice

Lecture Notes in Computer Science

Strany od

172

Strany do

190

Strany počet

19

URL

Plný text v Digitální knihovně

BibTex

@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"
}