# PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games

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

## Key facts

- Cited by 32 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 May 2019.

## Built on by (most cited first, 30 of 32)

- [Multi-Agent Reinforcement Learning with Temporal Logic Specifications](https://mlsanity.com/paper/2102.00582/) (2021)
- [Policy Optimization with Linear Temporal Logic Constraints](https://mlsanity.com/paper/2206.09546/) (2022)
- [On the (In)Tractability of Reinforcement Learning for LTL Objectives](https://mlsanity.com/paper/2111.12679/) (2021)
- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [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)
- [Policy Synthesis and Reinforcement Learning for Discounted LTL](https://mlsanity.com/paper/2305.17115/) (2023)
- [Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise](https://mlsanity.com/paper/2110.12662/) (2021)
- [Computably Continuous Reinforcement-Learning Objectives are PAC-learnable](https://mlsanity.com/paper/2303.05518/) (2023)
- [A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs](https://mlsanity.com/paper/2310.12248/) (2023)
- [Decision-Making Under Uncertainty: Beyond Probabilities](https://mlsanity.com/paper/2303.05848/) (2023)
- [Monitoring Algorithmic Fairness](https://mlsanity.com/paper/2305.15979/) (2023)
- [Monitoring Algorithmic Fairness under Partial Observations](https://mlsanity.com/paper/2308.00341/) (2023)
- [Certifiably Robust Policies for Uncertain Parametric Environments](https://mlsanity.com/paper/2408.03093/) (2024)
- [What Are the Odds? Improving the foundations of Statistical Model Checking](https://mlsanity.com/paper/2404.05424/) (2024)
- [PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP](https://mlsanity.com/paper/2206.01465/) (2022)
- [Learning Optimal Strategies for Temporal Tasks in Stochastic Games](https://mlsanity.com/paper/2102.04307/) (2021)
- [On the Uniqueness of Solution for the Bellman Equation of LTL Objectives](https://mlsanity.com/paper/2404.05074/) (2024)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access](https://mlsanity.com/paper/2303.12718/) (2023)
- [Robust Parameter Learning for Uncertain MDPs](https://mlsanity.com/paper/2605.01339/) (2026)
- [Reinforcement Causal Structure Learning on Order Graph](https://mlsanity.com/paper/2211.12151/) (2022)
- [Monitoring of Static Fairness](https://mlsanity.com/paper/2507.03048/) (2025)
- [Resilient Strategies for Stochastic Systems: How Much Does It Take to Break a Winning Strategy?](https://mlsanity.com/paper/2602.24191/) (2026)
- [Missingness-MDPs: Bridging the Theory of Missing Data and POMDPs](https://mlsanity.com/paper/2605.12262/) (2026)
- [Reinforcement Learning for Reachability: Guaranteeing Asymptotic Optimality](https://mlsanity.com/paper/2605.24740/) (2026)
- [Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees](https://mlsanity.com/paper/2606.29681/) (2026)
- [PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance](https://mlsanity.com/paper/2607.14877/) (2026)
- [Exact Model-Free Policy Iteration for Co-safe LTL Planning](https://mlsanity.com/paper/2608.05047/) (2026)
- [Adaptive Probabilistic Shielding by Learning MDPs for Safe Reinforcement Learning](https://mlsanity.com/paper/2608.19836/) (2026)

## Abstract (arXiv)

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.