Explanations for Unrealizability of Infinite-State Safety Shields

TL;DR

This paper introduces a method to explain why certain safety shields in infinite-state reinforcement learning environments are unrealizable, using temporal formula unrolling to identify inconsistencies in specifications.

Contribution

It presents a novel approach for generating simple explanations for unrealizability of safety shields in infinite-state domains, addressing a key gap in current shielding techniques.

Findings

The method effectively identifies inconsistent specifications.

It applies to both unconditional and conditional unrealizability cases.

The technique is demonstrated on various examples.

Abstract

Safe Reinforcement Learning focuses on developing optimal policies while ensuring safety. A popular method to address such task is shielding, in which a correct-by-construction safety component is synthesized from logical specifications. Recently, shield synthesis has been extended to infinite-state domains, such as continuous environments. This makes shielding more applicable to realistic scenarios. However, often shields might be unrealizable because the specification is inconsistent (e.g., contradictory). In order to address this gap, we present a method to obtain simple unconditional and conditional explanations that witness unrealizability, which goes by temporal formula unrolling. In this paper, we show different variants of the technique and its applicability.