Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

The paper tackles ensuring safety and liveness for reinforcement learning agents when environmental assumptions may be violated. It introduces RepairRL, an online framework that uses GR(1) specifications to synthesize a shield, detects runtime assumption violations via an Environment Checker, and repairs the specification online with ILP-guided SpecRepair to yield a new shield and updated winning region. This approach preserves safety with minimal intervention, while enabling near-optimal rewards, as demonstrated in Minepump and Seaquest experiments. The framework emphasizes interpretability, providing human-readable explanations of shield changes, and shows practical viability through polynomial-time GR(1) synthesis and online adaptation. Overall, adaptive GR(1) specification repair offers a principled, scalable way to maintain safety and liveness in RL under evolving or misspecified environments.

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 the first adaptive shielding framework - to the best of our knowledge - 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 that the shield evolves gracefully, ensuring liveness is achievable and weakening goals only when necessary. We consider two case studies: Minepump and Atari Seaquest; showing that (i) static symbolic controllers are often severely suboptimal when optimizing for auxiliary rewards, and (ii) RL agents equipped with our adaptive shield maintain near-optimal reward and perfect logical compliance compared with static shields.

Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning

TL;DR

The paper tackles ensuring safety and liveness for reinforcement learning agents when environmental assumptions may be violated. It introduces RepairRL, an online framework that uses GR(1) specifications to synthesize a shield, detects runtime assumption violations via an Environment Checker, and repairs the specification online with ILP-guided SpecRepair to yield a new shield and updated winning region. This approach preserves safety with minimal intervention, while enabling near-optimal rewards, as demonstrated in Minepump and Seaquest experiments. The framework emphasizes interpretability, providing human-readable explanations of shield changes, and shows practical viability through polynomial-time GR(1) synthesis and online adaptation. Overall, adaptive GR(1) specification repair offers a principled, scalable way to maintain safety and liveness in RL under evolving or misspecified environments.

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 the first adaptive shielding framework - to the best of our knowledge - 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 that the shield evolves gracefully, ensuring liveness is achievable and weakening goals only when necessary. We consider two case studies: Minepump and Atari Seaquest; showing that (i) static symbolic controllers are often severely suboptimal when optimizing for auxiliary rewards, and (ii) RL agents equipped with our adaptive shield maintain near-optimal reward and perfect logical compliance compared with static shields.

Paper Structure

This paper contains 44 sections, 4 theorems, 8 equations, 4 figures, 6 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Reinforcement Learning
  4. Linear Temporal Logic
  5. GR(1) Synthesis and Realizability
  6. Example (Minepump).
  7. The RepairRL Shielding Approach
  8. GR(1) Winning Region as Shield
  9. Integration with Reinforcement Learning
  10. Definition of Safe Action
  11. Derived Safe Action Set
  12. Division of Responsibilities
  13. Online Shield Adaptation
  14. Initial Shield Synthesis
  15. Deployment and Monitoring
  16. ...and 29 more sections

Key Result

corollary 1

Given a realisable specification $\Phi$ synthesised as a fairness-free FDS $\mathcal{S}h = \langle\mathcal{V}, \hat{\theta}, \hat{\rho}\rangle$, a run of consecutive states $(\nu_0,\nu_1,\nu_2,\dots)\in (2^{\Sigma})^\omega$ that satisfies the initial environment condition $\nu_0\models\theta^e$ and

Figures (4)

  • Figure 1: RepairRL: A shield repair framework for logical constraints in GR(1).
  • Figure 2: Atari Seaquest: rescue divers (blue people), while shooting enemy sharks and submarines to collect reward.
  • Figure 3: Learning curves for the Minepump
  • Figure 4: Learning curves for the Seaquest

Theorems & Definitions (4)

  • corollary 1: Shield Closure under the Winning Region
  • corollary 2: Correctness and Minimal Deviation
  • corollary 3: Soundness of SpecRepair
  • corollary 4