CoChat
Sign Up
Cited by 700Reinforcement Learning in RoboticsFormal Methods in VerificationLogic, Reasoning, and Knowledge

Safe Reinforcement Learning via Shielding

Open access
Alshiekh, Mohammed, Bloem, Roderick, Ehlers, Rüdiger, Könighofer, Bettina, Niekum, Scott, Topcu, Ufuk·2018·Proceedings of the AAAI Conference on Artificial Intelligence
DOI 10.1609/aaai.v32i1.11797
Open this paper in CoChat — free account

Abstract

Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. We introduce a new approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given the temporal logic specification that is to be obeyed by the learning system, we propose to synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification. We discuss which requirements a shield must meet to preserve the convergence guarantees of the learner. Finally, we demonstrate the versatility of our approach on several challenging reinforcement learning scenarios.

Verified 2026-10-24 · 4 references not checked yet

AI snapshot

Written from the paper’s full text.

TL;DR

The paper proposes shielded reinforcement learning, where a reactive shield synthesized from a temporal-logic safety specification and an environment abstraction monitors learner actions and replaces them only when needed to avoid unsafe behavior. It proves correctness and minimal interference, gives conditions for preserving convergence, and demonstrates safety and often faster learning in four simulated domains.

Key findings

  • Shields can enforce safety during both learning and execution without changing the reward signal, and they are minimally interfering: they block an action only when it could lead to a specification violation under the abstraction.
  • In the water-tank example, the product game had 602 states, and the shield prevented opening the inflow valve above level 93 and forced opening when the level became too low.
  • Shield synthesis was fast in the reported experiments: under 2 seconds for the grid-world cases, about 2 seconds for the self-driving car, under 1 second for the water tank, and under 7 seconds for Pacman.
  • In the 15x9 grid world, only the shielded setting with a ranking of 3 actions and no penalty found the optimal path; in the water-tank experiments, shielded Q-learning and SARSA reached optimal policies in significantly fewer episodes than unshielded versions; in the self-driving car case, the shielded learner never crashed and learned faster; in Pacman, the shielded agent cleared the game from the first episode.

Methods

  • The approach specifies safety in linear temporal logic, converts it to a deterministic safety automaton, builds a conservative finite-state abstraction of the MDP environment, and solves a safety game to synthesize a shield.
  • The shield receives the learner’s action or ranked list of actions and executes the highest-ranked safe action; it deviates only if every ranked action is unsafe, in which case it chooses some safe action.
  • The paper proves correctness and minimal interference, constructs a product MDP to argue convergence for standard MDP learners, and evaluates the method in simulations: 9x9 and 15x9 grid worlds, a 480x480-pixel self-driving car task, the water-tank controller, and an 18x5 Pacman-like maze, using tabular Q-learning, deep Q-networks, and approximate Q-learning.

Limitations

  • The paper states that the main downside is the need for an approximate model or abstraction indicating when actions are unsafe, and argues this is unavoidable when allowed actions depend on the environment state.
  • The convergence argument requires that when the learner’s ranking contains no safe action, the shield’s choice among safe actions follows a fixed probability distribution over time, and it assumes the learner can observe the shield state.
  • Evident from the text: the evaluation is entirely simulation-based, with no real-world deployment; the approach relies on the abstraction being conservative, and the shield must remain active after learning because unsafe actions may still be part of the learned policy.

Model-written summary. Check it against the paper before relying on it.

Integrity signals

Registry

Crossref · 10.1609/aaai.v32i1.11797

Cites

27 of 31 references verified0 citation errors · 0 not checkable

Statistics

Nothing to recompute.

Claims the paper makes

