Explanations for Unrealizability of Infinite-State Safety Shields

Andoni Rodríguez, Irfansha Shaik, Davide Corsi, Roy Fox, and César Sánchez

22nd International Conference on Principles of Knowledge Representation and Reasoning (KR), 2025

BibTeX

@conference{ Rodríguez2025Unrealizability,
  Title = "Explanations for Unrealizability of Infinite-State Safety Shields",
  Author = "Andoni Rodríguez and Irfansha Shaik and Davide Corsi and Roy Fox and César Sánchez",
  Booktitle = "22nd International Conference on Principles of Knowledge Representation and Reasoning (KR)",
  Year = "2025"
}

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.