# COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking

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

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 40 references that are in the map.
- First posted on arXiv 15 Sep 2022.

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

- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [End-to-End Training of Deep Visuomotor Policies](https://mlsanity.com/paper/1504.00702/) (2015)
- [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)
- [Scalar reward is not enough: A response to Silver, Singh, Precup and Sutton (2021)](https://mlsanity.com/paper/2112.15422/) (2021)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Safety-Constrained Reinforcement Learning for MDPs](https://mlsanity.com/paper/1510.05880/) (2015)
- [Permissive Controller Synthesis for Probabilistic Systems](https://mlsanity.com/paper/1504.04662/) (2015)
- [Enforcing Almost-Sure Reachability in POMDPs](https://mlsanity.com/paper/2007.00085/) (2020)
- [Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning](https://mlsanity.com/paper/2004.00273/) (2020)
- [Specification-Guided Learning of Nash Equilibria with High Social Welfare](https://mlsanity.com/paper/2206.03348/) (2022)
- [Mungojerrie: Reinforcement Learning of Linear-Time Objectives](https://mlsanity.com/paper/2106.09161/) (2021)
- [Verified Probabilistic Policies for Deep Reinforcement Learning](https://mlsanity.com/paper/2201.03698/) (2022)

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

- [LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/2209.10341/) (2022)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Enhancing RL Safety with Counterfactual LLM Reasoning](https://mlsanity.com/paper/2409.10188/) (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)
- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [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)
- [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)
- [Safe But Not Sorry: Reducing Over-Conservatism in Safety Critics via Uncertainty-Aware Modulation](https://mlsanity.com/paper/2510.18478/) (2025)
- [Formal Verification of Noisy Quantum Reinforcement Learning Policies](https://mlsanity.com/paper/2512.01502/) (2025)
- [Translating the Rashomon Effect to Sequential Decision-Making Tasks](https://mlsanity.com/paper/2512.17470/) (2025)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance](https://mlsanity.com/paper/2603.07546/) (2026)
- [Formal Verification of Learned Multi-Agent Communication Policies via Decision Tree Distillation](https://mlsanity.com/paper/2606.19632/) (2026)
- [Gimitest: A Comprehensive Tool for Testing Reinforcement Learning Policies](https://mlsanity.com/paper/2607.07029/) (2026)
- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

This paper presents COOL-MC, a tool that integrates state-of-the-art reinforcement learning (RL) and model checking. Specifically, the tool builds upon the OpenAI gym and the probabilistic model checker Storm. COOL-MC provides the following features: (1) a simulator to train RL policies in the OpenAI gym for Markov decision processes (MDPs) that are defined as input for Storm, (2) a new model builder for Storm, which uses callback functions to verify (neural network) RL policies, (3) formal abstractions that relate models and policies specified in OpenAI gym or Storm, and (4) algorithms to obtain bounds on the performance of so-called permissive policies. We describe the components and architecture of COOL-MC and demonstrate its features on multiple benchmark environments.