PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA18-11193S" target="_blank" >GA18-11193S: Algorithms for Infinite-State Discrete Systems and Games</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Computer Aided Verification (CAV 2019)
ISBN
9783030255398
ISSN
0302-9743
e-ISSN
—
Number of pages
23
Pages from-to
497-519
Publisher name
Springer
Place of publication
Cham
Event location
Cham
Event date
Jan 1, 2019
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
000491468000029