mlsanityData to 7 Oct 2026

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

arXiv 2404.05424 ↗First posted 8 Apr 2024cs.AI cs.LG cs.SYcited by 5

Not on the map. Why?

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.

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

Builds on

29 of 108 references.

References · 29

  1. 2017Safe Reinforcement Learning via Shieldingcited by 427
  2. 2020Reward-Free Exploration for Reinforcement Learningcited by 177
  3. 2019Model-Based Reinforcement Learning with a Generative Model is Minimax Optimalcited by 124
  4. 2022Pessimistic Q-Learning for Offline Reinforcement Learning: Towards Optimal Sample Complexitycited by 84
  5. 2018Omega-Regular Objectives in Model-Free Reinforcement Learningcited by 74
  6. 2014Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraintscited by 53
  7. 2016Safe Policy Improvement by Minimizing Robust Baseline Regretcited by 51
  8. 2021Beyond No Regret: Instance-Dependent PAC Reinforcement Learningcited by 41
  9. 2014Verification of Markov Decision Processes using Learning Algorithmscited by 38
  10. 2020Learning with Safety Constraints: Sample Complexity of Reinforcement Learning for Constrained MDPscited by 32
  11. 2019PAC Statistical Model Checking for Markov Decision Processes and Stochastic Gamescited by 30
  12. 2022Robust Anytime Learning of Markov Decision Processescited by 16
17 more
  1. 2023Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractionscited by 16
  2. 2020On the exact feasibility of convex scenario programs with discarded constraintscited by 15
  3. 2023A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPscited by 12
  4. 2015Faster Statistical Model Checking for Unbounded Temporal Propertiescited by 9
  5. 2023More for Less: Safe Policy Improvement With Stronger Performance Guaranteescited by 9
  6. 2018Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraintscited by 8
  7. 2023Decision-Making Under Uncertainty: Beyond Probabilitiescited by 8
  8. 2017Value Iteration for Long-run Average Reward in Markov Decision Processescited by 7
  9. 2017The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processescited by 4
  10. 2022PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDPcited by 4
  11. 2014Smart Sampling for Lightweight Verification of Markov Decision Processescited by 3
  12. 2013Scalable Verification of Markov Decision Processescited by 2
  13. 2023Graph-Based Reductions for Parametric and Weighted MDPscited by 2
  14. 2016ARES: Adaptive Receding-Horizon Synthesis of Optimal Planscited by 1
  15. 2022Tight relative estimation in the mean of Bernoulli random variablescited by 1
  16. 2023Strategy Synthesis in Markov Decision Processes Under Limited Sampling Accesscited by 1
  17. 2024Learning Algorithms for Verification of Markov Decision Processescited by 1

Built on by

Cited by year

Citing papers per year: 2024: 2; 2025: 3.

5 papers.

  1. 2024Robust Markov Decision Processes: A Place Where AI and Formal Methods Meetcited by 18
  2. 2024Certifiably Robust Policies for Uncertain Parametric Environmentscited by 6
  3. 2025Pick-to-Learn for Systems and Control: Data-driven Synthesis with State-of-the-art Safety Guaranteescited by 4
  4. 2025Data-Efficient Safe Policy Improvement Using Parametric Structurecited by 2
  5. 2025Efficient Solution and Learning of Robust Factored MDPscited by 1