PaperlayerView exact revision on arXiv

Source-linked AI summary

RECREG: Recovery-based Shielding for Regular Safety Properties in Reinforcement Learning

Alexander W. Goodall, Francesco Belardinelli

arXiv:2610.23445v1cs.LGcs.AI

TL;DR

Safe RL needs to meet formal safety requirements, including when environment dynamics are unknown. RECREG applies recovery-based shielding through modes for different levels of model knowledge, and the paper reports theoretical guarantees and empirical results across tabular and deep RL settings.

  • Problem

    Safe RL approaches may lack rigorous guarantees, while obtaining meaningful safety guarantees with unknown environment dynamics remains an open question.

    Source: §1 · pp. 1–2

  • Method

    RECREG learns a safety-maximizing backup policy and shields actions using probabilistic safe sets, with EXACT, MODELBASED, and MODELFREE modes.

    Source: §1 · p. 2

  • Results

    Tabular experiments validate the theory, and deep RECREG reduces safety violations with good returns; with known dynamics, it achieves stronger returns than PROBSHIELD while both satisfy safety constraints.

    Source: §1 · p. 2, §4 · p. 9

  • Takeaways & Limitations

    The results support separating reward and safety objectives as an effective strategy for safety-aware decision making.

    Source: §5 · p. 9

    The guarantees rely on a finite horizon H* within which unsafe actions can be detected; increasing H* beyond its minimum may add computational overhead.

    Source: §3.1 · p. 6

Abstract

from arXiv · show

In many real-world scenarios we need to consider formal requirements, such as safety and constraint compliance, to deploy Reinforcement Learning (RL) agents. In this paper we introduce RecReg, a safe RL framework capable of enforcing non-Markovian regular safety properties via recovery-based shielding. RecReg is a unified approach that supports different levels of a priori knowledge and safety guarantees. The paper primarily focuses on building the theoretical foundations for RecReg in the tabular setting, providing rigorous safety and convergence guarantees that are not present in related work. We provide an extensive set of empirical results using the MASA-Safe-RL library, and we outline an extension of RecReg to deep RL domains using SOTA model-based RL. Our empirical results demonstrate that RecReg achieves efficient learning and matches the theory in this paper.

1 Introduction

RECREG addresses the challenge of enforcing safety in reinforcement learning when environment dynamics are unknown. It combines recovery-based shielding with formal safety and convergence guarantees across different levels of model knowledge.

1 Introduction

  • CMDPs enforce safety through cost functions and expected cumulative-cost thresholds, but may lack rigorous guarantees in safety-critical settings.The related-work discussion also notes that CMDP safety constraints are enforced only in expectation.Source: §1 · pp. 1–2
  • Classical shielding relies on pessimistic environment models, while probabilistic shielding still requires a known transition kernel; model-based RL offers a route to estimating unknown dynamics.RECREG addresses the question of meaningful safety guarantees when environment dynamics are unknown.Source: §1 · pp. 1–2
  • RECREG combines a learned safety-maximizing backup policy with probabilistic safe-set shielding across EXACT, MODELBASED, and MODELFREE modes.The paper also reports a deep RL variant using latent rollout models and safety critics, with guarantees under correct model calibration.Source: §1 · p. 2
  • RECREG enforces regular safety properties with high probability and offers guarantees when transition dynamics or structure are unknown, unlike approaches whose guarantees apply only at convergence.Automata Constrained Q-learning is described as lacking explicit safety guarantees during learning.Source: §1 · p. 2
  • Reward Machines work primarily on task specification, but counterfactual experiences and reward shaping from that literature could also be applied in RECREG.The paper identifies these as potential ways to speed up learning over Reward Machines.Source: §1 · pp. 2–3

2 Preliminaries

The preliminaries define regular safety through finite bad prefixes and a DFA, then formulate a reward-maximization objective subject to a safety-probability threshold. They also note that memoryless policies may not meet that threshold for more complex regular safety properties.

