Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC

Dennis Gross

cs.AIFeb 16, 2026

Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC

Authors: Dennis Gross

Abstract

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.

Figures & tables

Panel of Figure 3 — Figure 3. State handling example within COOL-MC. Internally, COOL-MC uses PRISM’s integer state encoding for model checking. Whenever a state is passed to the policy, an explainability method, or state labeling, the observation function $\displaystyle\mathbb{O}$ maps it to its corresponding 47-dimensional observation, enabling decisions, analyses, and annotations based on clinically meaningful patient characteristics.

ID	Description	PCTL Property	Prob.
2max	Best achievable survival	$\displaystyle P_{\max}(\lozenge\ \texttt{survived})$	0.8751
2min	Worst-case survival	$\displaystyle P_{\min}(\lozenge\ \texttt{survived})$	0.633
2a	Best clean survival (no severe organ failure)	$\displaystyle P_{\max}(\ \neg\texttt{high\_sofa}\ \mathcal{U}\ \texttt{survived})$	0.4667
2b	Worst clean survival (no severe organ failure)	$\displaystyle P_{\min}(\ \neg\texttt{high\_sofa}\ \mathcal{U}\ \texttt{survived})$	0.2986
2c	Min. deaths without organ failure	$\displaystyle P_{\min}(\ \neg\texttt{high\_sofa}\ \mathcal{U}\ \texttt{died})$	0.0504
2d	Unavoidable low blood pressure	$\displaystyle P_{\min}(\lozenge\ \texttt{low blood pressure})$	0.5274

Table 1. Full MDP analysis: best-case and worst-case probabilities over all possible treatment policies. Labels, such as high_sofa , are atomic propositions assigned to states.

ID	Description	PCTL Property	Prob.
5a	Survival probability	$\displaystyle P_{=?}(\lozenge\;\texttt{survived})$	0.8751
5b	Death probability	$\displaystyle P_{=?}(\lozenge\;\texttt{died})$	0.1249
6a	Survive via no-treatment path	$\displaystyle P_{=?}(\texttt{fl0\_vp0}\;\mathcal{U}\;\texttt{survived})$	0.2159
6b	Reach max fluids, no vasopressors	$\displaystyle P_{=?}(\lozenge\;\texttt{fl4\_vp0})$	0.5414
6c	Reach max fluids + max vasopressors	$\displaystyle P_{=?}(\lozenge\;\texttt{fl4\_vp4})$	0.1029
7a	Reach state with input_4hourly as most important feature	$\displaystyle P_{=?}(\lozenge\;\texttt{imp\_input\_4hourly})$	1.0

Table 2. Trained policy (induced DTMC

\displaystyle D^{\pi}

): baseline outcomes and treatment trajectory properties. Action labels

\displaystyle\texttt{fl}_{i}\texttt{vp}_{j}

encode IV-fluid level

\displaystyle i

and vasopressor level

\displaystyle j

(

\displaystyle 0

= none,

\displaystyle 4

= maximum).

Panel of Figure 4 — Figure 4. Feature importance ranking via feature pruning. Each bar shows the change in survival probability when the corresponding feature $\displaystyle f_{i}$ is removed from the policy’s input. The feature input_4hourly dominates, indicating the policy relies heavily on the previous dosing window.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 323 papers

COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management
Mar 2, 2026Dennis GrossInventory Control Reinforcement Learning
EHR-MPC: Inference-Time Control for Sepsis Treatment with Generative Patient Digital Twins
Jul 7, 2026Joshua Pickard, Wei Qi, Na Li +4Inference-Time Optimization Model Predictive Control
Broad Institute of MIT and Harvard · Harvard University · Brigham and Women’s Hospital +2
Robust Counterfactual Policy Optimisation via Nondeterministic Causal Models
Aug 3, 2026Jessica Lally, Milad Kazemi, Nicola Paoletti +2Markov Decision Processes Structural Causal Models
1King’s College London · 2Durham University · University College London

Mar 2, 2026J/K move · Enter open · S save

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

Dennis Gross

Inventory Control Reinforcement Learning Interpretability in RL Formal Verification

Open paper AskPDF 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.

Abstract

Formal Verification

Explore similar work

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

EHR-MPC: Inference-Time Control for Sepsis Treatment with Generative Patient Digital Twins

Robust Counterfactual Policy Optimisation via Nondeterministic Causal Models