Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC
Not on the map. Why?
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.
Key facts. Cited by 3 papers in the map (data through 7 Oct 2026). Builds on 32 of its 76 references that are in the map. First posted on arXiv 16 Feb 2026.
Builds on
32 of 76 references.
References · 32
- 2017Safe Reinforcement Learning via Shieldingcited by 427
- 2019Reinforcement Learning in Healthcare: A Surveycited by 308
- 2022When Should We Prefer Offline Reinforcement Learning Over Behavioral Cloning?cited by 86
- 2020The Probabilistic Model Checker Stormcited by 64
- 2021Scalar reward is not enough: A response to Silver, Singh, Precup and Sutton (2021)cited by 55
- 2022Safe Reinforcement Learning via Shielding under Partial Observabilitycited by 49
- 2019An Inductive Synthesis Framework for Verifiable Reinforcement Learningcited by 39
- 2019Improving Sepsis Treatment Strategies by Combining Deep and Kernel-Based Reinforcement Learningcited by 34
- 2022COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checkingcited by 19
- 2015Permissive Controller Synthesis for Probabilistic Systemscited by 16
- 2021Unifying Cardiovascular Modelling with Deep Reinforcement Learning for Uncertainty Aware Control of Sepsis Treatmentcited by 16
- 2022Robust Anytime Learning of Markov Decision Processescited by 16
20 more
- 2023Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractionscited by 16
- 2021dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Expertscited by 14
- 2022Safe Reinforcement Learning From Pixels Using a Stochastic Latent Representationcited by 11
- 2023Safe Policy Improvement for POMDPs via Finite-State Controllerscited by 10
- 2019SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processescited by 9
- 2021Offline reinforcement learning with uncertainty for treatment strategies in sepsiscited by 9
- 2021Explaining Deep Reinforcement Learning Agents In The Atari Domain through a Surrogate Modelcited by 9
- 2023More for Less: Safe Policy Improvement With Stronger Performance Guaranteescited by 9
- 2024Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policiescited by 9
- 2024Reinforced Sequential Decision-Making for Sepsis Treatment: The POSNEGDM Framework with Mortality Classifier and Transformercited by 6
- 2024ICU-Sepsis: A Benchmark MDP Built from Real Medical Datacited by 6
- 2024Enhancing RL Safety with Counterfactual LLM Reasoningcited by 6
- 2019Strategy Representation by Decision Trees with Linear Classifierscited by 5
- 2022Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checkingcited by 5
- 20241-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalizationcited by 5
- 2022Learning Optimal Treatment Strategies for Sepsis Using Offline Reinforcement Learning in Continuous Spacecited by 4
- 2025Exploring Time-Step Size in Reinforcement Learning for Sepsis Treatmentcited by 4
- 2024How Consistent are Clinicians? Evaluating the Predictability of Sepsis Disease Progression with Dynamics Modelscited by 2
- 2025Probabilistic Model Checking: Applications and Trendscited by 1
- 2025Explainable AI For Early Detection Of Sepsiscited by 1
Built on by
Citing papers per year: 2026: 3.
3 papers.