2 Preliminaries

  • The RL environment is modeled as an MDP with finite state and action sets, an initial-state set, a generally unknown transition kernel, and a reward function.The preliminaries describe memoryless stochastic policies and their induced Markov chains.Source: §2 · p. 3
  • A regular safety property has finite bad prefixes forming a regular language, represented by a DFA that accepts exactly those prefixes.A trace is safe when no finite prefix is accepted; the paper notes that LTL safety constraints can be handled through this representation.Source: §2 · p. 3
  • Safety probability is the probability that a policy-generated trace satisfies the property, equivalently that no finite prefix is accepted by its bad-prefix DFA.The definition is evaluated from a specified starting state.Source: §2 · p. 3
  • The objective is to maximize reward while requiring safety probability of at least 1−ε from every initial state, with ε chosen by the user.For complex regular safety properties, memoryless policies may fail to meet the bound or may be suboptimal under it.Source: §2 · pp. 3–4

3 RECREG: Recovery-based Shielding

RECREG represents regular safety constraints in a product MDP and shields a task policy using probabilistic safe sets and a backup policy. Its tabular guarantees depend on stated assumptions, while its deep-RL extension uses latent dynamics and cost predictions to estimate safety.

3 RECREG: Recovery-based Shielding

  • The product MDP synchronizes environment states with DFA states, turning safety into reachability and allowing memoryless product-state policies to represent non-Markovian policies in the original state space.Safety probability can be evaluated by probabilistic model checking in the product state space.Source: §3 · p. 4
  • A task policy proposes actions while a backup policy characterizes probabilistic safe sets; eventual discounting makes the backup maximally safe by minimizing the probability of reaching unsafe states.The shield replaces proposed actions based on estimated safe-set membership.Source: §3 · p. 5
  • If initial states are safe under the backup policy and stepwise risk budgets sum to at most ϵ, shielding guarantees global safety probability of at least 1−ϵ.Theorem 1 gives this guarantee for every initial state.Source: §3 · p. 5
  • As the backup policy converges, RECREG’s shield approaches the largest certifiable safe-action set, unlike Recovery RL’s potentially smaller recovery set that can cause unnecessary interventions [49].The distinction matters when task reward and safety conflict.Source: §3 · p. 5
  • The safety-aware Bellman operator accounts for action replacement during value updates and converges to the reward-optimal Q-function subject to maximal safe-action restrictions.The contraction guarantee assumes γ<1 and bounded, non-negative rewards.Source: §3 · pp. 5–6

