PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00108294" target="_blank" >RIV/00216224:14330/19:00108294 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-25540-4_29" target="_blank" >http://dx.doi.org/10.1007/978-3-030-25540-4_29</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-25540-4_29" target="_blank" >10.1007/978-3-030-25540-4_29</a>

Jazyk výsledku

angličtina

Název v původním jazyce

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Popis výsledku v původním jazyce

Statistical model checking (SMC) is a technique for analysis of probabilistic systems that may be (partially) unknown. We present an SMC algorithm for (unbounded) reachability yielding probably approximately correct (PAC) guarantees on the results. We consider both the setting (i) with no knowledge of the transition function (with the only quantity required a bound on the minimum transition probability) and (ii) with knowledge of the topology of the underlying graph. On the one hand, it is the first algorithm for stochastic games. On the other hand, it is the first practical algorithm even for Markov decision processes. Compared to previous approaches where PAC guarantees require running times longer than the age of universe even for systems with a handful of states, our algorithm often yields reasonably precise results within minutes, not requiring the knowledge of mixing time.

Název v anglickém jazyce

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Popis výsledku anglicky

Statistical model checking (SMC) is a technique for analysis of probabilistic systems that may be (partially) unknown. We present an SMC algorithm for (unbounded) reachability yielding probably approximately correct (PAC) guarantees on the results. We consider both the setting (i) with no knowledge of the transition function (with the only quantity required a bound on the minimum transition probability) and (ii) with knowledge of the topology of the underlying graph. On the one hand, it is the first algorithm for stochastic games. On the other hand, it is the first practical algorithm even for Markov decision processes. Compared to previous approaches where PAC guarantees require running times longer than the age of universe even for systems with a handful of states, our algorithm often yields reasonably precise results within minutes, not requiring the knowledge of mixing time.

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/GA18-11193S" target="_blank" >GA18-11193S: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy</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

Computer Aided Verification (CAV 2019)

ISBN

9783030255398

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

23

Strana od-do

497-519

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Cham

Datum konání akce

1. 1. 2019

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

CST - Celostátní akce

Kód UT WoS článku

000491468000029