2 of 6 cited sources checked · 0 supported · 1 flagged · accuracy not yet measured

  • Findingown data

    In the 9x9 grid world, only the unshielded versions experience negative rewards.

    “The results show that only the unshielded versions experience negative rewards.”
    Quote in the paperSubstantial claim
  • Findingown data

    In the water tank example, both shielded and unshielded Q-learning and SARSA experiments reach an optimal policy.

    “Fig. 11 shows that both shielded (dashed lines) and unshielded Q-learning and SARSA experiments (solid lines) do reach an optimal policy.”
    Quote in the paperNot a substantial claim
  • Findingown data

    In all experiments, the learning performance of the shielded agents improved compared to the unshielded case.

    “In all of them, the learning performance of the shielded agents improved compared to the unshielded case.”
    Quote in the paperSubstantial claim
  • Findingown data

    In the pacman example, in the shielded case, pacman is always able to clear the game starting from the first episode.

    “As expected, in the shielded case, pacman is always able to clear the game starting from the first episode.”
    Quote in the paperNot a substantial claim
  • Findingown data

    In the water tank example, the shielded implementations reach the optimal policy in a significantly shorter time than the unshielded implementations.

    “However, the shielded implementations reach the optimal policy in a significantly shorter time than the unshielded implementations.”
    Quote in the paperSubstantial claim
  • Classified as probably not a substantial claim. 17
  • May combine two claims. 17

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation

    Safe exploration can only be achieved through the incorporation of external knowledge.

    “An exploration process is called safe if no undesirable states are ever visited, which can only be achieved through the incorporation of external knowledge (García and Fernández 2015;Moldovan and Abbeel 2012).”
    Quote in the paperNot a substantial claim1 of 2 sources checked
    • cites García and Fernández 2015
    • cites Moldovan and Abbeel 2012 source

      The Safety Constraint section (p. 3) defines safety as preserving ergodicity with a user-specified probability, not as never visiting an undesirable state. The Safety Counter-Examples section (p. 3) explicitly argues against defining safety by safe and unsafe states. The paper uses a prior belief and information learned during exploration, but does not say that incorporating external knowledge is the only way to achieve safety. (LLM, conf=0.82)

      Checked by a reasoning model — may be wrong.

      Experimental — accuracy not yet measured

  • May combine two claims.

    Premisecitation

    Wen et al.'s technique does not work with function approximation, which prevents it from being used in complex scenarios.

    “Unlike the approach in the paper, their technique does not work with function approximation, which prevents it from being used in complex scenarios.”
    Quote in the paperNot a substantial claim1 of 1 sources checked
    • cites Wen, Ehlers, and Topcu 2015 source

      Section V (Examples; page unavailable) shows that learning time and iterations grow as the grid grows, and describes a trade-off between performance and computation cost. This supports a scalability concern, but the paper does not say that its technique cannot work with function approximation or that it cannot be used in complex scenarios. (LLM, conf=0.76)

      Experimental — accuracy not yet measured

  • May combine two claims.

    Findingown data

    In the self-driving car example, the accumulated rewards for unshielded RL increase over time, but the car still crashes at the end of the simulation.

    “The plot in Fig. 10 shows that the accumulated rewards for unshielded RL (red, dashed) increases over time, but the car still crashes at the end of the simulation.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    In the 15x9 grid world, scenarios with |rank_t| = 1 or with penalties compute a suboptimal path.

    “In scenarios with |rank t | = 1 (red) or with penalties (solid), the agent computes a suboptimal path.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    In the 15x9 grid world, only the shielded version with |rank_t| = 3 without penalty finds the optimal path, resulting in a higher average reward.

    “Only the shielded version with |rank t | = 3 without penalty (blue, dashed) finds the optimal path, resulting in a higher average reward.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    In the 9x9 grid world, the shielded version is not only safe, but also tends to learn more rapidly.

    “Furthermore, the shielded version is not only safe, but also tends to learn more rapidly.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    In the self-driving car example, the shielded version without punishment learns more rapidly than the unshielded learner and never crashes.

    “The shielded version without punishment (blue, solid) learns more rapidly than the unshielded learner and never crashes.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim. May combine two claims.

    Premisecitation

    For specifications in LTL, it is known how to check if it is a safety language and how to compute a safety automaton that represents it.

    “For specifications in LTL, it is known how to check if it is a safety language and how to compute a safety automaton that represents it (Kupferman and Vardi 2001).”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites Kupferman and Vardi 2001 source

  • Probably not a substantial claim: may not pass S2 (checkable), S4 (based). May combine two claims.

    Interpretationnone given

    An abstraction of an MDP describes how its executions can possibly evolve, and provides the needed information about the environment to allow planning ahead with respect to the safety properties of interest.

    “An abstraction of an MDP describes how its executions can possibly evolve, and provides the needed information about the environment to allow planning ahead w.r.t. the safety properties of interest.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Interpretationnone given

    The computational cost of constructing the shield is independent of state space components of the system to be controlled that are irrelevant for enforcing the safety specification.

    “and is independent of the state space components of the system to be controlled that are irrelevant for enforcing the safety specification.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S4 (based). May combine two claims.

    Interpretationnone given

    The shield ensures safety and minimum interference.

    “It ensures safety and minimum interference.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Interpretationnone given

    The shield is computed upfront from the safety part of the given system specification and an abstraction of the agent's environment dynamics.

    “The shield is computed upfront from the safety part of the given system specification and an abstraction of the agent's environment dynamics.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Interpretationreasoning

    The boundary between the learning agent and the shield helps separate safety and correctness from convergence and optimality.

    “This boundary helps to separate the concerns, e.g., safety and correctness on one side and convergence and optimality on the other”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Interpretationreasoning

    Preventing the inflow valve from being opened when the level is above 93 is necessary because the valve has to stay open for at least three time steps, and during this time the inflow may be up to 2 liters/second while the outflow may be 0, so there is otherwise an overflow risk.

    “The latter is necessary as the valve has to stay open for at least three time steps.So as the inflow may be up to 2 liters/second during this time and the outflow may be 0, there is otherwise an overflow risk.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Interpretationreasoning

    The approximation of the environment dynamics may have finitely many states even if the MDP has infinitely many states and/or is only approximately known.

    “This approximation may have finitely many states even if the MDP has infinitely many states and/or is only approximately known.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Interpretationnone given

    The shielding framework is compatible with mechanisms such as function approximation employed by learning algorithms to improve scalability.

    “Last but not least, the shielding framework is compatible with mechanisms such as function approximation, employed by learning algorithms in order to improve their scalability.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Interpretationnone given

    The algorithms presented for computation of shields make relatively mild assumptions on the input-output structure of the learning algorithm rather than its inner working.

    “The algorithms we present for the computation of shields make relatively mild assumptions on the input-output structure of the learning algorithm (rather than its inner working).”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Premisenone given

    Reactive synthesis enforces a safety specification by solving a safety game built from the specification and an abstraction of the environment in which the policy is to be executed.

    “Reactive synthesis enforces ϕ s by solving a safety game built from ϕ s and an abstraction of the environment in which the policy is to be executed.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Interpretationnone given

    Planning ahead does not require the environment dynamics to be completely known in advance.

    “Planning ahead does not require the environment dynamics to be completely known in advance.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Premisereasoning

    All traditional correct-by-construction controller computation approaches require a faithful, yet precise enough, abstraction of the physical environment, which is difficult to obtain in practice and introduces computational burden.

    “All of the above approaches have in common that a faithful, yet precise enough, abstraction of the physical environment is required, which is not only difficult to obtain in practice, but also introduces the mentioned computa-tional burden.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Interpretationreasoning

    The boundary between the learning agent and the shield provides a basis for the convergence analysis of a shielded RL algorithm.

    “and provides a basis for the convergence analysis of a shielded RL algorithm.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Interpretationnone given

    The assumption that the abstraction automaton has no states in F from which all infinite paths eventually leave F ensures that paths that model traces that cannot occur in M are rejected by the abstraction as early as possible.

    “This ensures that paths that model traces that cannot occur in M are rejected by ϕ M as early as possible.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationreasoning

    As the shield is generated using the specification, it plans ahead for this not to happen, so it must prevent the opening of the inflow valve if the level is above 93.

    “As the shield is generated using the specification, it plans ahead for this not to happen, so it must prevent the opening of the inflow valve if the level is above 93.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Interpretationnone given

    The setup introduces a clear boundary between the learning agent and the shield.

    “Our setup introduces a clear boundary between the learning agent and the shield.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Interpretationreasoning

    Given that the environment is often represented as an MDP, an abstraction of the environment dynamics has to be conservative with respect to the behavior of the real MDP.

    “Given that the environment is often represented as an MDP, such an abstraction has to be conservative w.r.t. the behavior of the real MDP.”
    Quote in the paperNot a substantial claim
    • Rests on an assumption: The environment is often represented as an MDP.

  • May combine two claims.

    Premisenone given

    Control methods based on RL partly address the abstraction problem, but do not typically incorporate any correctness guarantees.

    “Control methods based on RL partly address this problem, but do not typically incorporate any correctness guarantees.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Interpretationreasoning

    Shielding exploits the possibility that safety criteria may be enforced by simple means.

    “Shielding exploits this possibility.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Interpretationreasoning

    Since an unsafe action is always mapped to a safe one, this does not pose a problem and the agent never has to learn to avoid unsafe actions; consequently, the shield is needed during the learning and execution phases.

    “Since an unsafe action is always mapped to a safe one, this does not pose a problem and the agent never has to learn to avoid unsafe actions.Consequently, the shield is (again) needed during the learning and execution phases.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Interpretationown data

    In applications in which safe learning is needed, the effort to construct an abstraction is well-spent, as the approach makes learning safe and shows promise of improving learning performance.

    “Our experiments show, however, that in applications in which safe learning is needed, the effort to construct an abstraction is well-spent, as our approach not only makes learning safe, but also shows great promise of improving learning performance.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Interpretationreasoning

    The agent assigns a punishment r_{t+1} < 0 to a1_t and learns that selecting a1_t at state s_t is unsafe, without ever violating φ_s.

    “The agent assigns a punishment r t+1 < 0 to a 1 t and learns that selecting a 1 t at state s t is unsafe, without ever violating ϕ s .”
    Quote in the paperNot a substantial claim
    • The authors state this as an assumption: The environment can be modeled as an MDP M = (S, s_I, A, P, R).
    • The authors state this as an assumption: We have constructed an abstraction ϕ_M.
    • The authors state this as an assumption: The learner accepts elements from S × Q as state input (for the state space of the shield Q).

  • May combine two claims.

    Interpretationreasoning

    There is no guarantee that unsafe actions are not part of the final policy; therefore, the shield has to remain active even after the learning phase.

    “However, there is no guarantee that unsafe actions are not part of the final policy.Therefore, the shield has to remain active even after the learning phase.”
    Quote in the paperSubstantial claim
