# Probabilistic Model Checking of Stochastic Reinforcement Learning Policies

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 13 of its 33 references that are in the map.
- First posted on arXiv 27 Mar 2024.

## Placed in

- Deep reinforcement learning methods / [Safe and constrained RL](https://mlsanity.com/deeprl/safe-and-constrained-rl/)

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

- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Environment-Independent Task Specifications via GLTL](https://mlsanity.com/paper/1704.04341/) (2017)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Safe Reinforcement Learning via Shielding under Partial Observability](https://mlsanity.com/paper/2204.00755/) (2022)
- [Scalar reward is not enough: A response to Silver, Singh, Precup and Sutton (2021)](https://mlsanity.com/paper/2112.15422/) (2021)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [Explainable Deep Reinforcement Learning: State of the Art and Challenges](https://mlsanity.com/paper/2301.09937/) (2023)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Permissive Controller Synthesis for Probabilistic Systems](https://mlsanity.com/paper/1504.04662/) (2015)
- [Probabilistic Guarantees for Safe Deep Reinforcement Learning](https://mlsanity.com/paper/2005.07073/) (2020)
- [Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning](https://mlsanity.com/paper/2004.00273/) (2020)

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

- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Verifying Memoryless Sequential Decision-making of Large Language Models](https://mlsanity.com/paper/2510.06756/) (2025)
- [Easy-to-Use Shielding for Reinforcement Learning](https://mlsanity.com/paper/2606.03804/) (2026)
- [Formal Verification of Noisy Quantum Reinforcement Learning Policies](https://mlsanity.com/paper/2512.01502/) (2025)
- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

We introduce a method to verify stochastic reinforcement learning (RL) policies. This approach is compatible with any RL algorithm as long as the algorithm and its corresponding environment collectively adhere to the Markov property. In this setting, the future state of the environment should depend solely on its current state and the action executed, independent of any previous states or actions. Our method integrates a verification technique, referred to as model checking, with RL, leveraging a Markov decision process, a trained RL policy, and a probabilistic computation tree logic (PCTL) formula to build a formal model that can be subsequently verified via the model checker Storm. We demonstrate our method's applicability across multiple benchmarks, comparing it to baseline methods called deterministic safety estimates and naive monolithic model checking. Our results show that our method is suited to verify stochastic RL policies.