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

The DOI matches its Crossref record; 27 of the 31 references it cites were found in a registry or an index, and 4 are not checked yet; 2 of the 6 sources its claims cite were checked for support.

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

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

Overview

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.

Verification

Claims the paper makes

45 Own interpretation · 10 Own result · 4 No basis given · 1 Partly supported · 1 Not supported · 1 No full text of the sources · 1 Not checked yet · accuracy not yet measured

Show all 32 claims

  • Probably not a substantial claim. 17
  • It may state two separate claims as one. 17
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?

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.

2 of 2

Citations

Cites

Show all 19 references

Cited by

Sorted by citations

Items 401–500 of 700

Metadata

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)
Venue
Proceedings of the AAAI Conference on Artificial Intelligence
Published
2018-04-29
Volume
32
Issue
1
ISSN
  • 2159-5399 (ISSN-L)
  • 2374-3468
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.

A language model drew the claims from the paper on 2026-10-24, under version 3 of the claim definition (model deepseek-v4.1-flash, prompt extract-v3).

A second model labelled each claim on 2026-10-24 (model jev-1.13-20260917, definition revision gold-guideline-v0.2).

Cited sources are checked with a language model’s help (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