Explainably Safe Reinforcement Learning

Summary

This partial ingest is based on the extracted full PDF text. Rieder et al. propose explainably safe RL: a shielded-RL framework that explains the shield’s safety decisions using a hierarchy of compact decision trees. The method computes risk of safety violation from an MDP and CTL-style safety property, classifies states as safe, critical, dangerous, or unsafe, derives a probabilistic shield, and uses level-specific trees to explain state risk, allowed actions, and unsafe-action evidence.

Key Claims

• Shielded RL adds formal safety guarantees, but lookup-table shields can be almost as opaque as the learned policy they wrap.
• Explaining the shield rather than the neural policy gives a tractable explanation target for the safety aspect of behavior.
• A hierarchy of decision trees can provide top-down case-based explanations without representing the entire nondeterministic shield as one huge tree.
• The framework requires no additional model beyond the MDP abstraction and safety specification already needed for probabilistic shielding.
• Reported benchmarks show explanation trees several orders of magnitude smaller than raw shield lookup tables or monolithic shield trees.

Methods / Formalism

• The input is an MDP M=<S,s_0,A,P>, a safety property phi, finite horizon h, and risk threshold epsilon.
• Risk of a state is the minimal probability of violating phi within h steps under the safest policy. Risk of (s,a) is the probability-weighted successor risk after action a.
• An action is safe in state s when risk(s,a,h) <= epsilon.
• States are partitioned into safe, critical, dangerous, and unsafe categories depending on whether all, some, no, or already-violated actions satisfy the risk threshold.
• The shield permits all safe actions and, in dangerous states, allows the lowest-risk action. Shield Risk Decision Trees records the Level 1, Level 2, and Level 3 explanation construction.

Evidence / Experiments

• Benchmarks include Frozen Lake, Highway, and Taxiing environments.
• The Level 1 tree explains state category; Level 2 trees explain action availability inside critical/dangerous regions; Level 3 execution trees give evidence traces for a selected unsafe action.
• For Frozen Lake grids of increasing size, the decision-tree explanations remain much smaller than the shield lookup table and a monolithic shield tree.
• Experiments use probabilistic model-checking queries and decision-tree tooling to compare shield/table/tree sizes as the main explainability metric.

Connections

• Extends Shielding with human-facing explanations for why the shield blocks or permits actions.
• Connects Explainable AI to Formal Methods by explaining a formally generated safety layer rather than post hoc rationalizing a learned policy.
• Relies on Probabilistic Model Checking for state/action risk computation over an MDP abstraction.
• Complements Bloem2015 - Shield Synthesis, which focuses on reactive-system shield construction rather than shield legibility.

Open Questions

• How faithful are compact trees when user-defined predicates are needed to make explanations intuitive?
• Can the approach explain shields synthesized for continuous, high-dimensional, or learned abstractions without losing the formal safety interpretation?
• How should users act on dangerous-state explanations when all actions exceed the risk threshold and the shield merely picks the least risky action?

Citation

Rieder, Sabine, Stefan Pranger, Debraj Chakraborty, Jan Kretinsky, and Bettina Koenighofer. 2025. “Explainably Safe Reinforcement Learning.” In Advances in Neural Information Processing Systems 39.