PAC Statistical Model Checking for Markov Decision Processes
and Stochastic Games

D 2019

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

ASHOK, Pranav, Jan KŘETÍNSKÝ a Maximilian WEININGER

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

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

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ěněno: 28. 4. 2020 16:29, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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

Investor: Grantová agentura ČR, Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Citovat

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.

@inproceedings{1649047,
   author = {Ashok, Pranav and Křetínský, Jan and Weininger, Maximilian},
   address = {Cham},
   booktitle = {Computer Aided Verification (CAV 2019)},
   doi = {http://dx.doi.org/10.1007/978-3-030-25540-4_29},
   keywords = {PAC; Statistical Model Checking; Markov Decision Processes; Stochastic Games},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-25539-8},
   pages = {497-519},
   publisher = {Springer},
   title = {PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games},
   year = {2019}
}

TY  - JOUR
ID  - 1649047
AU  - Ashok, Pranav - Křetínský, Jan - Weininger, Maximilian
PY  - 2019
TI  - PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
PB  - Springer
CY  - Cham
SN  - 9783030255398
KW  - PAC
KW  - Statistical Model Checking
KW  - Markov Decision Processes
KW  - Stochastic Games
N2  - 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.
ER  -

ASHOK, Pranav, Jan KŘETÍNSKÝ a Maximilian WEININGER. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. In \textit{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.

Podrobný výpis o publikaci