3.1 RECREG for Tabular RL

  • In tabular model-based mode, empirical transitions support finite-horizon safety checking; the stated sample bound yields a high-probability global safety guarantee under the paper’s assumptions.Theorem 2 requires each state-action pair to be visited O((H*/ϵ')^2|S| log(|A||S|/δ)) times.Source: §3.1 · pp. 6–7
  • Model-free mode estimates finite-horizon reachability through Bellman updates and threshold checks; under the stated assumptions, task Q-iterates converge and the deployed policy satisfies the global safety constraint.The convergence result requires bounded non-negative rewards, standard step sizes, Theorem 1 conditions, and the finite-horizon assumption.Source: §3.1 · p. 7

3.2 RECREG with Deep RL

  • In deep RL, an RSSM cost head and fixed-horizon latent rollouts estimate safety without constructing the product MDP.Figure 1 reports normalized returns and safety probabilities averaged over 10 seeds for the final 100 training episodes; its dashed line marks Theorem 1’s theoretical safety probability.Source: §3.2 · pp. 7–8, Figure 1 · p. 8

4 Experimental Evaluation

RECREG is evaluated in tabular environments with varied safety properties, and risk can be allocated through different update strategies. Across the reported comparison, RECREG meets safety constraints and achieves stronger returns than PROBSHIELD.

4 Experimental Evaluation

  • Across tabular environments, both RECREG modes consistently meet the desired safety probability in almost all cases, with deviations mainly in larger state spaces.The reported deviations are attributed primarily to estimation or exploration challenges.Source: §4 · p. 8
  • Risk allocation can use uniform budgets, residual budgets conditioned on survival, or exact or estimated immediate and tail risk; treating budgets as free hyperparameters forfeits formal guarantees.Subtracting only immediate violation risk and conditioning on survival avoids double-counting future risk and is described as more accurate and less conservative.Source: §4 · pp. 8–9
  • Both methods satisfy safety constraints across environments, while RECREG-EXACT achieves stronger returns across the board.Table 1 compares PROBSHIELD and RECREG-EXACT; bold marks the best return and grey marks algorithms that fail the safety threshold.Source: §4 · p. 9, Table 1 · p. 9

5 Conclusion

RECREG enforces high-probability satisfaction of regular safety properties and provides formal safety and convergence guarantees. The paper reports experimental validation of its theoretical claims and identifies future extensions to other RL algorithms and scenarios.

5 Conclusion

  • RECREG enforces high-probability satisfaction of regular safety properties, with formal safety and convergence guarantees and optimality under step-wise constraints.The conclusion contrasts these guarantees with the closely related Recovery RL literature [49].Source: §5 · p. 9
  • The experiments validate the theoretical claims and provide further evidence that separating reward and safety objectives is effective for safety-aware decision making.Source: §5 · p. 9
  • Future work includes extending RECREG to more RL algorithms and scenarios such as safe control and policy-gradient methods.Source: §5 · p. 9

A.1 Theorem 10.52 in [7]

The appendix establishes how regular safety violations correspond to reaching accepting states in a product MDP, then proves safety and optimality properties under stated conditions.

A.1 Theorem 10.52 in [7]

  • A path violates the safety property exactly when its DFA run reaches an accepting state, which is represented as eventually reaching an unsafe state in the product MDP.The deterministic DFA gives a unique run for each path trace.Source: §A.1 · p. 14

A.2 Proof of Proposition 1

  • Under the assumption that some policy has non-zero safety probability, minimizing eventual-discounted return yields a maximally safe policy.The proof uses zero discounted return for safe paths and return 1/(1 − γ) for unsafe paths.Source: §A.2 · pp. 15–16

A.3 Proof of Theorem 1

  • If initial states satisfy the global safety constraint under the safe policy and step-wise risk budgets sum to at most ϵ, the shielded policy satisfies the global safety bound.The stated guarantee is Pπ♢(s0 |= Psafe) ≥ 1 − ϵ for every initial state.Source: §A.3 · p. 16

A.4 Proof of Proposition 2

The proof shows that the safety-restricted Bellman operator converges to a unique fixed point under bounded nonnegative rewards and discounting. That fixed point gives the optimal value among policies restricted to maximally safe actions.

A.4 Proof of Proposition 2

  • With γ in [0, 1) and bounded nonnegative rewards, Bsafe is a sup-norm contraction that converges to a unique fixed point.The proof identifies this fixed point as Q*safe.Source: §A.4 · pp. 17–18
  • The fixed point Q*safe is the optimal state-action value function under the action restrictions imposed by the maximally safe set.The corresponding greedy policy upper-bounds every safe policy in discounted reward.Source: §A.4 · pp. 17–18
  • Actions outside the maximally safe set are assigned value zero, so the safety-restricted update maximizes only over permissible actions.Source: §A.4 · p. 18

A.5 Proof of Proposition 3

Proposition 3 shows how model checking under an empirical transition kernel can estimate finite-horizon safety risk while accounting for model and sampling error. A conservative threshold then certifies safe actions.

A.5 Proof of Proposition 3

  • Statistical model checking needs at least 1/(2ϵ′²) log(2/δ′) sampled paths to estimate the risk with error ϵ′ and confidence at least 1−δ′.The proof applies this sample bound to paths drawn under the empirical product transition kernel.Source: §A.5 · pp. 19, 21
  • Empirical and true path distributions differ by at most a horizon-linear error when each transition-kernel estimate has bounded L1 error.This error-amplification bound supplies the model-error step used to establish Proposition 3.Source: §A.5 · p. 20
  • With transition-kernel total-variation error at most ϵ′/H, exact or statistical model checking estimates finite-horizon risk within ϵ′, with confidence 1 or at least 1−δ, respectively.The safe-set test uses the estimate threshold ϵt−ϵ′ to avoid false positives.Source: §A.5 · pp. 20–22
  • When the estimated risk is at most ϵt−ϵ′, the true risk is at most ϵt with the same guarantee as the estimate.Under Assumption 1, meeting the finite-horizon risk bound also implies the stated infinite-horizon risk bound.Source: §A.5 · p. 22

A.6 Proof of Theorem 2

Theorem 2 gives a visitation requirement under which an empirical model supports step-wise and global safety guarantees. The proof combines transition estimation with the finite-horizon risk test.

A.6 Proof of Theorem 2

  • Visiting every state-action pair O(|S|/p² log(|S||A|/δ)) times bounds all empirical transition-kernel L1 errors by p with probability at least 1−δ.A union bound over state-action pairs yields the simultaneous guarantee.Source: §A.6 · p. 22
  • If every state-action pair is visited O((H∗/ϵ′)²|S| log(|A||S|/δ)) times, the shielded policy meets the step-wise risk level with probability at least 1−2δ and the global safety constraint with the stated bound.This follows by applying the empirical-kernel error bound and Proposition 3.Source: §A.6 · p. 22
  • Lemma 7 shows that visiting each (s,a) at least O((H*/ϵ')^2|S| log(|A||S|/δ)) times gives ||bP(·|s,a)−P(·|s,a)||1 ≤ ϵ'/H* for all pairs with probability at least 1−δ.These estimates satisfy Proposition 3’s conditions.Source: §A.6 · p. 22

A.7 Proof of Theorem 3

Theorem 3 establishes convergence of RecReg’s task-value updates and global safety of its deployed shielded policy under the stated assumptions. The proof treats exact, model-based, and model-free operation, then sketches a deep-RL implementation using an RSSM.

A.7 Proof of Theorem 3

  • The convergence argument assumes bounded non-negative rewards, standard stochastic-approximation step sizes, infinite state-action visitation, and the stated safety conditions.The eventual-discounting argument also invokes a proper stochastic-shortest-path condition.Source: §A.7 · pp. 23–24
  • Under the theorem’s assumptions, task Q-iterates converge almost surely to the optimal Q-function subject to safe-set action restrictions, and the deployed shield satisfies the global safety constraint.The guarantee applies across all three operation modes.Source: §A.7 · pp. 23, 27
  • The backup policy converges to a maximally safe policy, and its estimated safe-set indicator eventually stops making mistakes almost surely.The proof establishes convergence for both model-based and model-free modes.Source: §A.7 · pp. 23, 25
  • Eventual indicator correctness lets the task update reduce to ordinary stochastic approximation of the safety-aware Bellman operator.The stated convergence uses Robbins–Monro step sizes and infinite visitation of each state-action pair.Source: §A.7 · pp. 25–26
  • In exact mode, the true product MDP supplies the safe-set indicator; contraction of the safety-aware Bellman operator yields convergence to its unique fixed point.In model-based and model-free modes, the learned indicator becomes correct almost surely, after which the task update converges to that same fixed point.Source: §A.7 · p. 27
  • With statistical model checking, the additional error is a failure probability δ that decreases exponentially with the number of sampled paths.The proof states that the desired confidence has only logarithmic dependence on sample count.Source: §A.7 · p. 27

B.1 Overview

  • In DEEP-RECREG, an RSSM estimates safety probability from sampled trajectories, and the algorithm can replace the task action with the safe policy when estimated risk exceeds ϵt.The task and safe policies are optimized separately using imagined sequences from the learned world model.Source: §B.1 · p. 28

B.2 Implementation Details

The appendix describes the deep-RL experiment settings and points to tabular and learning-curve results for Atari Seaquest. The supplied passages identify the results’ scope but do not report comparative outcome values.

B.2 Implementation Details

  • Seaquest uses 18 Atari controller actions, partially observed image inputs scaled to 64 × 64 × 3, and two safety properties with different automaton sizes and model-checking horizons.The horizons are H=30 for Property 1 and H=50 for Property 2; their automata have 5 and 32 states, respectively.Source: §B.2 · p. 29
  • SafetyGym experiments cover PointGoal1, PointGoal2, and CarGoal1, using constraints that prohibit hazards or the joint occurrence of a hazard and vase.The setup also specifies image observations and rewards for reaching a goal.Source: §B.2 · pp. 29–30
  • The reported learning-curve intervals are bootstrap 95% confidence intervals, based on 1,000 resamples.The stated uncertainty includes randomness in initialization, the environment, and batch sampling.Source: §B.2 · p. 31

B.3 Atari Seaquest results

  • Seaquest results are presented as tabular scores and learning curves averaged over five random seeds.Table 2 reports deep-RL Seaquest results, with violation rate scaled by 10^-4.Source: §B.3 · p. 31, Table 2 · p. 31, Figure 7 · p. 31

B.4 SafetyGym results

The supplementary results point to SafetyGym tables and learning curves, additional raw- and normalized-return summaries, and learning curves for tabular environments and RECREG-EXACT versus PROBSHIELD.

B.4 SafetyGym results

  • SafetyGym results are summarized in Table 3 and Figure 8, with the figure reporting episodic reward and violation rate averaged over five random seeds.The supplied passages identify the result displays but do not provide their values or comparisons.Source: §B.4 · p. 31, Table 3 · p. 32, Figure 8 · p. 32

C Additional Results

  • Tables 5 and 6 report experimental results with raw and normalized returns, marking the best safety-threshold-satisfying values in bold and failures in grey.The supplied table captions do not expose the cell values.Source: Table 5 · p. 34, Table 6 · p. 34

C.1 Learning Curves (tabular)

  • Learning-curve figures cover the MASA-Safe-RL tabular experiments, including Bridge Crossing, Colour Bomb Gridworld variants, Mini Pacman, and Media Streaming.The supplied captions identify curves across these tasks but do not state their outcomes.Source: §C.1 · p. 35, Figure 10 · p. 35, Figure 11 · p. 35

C.2 Learning Curves (PROBSHIELD)

  • The RECREG-EXACT versus PROBSHIELD learning-curve comparisons include Media Streaming, Bridge Crossing, Colour Bomb Gridworld V2 Property 3, and Mini Pacman.The supplied passages identify the comparison and plotted tasks, not which method performs better.Source: §C.2 · p. 37, Figure 18 · p. 38, Figure 19 · p. 38

C.3 Ablation Studies

The ablations examine counterfactual experiences and two potential-based shaping approaches, while the runtime analysis identifies model-checking overhead and its dependence on problem size.

C.3 Ablation Studies

  • Automated shaping assigns potentials to automaton states using value iteration with a discount factor below the original, whereas cycle-based shaping uses shortest-path lengths to the DFA initial state and assigns infinite value to accepting states.Both approaches redefine the safe-policy cost function using potential-based shaping.Source: §C.3 · p. 39
  • Without counterfactual experiences, RECREG-MODELFREE converges slowly and has low safety probability; cycle-based shaping improves stability and reaches optimal convergence, while automated shaping destabilizes learning slightly.The comparison is for Colour Bomb Gridworld V2 with the two potential-based shaping approaches.Source: §C.3 · pp. 39–40, Figure 22 · p. 40
  • Without counterfactual experiences, QL-λ struggles to converge quickly; automated and potential shaping destabilize learning, while cycle-based shaping improves safety and task performance uniformly.The authors attribute the difficulty of balancing task performance and safety to tuning Lagrangian cost functions and penalty magnitudes.Source: §C.3 · p. 40, Figure 23 · p. 40

C.4 Runtime Analysis

  • Model checking at every decision incurs computational overhead that grows with MDP or DFA size; the runtime comparison reports frames per second across RECREG modes.The authors report that EXACT and MODELFREE run at roughly the speed of mode-free tabular baselines such as Q-learning.Source: §C.4 · p. 40, Table 7 · p. 40

D Environment Details

The appendices describe the tabular environments and provide code and hyperparameter references for the evaluated algorithms.

D Environment Details

  • The environment suite spans gridworld navigation, buffer management, and Mini Pacman, with safety constraints ranging from invariants to more complex automaton-specified properties.Examples include preventing buffer underflow, avoiding lava or ghosts, and property variants for Colour Bomb Gridworld V2.Source: D Environment Details · pp. 41, 44

E Hyperparameters and Code

  • The tabular environments are provided by MASA-Safe-RL and implemented with Gymnasium; model checking uses JAX, while PPO-Lag and CPO implementations come from Omnisafe.The authors state that private code can be made available upon reasonable request.Source: E Hyperparameters and Code · pp. 44–45

E.1 Hyperparameters for Tabular Algorithms

  • Table 8 provides hyperparameter details for the Q-learning-based algorithms, including RECREG, Rec. RL, QL-λ, SEM, and LCRL.The authors direct readers to supplementary scripts for per-environment settings.Source: §E.1 · p. 46, Table 8 · p. 46

E.2 Hyperparameters for PPO-Lag and CPO

  • Table 9 provides hyperparameter details for PPO-Lag, TRPO-Lag, and CPO.The supplied passage identifies the table’s scope but not its settings.Source: Table 9 · p. 47

E.3 Hyperparameter details for PROBSHIELD

  • Table 10 provides hyperparameter details for PROBSHIELD.The supplied passage identifies the table but does not provide its settings.Source: Table 10 · p. 48
Loading 2610.23445v1…