31 of 31

  • The authors state this as an assumption.

    The specification ϕ is a set of properties {ϕ1,...,ϕl} such that L(ϕ) is the intersection of the languages of its properties.

    “We assume ϕ is a set of properties {ϕ 1 , . . ., ϕ l } such that L(ϕ) = i L(ϕ i ).”

  • The paper relies on this without support.

    The environment is often represented as an MDP.

    “Given that the environment is often represented as an MDP, such an abstraction has to be conservative w.r.t. the behavior of the real MDP.”

  • The paper relies on this without support.

    Safety or more generally correctness during learning and execution of controllers has attracted significantly less attention than convergence, optimality and data-efficiency of learning algorithms.

    “While convergence, optimality and data-efficiency of learning algorithms are relatively well understood, safety or more generally correctness during learning and execution of controllers has attracted significantly less attention.”

  • The authors state this as an assumption.

    The environment can be modeled as an MDP M = (S, s_I, A, P, R).

    “Assumption 1 (i) The environment can be modeled as an MDP M = (S, s I , A, P, R).”

  • The authors state this as an assumption.

    We have constructed an abstraction ϕ_M.

    “(ii) We have constructed an abstraction ϕ M .”

  • The authors state this as an assumption.

    The learner accepts elements from S × Q as state input (for the state space of the shield Q).

    “(iii) The learner accepts elements from S × Q as state input (for the state space of the shield Q).”

  • The authors state this as an assumption.

    Some abstraction ϕ_M = (Q_M, q_0,M, A × L, δ_M, F_M) of M for some MDP observer function f : S → L is given.

    “We assume some abstraction ϕ M = (Q M , q 0,M , A × L, δ M , F M ) of M for some MDP observer function f : S → L to be given.”

  • The authors state this as an assumption.

    ϕ_s has Σ = L × A, i.e., it reads the part of the system behavior that the abstraction is concerned with.

    “Since ϕ s models a restriction of the traces of the MDP and the learner together that we want to enforce, we assume it to have Σ = L × A, i.e., it reads the part of the system behavior that the abstraction is concerned with.”

  • The authors state this as an assumption.

    A shield S = (Q_S, q_0,S, Σ_I,S, Σ_O,S, δ_S, λ_S) is given for M and for some MDP labeling function f : S → L.

    “Assume also that a shield S = (Q S , q 0,S , Σ I,S , Σ O,S , δ S , λ S ) is given for M and for some MDP labeling function f : S → L.”

  • The authors state this as an assumption.

    Whenever an action ranking is chosen by the learner that does not contain a safe action, there is a fixed probability distribution over the safe actions executed instead, constant over time.

    “Note that this argument requires that whenever an action ranking is chosen by the learner that does not contain a safe action, there is a fixed probability distribution over the safe actions executed instead.”

  • The authors state this as an assumption.

    The learner has access to the state of the shield and can base its actions on it.

    “Note that we made use of the fact that the learner has access to the state of the shield and can base its actions on it in this argument.”
