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

arXiv: https://arxiv.org/abs/2404.05424 · HTML: https://mlsanity.com/paper/2404.05424/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 108 references that are in the map.
- First posted on arXiv 8 Apr 2024.

## Builds on (most cited first, 29 of 29)

- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Reward-Free Exploration for Reinforcement Learning](https://mlsanity.com/paper/2002.02794/) (2020)
- [Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal](https://mlsanity.com/paper/1906.03804/) (2019)
- [Pessimistic Q-Learning for Offline Reinforcement Learning: Towards Optimal Sample Complexity](https://mlsanity.com/paper/2202.13890/) (2022)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints](https://mlsanity.com/paper/1404.7073/) (2014)
- [Safe Policy Improvement by Minimizing Robust Baseline Regret](https://mlsanity.com/paper/1607.03842/) (2016)
- [Beyond No Regret: Instance-Dependent PAC Reinforcement Learning](https://mlsanity.com/paper/2108.02717/) (2021)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games](https://mlsanity.com/paper/1905.04403/) (2019)
- [Learning with Safety Constraints: Sample Complexity of Reinforcement Learning for Constrained MDPs](https://mlsanity.com/paper/2008.00311/) (2020)
- [Robust Anytime Learning of Markov Decision Processes](https://mlsanity.com/paper/2205.15827/) (2022)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [On the exact feasibility of convex scenario programs with discarded constraints](https://mlsanity.com/paper/2003.13433/) (2020)
- [A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs](https://mlsanity.com/paper/2310.12248/) (2023)
- [Faster Statistical Model Checking for Unbounded Temporal Properties](https://mlsanity.com/paper/1504.05739/) (2015)
- [Decision-Making Under Uncertainty: Beyond Probabilities](https://mlsanity.com/paper/2303.05848/) (2023)
- [More for Less: Safe Policy Improvement With Stronger Performance Guarantees](https://mlsanity.com/paper/2305.07958/) (2023)
- [Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints](https://mlsanity.com/paper/1804.08924/) (2018)
- [Value Iteration for Long-run Average Reward in Markov Decision Processes](https://mlsanity.com/paper/1705.02326/) (2017)
- [The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes](https://mlsanity.com/paper/1710.07903/) (2017)
- [PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP](https://mlsanity.com/paper/2206.01465/) (2022)
- [Smart Sampling for Lightweight Verification of Markov Decision Processes](https://mlsanity.com/paper/1409.2116/) (2014)
- [Scalable Verification of Markov Decision Processes](https://mlsanity.com/paper/1310.3609/) (2013)
- [Graph-Based Reductions for Parametric and Weighted MDPs](https://mlsanity.com/paper/2305.05739/) (2023)
- [ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans](https://mlsanity.com/paper/1612.07059/) (2016)
- [Tight relative estimation in the mean of Bernoulli random variables](https://mlsanity.com/paper/2210.12861/) (2022)
- [Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access](https://mlsanity.com/paper/2303.12718/) (2023)
- [Learning Algorithms for Verification of Markov Decision Processes](https://mlsanity.com/paper/2403.09184/) (2024)

## Built on by (most cited first, 5 of 5)

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Certifiably Robust Policies for Uncertain Parametric Environments](https://mlsanity.com/paper/2408.03093/) (2024)
- [Pick-to-Learn for Systems and Control: Data-driven Synthesis with State-of-the-art Safety Guarantees](https://mlsanity.com/paper/2512.04781/) (2025)
- [Data-Efficient Safe Policy Improvement Using Parametric Structure](https://mlsanity.com/paper/2507.15532/) (2025)
- [Efficient Solution and Learning of Robust Factored MDPs](https://mlsanity.com/paper/2508.00707/) (2025)

## Abstract (arXiv)

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.