Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning
Tiberiu-Andrei Georgescu, Alexander W. Goodall, Dalal Alrajeh, Francesco Belardinelli, Sebastian Uchitel

TL;DR
This paper presents an adaptive shielding framework for reinforcement learning that detects environment assumption violations and automatically repairs GR(1) specifications online, maintaining safety and liveness while optimizing rewards.
Contribution
It introduces a novel method combining GR(1) specification repair with ILP to adapt shields dynamically during RL, improving safety and performance.
Findings
Adaptive shields maintain near-optimal rewards.
Static shields are often suboptimal.
The method ensures liveness and minimal goal weakening.
Abstract
Shielding is widely used to enforce safety in reinforcement learning (RL), ensuring that an agent's actions remain compliant with formal specifications. Classical shielding approaches, however, are often static, in the sense that they assume fixed logical specifications and hand-crafted abstractions. While these static shields provide safety under nominal assumptions, they fail to adapt when environment assumptions are violated. In this paper, we develop an adaptive shielding framework based on based on Generalized Reactivity of rank 1 (GR(1)) specifications, a tractable and expressive fragment of Linear Temporal Logic (LTL) that captures both safety and liveness properties. Our method detects environment assumption violations at runtime and employs Inductive Logic Programming (ILP) to automatically repair GR(1) specifications online, in a systematic and interpretable way. This ensures…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Logic, programming, and type systems
