Podrobný výpis o publikaci

ASHOK, Pranav, Jan KŘETÍNSKÝ a Maximilian WEININGER. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. In Computer Aided Verification (CAV 2019). Cham: Springer, 2019, s. 497-519. ISBN 978-3-030-25539-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-25540-4_29.

Další formáty: BibTeX LaTeX RIS

Základní údaje
Originální název	PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Autoři	ASHOK, Pranav (356 Indie), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí) a Maximilian WEININGER (276 Německo).
Vydání	Cham, Computer Aided Verification (CAV 2019), od s. 497-519, 23 s. 2019.
Nakladatel	Springer

Další údaje
Originální jazyk	angličtina
Typ výsledku	Stať ve sborníku
Obor	10201 Computer sciences, information science, bioinformatics
Stát vydavatele	Švýcarsko
Utajení	není předmětem státního či obchodního tajemství
Forma vydání	tištěná verze "print"
Impakt faktor	Impact factor: 0.402 v roce 2005
Kód RIV	RIV/00216224:14330/19:00108294
Organizační jednotka	Fakulta informatiky
ISBN	978-3-030-25539-8
ISSN	0302-9743
Doi	http://dx.doi.org/10.1007/978-3-030-25540-4_29
UT WoS	000491468000029
Klíčová slova anglicky	PAC; Statistical Model Checking; Markov Decision Processes; Stochastic Games
Štítky	core_A, firank_1
Změnil	Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2020 16:29.

Anotace
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.

Anotace

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ávaznosti
GA18-11193S, projekt VaV	Název: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy
GA18-11193S, projekt VaV	Investor: Grantová agentura ČR, Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy