Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC

TL;DR

COOL-MC 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, illustrating how COOL-MC could serve as a tool for clinicians to investigate and debug sepsis treatment policies before deployment.

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 (4)

• Figure 1: Sequential decision-making loop. The agent receives an observation and reward from the environment, selects an action according to its policy, and the environment transitions to a new state.
• Figure 2: General model checking workflow DBLP:journals/sttt/HenselJKQV22. The system is formally modeled, the requirements are formalized, and both are input to a model checker such as Storm, which verifies the property.
• 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 $\mathbb{O}$ maps it to its corresponding 47-dimensional observation, enabling decisions, analyses, and annotations based on clinically meaningful patient characteristics.
• Figure 4: Feature importance ranking via feature pruning. Each bar shows the change in survival probability when the corresponding feature $f_i$ is removed from the policy's input. The feature input_4hourly dominates, indicating the policy relies heavily on the previous dosing window.

Theorems & Definitions (4)

• Definition 1: MDP
• Definition 2: DTMC
• Definition 3: Observation
• Definition 4