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Ý and Maximilian WEININGER

Basic information

Original name

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

Authors

ASHOK, Pranav (356 India), Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution) and Maximilian WEININGER (276 Germany)

Edition

Cham, Computer Aided Verification (CAV 2019), p. 497-519, 23 pp. 2019

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00108294

Organization unit

Faculty of Informatics

ISBN

978-3-030-25539-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-25540-4_29

UT WoS

000491468000029

Keywords in English

PAC; Statistical Model Checking; Markov Decision Processes; Stochastic Games

Abstract

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.

Links

GA18-11193S, research and development project

Name: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy

Investor: Czech Science Foundation

Citovat

ASHOK, Pranav, Jan KŘETÍNSKÝ and Maximilian WEININGER. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. In Computer Aided Verification (CAV 2019). Cham: Springer, 2019, p. 497-519. ISBN 978-3-030-25539-8. Available from: 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Ý and Maximilian WEININGER. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. In \textit{Computer Aided Verification (CAV 2019)}. Cham: Springer, 2019, p.~497-519. ISBN~978-3-030-25539-8. Available from: https://dx.doi.org/10.1007/978-3-030-25540-4\_{}29.

Detailed Information on Publication Record