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

TL;DR

This work tackles the inefficiency of model-based statistical model checking for Markov decision processes with unknown transition probabilities by advocating a PAC framework and refining both probability estimation and structural exploitation. It establishes that the Clopper-Pearson interval offers tighter worst-case confidence bounds than Hoeffding's inequality for transition probability estimation, and it further reduces sample needs by exploiting model topology (Small Support, Independence) and property structure (Equivalence Structures, Fragment abstractions). The authors provide theoretical insights, practical algorithms, and extensive experiments on PRISM benchmarks showing improvements up to two orders of magnitude in sample efficiency with negligible overhead, reinforcing the approach's applicability to infinite-horizon reachability and beyond. Overall, the paper delivers a sound, broadly applicable toolkit that makes PAC-SMC of unknown-MDPs more scalable and reliable for diverse objectives and complex systems.

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.

Figures (2)

• Figure 1: Left: Ratio of worst-case sample complexity ($\hat{p}=0.5$) between Hoeffding bound and Clopper-Pearson interval for confidence $\delta=0.01$ and varying precision $\varepsilon$. Right: Ratio of sample complexity between Hoeffding bound and Clopper-Pearson interval for varying $\hat{p}$, precision $\varepsilon=0.01$, and confidence $\delta=0.01$. Note the logarithmic scale for the X-axis on the left and Y-axis on the right.
• Figure 2: A small MDP to illustrate several potential savings that can be obtained through Equivalence Structures. The boxed states form an end component, 1 denotes the designated target state. We omit transition probabilities, as these are also not visible to our algorithm. We also omit action labels for readability.

Theorems & Definitions (6)

• remark thmcounterremark
• theorem thmcountertheorem: From AKW19-arxiv and CloPea34
• proposition thmcounterproposition
• remark thmcounterremark: Applicability in the black-box Setting
• remark thmcounterremark
• proposition thmcounterproposition