# COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 80 of its 158 references that are in the map.
- First posted on arXiv 2 Mar 2026.

## Builds on (most cited first, 30 of 80)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [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)
- [End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks](https://mlsanity.com/paper/1903.08792/) (2019)
- [Programmatically Interpretable Reinforcement Learning](https://mlsanity.com/paper/1804.02477/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [A General Safety Framework for Learning-Based Control in Uncertain Robotic Systems](https://mlsanity.com/paper/1705.01292/) (2017)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [Reinforcement Learning for Safety-Critical Control under Model Uncertainty, using Control Lyapunov Functions and Control Barrier Functions](https://mlsanity.com/paper/2004.07584/) (2020)
- [Q-Learning for Robust Satisfaction of Signal Temporal Logic Specifications](https://mlsanity.com/paper/1609.07409/) (2016)
- [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 Multi-Agent Reinforcement Learning via Shielding](https://mlsanity.com/paper/2101.11196/) (2021)
- [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)
- [Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints](https://mlsanity.com/paper/1404.7073/) (2014)
- [Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/1801.08099/) (2018)
- [A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications](https://mlsanity.com/paper/1409.5486/) (2014)
- [Neurosymbolic Reinforcement Learning with Formally Verified Exploration](https://mlsanity.com/paper/2009.12612/) (2020)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [Safe Reinforcement Learning via Probabilistic Logic Shields](https://mlsanity.com/paper/2303.03226/) (2023)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [Iterative Reachability Estimation for Safe Reinforcement Learning](https://mlsanity.com/paper/2309.13528/) (2023)
- [Verifiably Safe Exploration for End-to-End Reinforcement Learning](https://mlsanity.com/paper/2007.01223/) (2020)
- [Safety-Constrained Reinforcement Learning for MDPs](https://mlsanity.com/paper/1510.05880/) (2015)

## Abstract (arXiv)

Platelets expire within five days. Blood banks face uncertain daily demand and must balance ordering decisions between costly wastage from overstocking and life-threatening shortages from understocking. Reinforcement learning (RL) can learn effective ordering policies for this Markov decision process (MDP), but the resulting neural policies remain black boxes, hindering trust and adoption in safety-critical domains. We apply COOL-MC, a tool that combines RL with probabilistic model checking and explainable RL, to verify and explain a trained policy for the MDP on platelet inventory management inspired by Haijema et al. By constructing a policy-induced discrete-time Markov chain (which includes only the reachable states under the trained policy to reduce memory usage), we verify PCTL properties and provide feature-level explanations. Results show that the trained policy achieves a 2.9% stockout probability and a 1.1% inventory-full (potential wastage) probability within a 200-step horizon, primarily attends to the age distribution of inventory rather than other features such as day of week or pending orders. Action reachability analysis reveals that the policy employs a diverse replenishment strategy, with most order quantities reached quickly, while several are never selected. Counterfactual analysis shows that replacing medium-large orders with smaller ones leaves both safety probabilities nearly unchanged, indicating that these orders are placed in well-buffered inventory states. This first formal verification and explanation of an RL platelet inventory management policy demonstrates COOL-MC's value for transparent, auditable decision-making in safety-critical healthcare supply chain domains.