PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

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.

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

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Switzerland
• Confidentiality degree: is not subject to a state or trade secret
• 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: 0302-9743
• 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
• Tags: core_A, firank_1

Abstract

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