# Faster Statistical Model Checking for Unbounded Temporal Properties

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Apr 2015.

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Policy Synthesis and Reinforcement Learning for Discounted LTL](https://mlsanity.com/paper/2305.17115/) (2023)
- [A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs](https://mlsanity.com/paper/2310.12248/) (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)
- [Robust Shielding for Safe Reinforcement Learning](https://mlsanity.com/paper/2606.00270/) (2026)
- [Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access](https://mlsanity.com/paper/2303.12718/) (2023)
- [Missingness-MDPs: Bridging the Theory of Missing Data and POMDPs](https://mlsanity.com/paper/2605.12262/) (2026)

## Abstract (arXiv)

We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, such as reachability and full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence and size of the state space. In comparison to previous algorithms for statistical model checking, for a given level of confidence, our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain, thus enabling almost complete black-box verification. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.