# Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in RL for clinical treatment and surgery, one of 15 directions in Deep reinforcement learning methods.
- Builds on 32 of its 76 references that are in the map.
- First posted on arXiv 16 Feb 2026.

## Placed in

- Deep reinforcement learning methods / [RL for clinical treatment and surgery](https://mlsanity.com/deeprl/rl-for-clinical-treatment-and-surgery/)

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

- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Reinforcement Learning in Healthcare: A Survey](https://mlsanity.com/paper/1908.08796/) (2019)
- [When Should We Prefer Offline Reinforcement Learning Over Behavioral Cloning?](https://mlsanity.com/paper/2204.05618/) (2022)
- [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)
- [Improving Sepsis Treatment Strategies by Combining Deep and Kernel-Based Reinforcement Learning](https://mlsanity.com/paper/1901.04670/) (2019)
- [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)
- [Unifying Cardiovascular Modelling with Deep Reinforcement Learning for Uncertainty Aware Control of Sepsis Treatment](https://mlsanity.com/paper/2101.08477/) (2021)
- [Robust Anytime Learning of Markov Decision Processes](https://mlsanity.com/paper/2205.15827/) (2022)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts](https://mlsanity.com/paper/2101.07202/) (2021)
- [Safe Policy Improvement for POMDPs via Finite-State Controllers](https://mlsanity.com/paper/2301.04939/) (2023)
- [Safe Reinforcement Learning From Pixels Using a Stochastic Latent Representation](https://mlsanity.com/paper/2210.01801/) (2022)
- [SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes](https://mlsanity.com/paper/1906.10640/) (2019)
- [Offline reinforcement learning with uncertainty for treatment strategies in sepsis](https://mlsanity.com/paper/2107.04491/) (2021)
- [Explaining Deep Reinforcement Learning Agents In The Atari Domain through a Surrogate Model](https://mlsanity.com/paper/2110.03184/) (2021)
- [More for Less: Safe Policy Improvement With Stronger Performance Guarantees](https://mlsanity.com/paper/2305.07958/) (2023)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Reinforced Sequential Decision-Making for Sepsis Treatment: The POSNEGDM Framework with Mortality Classifier and Transformer](https://mlsanity.com/paper/2403.07309/) (2024)
- [ICU-Sepsis: A Benchmark MDP Built from Real Medical Data](https://mlsanity.com/paper/2406.05646/) (2024)
- [Enhancing RL Safety with Counterfactual LLM Reasoning](https://mlsanity.com/paper/2409.10188/) (2024)
- [Strategy Representation by Decision Trees with Linear Classifiers](https://mlsanity.com/paper/1906.08178/) (2019)
- [Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking](https://mlsanity.com/paper/2212.05337/) (2022)
- [1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization](https://mlsanity.com/paper/2410.18293/) (2024)
- [Learning Optimal Treatment Strategies for Sepsis Using Offline Reinforcement Learning in Continuous Space](https://mlsanity.com/paper/2206.11190/) (2022)
- [Exploring Time-Step Size in Reinforcement Learning for Sepsis Treatment](https://mlsanity.com/paper/2511.20913/) (2025)
- [How Consistent are Clinicians? Evaluating the Predictability of Sepsis Disease Progression with Dynamics Models](https://mlsanity.com/paper/2404.07148/) (2024)

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

- [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)
- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

Safe and interpretable sequential decision-making is critical in healthcare, yet reinforcement learning (RL) policies for sepsis treatment optimization remain opaque and difficult to verify. Standard probabilistic model checkers operate on the full state space, which becomes infeasible for larger MDPs, and cannot explain why a learned policy makes particular decisions. COOL-MC wraps the model checker Storm but adds three key capabilities: it constructs only the reachable state space induced by a trained policy, yielding a smaller discrete-time Markov chain amenable to verification even when full-MDP analysis is intractable; it automatically labels states with clinically meaningful atomic propositions; and it integrates explainability methods with probabilistic computation tree logic (PCTL) queries to reveal which features drive decisions across treatment trajectories. We demonstrate COOL-MC's capabilities on the ICU-Sepsis MDP, a benchmark derived from approximately 17,000 sepsis patient records, which serves as a case study for applying COOL-MC to the formal analysis of sepsis treatment policies. Our analysis establishes hard bounds via full MDP verification, trains a safe RL policy that achieves optimal survival probability, and analyzes its behavior via PCTL verification and explainability on the induced DTMC. This reveals, for instance, that our trained policy relies predominantly on prior dosing history rather than the patient's evolving condition, a weakness that is invisible to standard evaluation but is exposed by COOL-MC's integration of formal verification and explainability. Our results illustrate how COOL-MC could serve as a tool for clinicians to investigate and debug sepsis treatment policies before deployment.