11 of 11

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • SafeCodeRL incorporates a hard shielding mechanism to provide system-level, physically absolute safety guarantees.

    “To provide system-level, physically absolute safety guarantees, SafeCodeRL incorporates a hard shielding mechanism [37].”

    From SafeCodeRL: Security-Constrained Multi-Agent Reinforcement Learning for Trustworthy LLM-Generated IoT/CPS Software (2026) · cites this paper as [37]

    The Abstract and Conclusion describe a shield that corrects actions that would violate a temporal-logic safety specification, supporting the shielding mechanism. The Safety, Abstractions, and Games section says this protection depends on a conservative abstraction of the environment; it does not establish physically absolute safety guarantees for SafeCodeRL. (LLM, conf=0.86)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

Each contradiction between two passages listed here was confirmed by an independent check.

  • Abstraction alphabet order conflicts with its transitions

    Minor

    The abstraction is declared to read action-label pairs, A × L, but the product-game transition supplies it label-action pairs, (l, a). These are different input orders for the same abstraction automaton.

  • Safe specification states are called error states

    Minor

    The game definition includes states in F × Q M among its safe states, but the example says those same states are merged into an error state. Taken literally, that reverses which specification states represent an error in the reported game construction.

2 of 2

Cites

Flagged first, then by citations

