Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Realizable Continuous-Space Shields for Safe Reinforcement Learning

Kyungmin Kim, Davide Corsi, Andoni Rodriguez, JB Lanier, Benjami Parellada, Pierre Baldi, Cesar Sanchez, Roy Fox

TL;DR

This work tackles safety guarantees for reinforcement learning in continuous spaces by introducing Proper Shields that realize safety specifications via LTLt. It develops offline realizability checks and a stateful shield that can override risky actions while minimizing deviation from the agent's original decision; it also introduces an anticipation fragment to enable decidable realizability for non-Markovian requirements. The approach is demonstrated on mapless navigation and particle-world experiments, showing formal safety guarantees with minimal impact on policy performance and applicability to multi-agent settings. The work advances safe RL for real-world robotics by providing a practical, verifiable shielding framework with continuous dynamics and non-Markovian constraints.

Abstract

While Deep Reinforcement Learning (DRL) has achieved remarkable success across various domains, it remains vulnerable to occasional catastrophic failures without additional safeguards. An effective solution to prevent these failures is to use a shield that validates and adjusts the agent's actions to ensure compliance with a provided set of safety specifications. For real-world robotic domains, it is essential to define safety specifications over continuous state and action spaces to accurately account for system dynamics and compute new actions that minimally deviate from the agent's original decision. In this paper, we present the first shielding approach specifically designed to ensure the satisfaction of safety requirements in continuous state and action spaces, making it suitable for practical robotic applications. Our method builds upon realizability, an essential property that confirms the shield will always be able to generate a safe action for any state in the environment. We formally prove that realizability can be verified for stateful shields, enabling the incorporation of non-Markovian safety requirements, such as loop avoidance. Finally, we demonstrate the effectiveness of our approach in ensuring safety without compromising the policy's success rate by applying it to a navigation problem and a multi-agent particle environment.

Realizable Continuous-Space Shields for Safe Reinforcement Learning

TL;DR

This work tackles safety guarantees for reinforcement learning in continuous spaces by introducing Proper Shields that realize safety specifications via LTLt. It develops offline realizability checks and a stateful shield that can override risky actions while minimizing deviation from the agent's original decision; it also introduces an anticipation fragment to enable decidable realizability for non-Markovian requirements. The approach is demonstrated on mapless navigation and particle-world experiments, showing formal safety guarantees with minimal impact on policy performance and applicability to multi-agent settings. The work advances safe RL for real-world robotics by providing a practical, verifiable shielding framework with continuous dynamics and non-Markovian constraints.

Abstract

While Deep Reinforcement Learning (DRL) has achieved remarkable success across various domains, it remains vulnerable to occasional catastrophic failures without additional safeguards. An effective solution to prevent these failures is to use a shield that validates and adjusts the agent's actions to ensure compliance with a provided set of safety specifications. For real-world robotic domains, it is essential to define safety specifications over continuous state and action spaces to accurately account for system dynamics and compute new actions that minimally deviate from the agent's original decision. In this paper, we present the first shielding approach specifically designed to ensure the satisfaction of safety requirements in continuous state and action spaces, making it suitable for practical robotic applications. Our method builds upon realizability, an essential property that confirms the shield will always be able to generate a safe action for any state in the environment. We formally prove that realizability can be verified for stateful shields, enabling the incorporation of non-Markovian safety requirements, such as loop avoidance. Finally, we demonstrate the effectiveness of our approach in ensuring safety without compromising the policy's success rate by applying it to a navigation problem and a multi-agent particle environment.
Paper Structure (33 sections, 2 theorems, 4 equations, 5 figures, 5 tables, 1 algorithm)

This paper contains 33 sections, 2 theorems, 4 equations, 5 figures, 5 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Concepts in Temporal Logic and Reactive Systems
  4. LTL.
  5. Satisfiability and Realizability.
  6. Realizability for Continuous Domains.
  7. Realizable Continuous Shields with Non-Markovian Requirements
  8. Non-Markovian Encoding in LTLt
  9. Case Study: Mapless Navigation with Reinforcement Learning
  10. Continuous Shield for Safe Navigation
  11. Markovian Requirements for Collision Avoidance.
  12. Non-Markovian Requirements for Loop Avoidance.
  13. Realizability and Shielding Implementation
  14. Experimental Results
  15. Realizability Check.
  16. ...and 18 more sections

Key Result

theorem 1

If $\varphi$ is an LTLt formula where the subset of the next values of the environment variables that appear in $\varphi$ are isolated and can be fully determined from the current environment and system values, then $\varphi$ can be rewritten without the use of $\lhd$ (proof in Appendix app:anticipa

Figures (5)

  • Figure 1: In the offline process, the realizability check verifies whether the system is realizable, taking the system configuration as input, i.e., the dynamics of the environment, the safety requirements, and the input domain. If not realizable, the system needs to be changed. When proved to be realizable (i.e., a Proper Shield), the shield can be safely deployed in the environment for the online process.
  • Figure 2: Average success rate and collision rate obtained during the DRL training process for 500 episodes (x-axis) without any shield applied (averaged over $5$ different random seeds).
  • Figure 3: Description of collision avoidance requirements that include the dynamic of the robot as part of the formula.
  • Figure 4: An unshielded agent collides with obstacles and avoids them when a collision shield is applied. By introducing non-Markovian requirements, the agent also avoids oscillations.
  • Figure 5: The Mapless Navigation environment (Left) and the Particle World environment (Right).

Theorems & Definitions (5)

  • definition 1: Proper Shield
  • theorem 1
  • definition 2: Anticipation Fragment
  • corollary 1
  • proof