PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

TL;DR

This paper introduces a practical PAC statistical model checking algorithm for Markov decision processes and stochastic games, capable of providing probabilistic guarantees with efficient runtime even for complex systems.

Contribution

It presents the first PAC algorithm for stochastic games and a practical approach for MDPs that does not rely on mixing time or full model knowledge.

Findings

First PAC algorithm for stochastic games.

Efficient runtime for complex models.

Provides reliable probabilistic guarantees within minutes.

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 or the topology of the whole model.