Cited by

Sorted by citations

Related

Authors
Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., & Topcu, U.
Affiliations
  • The University of Texas at Austin (US)
  • Graz University of Technology (AT)
  • University of Bremen (DE)
ORCID
Venue
Proceedings of the AAAI Conference on Artificial Intelligence
Publisher
Association for the Advancement of Artificial Intelligence (AAAI)
Published
2018-04-29
Volume
32
Issue
1
ISSN
  • 2159-5399 (ISSN-L)
  • 2374-3468
DOI
10.1609/aaai.v32i1.11797
OpenAlex
W2751422670
Cited by
37
References
19
Citations by year
2026: 1 · 2025: 1 · 2024: 3 · 2023: 7 · 2022: 3 · 2021: 7 · 2020: 7 · 2019: 4 · 2018: 4
FWCI
2.24
Type
conference paper
Language
en
Open access
Locations
  • Proceedings of the AAAI Conference on Artificial Intelligence (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Funders
  • National Science Foundation (1652113, 1617639, 1646522)
  • Austrian Science Fund (S11406-N23, W1255)
  • Universität Bremen
  • Defense Advanced Research Projects Agency (W911NF-16-1-0001, FA8650-15C)
  • Army Research Office (W911NF-15-1-0592, W911NF-15-1-, W911NF-16-1-, W911NF, W911NF-15)
  • Air Force Research Laboratory (FA8650-15-C-2546, FA8650-15-, 8650-16-C-2610)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Reinforcement Learning in Robotics
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
Keywords
safe reinforcement learning, temporal logic specifications, reactive systems, convergence guarantees, policy learning

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Claims read by deepseek-v4.1-flash under definition version 3 (extract-v3) on 2026-10-24.

Classified by jev-1.13-20260917 (gold-guideline-v0.2) on 2026-10-24.

Cited sources are checked by gpt-6-sol.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review