What Are the Odds? Improving the foundations of Statistical Model Checking

TL;DR

This paper enhances statistical model checking for Markov decision processes by integrating advanced concentration inequalities and exploiting MDP knowledge, significantly reducing sampling requirements while providing reliable probabilistic guarantees.

Contribution

It introduces fundamental improvements to statistical model checking by applying better concentration inequalities and specialized methods that leverage MDP knowledge, leading to more efficient analysis.

Findings

Up to 100x reduction in sample size needed for analysis.

Improved concentration inequalities enhance statistical guarantees.

Methods are broadly applicable across different problem settings.

Abstract

Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. As this assumption is often unrealistic in practice, statistical model checking (SMC) was developed in the past two decades. It allows to analyse MDPs with unknown transition probabilities and provide probably approximately correct (PAC) guarantees on the result. Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: ``What are the odds?'' However, so far the statistical methods employed by the state of the art SMC algorithms are quite naive. Our contribution are several fundamental improvements to those methods: On the one hand, we survey statistics literature for better concentration inequalities; on the other hand, we propose specialised approaches that exploit our knowledge of the MDP. Our improvements are generally applicable to many kinds of problem statements because they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that the SMC algorithm has to collect by up to two orders of magnitude.