# Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Apr 2020.

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

- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [On the Limitations of Markovian Rewards to Express Multi-Objective, Risk-Sensitive, and Modal Tasks](https://mlsanity.com/paper/2401.14811/) (2024)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking](https://mlsanity.com/paper/2212.05337/) (2022)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [Turn-based Multi-Agent Reinforcement Learning Model Checking](https://mlsanity.com/paper/2501.03187/) (2025)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Co-Activation Graph Analysis of Safety-Verified and Explainable Deep Reinforcement Learning Policies](https://mlsanity.com/paper/2501.03142/) (2025)
- [Bounded PCTL Model Checking of Large Language Model Outputs](https://mlsanity.com/paper/2509.18836/) (2025)
- [Verifying Memoryless Sequential Decision-making of Large Language Models](https://mlsanity.com/paper/2510.06756/) (2025)
- [Formal Verification of Noisy Quantum Reinforcement Learning Policies](https://mlsanity.com/paper/2512.01502/) (2025)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)

## Abstract (arXiv)

Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model checking PCTL specifications statistically on Markov Decision Processes (MDPs) by sampling, e.g., checking whether there exists a feasible policy such that the probability of reaching certain goal states is greater than a threshold. We use reinforcement learning to search for such a feasible policy for PCTL specifications, and then develop a statistical model checking (SMC) method with provable guarantees on its error. Specifically, we first use upper-confidence-bound (UCB) based Q-learning to design an SMC algorithm for bounded-time PCTL specifications, and then extend this algorithm to unbounded-time specifications by identifying a proper truncation time by checking the PCTL specification and its negation at the same time. Finally, we evaluate the proposed method on case studies.