PCTL Model Checking for Temporal RL Policy Safety Explanations
Dennis Gross, Helge Spieker · 2025
Reinforcement learning (RL) policies can exhibit unsafe behaviors and are often difficult to explain. While local explainability methods for RL offer insights into specific decisions, they often lack the temporal context for comprehensive explanations, especially for understanding safe behavior. This paper combines local explainable RL with PCTL model checking to explain complex, safe sequential decision-making over time, providing deeper insights into the trained RL policy. Our method uses five inputs: (1) a Markov Decision Process (MDP) representing the RL environment, (2) a trained policy, (3) a PCTL formula for safety assessment, (4) a local explainable RL method, and (5) a PCTL formula for the explainable RL method quantification at each state. By incrementally building reachable parts of the MDP guided by the trained policy and incorporating additional explainable features into the MDP's factored state representation, we verify the policy's safety in an explainable manner using PCTL model checking over these explainable features. Through diverse RL environments and different PCTL queries, we demonstrate that our method can explain trained RL policies in the context of explainable safety.