Shepherding Hordes of Markov Chains

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APU132063" target="_blank" >RIV/00216305:26230/19:PU132063 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-030-17465-1_10" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-030-17465-1_10</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-17465-1_10" target="_blank" >10.1007/978-3-030-17465-1_10</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Shepherding Hordes of Markov Chains

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Shepherding Hordes of Markov Chains

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA17-12465S" target="_blank" >GA17-12465S: Verifikace a hledání chyb v pokročilém softwaru</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

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

ISBN

978-3-030-17464-4

ISSN

—

e-ISSN

—

Počet stran výsledku

19

Strana od-do

172-190

Název nakladatele

Springer International Publishing

Místo vydání

Praha

Místo konání akce

Praha

Datum konání akce

8. 4. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000681174300010