Conceptio › Archive › arXiv CS

arXiv CSopen access

Shields to Guarantee Probabilistic Safety in MDPs

2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

Open Source ↗Direct PDF ↓

knowledge-representation reasoning

artificial intelligence, reasoning, knowledge representation

Shields to Guarantee Probabilistic Safety in MDPs

arXiv:2605.10888v1 [cs.LO] 11 May 2026

Linus Heck1 , Filip Macák2 , Roman Andriushchenko2 , Milan Češka2 , and Sebastian Junges1 Radboud University, Nijmegen, the Netherlands {linus.heck,sebastian.junges}@ru.nl Brno University of Technology, Czechia {iandri,ceskam,imacak}@fit.vut.cz

Abstract. Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that nothing bad ever happens and comes with strong guarantees about safety and maximal permissiveness. However, shielding systems for probabilistic safety, where something bad is allowed to happen with an acceptable probability, has proven to be more intricate. This paper presents a formal framework that conservatively extends classical shields to probabilistic safety. In this framework, we (i) demonstrate the impossibility of preserving the strong guarantees on safety and permissiveness, (ii) provide natural shields with weaker guarantees, and (iii) introduce offline and online shield constructions ensuring strong safety guarantees. The empirical evaluation highlights the practical advantages of the new shields, as well as their computational feasibility.

Introduction

Markov decision processes (MDPs) are ubiquitous models to describe sequential decision making under uncertainty. In any state, a (non-deterministic) action choice yields a distribution over the successor states. Agents (or policies) select these actions and thus resolve the nondeterminism. Reinforcement learning (RL) and online planning methods generate agents, often by iteratively interacting with the environment. A key concern preventing adoption in various domains is the lack of clear safety guarantees about the agents. Among the various research directions that aim to make RL safe [17, 29], runtime enforcement, in particular shielding [1], has become popular: A shield uses knowledge about the underlying model to enforce that an agent’s decisions are safe (within the assumed model); operationally, this is done by blocking or overruling any unsafe actions that an agent wants to take. Shielding is policy-agnostic, in contrast to (standard) policy synthesis or methods that train a policy and a certificate [4]. Shields (and safety masking [39] and supervisory control theory [20]) were developed for non-stochastic settings and/or absolute safety guarantees [1]: A shield should guarantee that a bad state is never reached. In many scenarios, however, absolute safety is not attainable, and therefore shields for probabilistic safety have been developed [22]. A natural statement for probabilistic shielding is

L. Heck et al.

0.1 α s0

γ 0.9 s1

0.9 δ

1/2

0.1

1 0.1

0.9

Fig. 1. MDP from [26]

ε 1/2

α β

γ s2

Fig. 2. MDP for Theorem 3

that a shield should guarantee that a bad state is reached with probability at most λ; however, standard probabilistic shields do not provide this guarantee [26]. This paper contributes a framework for shielding with various concrete instantiations that do provide probabilistic safety guarantees. As such, the paper is orthogonal to the vast literature on shielding that provides shields for continuous [24, 42], partially observable [8, 11, 36], or multi-agent settings [7, 15], that addresses the construction of shields in model-free settings [9, 37, 41], or other concerns [35]. Classical shields: Local and minimal interference for global safety. Classical shields are safe: They ensure that a bad state is globally not reached, whenever the system starts in a safe state. Operationally, classical (post-)shields take the system state and the action selected by the agent, and return an action; if the action is the one picked by the agent, it allows the action, otherwise, it blocks it. Classical shields allow any action where the system transitions to safe states. Indeed, this simple local mechanism guarantees global safety. Classical shields are also maximally permissive (aka minimally interfering): If an agent already satisfies the (qualitative!) safety specification, the shield never blocks its actions. δ-shields: practical probabilistic shielding. Classical shields block each action that (later) leads to a bad state with any positive, potentially tiny, probability. Despite the maximal permissiveness, it may thus block most actions. Probabilistic δ-shields [22] take a practical approach to overcome this weakness: In state s, they block any action where the probability to reach the bad state from s increases by more than factor δ. While this yields more permissive shields, the locally operating δ-shields and variants thereof do not guarantee any safety. Consider Fig. 1 and a safety specification where bad states are reached with probability ≤0.1. A δ-shield (with nontrivial δ) allows α in s0 and γ in s1 ; however, a policy taking both actions reaches the bad state with probability >0.1. Novel framework for shields. Thus: What are safe and permissive shields for probabilistic safety? Fig. 1 demonstrates that such shields can be complex objects: Assume we must reach bad states with probability ≤0.1. When reaching s1 , it is only safe to allow γ if previously action β was taken: Whether an action can be allowed depends on the history, even though classical and δ-shields are memoryless. Further, many policies in RL are stochastic and they can be history-dependent. We provide a generic framework for history-dependent shields shielding arbitrary policies. The framework covers the classical and δ-shields and novel shields introduced in this paper, see Tab. 1 for an overview.

Shields to Guarantee Probabilistic Safety in MDPs

Shield

Guarantees Notes Safety Perm.

old

Classical [1] δ-shield [22]

(S+) No

new!

Table 1. Shields in this paper. (S+): strong safety, (S−): weak safety, (P+): strong permissiveness, (P−): weak perm., (P*): saturated perm.; ∗ converges toward (P*)

Optimistic (Def. 9) (S−) (P+) Extends classical shield, limited safety Pessimistic (Def. 10) (S+) (P−) Extends classical shield, still overly conservative Saturated (Section 5) (S+) (P*) Maximal element of the safe shields, no algorithm Offline/Online (Def. 15) (S+) No∗ Shields given log file and/or incrementally Memoryless (Def. 16) (S+) No∗ Offline, favors generalizing smaller logs

No No

(P+) in qualitative case, overly conservative Shields heuristically; hard to tune hyperparameter

No maximally permissive safe shields. None of the shields for probabilistic safety are maximally permissive and safe: Using the framework, we prove with a surprisingly simple proof (Theorem 3), that no such shield exists. Consider an MDP in Fig. 2. The safety specification is that bad states are reached with probability at most 0.5. In particular, consider that if we reach s1 (via a unique path), should we block β? If not, then a policy that picks β in s1 and δ in s2 reaches the bad state with probability one. We then must block β to be safe, thereby interfering with the safe policy taking action β and γ, respectively. Optimistic and pessimistic shields. The overarching challenge in providing safe and permissive shields is that probabilistic safety makes statements about the computation tree, whereas shields observe only one path in that tree. A shield must therefore make assumptions about what happens elsewhere in the tree. We introduce pessimistic shields, which assume a worst-case policy in terms of safety. They track how much the shielded policy exceeds that assumption along the observed path. Once enough safe actions are taken, it can permit unsafe actions. Dually, an optimistic shield takes a best-case baseline policy and tracks how much risk was taken violating the best-case assumption. Once this risk exceeds the threshold, only the safest actions are allowed. Both shields can be computed tractably and come with clear albeit weak guarantees. Empirically, pessimistic shields permit the same actions as classical shields, while optimistic shields block only a few (clearly dangerous) actions. Saturated permissiveness. Towards less pessimistic but safe shielding, we introduce saturated permissiveness. It is a guarantee rooted in comparing shields based on the set of policies they allow to be executed unchanged. Consider Fig. 2: a safe shield can allow either the policy picking β or the policy picking δ. Once the shield chooses to allow one of these policies, no additional policies can be allowed without violating the safety guarantee. The shield is saturated, in the sense that we have reached a maximal element in the lattice of safe shields. There are generally many saturated shields in any MDP, all more permissive than the pessimistic shield, while providing the same safety guarantee. Offline and online shield construction. We develop an incremental approach that builds shields based on history-action pairs, obtained, e.g., from a log file. These safe shields become increasingly permissive and converge to saturated permissiveness. Beyond this offline construction of shields, we demonstrate an online

L. Heck et al.

construction that interleaves the safe, shielded execution with the incremental extension of the shields. Empirically, these shields are indeed permissive while also guaranteed to be safe. The main weakness is that constructing permissive shields can require large sets of history-action pairs. We investigate constructing shields that generalize by ignoring parts of the history: In the paper, we consider memoryless shields, which also provide a connection to the memoryless permissive policies from the literature [13, 14, 23]. Contributions. In summary, this paper contributes: (1) A generic framework for shielding in MDPs. Within the framework, we prove the impossibility of combining maximal permissiveness and probabilistic safety and instantiate various shields, such as the intuitive optimistic and pessimistic shields. (2) Saturated safe shields, which combine safety and a saturated permissiveness, a natural variant of maximal permissiveness. We pair these shields with online and offline learning routines. (3) Experiments for all new shields and a comparison with the baseline shields that demonstrate the relative strengths and weaknesses of these shields. In particular, the incremental online construction provides shields that are guaranteed to be safe and significantly more permissive than the alternatives. We prove all theorems and lemmas stated without proof in Appendix A.

Preliminaries

For any function f : A → B and a set X ⊆ A, we write f (X) := {f (x) P| x ∈ X}. A distribution over a countable set A is a function d : A → [0, 1] s.t. a d(a)=1. Supp(d) = {a ∈ A | d(a) > 0} is the support of d. The set ∆(A) contains all distributions over A. For a ∈ A, let 1a := {a 7→ 1} denote the Dirac distribution. Given a distribution d and a set X with X ∩ Supp(d) ̸= ∅, we define d|X using a suitable normalization constant α s.t. d|X (x) = 0 if x ̸∈ X and d|X (x) = α · d(x) otherwise. If X ∩ Supp(d) = ∅, d|X is the uniform distribution over X. Markov decision processes. A Markov decision process (MDP) is a tuple M = (S, s0 , Act, P) with a finite set S of states, an initial state s0 ∈ S, a finite (indexed) set Act of actions, and a partial transition function P : S × Act ↛ ∆(S). For an MDP M, we define the available actions in s ∈ S as Act(s). An MDP M with |Act(s)| = 1 for each s ∈ S is a Markov chain (MC) M = (S, s0 , P). A finite path is denoted τ = s0 α1 s1 · · · st for si ∈ S, αi ∈ Act(si−1 ). The set of (finite) paths is denoted Paths(M) and FinPaths(M). We consider stochastic policies: A policy is a function π : FinPaths(M) → ∆(Act) with Supp(π(τ )) ⊆ Act(s) for all τ ∈ FinPaths(M) and with s the last state in τ . For an MDP M, ΠM denotes the set of policies in M. A policy π ∈ ΠM induces the (infinite) MC Mπ [3, p. 843]. Specifications and values. We consider a (quantitative) safety specification given as an indefinite-horizon reachability property. For simplicity, we formalize our approach only for the safety specification given as φ = PrM (s0 ⊨ ⋄ ) ≤ ν, where ⊆ S denotes a set of bad states, ν ∈ Q, and PrM (s ⊨ ⋄ ) denotes the probability of reaching (some state in) from s in M. We call ν the safety threshold. For MDP M and every state s ∈ S, we define the minimal value

Shields to Guarantee Probabilistic Safety in MDPs

as Vmin (s) := inf π∈ΠM PrMπ (s ⊨ ⋄ ). Similarly, we define the maximal value Vmax (s) := supπ∈ΠM PrMπ (s ⊨ ⋄ ). Safe actions and policies. We call a policy π safe w.r.t. an MDP M φ if φ holds on Mπ . Let Safe(ΠM ) := {π ∈ ΠM | π safe} be the set of safe policies. For the rest of the paper, we assume that Vmin (s0 ) ≤ ν, i.e., at least one safe policy exists. A policy π is safety-optimal if PrMπ (s ⊨ ⋄ ) = Vmin (s) for all s ∈ S. Safety-optimal policies always exist. The set of safe actions ActSafe (s) for P state s are those actions that do not change Vmin : ActSafe (s) := ′ {α ∈ Act(s) | s′ ∈SPP(s, α, s′ ) · VP min (s ) = Vmin (s)}. For dir ∈ {min, max}, we define Qdir (s, d) := α∈Act d(α) · s′ ∈S P(s, α, s′ ) · Vdir (s′ ).

Shields for Probabilistic Safety

We provide a general notion of shields. First, histories are annotated paths: Definition 1 (History). A history is a sequence h := s0 d1 α1 s1 d2 α2 · · · st such that s0 α1 s1 α2 · · · st is a path, and for all 0 ≤ k < t: dk+1 ∈ ∆(Act(sk )). We write Hist(M) as the set of histories. Histories extend paths with distributions over actions di ∈ ∆(Act), which we call choices. Intuitively, these represent a choice made by the policy of some agent at each step. Including these distributions becomes relevant when considering choices made by stochastic policies. On the other hand, for deterministic policies, the additional information in a history can be derived directly from the path. We define some operations on histories: Definition 2 (History Operations). Given a history h = s0 d1 α1 s1 · · · st , – last(h) := st is the last state of the history, – path(h) := s0 α1 s1 · · · st is the path of the history, – choice(h, k) := dk is the k-th history choice for 1 ≤ k ≤ t, – h|k := s0 d1 α1 · · · sk is the history prefix up to step k for 0 ≤ k ≤ t. History h is consistent with policy π if for all k: choice(h, k) = π(path(h|k−1 )). 3.1

Shields

An agent interacts with the environment and selects actions according to a policy. Shields can intervene in this loop, mapping the agent’s choice to a potentially different choice that will be executed in the environment. Formally, they map a history and a choice to another choice. Definition 3 (Shield). A shield is a function

: Hist(M)×∆(Act) → ∆(Act).

Crucially, shields are independent of the policy played. The shields in [1, 22, 27, 29, 42] satisfy Def. 3. Our definition is a conservative stochastic extension of both shielding in deterministic systems and shielding deterministic policies. We give examples of shields that, intuitively, aim to minimize the probability of eventually reaching at each state s.

L. Heck et al.

Example 1. The shield Safe (a conservative stochastic extension of [1]) is given by Safe (h, d) := d|ActSafe (last(h)) . This shield maps to choices over safe actions. Example 2. Given some δ ∈ [0, 1], a (multiplicative) δ-shield δ [22] is given by ( d if Qmin (last(h), d) · δ ≤ Vmin (s), δ (h, d) = d|ActSafe (last(h)) otherwise. In the experiments, we also use the following additive δ-shield: ( d if Qmin (last(h), d) − δ ≤ Vmin (s), δ + (h, d) = d|ActSafe (last(h)) otherwise. Example 3. The following shield for the MDP in Fig. 1 is history-dependent: (h, d) := 1δ if last(h) = s1 and choice(h, 1)(α) > 0,

(h, d) := d otherwise.

Pre-Shields. Our shields are post-shields, where the policy’s choice is transformed. In pre-shielding [25], the shield instead presents a set of possible choices to the policy as an input. Formally, pre-shields are functions pre : Hist(M) → 2∆(Act) . Given a post-shield post , one can define the pre-shield: pre (h) := {d ∈ ∆(Act) |

post (h, d) = d}.

To create a post-shield from a pre-shield, one needs to replace the disallowed choices with a safe choice. We pick the projection to the safe actions [29]. Thus: post (h, d) := d if d ∈

pre (h),

and d|ActSafe (last(h)) otherwise.

Permissive Controllers. Pre-shields with additional constraints can be seen as permissive controllers as in [13, 14, 23]. We discuss a connection to such (memoryless) permissive controllers in Section 7. 3.2

Shields as Policy Transformers

Shields modify policy choices, thus they naturally induce policy transformers: Definition 4 (Policy Transformer of a Shield). Given a shield transformer is the function T : ΠM → ΠM defined recursively by

, its policy

T (π)(s0 α1 s1 · · · αt st ) := (ht , π(s0 α1 s1 · · · αt st )), where ht := s0 T (π)(s0 ) α1 s1 T (π)(s0 α1 s1 ) α2 · · · αt st . Example 4. Reconsider the shield from Example 3. Given a policy π ∈ ΠM , if π(s0 )(α) = 0, we have T (π) = π. Otherwise, we have T (π) = π ′ , where π ′ (s0 αs1 ) = π ′ (s0 βs1 ) = 1δ and π ′ (τ ) = π(τ ) for all other finite paths τ .

Shields to Guarantee Probabilistic Safety in MDPs

At each step, the policy transformer uses the previous shielding decisions to construct a history to give to the shield. allows a policy π if T (π) = π. We write Definition 5 (Allow). A shield Allow( ) = {π ∈ ΠM | T (π) = π} as the set of allowed policies of . Note that Allow( ) ⊆ T (ΠM ) := {T (π) | π ∈ ΠM }, i.e., the set of allowed policies is a subset of the policy transformer’s image. Allowed sets exhibit relevant properties: Intuitively, if a shield allows two policies, it must act like either policy on all histories. We call this history mixing. Definition 6 (History Mixing). Given a set of policies P ⊆ ΠM , the history mixing is the set mix (P ) ⊆ ΠM such that π ∈ mix (P ) if: ∀h ∈ Hist(M). h is consistent with π =⇒ (∃π ′ ∈ P. h is consistent with π ′ ). Example 5. Consider the MDP in Fig. 2 and suppose that P contains policy π1 with π1 (s0 εs1 ) = 1β and another policy π2 with π2 (s0 εs2 ) = 1δ . Then mix (P ) contains a policy π3 with π3 (s0 εs1 ) = 1β and π3 (s0 εs2 ) = 1δ . Lemma 1. Given shield

and policies P ⊆ Allow( ). Then mix (P ) ⊆ Allow( ).

Lemma 1 implies that the allow sets of shields are mix -closed. Shields are not uniquely characterised by their allow sets, i.e., two different shields may have the same allow set. In what follows, it is helpful to ensure that an allow set uniquely identifies a shield. To this end, we restrict ourselves to canonical shields. Definition 7 (Canonical Shield). A shield is canonical if (1) for all h ∈ Hist(M), d ∈ ∆(Act): (h, d) ∈ {d, d|ActSafe (last(h)) }, and (2) for all h not consistent with a policy in Allow( ), (h, d) = d|ActSafe (last(h)) . Thus, (1) if a canonical shield transforms a choice, it uses action projection to the safe actions. Moreover, (2) only reachable histories under the allow set are relevant. The canonical shields have a one-to-one correspondence with sets of policies that are closed under allowing the safe actions. Theorem 1. Let P be a mix-closed set of policies such that for any history h that is consistent with some policy in P and any d ∈ ∆(ActSafe (last(h))), there exists a policy π ∈ P such that h is consistent with π and π(path(h)) = d. There is a unique canonical shield with Allow( ) = P . Theorem 1 says that a canonical shield can be thought of as a mix -closed set of allowed policies. This lifts the local shielding mechanism to the exact set of allowed policies, which will be useful when investigating the properties of shields.

Shields with Strong and Weak Guarantees

We formalize safety and permissiveness guarantees, show that satisfying both is not possible in the probabilistic case, and introduce weaker guarantees.

4.1

L. Heck et al.

Strong Guarantees

Intuitively, shields should ensure safety while allowing as many policies as possible. Thus, we consider safety and permissiveness guarantees. Let M be an MDP and a shield. (S+): Strong Safety. T (ΠM ) ⊆ Safe(ΠM ). (P+): Strong Permissiveness. Safe(ΠM ) ⊆ Allow( ). We call a shield safe if it satisfies (S+) and permissive if it satisfies (P+). These guarantees are introduced in [1] as correctness and minimum interference. (S+) ensures that the shield transforms every policy into a safe policy. (P+) ensures that every safe policy is allowed by the shield. Theorem 2 ([1]). For safety threshold ν = 0 (i.e., for a qualitative specification), the shield Safe (Ex. 1) satisfies (S+) and (P+). Theorem 3. For a safety threshold 0 < ν < 1, there is an (acyclic, 5-state) MDP such that no shield satisfies (S+) and (P+). Proof (sketch). Consider the MDP M in Fig. 2. For conciseness, we assume ν = 0.5. A full proof is given in App. A.2. Suppose the shield satisfies (S+) and (P+). Consider the unsafe policy π = {s0 7→ 1ε , s0 εs1 7→ 1β , s0 εs2 7→ 1δ }. We have two cases: (1) Suppose that T (π)(s0 εs1 ) ̸= π(s0 εs1 ). Then, for safe π ′ = {s0 7→ 1ε , s0 εs1 7→ 1β , s0 εs2 7→ 1γ }, we have T (π ′ ) ̸= π ′ , meaning the shield violates (P+). (2) Suppose that T (π)(s0 εs1 ) = π(s0 εs1 ) = 1β . Then it must hold that T (π)(s0 εs2 ) ̸= 1δ since satisfies (S+). However, for the safe policy π ′ = {s0 7→ 1ε , s0 εs1 7→ 1α , s0 εs2 7→ 1δ }, we have T (π ′ ) ̸= π ′ , i.e., the shield violates (P+). Intuitively, the behavior of a shield satisfying (S+) and (P+) depends on the policy’s decision on paths that were never visited in the current execution, as these guarantees take the entire computation tree into account. 4.2

Optimistic and Pessimistic Shields

Given the impossibility of combining the strong guarantees in the probabilistic setting, we describe two natural shields, each combining one strong guarantee on safety or permissiveness with a weak guarantee on permissiveness or safety. We construct an optimistic shield and a pessimistic shield. Intuitively, both shields assume a bound on the safety of the alternative paths that are not part of the current execution. The difference is that the optimistic shield acts as if it had taken the safest possible actions in those paths, whereas the pessimistic shield acts as if it had taken the most unsafe possible actions. To define these shields, we introduce the notions of incurred risk and safety. Incurred risk quantifies how much riskier the policy played compared to a safetyoptimal policy. Dually, incurred safety quantifies how much safer the policy played compared to a policy that is maximally unsafe. For a history h, let Pr(h) denote the probability of the path path(h) occurring in M given the choices taken in h.

Shields to Guarantee Probabilistic Safety in MDPs

Definition 8 (Incurred Risk and Safety). Given a history h = s0 d1 α1 s1 · · · st and a choice dt+1 ∈ ∆(Act), the incurred risk and incurred safety are: irisk (h, dt+1 ) :=

Pr(h|k ) (Qmin (sk , dk+1 ) − Vmin (sk )) ,

0≤k≤t

isafety(h, dt+1 ) :=

Pr(h|k ) (Vmax (sk ) − Qmax (sk , dk+1 )) ,

0≤k≤t

Definition 9 (Optimistic Shield). Let safety threshold ν ∈ [0, 1] and bmin = ν − Vmin (s0 ). Note that 0 ≤ bmin ≤ 1 because Vmin (s0 ) ≤ ν. The optimistic shield is given by ( d if irisk (h, d) ≤ bmin , opt (h, d) = d|ActSafe (last(h)) otherwise. Definition 10 (Pessimistic Shield). Let safety threshold ν ∈ [0, 1] and bmax = Vmax (s0 ) − ν. Note that −1 ≤ bmax ≤ 1. The pessimistic shield is given by ( d if isafety(h, d) ≥ bmax , pess (h, d) = d|ActSafe (last(h)) otherwise. Intuitively, the optimistic shield considers the policy “innocent” at first, mapping to the proposed choice until the policy is proven “proven guilty” as soon as the risk rises above the threshold. Conversely, the pessimistic shield starts out by considering the policy “guilty” until it is “proven innocent” as soon as the safety rises above the threshold, after which it starts mapping to the proposed choice. For conciseness, the presented definitions of these shields do not satisfy the second condition of canonicity (Def. 7), we give the full definition in App. A.3. Example 6. Consider the MDP M in Fig. 1. For states (s0 , s1 , s2 ), we have Vmin (M) = (0.1, 0.1, 0.1) and Vmax (M) = (0.271, 0.19, 0.1). Let φ = Pr(s0 ⊨ ⋄ ) ≤ 0.2. Suppose the policy plays π(s0 ) = {α 7→ 0.5, β 7→ 0.5}. For the optimistic shield, we have bmin = 0.2−0.1 = 0.1. The incurred risk is irisk (s0 , π(s0 )) = (0.5·(0.1·1+0.9·0.1)+0.5·1·0.1)−0.1 = 0.045. As 0.045 ≤ bmin , the policy is allowed to play this choice. For the pessimistic shield, we have bmax = 0.271 − 0.2 = 0.071. The incurred safety is: isafety(s0 , π(s0 )) = 0.271 − (0.5 · (0.1 · 1 + 0.9 · 0.19) + 0.5 · 1 · 0.19) = 0.0405. As 0.0405 < bmax , the policy is not allowed to play this choice. The pessimistic and optimistic shields are a conservative extension of the shield from Example 1: Lemma 2. Allow( pess = Safe .

Safe ) ⊆ Allow(

pess ) ⊆ Allow(

opt ). If ν = 0, then

Lemma 3. Given Vmin (resp. Vmax ), the computation time for pess (h, d)) is in O(|h| · |Act| · |S|).

opt =

opt (h, d) (resp.

L. Heck et al. Actions

0.5

Allowed if shield has

s0 s1 s2 Safe? (S+) (S−) (P+) (P−) s1

0.5

0.8 0.2 s0

π1 π2 π3 π4

✓ ✓ ✗ ✗

? ? ✗ ✗

? ? ? ✗

✓ ✓ ? ?

? ✓ ? ?

Fig. 3. A navigation environment MDP Fig. 4. Guarantees on environment policies

4.3

Weak Guarantees

The optimistic and pessimistic shields satisfy a weaker set of guarantees: Let M be an MDP and a shield. Property X is satisfied, if for all π ∈ ΠM and for all τ ∈ FinPaths(M): (S−): Weak Safety. There is a safe policy πsafe with πsafe (τ ′ ) = T (π)(τ ′ ) for all prefixes τ ′ of τ . (P−): Weak Permissiveness. If T (π)(τ ) ̸= π(τ ), then there is an unsafe policy πunsafe with πunsafe (τ ′ ) = π(τ ′ ) for all prefixes τ ′ of τ . Lemma 4. (S+) implies (S−) and (P+) implies (P−). Theorem 4. The optimistic shield satisfies (S−) and (P+). The pessimistic shield satisfies (S+) and (P−). If the observed choices are not consistent with any safe policy, (S−) prevents the shield from allowing the proposed choice. This is treating the policy “innocent until proven guilty”: As long as the policy might be safe, the shield can allow it. Conversely, (P−) only permits blocking the policy if the current choices are consistent with some unsafe policy. This is treating the policy “guilty until proven innocent”: As long as the policy might be unsafe, the shield can transform it. Example 7. Consider the MDP in Fig. 3 with actions { , , } and ν = 0.5. Fig. 4 compares the guarantees of four memoryless policies: ✓ denotes that the policy is always allowed by a shield satisfying that guarantee, ✗ denotes that it is never allowed, and ? denotes that some shields with that guarantee allow that policy and some do not. We exemplify a shield satisfying (P−): If the agent plays as π1 at s0 , the unsafe policy π3 is consistent with π1 on the observed histories, so the shield may transform the choice. If the agent plays as π2 , no observed history is consistent with any unsafe policy, so the shield may not transform it. Lemma 5. For 0 < δ,ν < 1, there is an MDP such that the δ-shield does not satisfy (S−) (resp. (P−)).

Saturated Safe Shields

We introduce safe shields that are more permissive than the pessimistic shield.

Shields to Guarantee Probabilistic Safety in MDPs

Example 8. Consider the MDP from Fig. 2. The pessimistic shield does not allow anything other than safe actions, as it assumes the worst-case behavior towards at the other state; allowing anything else would lead to unsafe behavior. However, it is safe to allow a policy to take an unsafe action at either s1 or s2 . Such a shield allows additional policies and is safe. We introduce saturated permissiveness, which states that a given shield cannot allow more policies without becoming unsafe: Guarantee (P*): Saturated Permissiveness. For all π ∈ ΠM \ Allow( ), there is no safe shield ′ such that Allow( ) ∪ {π} ⊆ Allow( ′ ). We call a shield saturated if it satisfies (S+) and (P*). Remark 1. (P*) implies (P−). Example 9. Consider the MDP M in Fig. 2 and ν = 0.5. For every p ∈ [0, 1], the following shield is saturated: ( d if (last(h) = s1 and d(β) ≤ p) or (last(h) = s2 and d(γ) ≤ (1 − p)), (h, d) := d|ActSafe (last(h)) otherwise. Allow sets of distinct canonical saturated shields are incomparable. Saturated shields allow a convex set of choices at each state. Lemma 6. For all saturated shields {d ∈ ∆(Act) | (h, d) = d} is convex.

and histories h ∈ Hist(M), the set

In contrast to shields satisfying (S+) and (P+), saturated shields always exist: Theorem 5. The axiom of choice implies that for any MDP and any ν ∈ [0, 1], a saturated shield exists. Lemma 7. For acyclic MDPs, Theorem 5 is true independent of the axiom of choice. The challenge in showing Theorem 5 is that the set of finite paths and the set of choices are infinite, yielding an infinite number of policies.

Constructed Shields

Shielding safely without being overly conservative requires deciding which choices to allow. Suppose that we have a sequence of history-choice pairs J, e.g., from execution logs. The goal is to obtain a shield that (1) is safe, (2) does not transform the choice for as many history-choice pairs in J as possible, and (3) is efficiently constructed. To do this, we construct a shield by iteratively adding history-choice pairs while ensuring that that the resulting shield is still safe.

L. Heck et al.

...

saturated shields (antichain) ∗ ...

pess

Safe

opt

∗

...

′ 1 ◦

′ 2 ◦

∗ δ

′ 3

safe shields

permissive shields

...

Fig. 5. Illustration of the lattice of shields. Here, X → Y means Allow(X) ⊆ Allow(Y ).

Example 10. Consider the MDP in Fig. 2 and the safety threshold ν = 0.5. We start from a conservative shield 0 that only allows optimally safe policies. Let J = ((s0 1ε εs1 , 1β ), (s0 1ε εs2 , 1δ ), . . .). We add (s0 1ε εs1 , 1β ) to 0 . We obtain a safe shield 1 with 1 (s0 1ε εs1 , 1β ) = 1β . Now, we add the second history-choice pair to 1 . The resulting shield is unsafe, as it allows going to with probability one. Thus, we would continue with 1 .

6.1

A Lattice Of Shields

We order (canonical) shields by permissiveness. Canonical shields form a lattice by the sets of their allowed policies. Let CShields be the set of canonical shields. Definition 11 (Lattice of Canonical Shields). We define the lattice of canonical shields L := (CShields, ⊑) using ⊑ ′ iff Allow( ) ⊆ Allow( ′ ). We characterize the lattice’s join and meet operations: Theorem 6. L = (CShields, ⊑) is a complete lattice, where for ( ⊔

′

)(h, d) = d iff

(h, d) = d or

′

( ⊓

′

)(h, d) = d iff

(h, d) = d and

′

∈ L:

(h, d) = d, ′

(h, d) = d.

Lemma 8. The supremum (resp. infimum) of L = (CShields, ⊑) is: G

L =

id ,

L =

Safe .

We illustrate this lattice in Fig. 5. In this lattice, the set of saturated canonical shields is an antichain. Let SatShields be the set of saturated shields. Theorem 7. We have

pess ⊑

SatShields and

Conjecture 1. We have

pess =

SatShields.

opt =

SatShields.

Shields to Guarantee Probabilistic Safety in MDPs

6.2

Offline Shielding

As motivated at the start of the section, our goal is to build a safe shield that allows as many of the given history-choice pairs as possible. The join operation from Theorem 6 gives us a principled way to combine shields. A natural strategy is thus to define minimal shields allowing only one history-choice pair and compose them with the lattice joins. Our minimal building blocks are the point shields. They allow only one history-choice pair, together with the choices along the history, to ensure that this pair is reached. Definition 12 (Point Shield). Given (h, d) ∈ Hist(M) × ∆(Act), the point shield on (h, d) is the following canonical shield: ( d′ if h′ d′ is a prefix of hd or h′ d′ = hd, ′ ′ := (h , d ) (h,d) d′ |ActSafe (last(h′ )) otherwise. Example 11. Consider the point shield indeed have 1 (s0 1ε εs1 , 1β ) = 1β .

1 =

(s0 1ε εs1 ,1β ) (Example 10). We

Because safety is not preserved under joins, we check (S+) after each join operation. To verify safety of the resulting shield, we compute the (safety) value of the resulting shield. Definition 13 (Value of Shield). Given a finite set of history-choice pairs F J ⊆ Hist(M) × ∆(Act), let = (h,d)∈J (h,d) . We define the value V (ĥ) of for history ĥ ∈ Hist(M) as: V (ĥ) := max {C (ĥ, d) | (ĥ, d) ∈ J ′ } ∪ {Vmin (last(ĥ))}, where J ′ := J ∪ {(h′ , d′ ) | (h, d) ∈ J, h′ d′ is a prefix of hd} and X X d(α) P(last(h), α, s′ ) · V (h · d · α · s′ ). C (h, d) := α∈Supp(d)

s′ ∈S

Def. 13 is essentially computing the value of the worst-case allowed policy using a Bellman operator. The set J ′ extends J with the prefixes. Then, V maximizes over the available choices, while C defines the probability after taking a choice. Note that the definition of V (ĥ) is recursive, but well-defined: As J ′ is finite and the definition recursively invokes V only on strictly larger histories, the set that is being maximized over will eventually only contain Vmin (last(ĥ)). F Lemma 9. = (h,d)∈J (h,d) is safe if and only if V (s0 ) ≤ ν. Example 12. Consider the shield ′ = (s0 1ε εs1 ,1β ) ⊔ (s0 1ε εs2 ,1δ ) (Example 10). This shield allows policies taking 1β at s1 and 1δ at s2 , so the worst-case probability to reach is one. Indeed, we have V ′ (s0 ) = 1. We allow an additional history-distribution pair only if the resulting shield is strongly safe, which we formalize as the safe extension operator.

L. Heck et al.

Definition 14 (Safe Extension). Let , ′ ∈ L . Then the safe extension of by ′ is the following (non-commutative and non-associative!) operation: ( ⊔ ′ if ⊔ ′ is safe, ′ := ⊕safe otherwise. We construct a shield by iteratively applying the safe extension. Definition 15 (Constructing Shields). Given a sequence of history-choice pairs J = ((h0 , d0 ), . . . , (ht , dt )), and the shield Safe from Example 1, we set: 0 :=

Safe ,

i+1 :=

i ⊕safe

(hi ,di ) .

All shields in this sequence are safe. Reconsider Fig. 5. We illustrate the constructed shields in the upper part of the set of safe shields. We converge towards a saturated shield ∗ in the limit, but possibly not in finite time. Formally, for all history-choice pairs involved in the construction of n+1 , the shield n+1 makes the same allow and block decisions as ∗ . Theorem 8. Given a sequence of history-choice pairs J = ((h0 , d0 ), . . . , (ht , dt )), let t+1 be the shield from Def. 15. There exists a saturated shield ∗ such that for all 0 ≤ i ≤ t: t+1 (ht , dt ) = ∗ (ht , dt ). Remark 2. Additionally, closing the allowed distributions under convex combination in Def. 14 will still yield safe shields that satisfy Theorem 8. This is a consequence of Lemma 6. The safe extension operator from Def. 14 is neither commutative nor associative. Therefore, constructed shields strongly depend on the order in which point shields are added. Adding less useful choices early may prevent us from adding useful ones later. Filtering which choices to add early by prepending another shield can, therefore, be beneficial. This is illustrated at the bottom of Fig. 5. F Lemma 10. Given a constructed shield = (h,d)∈J (h,d) for a finite J, (h, d) can be computed in time O(|h| · |J| · |Act|), while V (s0 ) can be computed in time O(|J| · L · |Act| · |S|), where L is the length of the longest history in J. 6.3

Online Shielding

We ask a simple question: Can we collect history-choice pairs from a policy while shielding? A shield doing this prefers allowing actions that the agent is currently playing, which yields an empirically more permissive shield. We partition the interaction with the MDP into episodes, which start at the initial state. Suppose that we are in episode e = (h0 , d0 ) · · · (hj , dj ), where dj is the choice that is currently proposed by the policy, and each hj extends hj−1 by one step. An intuitive idea would be to immediately allow the choice if it can be included in the safe shield . To do this, we compute the shield ′ := ⊕safe (hj ,dj ) , switch to this shield “on-the-fly”, and execute the choice

Shields to Guarantee Probabilistic Safety in MDPs

′

(hj , dj ). However, even though ′ is a safe shield, this may allow unsafe policies! Formally, a policy transformer that updates the shield along a path—in contrast to Def. 4—does not guarantee a safe policy. Theorem 9. Let be a safe shield constructed using Def. 15. The policy transformer T ′ as defined below, allows unsafe policies: T ′ (π)(s0 α1 s1 · · · αt st ) :=

t+1 (ht , dt ), where ht := s0 T ′ 1 (π)(s0 ) α1 s1 T ′ 2 (π)(s0 α1 s1 ) α2

dt := π(s0 α1 s1 · · · αt st ), and 0 := , t+1 := t ⊕safe

· · · αt st ,

(ht ,dt ) .

Instead, to guarantee safe behavior, we have to keep a shield fixed for the entire episode, using the policy transformer from Def. 4. After an episode finishes, we can update the shield with the collected history-choice pairs. This delayed extension of the shield allows us to collect history-choice pairs while safely shielding over multiple episodes. Lemma 11. Shielding an episode with any fixed constructed shield is safe.

Memoryless Shields

We explore constructing shields that do not depend on the (full) history. This has two advantages: The construction of offline/online shields generalizes faster as we decide to allow an action at a state independently of the history. Additionally, the shields can be stored more compactly. We define a memoryless shield: Definition 16 (Memoryless Shield). function S × ∆(Act) → ∆(Act).

A memoryless (ML) shield

is a

Memoryless shields are similar to permissive policies [13,14,23]. For deterministic policies, a memoryless pre-shield is essentially the same mathematical object as a permissive policy. For stochastic policies, notions diverge: A memoryless preshield is a function S → 2∆(Act) , as is the notion of permissive policy used by [23]. In contrast, [14] define a stochastic permissive policy as a function S → ∆(2Act ). A key difference is that the permissive policy synthesis literature considers an NPhard problem to find such policies based on global scores, whereas we construct shields based on provided behavior. Having defined memoryless shields, we define a memoryless variant of (P*): Guarantee (ML-P*): ML-Saturated Permissiveness. For all π ∈ ΠM \ Allow( ), there is no safe memoryless shield ′ s.t. Allow( )∪ {π} ⊆ Allow( ′ ). This variant of saturated permissiveness relates to the notion of optimally permissive controllers, e.g., as in [14]. Optimality of such controllers refers to a (totally

L. Heck et al.

ordered) permissiveness score, while in saturated shields, it refers to a (partially ordered) set of allowed policies. In App. C, we briefly discuss generalizing these shields towards sliding-window shields, together with an adaptation of saturated permissiveness. Specifically, memoryless (or sliding window) constructed shields are analogously defined using memoryless (or sliding window) point shields, adapting Def. 12.

Experiments

We investigate the performance of the proposed shielding framework with a prototype implementation1 . We focus on the following questions: Q1: How do different shields compare in terms of permissiveness and safety? Q2: Can we efficiently compute and query our shields? How much data do we need to construct shields that are more permissive than trivial baselines? Implementation. Our shielding framework is implemented in Python and uses Storm [19] for model-checking queries. The framework is integrated into an environment for the construction and simulation of RL-based agents [21] that uses a specialized C++ library and TensorFlow for efficient agent training. Benchmarks. We consider three grid-based environments: corridor, which is a 5x3 grid with slippery cells with a pit to avoid, and two variants of a drone delivery task (13x8 and 21x15), featuring static obstacles, a zone where the drone can crash into other drones, and target cells. Additionally, we consider a variant of the dynamic power management problem (dpm) [32], where the goal is to maximize the number of incoming requests served before the battery runs out. Q1: Comparing Safety and Permissiveness of the Considered Shields Setup and baselines. (Agents): For each model, we consider three different agents: i) a greedy agent that optimizes the original model reward and disregards safety, ii) a timid agent that was trained with modified rewards to prefer safe choices, and iii) an agent that plays uniformly across the available actions in each state. (Shields): We consider our novel shields: optimistic ( opt ), pessimistic ( pess ), offline ( off ), online ( onl ), and offline memoryless ( ML ). We consider three baselines: i) the classical shield Safe [1], ii) the multiplicative δ-shield δ [22], and its additive variant δ+ (see Example 2). For each model and agent, we consider three safety thresholds ν. We report the results for a selection of shields in Table 2 and the full results in App. B.2. Details of the evaluation procedure are described in App. B.1. Main result: Tab. 2 compares the shields in terms of safety and permissiveness and demonstrates that our shields are the most permissive among the safe shields. 1

https://doi.org/10.5281/zenodo.19819788

Shields to Guarantee Probabilistic Safety in MDPs

Table 2. Comparison of different shields. The table reports combinations of the model, agent, threshold, and different shields. For each combination, we report two values: the left value is the safety value of the shielded agent, and the right value is the ratio of allowed actions (higher is better). For each row, the most permissive safe shields are in boldface. A red background means that the safety threshold has been violated. The values for onl are obtained using simulations and are thus subject to a statistical imprecision. The second column also reports the safety values of the unshielded agents. Model

corridor

dpm

drone

drone-b

Agent (value)

Safe

δ+

onl

off

SAFE

UNSAFE

SAFE

greedy (.125)

0.05 0.1 0.2

.000 .020 .000 .020 .000 .020

.000 .020 .000 .020 .125 .735

.000 .020 .100 .204 .125 .936

.000 .020 .100 .202 .125 .968

.000 .020 .000 .020 .125 .735

timid (.125)

0.05 0.1 0.2

.000 .020 .000 .020 .000 .020

.000 .020 .000 .020 .125 =1

.000 .020 .100 .406 .124 .993

.000 .020 .100 .406 .125 .997

.000 .020 .000 .020 .125 .925

random (.733)

0.05 0.1 0.2

.000 .116 .000 .116 .000 .116

.049 .134 .098 .153 .199 .190

.050 .142 .100 .148 .200 .215

.000 .116 .000 .116 .000 .116

greedy (.479)

0.01 0.05 0.2

.000 .771 .000 .771 .000 .771

.479 .479 .479

=1 =1 =1

.010 .790 .047 .839 .062 .870

.010 .792 .050 .848 .097 .908

.009 .794 .044 .844 .155 .924

timid (.063)

0.01 0.05 0.2

.000 .981 .000 .981 .000 .981

.063 .063 .063

=1 =1 =1

.000 .979 .000 .979 .000 .979

.000 .981 .000 .981 .000 .981

.000 .981 .010 .984 .063 =1

random (.131)

0.01 0.05 0.2

.000 .798 .000 .798 .000 .798

.131 .131 .131

=1 =1 =1

.005 .831 .005 .831 .005 .831

.006 .841 .006 .841 .006 .841

.006 .839 .037 .989 .131 =1

greedy (.240)

0.01 0.05 0.2

.000 .207 .000 .207 .000 .207

.001 .211 .001 .211 .240 =1

.009 .214 .049 .254 .160 .538

.010 .218 .050 .259 .200 .656

.000 .208 .000 .208 .054 .239

timid (.014)

0.01 0.05 0.2

.000 .554 .000 .554 .000 .554

.002 .728 .002 .728 .014 =1

.009 .808 .008 .811 .009 .810

.010 .830 .011 .855 .011 .855

.000 .554 .000 .554 .001 .640

random (.962)

0.01 0.05 0.2

.000 .722 .000 .722 .000 .722

.052 .839 .052 .839 .052 .839

.000 .721 .000 .723 .000 .722

.000 .722 .000 .722 .000 .722

.000 .722 .006 .749 .027 .812

greedy (.912)

0.01 0.05 0.2

.000 .160 .000 .160 .000 .160

.000 .160 .000 .160 .139 .915

.000 .160 .050 .247 .197 .733

.000 .160 .050 .256 .200 .743

.000 .160 .000 .160 .000 .160

timid (.016)

0.01 0.05 0.2

.000 .987 .000 .987 .000 .987

.000 .987 .014 .999 .014 .999

.002 .989 .002 .989 .002 .989

.004 .990 .004 .990 .004 .990

.000 .987 .000 .987 .000 .987

random ( =1)

0.01 0.05 0.2

.000 .762 .000 .762 .000 .762

.016 .764 .101 .764 .101 .764

.010 .762 .042 .764 .044 .763

.010 .763 .050 .765 .074 .766

.000 .762 .000 .762 .000 .762

Safety. Unsafe shields (UNSAFE) do not ensure safety bounds across different benchmarks, while the safe shields (SAFE) provably do. The classical shield Safe indeed keeps the probability of reaching at zero, which is attainable by some policy in all of our benchmarks (i.e., Vmin (s0 ) = 0). We observe that in many models, δ+ (which can allow more policies compared to Safe if Vmin (s0 ) = 0) still behaves either as if no shield was applied or like Safe . The results in App. B.2

L. Heck et al.

further show that i) since Vmin (s0 ) = 0, δ (for arbitrary δ) does not allow any risky choice (i.e. behaves as Safe ), ii) pess is also overly conservative, and iii) our unsafe shield opt offers no advantage over δ+ on these benchmarks. Permissiveness. Our shields are, in most cases, the most permissive among the shields that achieved the required safety value; the only exceptions having bigger gaps in permissiveness (compared to δ+ ) are drone/timid, drone/random, and drone-b/greedy for ν = 0.2. We further observe that the online construction of onl is only slightly less permissive than that of off . This demonstrates that we can deploy safe, permissive shields without collecting the agent’s trajectories in advance. Shields benefit from memory. Table 2 further demonstrates that shields generally need memory to be safe and permissive: In many cases, memoryless shields ML discussed in Section 7 are considerably less permissible than off . On the other hand, we observe that sometimes memoryless shields suffice, see e.g. dpm. Q2: Computational and Data Demands Computational demands. Table 3 reports, for the individual shields, the average number of shield queries that can be executed per second, including the simulation overhead and initialization2 . We observe that Safe and δ+ have similar performance, which is expected as both compute the next-state probability and then perform a comparison. The shields δ , opt and pess perform similar to Safe and δ + . Note that although opt and pess depend on the full history, we only need to keep a running tally of incurred safety or risk in practice. The shields onl and off have a more involved shielding procedure: A linear program must be solved in order to check whether an input choice belongs to the convex set of allowed choices at the given history (see Remark 2). As expected, onl introduces the largest overhead compared to Safe due to the shield updates performed during execution. Even for the largest model, onl still performs more than 700 queries per second. As expected, onl queries become linearly slower with episode length (see Table 9 in App. B.3). However, with a fixed episode length, the queries can become faster with the number of construction steps since the number of blocked choices (and thus shield updates) decreases over time (see Table 8 in App. B.3). The query time for constructed ML is similar to that of off , but the construction steps for obtaining a memoryless shield can be more expensive than in onl , since they require model checking of M. All the omitted results are reported in App. B.2. Table 4 reports the peak memory usage overhead of using the shields on top of the simulator process. For all models, the memory overhead of using constructed shields never exceeds 500MB compared to using no shield at all. We note that the constructed shield’s size will, in the worst case, grow linearly in the number of state-action pairs, which is in turn bounded by the number of shield queries. 2

Pre-computation of Vmin values, required for all the considered shields, is performed via standard model checking methods and, for our benchmarks, takes under a second.

Shields to Guarantee Probabilistic Safety in MDPs

Table 3. Comparison of runtimes of different shields. We report the number of shield queries per second based on simulations (including the simulation overhead). For all experiments, we used the greedy agent and ν = 0.2. |M |

Safe

corridor 15 dpm 797 drone 1859 drone-b 87k

2.7k 2.9k 2.7k 2.2k

Model

δ+

opt

pess

onl

off

2.2k 2.2k 3.0k 3.0k 2.6k 2.6k 2.2k 2.2k

1.9k 2.4k 1.8k 1.5k

1.9k 2.6k 2.3k 1.7k

1.8k 1.6k 0.7k 0.9k

2.1k 2.3k 1.6k 1.8k

Table 4. Comparison of memory usage of different shields. We report the difference in peak memory usage in MBs of the simulator process equipped with the given shield compared to the simulator with no shield. For all experiments, we used the greedy agent and ν = 0.2. Model

|M |

corridor 15 dpm 797 drone 1859 drone-b 87k

Safe

δ+

opt

4.5 2.3 2.3 2.1 1.2 1.3 1.3 3.8 1.7 1.9 1.9 4.1 10.5 13.8 13.8 10.1

pess

onl

off

6.3 72.3 40.1 40.1 4.1 362.1 391.1 391.1 1.6 431.6 228.6 228.6 9.5 98.8 126.4 126.4

Convergence. Fig. 6 shows how the permissiveness of off (i.e. the ratio of allowed choices) improves with the number of construction steps. It shows the results for safety threshold ν = 0.2 (the plots are similar for other values of ν). In most cases (except for drone/greedy), we obtain the permissiveness close to the maximum achieved value after 40K steps. This clearly shows that our shield construction needs a feasible amount of data. Recall that in some cases, ML converges faster and achieves better permissiveness than off .

Related Work

The existing work on probabilistic shields that is closest to our approach has been discussed in the introduction. We expand on further topics related to shielding. Classical shielding and beyond. Classical shielding [1] has recently been extended to a rich array of temporal safety specifications, including e.g. LTL modulo theories [35]. Another active research direction focuses on shielding in more expressive models such as continuous [42], partially observable [8,36], or multi-agent systems [7, 15]. Shielding can also be seen as a counterpart to safety filtering in continuous control [20, 40] or to simplex architectures [31, 33] that enhance the safety of learning-based autonomous systems via a fail-safe mechanism. In reactive systems, shielding can be seen as a type of runtime enforcement [2]. In online planning, on-the-fly construction of a shield (so-called symbolic advice) can be used to prune parts of the search tree violating the safety specifications [9] and thus to provide statistical safety guarantees. Shielding is also closely related to safe learning methods such as risk-aware learning [6, 10], online safety verifica-

L. Heck et al. Allowed actions (%)

20 1.0

Model corridor dpm drone drone-b

0.8 0.6 0.4

Agent greedy timid random

0.2 4k

200k 400k 600k 800k Construction steps

Fig. 6. Convergence of the allowed choices for off with ν = 0.2. Results collected every 4K steps and interpolated. Step 0 corresponds to S .

tion during training [30], or training policies that account for their own safety budget [12], all of which are related to our pessimistic shields. Online and adaptive shielding. To avoid computing the shield for all state-action combinations, an online shielding approach has been proposed in [28], where actions are evaluated and blocked based on a finite lookahead horizon. Further research focuses on relaxing the assumption that the safety model is known a priori: Dynamic shielding techniques construct an approximate safety model using automata learning in parallel with policy training [37, 41]. In cautious RL [18], a safe padding is used to block actions that lead to states that are too close to the unsafe states according to the learned model. Recently, several studies have started investigating the possibility of adapting the safety model based on the data observed by the agent. In [5], a contrastive autoencoder is used to learn latent representations that distinguish safe and unsafe state-action pairs. Alternatively, a programming-language framework [16] or abstraction refinement [34] are used to adapt the model. If formal guarantees on model accuracy are available, these approaches can be integrated with our shielding to provide provable safety.

Conclusions and Future Work

In this paper, we propose various new shields that do guarantee to be safe with respect to a probabilistic safety specification: Optimistic and pessimistic shields, and saturated safe shields with associated online and offline learning routines. We show that these shields are permissive and feasible to construct. Future work. The developed framework assumes full knowledge of the underlying MDP, but can be lifted to cases where only a safety-relevant quotient of the MDP is known [22], which requires careful treatment of guarantees and the relationship between the quotient and the model. We will also further investigate the sliding-window generalization of the memoryless shields (from Section 7), as it has the potential to improve the convergence to more permissive shields from limited data. Acknowledgements. This work has been executed under the project VASSAL: “Verification and Analysis for Safety and Security of Applications in Life”

Shields to Guarantee Probabilistic Safety in MDPs

funded by the European Union under Horizon Europe WIDERA Coordination and Support Action/Grant Agreement No. 10116002.

L. Heck et al.

References 1. Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI. pp. 2669–2678 (2018) 2. Anand, A., Germerie Guizouarn, L., Jéron, T., Mukherjee, S., Pinisetty, S., Sankur, O.: Prompt runtime enforcement. In: ATVA. pp. 135–156 (2025) 3. Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008) 4. Barrett, C., Henzinger, T.A., Seshia, S.A.: Certificates in AI: Learn but verify. Commun. ACM 69(1), 66–75 (2025) 5. Bethell, D., Gerasimou, S., Calinescu, R., Imrie, C.: Safe reinforcement learning in black-box environments via adaptive shielding. In: ECAI (2025) 6. Brázdil, T., Chatterjee, K., Novotný, P., Vahala, J.: Reinforcement learning of risk-constrained policies in Markov decision processes. In: AAAI. pp. 9794–9801 (2020) 7. Brorholt, A.H., Larsen, K.G., Schilling, C.: Compositional shielding and reinforcement learning for multi-agent systems. In: AAMAS. pp. 399–407 (2025) 8. Carr, S., Jansen, N., Junges, S., Topcu, U.: Safe reinforcement learning via shielding under partial observability. In: AAAI. pp. 14748–14756 (2023) 9. Chakraborty, D., Busatto-Gaston, D., Raskin, J.F., Pérez, G.A.: Formally-sharp dagger for mcts: Lower-latency monte carlo tree search using data aggregation with formal methods. In: AAMAS. pp. 1354–1362 (2023) 10. Chapman, M.P., Faus, M., Smith, K.M.: On optimizing the conditional value-at-risk of a maximum cost for risk-averse safety analysis. IEEE Transactions on Automatic Control 68(6), 3720–3727 (2022) 11. Chatterjee, K., Novotný, P., Pérez, G.A., Raskin, J., Zikelic, D.: Optimizing expectation with guarantees in pomdps. In: AAAI. pp. 3725–3732 (2017) 12. le Court, E.H., Belardinelli, F., Goodall, A.W.: Probabilistic shielding for safe reinforcement learning. In: AAAI. pp. 16091–16099 (2025) 13. David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal stratego. In: TACAS. pp. 206–211 (2015) 14. Dräger, K., Forejt, V., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log. Methods Comput. Sci. 11(2) (2015) 15. ElSayed-Aly, I., Bharadwaj, S., Amato, C., Ehlers, R., Topcu, U., Feng, L.: Safe multi-agent reinforcement learning via shielding. In: AAMAS. p. 483–491 (2021) 16. Feng, Y., Zhu, J., Platzer, A., Laurent, J.: Adaptive shielding via parametric safety proofs. Proceedings of the ACM on Programming Languages 9(OOPSLA1), 816–843 (2025) 17. Gu, S., Yang, L., Du, Y., Chen, G., Walter, F., Wang, J., Knoll, A.: A review of safe reinforcement learning: Methods, theories and applications. IEEE Transactions on Pattern Analysis and Machine Intelligence (2024) 18. Hasanbeig, M., Abate, A., Kroening, D.: Cautious reinforcement learning with logical constraints. In: AAMAS. pp. 483–491 (2020) 19. Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589–610 (2022) 20. Hsu, K.C., Hu, H., Fisac, J.F.: The safety filter: A unified view of safety-critical control in autonomous systems. Annual Review of Control, Robotics, and Autonomous Systems 7 (2024) 21. Hudák, D., Galesloot, M.F., Tappler, M., Kurečka, M., Jansen, N., Češka, M.: Finite-state controllers for (hidden-model) POMDPs using deep reinforcement learning. In: AAMAS (2026), To appear

Shields to Guarantee Probabilistic Safety in MDPs

22. Jansen, N., Könighofer, B., Junges, S., Serban, A., Bloem, R.: Safe reinforcement learning using probabilistic shields (invited paper). In: CONCUR. pp. 1–16 (2020) 23. Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.: Safety-constrained reinforcement learning for MDPs. In: TACAS. pp. 130–146 (2016) 24. Kochdumper, N., Krasowski, H., Wang, X., Bak, S., Althoff, M.: Provably safe reinforcement learning via action projection using reachability analysis and polynomial zonotopes. IEEE Open Journal of Control Systems 2, 79–92 (2023) 25. Könighofer, B., Alshiekh, M., Bloem, R., Humphrey, L.R., Könighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332– 361 (2017). https://doi.org/10.1007/S10703-017-0276-9, https://doi.org/ 10.1007/s10703-017-0276-9 26. Könighofer, B., Bloem, R., Jansen, N., Junges, S., Pranger, S.: Shields for safe reinforcement learning. Commun. ACM 68(11), 80–90 (2025) 27. Könighofer, B., Lorber, F., Jansen, N., Bloem, R.: Shield synthesis for reinforcement learning. In: ISoLA. pp. 290–306 (2020) 28. Könighofer, B., Rudolf, J., Palmisano, A., Tappler, M., Bloem, R.: Online shielding for reinforcement learning. Innovations in Systems and Software Engineering 19(4) (2023) 29. Krasowski, H., Thumm, J., Müller, M., Schäfer, L., Wang, X., Althoff, M.: Provably safe reinforcement learning: Conceptual analysis, survey, and benchmarking. Trans. Mach. Learn. Res. 2023 (2023) 30. Marzari, L., Cicalese, F., Farinelli, A., Amato, C., Marchesini, E.: Verifying online safety properties for safe deep reinforcement learning. ACM Trans. Intell. Syst. Technol. (2025) 31. Nesti, F., Salamini, N., Marinoni, M., Cicero, G.M., Serra, G., Biondi, A., Buttazzo, G.: The use of the simplex architecture to enhance safety in deep-learning-powered autonomous systems. arXiv preprint arXiv:2509.21014 (2025) 32. Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Formal analysis and validation of continuous time Markov chain based system level power management strategies. In: HLDVT. pp. 45–50 (2002) 33. Phan, D.T., Grosu, R., Jansen, N., Paoletti, N., Smolka, S.A., Stoller, S.D.: Neural simplex architecture. In: NASA Formal Methods Symposium. pp. 97–114 (2020) 34. Pranger, S., Könighofer, B., Tappler, M., Deixelberger, M., Jansen, N., Bloem, R.: Adaptive shielding under uncertainty. In: ACC (2021) 35. Rodriguez, A., Amir, G., Corsi, D., Sánchez, C., Katz, G.: Shield synthesis for LTL modulo theories. In: AAAI. pp. 15134–15142 (2025) 36. Sheng, S., Parker, D., Feng, L.: Safe POMDP online planning via shielding. In: ICRA. pp. 126–132 (2024) 37. Tappler, M., Pranger, S., Könighofer, B., Muškardin, E., Bloem, R., Larsen, K.: Automata learning meets shielding. In: ISoLA. pp. 335–359 (2022) 38. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285–309 (1955). https://doi.org/10.2140/pjm.1955.5.285 39. Van Havermaet, S., Khaluf, Y., Simoens, P.: No more hand-tuning rewards: Masked constrained policy optimization for safe reinforcement learning. In: AAMAS. pp. 1344–1352 (2021) 40. Wabersich, K.P., Taylor, A.J., Choi, J.J., Sreenath, K., Tomlin, C.J., Ames, A.D., Zeilinger, M.N.: Data-driven safety filters: Hamilton-jacobi reachability, control barrier functions, and predictive methods for uncertain systems. IEEE Control Systems Magazine 43(5), 137–177 (2023)

L. Heck et al.

41. Waga, M., Castellano, E., Pruekprasert, S., Klikovits, S., Takisaka, T., Hasuo, I.: Dynamic shielding for reinforcement learning in black-box environments. In: ATVA. pp. 25–41 (2022) 42. Yang, W., Marra, G., Rens, G., Raedt, L.D.: Safe reinforcement learning via probabilistic logic shields. In: IJCAI. pp. 5739–5749 (2023)

Shields to Guarantee Probabilistic Safety in MDPs

Proofs

This appendix contains the proofs for all theorems and lemmas stated without proof in the paper. A.1

Shields for Probabilistic Safety

Lemma 1. Given shield

and policies P ⊆ Allow( ). Then mix (P ) ⊆ Allow( ).

Proof (Lemma 1). Given a policy π ∈ mix (P ). Suppose that π ∈ / Allow( ). Then, there exists a history h consistent with π such that (h, π(path(h)) ̸= π(path(h)). Assume an extended history h′ := h · π(path(h)) · α · s consistent with π. From π ∈ mix (P ) it follows that there exists a policy π ′ ∈ P ⊆ Allow( ) such that h′ is consistent with π ′ . Then, π(path(h)) = choice(h, path(h)) = choice(h′ , path(h)) = π ′ (path(h)). Therefore, T (π ′ )(path(h)) = π ′ (path(h)) = π(path(h)). Thus, it must be the case that (h, π(path(h))) = π(path(h)) =⇒ Contradiction. Theorem 1. Let P be a mix-closed set of policies such that for any history h that is consistent with some policy in P and any d ∈ ∆(ActSafe (last(h))), there exists a policy π ∈ P such that h is consistent with π and π(path(h)) = d. There is a unique canonical shield with Allow( ) = P . Proof (Theorem 1). The shield is given by ( d if ∃π ∈ P s.t. h is consistent with π and π(path(h)) = d, P (h, d) = d|ActSafe (last(h)) otherwise. Clearly, P is canonical. We show that Allow( P ) = P . “⇒” Let π ∈ Allow( P ). Then for all h ∈ Hist(M), we have π(path(h))). As P is mix -closed, it suffices to show:

P (h, π(path(h))) =

∀h ∈ Hist(M). ∃π ′ ∈ P. (h consistent with π =⇒ h consistent with π ′ ). Let h ∈ Hist(M) and suppose that h is consistent with π. Let d := π(path(h)). We have two cases: – If P (h, d) = d ̸= d|ActSafe (last(h)) , then there exists a π ′ ∈ P s.t. h is consistent with π ′ by definition of P . – If P (h, d) = d = d|ActSafe (last(h)) , then there exists a π ′ ∈ P s.t. h is consistent with π ′ because P satisfies the condition from the theorem. “⇐” Let π ∈ P . Then for all h ∈ Hist(M) that are consistent with π, we have (h, π(path(h))) = π(path(h))). Thus, π ∈ Allow( ). P Uniqueness of the shield follows from the definition of canonicity: Intuitively, a different shield must make a different decision on a history consistent with some allowed policy, so it will not have the same allow set.

L. Heck et al. (1 − ν) − x2

1/2

α β

s1 γ δ

ν − x2 Fig. 7. MDP

A.2

Shields with Strong and Weak Guarantees

Theorem 3. For a safety threshold 0 < ν < 1, there is an (acyclic, 5-state) MDP such that no shield satisfies (S+) and (P+). Proof (Theorem 3). We prove Theorem 3 for arbitrary 0 < ν < 1. Given such a ν, pick x = min{ ν2 , 1−ν 2 } and consider Fig. 7. Note that Pr(s0 ⊨ ⋄ ) ≤ ν if and only if Pr(s1 ⊨ ⋄ ) ≤ 0.5. By invoking the special case for 0.5 in the main paper, we then get the general statement. A.3

Optimistic and Pessimistic Shields

We first give the definitions of the optimistic and pessimistic shield (Def. 9, Def. 17) in their canonical form. This adaptation ensures that the shield projects to the safe actions on histories that are not consistent with any allowed policy. On all other histories, the canonical and non-canonical versions coincide. Definition 17 (Optimistic Shield). Let ν ∈ [0, 1] and bmin = ν − Vmin (s0 ). Note that 0 ≤ bmin ≤ 1 because Vmin (s0 ) ≤ ν. The optimistic shield is given by   if irisk (h, d) ≤ bmin and for all 0 ≤ k < |h| : d (h, d) = irisk (choice(h, k + 1)) ≤ bmin , opt   d|ActSafe (last(h)) otherwise. Definition 18 (Pessimistic Shield). Let ν ∈ [0, 1] and bmax = Vmax (s0 ) − ν. Note that −1 ≤ bmax ≤ 1. The pessimistic shield is given by   if isafety(h, d) ≥ bmax and for all 0 ≤ k < |h| : d isafety(choice(h, k + 1)) ≥ bmax , pess (h, d) =   d|ActSafe (last(h)) otherwise. Lemma 2. Allow( pess = Safe .

Safe ) ⊆ Allow(

pess ) ⊆ Allow(

opt ). If ν = 0, then

opt =

Shields to Guarantee Probabilistic Safety in MDPs

Proof (Lemma 2). – Allow( Safe ) ⊆ Allow( pess ): If Safe (h, d) = d, then d = d|ActSafe (last(h)) , and then pess (h, d) = d. If a policy is allowed by Safe , it only returns choices over safe actions, and is thus allowed by the pessimistic shield. – Allow( pess ) ⊆ Allow( opt ): We jump ahead and use Theorem 4. This statement is a corollary: Allow( pess ) only allows safe policies and Allow( opt ) allows all safe policies. – If ν = 0, then Safe = pess : Suppose pess (h, d) = d. Then either d = d|ActSafe (last(h)) , or isafety(h, d) ≥ bmax = Vmax (s0 ), which also implies d = d|ActSafe (last(h)) . Thus Safe (h, d) = d. – If ν = 0, then Safe = opt : Suppose opt (h, d) = d. Then either d = d|ActSafe (last(h)) , or irisk (h, d) ≤ bmin = −Vmin (s0 ), which also implies d = d|ActSafe (last(h)) . Thus Safe (h, d) = d. Lemma 3. Given Vmin (resp. Vmax ), the computation time for pess (h, d)) is in O(|h| · |Act| · |S|).

opt (h, d) (resp.

Proof (Lemma 3). We discuss the optimistic shield, the pessimistic shield is analogous. To compute opt (h, d) given a history h ∈ Hist(M) and choice d ∈ ∆(Act), we need to compute irisk (h, d), then, computing the shield can clearly be done in O(|Act| · |S|). This algorithm is given in Algorithm 1. This is clearly in O(|h| · |Act| · |S|) Algorithm 1 Computing incurred risk Input: h = s0 d1 α1 · · · st ∈ Hist(M), dt+1 ∈ ∆(Act) Output: irisk (h, dt+1 ) r←0 p←1 for k ∈ {0, . . . , t} do q←0 for α ∈ Act do for s′ ∈ S do q ← q + dk+1 (α) · P(sk , α, s′ ) · Vmin (s′ ) end for end for r ← r + p · (q − Vmin (sk )) if k < t then p ← p · dk+1 (αk+1 ) · P(sk , αk+1 , sk+1 ) end if end for return r

For any π ∈ Π(M), τ s ∈ FinPaths(M) and function f : FinPaths(M) → R we write: X X Eπ [f | τ s] := π(τ s)(α) P(s, α, s′ )f (τ sαs′ ). α∈Act

s′ ∈S

L. Heck et al.

Lemma 12. For any non-negative function f , for all τ sα̂ŝ ∈ FinPaths(M) it holds that: Prπ (τ s)Eπ [f | τ s] ≥ Prπ (τ sα̂ŝ)f (τ sα̂ŝ). Lemma 4. (S+) implies (S−) and (P+) implies (P−). Proof (Lemma 4). (S+) implies (S−): Suppose satisfies (S+), i.e. T (ΠM ) ⊆ Safe(ΠM ). Then, (for every finite path τ ∈ FinPaths(M) and) for every policy π ∈ ΠM , T (π) is safe, and thus πsafe = T (π) satisfies the condition for (S−). (P+) implies (P−): Suppose satisfies (P+), i.e. Safe(ΠM ) ⊆ Allow( ). Then for every finite path τ ∈ FinPaths(M) and policy π ∈ ΠM with T (π)(τ ) ̸= π(τ ), we have that π is unsafe because T (π) ̸= π, and thus πunsafe = π satisfies the condition for (P−). Proof (Lemma 12). Prπ (τ s)Eπ [f | τ s] X X = Prπ (τ s) π(τ s)(α′ ) P(s, α′ , s′ )f (τ sα′ s′ ) α′ ∈Act

s′ ∈S

≥ Prπ (τ s)π(τ s)(α̂)P(s, α̂, ŝ)f (τ sα̂ŝ) = Prπ (τ sα̂ŝ)f (τ sα̂ŝ). to

For π ∈ Π(M) and τ ∈ FinPaths(Π), let Vπ (τ ) be the reachability probability under π given τ . We prove the following two lemmas:

Lemma 13. Given policy π ∈ ΠM and a history h ∈ Hist(M) consistent with π. Then irisk (h, π(path(h))) ≤ Vπ (s0 ) − Vmin (s0 ). Lemma 14. Given policy π ∈ ΠM and a history h ∈ Hist(M) consistent with π. Then isafety(h, π(path(h))) ≤ Vmax (s0 ) − Vπ (s0 ). Proof (Lemma 13). Define δπ (τ ) := Vπ (τ )−Vmin (τ ). Given any τ s ∈ FinPaths(M), we have Qmin (s, π(τ s)) = Eπ [Vmin | τ s]. For a history h = s0 d1 α1 s2 · · · st consistent with π, define τ := path(h) and dt+1 := π(path(h)). We obtain: irisk (h, dt+1 ) X = Pr(h|k ) (Qmin (sk , dk+1 ) − Vmin (sk )) , 0≤k≤t

Prπ (τ ′ s) (Qmin (s, π(τ ′ s)) − Vmin (s))

τ ′ s∈Prefix(τ )

X τ ′ ∈Prefix(τ )

Prπ (τ ′ ) (Eπ [Vmin | τ ′ ] − Vmin (τ ′ ))

Shields to Guarantee Probabilistic Safety in MDPs

Prπ (τ ′ ) (Eπ [Vmin | τ ′ ] − Vmin (τ ′ ) + Vπ (τ ′ ) − Eπ [Vπ | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ ) (δπ (τ ′ ) − Eπ [Vmin − Vπ | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ ) (δπ (τ ′ ) − Eπ [δπ | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ )δ(τ ′ ) − Prπ (τ ′ )Eπ [δπ | τ ′ ]

τ ′ ∈Prefix(τ ) (∗)

≤ δπ (s0 ) = Vπ (s0 ) − Vmin (s0 ). (*) follows from Lemma 12. Proof (Lemma 14). For π ∈ Π(M) and τ ∈ FinPaths(Π), let Vπ (τ ) be the reachability probability under π given τ . Define δ(τ ) := Vmax (τ ) − Vπ (τ ). Given any τ s ∈ FinPaths(M), we have Qmax (s, π(τ s)) = Eπ [Vmax | τ s]. For a history h = s0 d1 α1 s2 · · · st that is consistent with π, define τ := path(h) and dt+1 := π(path(h)). We obtain: isafety(h, dt+1 ) X = Pr(h|k ) (Vmax (sk ) − Qmax (sk , dk+1 )) 0≤k≤t

Prπ (τ ′ s) (Vmax (s) − Qmax (s, π(τ ′ s)))

′

τ s∈Prefix(τ )

Prπ (τ ′ ) (Vmax (τ ′ ) − Eπ [Vmax | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ ) (Vmax (τ ′ ) − Eπ [Vmax | τ ′ ] − Vπ (τ ′ ) + Eπ [Vπ | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ ) (δ(τ ′ ) − Eπ [Vπ − Vmax | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ ) (δ(τ ′ ) − Eπ [δ | τ ′ ])

τ ′ ∈Prefix(τ )

Prπ (τ ′ )δ(τ ′ ) − Prπ (τ ′ )Eπ [δ | τ ′ ]

τ ′ ∈Prefix(τ ) (∗)

≤ δ(s0 ) = Vmax (s0 ) − Vπ (s0 ). (*) follows from Lemma 12. Theorem 4. The optimistic shield satisfies (S−) and (P+). The pessimistic shield satisfies (S+) and (P−).

L. Heck et al.

Proof (Theorem 4). Proof that the optimistic shield satisfies (S−) and (P+): Recall (S−): For each τ ∈ FinPaths(M), there is a safe policy πsafe with πsafe (τ ′ ) = T (π)(τ ′ ) for all prefixes τ ′ of τ . Proof of (S−): Given policy π and any τ = s0 α1 · · · st ∈ FinPaths(M). Let h = s0 π(s0 )α1 · · · st . We know that irisk (h, T (π)(τ )) ≤ bmin by Def. 9. Construct the policy π ′ that plays T (π) on the prefixes of τ and plays according to an optimally safe policy πmin on every other path. Then we have: X Vπ′ (s0 ) ≤ Vmin (s0 ) + Pr(h|k ) (Qmin (sk , T (π)(path(h|k )) − Vmin (sk )) , 0≤k≤t

= Vmin (s0 ) + irisk (h, T (π)(τ )) ≤ Vmin (s0 ) + bmin = ν. Thus πsafe = π ′ . Recall (P+): Safe(ΠM ) ⊆ Allow( ). Proof of (P+): If π is safe, we have Vπ (s0 ) ≤ ν and thus by Lemma 13, for all histories h consistent with π, we have irisk (h, π(path(h)) ≤ Vπ (s0 ) − Vmin (s0 ) ≤ ν − Vmin (s0 ) = bmin , so the shield will never interfere. Proof that the pessimistic shield satisfies (P−) and (S+): Recall (P−): For each τ ∈ FinPaths(M) with T (π)(τ ) ̸= π(τ ), there is an unsafe policy πunsafe with πunsafe (τ ′ ) = π(τ ′ ) for all prefixes τ ′ of τ . Proof of (P−): Given a finite path τ = s0 α1 · · · st ∈ FinPaths(M) with T (π)(τ ) ̸= π(τ ). Let h = s0 π(s0 )α1 · · · st . We know that isafety(h, π(τ )) < bmax by Def. 10. Construct the policy π ′ that plays π on the prefixes of τ and according to an optimally unsafe policy πmax on every other path. Then we have: X Vπ′ (s0 ) ≥ Vmax (s0 ) − Pr(h|k ) (Vmax (sk ) − Qmax (sk , dk+1 )) 0≤k≤t

= Vmax (s0 ) − safety(h, π(τ )) > Vmax (s0 ) − bmax = ν. Thus, πunsafe = π ′ . Recall (S+): Safe(ΠM ) ⊆ Allow( ). Proof of (S+): Let π be a policy. We have two cases: (1) Suppose that isafety(h, π(τ )) < bmax for all histories h that are consistent with T (π). Then the shield blocks every choice proposed by π, so T (π) only plays safe actions. Thus T (π) is optimal w.r.t. safety and in particular safe. (2) Suppose that there exists some h ∈ Hist(M) that is consistent with T (π) s.t. isafety(h, T (π)(path(h))) ≥ bmax . Since the pessimistic shield returns d unchanged whenever isafety(h, d) ≥ bmax , we have T (π)(path(h)) = π(path(h)), and thus isafety(h, π(path(h))) ≥ bmax . Then by Lemma 14, we have bmax = Vmax (s0 ) − ν ≤ isafety(h, π(path(h))) ≤ Vmax (s0 ) − Vπ (s0 ), and thus Vπ (s0 ) ≤ ν, i.e., π is safe. As T (π) plays either optimally w.r.t. safety or agrees with π, we have VT (π) (s0 ) ≤ Vπ (s0 ) ≤ ν, so T (π) is safe. Lemma 5. For 0 < δ,ν < 1, there is an MDP such that the δ-shield does not satisfy (S−) (resp. (P−)).

Shields to Guarantee Probabilistic Safety in MDPs

1−ν

ν 1−x

1−ν

Fig. 9. MDP

Fig. 8. MDP

Proof (Lemma 5). For δ = 0, the shield is the same as id and trivially satisfies (P+). For δ = 1, the shield is the same as Safe and thus satisfies (S+). Suppose 0 < δ < 1 and 0 < ν < 1. The δ-shield does not satisfy (P−): consider the MDP in Fig. 8. There is no unsafe policy, so a shield satisfying (P−) must allow all policies. Consider the safe policy π = {s0 7→ 1α }. For d = 1α , because Vmin (s0 ) = 0 and δ·

(d(α) · P(s0 , α, s′ ) · Vmin (s′ )) = δ · ν > 0 = Vmin (s0 ),

α∈Act,s′ ∈S

we have δ (s0 , d) ̸= d, and thus, T δ (π) ̸= π. The δ-shield does not satisfy (S−): Consider the MDP in Fig. 9 and set x := min

ν √ √ , ν . δ

We’ve chosen x specifically such that for all 0 < ν < 1 and 0 < δ < 1: 0 < x < 1, x > ν, and δ · x ≤ ν. As x > ν, the policy π with π(s0 ) = 1β is unsafe and cannot be completed to a safe policy. But for d = 1β , we have: δ·

(d(α) · P(s0 , α, s′ ) · Vmin (s′ )) = δ · x ≤ ν = Vmin (s0 ).

α∈Act,s′ ∈S

Thus, we have A.4

δ (s0 , d) = d, and thus, we have T

(π)(s0 ) = π(s0 ).

Saturated Safe Shields

Lemma 6. For all saturated shields {d ∈ ∆(Act) | (h, d) = d} is convex.

and histories h ∈ Hist(M), the set

Proof (Lemma 6). Suppose that is saturated, and for some history h ∈ Hist(M) and choices d, d1 , . . . , dn ∈ ∆(Act), we have that – (h, d) ̸= d, – (h, di ) = di for all 1 ≤ i ≤ n, – d = a1 d1 + · · · + an dn for 0 ≤ ai ≤ 1.

L. Heck et al.

P Note that 1≤i≤n ai = 1. Consider the shield ′ that behaves like except that ′ (h, d) = d. We show that ′ is safe. Clearly, this shield allows strictly more policies than . Let π be any policy consistent with h such that π(path(h)) = d. If ′ was unsafe, it would be only because it included an unsafe policy that plays d at path(h). Construct the policies πi that behave the same as π everywhere, except at path(h), where they play di . Then, Vπ (path(h)) ≤ max{Vπi (path(h)) | 1 ≤ i ≤ n}, and thus, Vπ (s0 ) ≤ max{Vπi (s0 ) | 1 ≤ i ≤ n}. Thus, π is safe. As ′ is safe and allows strictly more policies than , is not saturated =⇒ Contradiction. Theorem 5. The axiom of choice implies that for any MDP and any ν ∈ [0, 1], a saturated shield exists. Proof (Theorem 5). We jump ahead and use the lattice L = (CShields, ⊑) defined in Def. 11. Let SShields := CShields ∩ { | safe} be the set of safe canonical shields. A canonical saturated shield is a maximal element within SShields w.r.t. ⊑. We will use Zorn’s lemma to show its existence. We already know that Safe ∈ SShields, thus, SShields is nonempty. We only need to show that each chain in SShields has F an upper bound in SShields. Let X be a chain := X is clearly an upper bound, but we need to in SShields. The shield prove that ∈ SShields. Suppose that there is an unsafe policy π such that π ∈ Allow( ). As an unsafe policy has a value strictly larger than ν, there exists a step bound N ∈ N such that Prπ (s0 ⊨ ⋄≤N ) > ν. Define H := {(s0 π(s0 )α1 s1 π(s0 α1 s1 ) · · · st , π(τ )) | τ := s0 α1 · · · st ∈ FinPaths(M), t ≤ N } Note that H is finite, nonempty, and prefix-closed. Then, we have (h, d) = d F for all (h, d) ∈ H, and the shield ′ := (h,d)∈H (h,d) is already unsafe, as PrT ′ (π) (s0 ⊨ ⋄≤N ) = Prπ (s0 ⊨ ⋄≤N ) > ν. Write H := {(h1 , d1 ), (h2 , d2 ), . . . , (hn , dn )}. Now pick a set of shields Y := { 1 , 2 , . . . , n } such that for all 1 ≤ i ≤ n: i (hi , di ) = di , and i ∈ X. These shields exist in X because the join of X allows these history-distribution pairs, and this means that some shield in X must allow them from the join characterization in Theorem 6. Because Y ⊆ X, and X is totally ordered, there exists a maximum w.r.t. ⊑ ∗ ∈ Y ⊆ X. Then, we have ∗ (h, d) = d for all (h, d) ∈ H (otherwise, some policy consistent with h and playing d at path(h) would not be allowed by ∗ but by a less permissive shield in Y ). This means that PrT ∗ (π) (s0 ⊨ ⋄≤N ) = Prπ (s0 ⊨ ⋄≤N ) > ν. Thus,

∗

is unsafe =⇒ Contradiction. Thus,

∈ SShields.

Lemma 7. For acyclic MDPs, Theorem 5 is true independent of the axiom of choice.

Shields to Guarantee Probabilistic Safety in MDPs

Proof (Lemma 7). Suppose that M is acyclic. Let N be the length of the longest path in M. In this case, policies can only use memory of size N . There is a finite number of paths in M. We can unfold the MDP to an MDP M′ that has one state for each path. All policies in M correspond to a positional policy in M′ . One can thus compute a saturated shield using an LP solver akin to computing an optimally permissive policy as in [14]. A.5

Constructed Shields

Lemma 15. The function mix is a closure operator on (2Π(M) , ⊆), i.e., it is monotone, extensive, and idempotent. Proof. Monotone: Let X ⊆ Y . Suppose π ∈ mix (X). Then for all h ∈ Hist(M), if h is consistent with π, there exists a π ′ ∈ X, and thus π ′ ∈ Y such that h is consistent with π ′ . Thus, π ∈ mix (Y ). Extensive: Let π ∈ X. Then, (“plugging in” the definition), for all histories h, it is the case that π ∈ X such that if h consistent with π, then h consistent with π. Thus, π ∈ mix (X). Idempotent: Let π ∈ mix (mix (X)). For all h ∈ Hist(M), suppose h consistent with π. Then there exists a π ′ ∈ mix (X) such that h consistent with π ′ . Then there exists a π ′′ ∈ X such that h consistent with π ′′ . Thus, π ∈ mix (X). Theorem 6. L = (CShields, ⊑) is a complete lattice, where for ( ⊔

′

)(h, d) = d iff

(h, d) = d or

( ⊓

′

)(h, d) = d iff

(h, d) = d and

′

∈ L:

(h, d) = d, ′

(h, d) = d.

Proof (Theorem 6). By Lemma 15, mix is a closure operator on (2Π , ⊆). Thus, the family of closed sets forms a complete lattice under inclusion [38]. In this lattice, the meet is set intersection X ⊓ Y = X ∩ Y (since the intersection of closed sets is closed) and the join is the closure of the union X ⊔ Y = mix (X ∪ Y ). We additionally require that the sets of policies allow all safe actions. This is a sublattice: the operations ⊓ and ⊔ are closed under this property, the infimum is the set of all safety-optimal policies, and the supremum is the set of all policies. Theorem 1 establishes an order-isomorphism between the mix -closed sets that allow all safe actions and the canonical shields. Therefore, the canonical shields L = (CShields, ⊑) inherit the lattice structure with the following join and meet: For a mix -closed set of policies P , let cshield (P ) be the canonical shield with allow set P . Then the lattice is characterized by: ⊔

′

⊓

′

= cshield (mix (Allow( ) ∪ Allow( = cshield (Allow( ) ∩ Allow(

′

))),

)).

The above characterization indeed follows from this, using the fact that the above shields allow the union (or cut) of policies and shields are additionally mix -closed. d F Theorem 7. We have pess ⊑ SatShields and opt = SatShields.

L. Heck et al.

Proof (Theorem 7). Proof of

[

SatShields =

opt : We need to show that

Allow( ) = Allow(

opt ).

∈SatShields

“⇒”: Suppose that π ∈ Allow( ∗ ) for some ∈ SatShields. Then, π is safe. As opt satisfies (P+), it follows that π ∈ Allow( opt ). “⇐”: Suppose that π ∈ Allow( opt ). Given any path τ ∈ FinPaths(M), as ′ ′ opt satisfies (S−), there is a safe policy πsafe s.t. πsafe (τ ) = T (π)(τ ) for all ′ prefixes τ of τ . As there is a saturated shield allowing πsafe (invoke proof of Theorem 1 on the shields allowing πsafe ), there exists some saturated shield with πsafe (τ ′ ) = T (π)(τ ′ ) for all prefixes τ ′ of τ . Thus, πsafe (τ ′ ) = TF SatShields (π)(τ ′ ) for all F prefixes τ ′ of τ . As this holds for all paths, by induction, we have π ∈ Allow( SatShields). d Proof of pess ⊑ SatShields: Suppose that π ∈ Allow( pess ). Suppose there is some saturated shield ∗ such that π ∈ / Allow( ∗ ). Then ∗ (h, d) ̸= d for some history h consistent with π and d = π(path(h)). We show that both cases lead to a contradiction: (1) d = d|ActSafe (last(τ )) . Then clearly, ∗ (h, d) = d as ∗ (h, d) is canonical. (2) d ̸= d|ActSafe (last(τ )) . By the proof of Theorem 4, all policies π ′ are safe if π ′ (τ ′ ) = π(τ ′ ) for all prefixes τ ′ of τ . Stated differently, there is no unsafe policy π ′ consistent with h and with π ′ (path(h)) = d. Thus, ∗ (h, d) = d, otherwise, it is not saturated. Lemma 9.

(h,d)∈J

(h,d) is safe if and only if V

(s0 ) ≤ ν.

Proof (Lemma 9). Before we get into the proof, note that we think about the value V (h) as the maximal probability to reach a bad state in an MDP where there is a state of each history present in J ′ , and a transition for each “allowed” choice. In this context, it is easier to see how a policy that follows only allowed choices will be a policy of that MDP and thus be safe, and an unsafe MDP will allow unsafe policies. However, the MDP is annoying to define, so we will instead directly prove the statement for the value equation at hand. F F First, note that = (h,d)∈J (h,d) = (h,d)∈J ′ (h,d) , as all added historydistribution pairs are prefixes which are already allowed by the point shields. F “⇒”: Suppose that the shield = (h,d)∈J ′ (h,d) is safe and suppose that V (s0 ) > ν. Construct the policy π with π(s0 α1 s1 · · · st ) := argmax {C (h, d) | (h, d) ∈ J ′ , h = s0 π(s0 )α1 s1 · · · st } d∈∆(Act)

∪ {Vmin (st )}. For this policy, we have T (π) = π, so π ∈ Allow( ). Moreover, we have Vπ (s0 ) = V (s0 ) > ν. Thus, the shield is unsafe =⇒ Contradiction.

Shields to Guarantee Probabilistic Safety in MDPs

“⇐”: Suppose that V (s0 ) ≤ ν. Let π ∈ Π M be any policy. Then the transformed policy π ′ := T (π) behaves as follows (by Theorem 6): ( dt if (ht , dt ) ∈ J ′ , π ′ (s0 α1 s1 · · · αt st ) = dt |ActSafe (last(ht )) otherwise, where ht = s0 T (π)(s0 ) α1 s1 T (π)(s0 α1 s1 ) α2 · · · αt st , and dt = π(s0 α1 s1 · · · αt st ). We will prove that for all paths τt = s0 α1 s1 · · · αt st , we have Vπ′ (τt ) ≤ V (ht ) by backward induction over t. Then, it follows that Vπ′ (s0 ) ≤ V (s0 ) and thus, the shield is safe. Note: In the context of the MDP mentioned above, we are performing value iteration on an induced Markov chain, and showing that this value is smaller than the maximal value of the entire MDP. The base cases are all t such that (ht , dt ) ∈ / J ′ . Then, Vπ′ (τt ) = V (ht ) = Vmin (last(h)). As the step, suppose (ht , dt ) ∈ J ′ . We have X X V (ht ) = C (ht , dt ) = dt (α) P(last(h), α, s′ ) · V (ht · dt · α · s′ ). α∈Supp(dt )

s′ ∈S

By the induction hypothesis, we know that for all α ∈ Supp(dt ), s′ ∈ S: Vπ (τt · α · s′ ) ≤ V (ht · dt · α · s′ ). Then we have: Vπ (τt ) =

dt (α)

P(last(h), α, s′ ) · Vπ (ht · α · s′ )

s′ ∈S

α∈Supp(dt )

≤

dt (α)

α∈Supp(dt )

P(last(h), α, s′ ) · V (ht · dt · α · s′ )

s′ ∈S

= V (ht , dt ). Theorem 8. Given a sequence of history-choice pairs J = ((h0 , d0 ), . . . , (ht , dt )), let t+1 be the shield from Def. 15. There exists a saturated shield ∗ such that for all 0 ≤ i ≤ t: t+1 (ht , dt ) = ∗ (ht , dt ). Proof (Theorem 8). The shield n+1 is safe by definition of ⊕safe . Consider the set F ⊆ L of safe canonical shields that are more permissive than n+1 . Following the proof of Theorem 5, F has at least one maximal element ∗ , which is a canonical saturated shield. Let (h, d) ∈ H. We show that n+1 (h, d) = ∗ (h, d): – If n+1 (h, d) = d, then ∗ (h, d) = d because n+1 ⊑ ∗ . – If n+1 (h, d) ̸= d, then n+1 ⊔ (h,d) is unsafe by definition of ⊕safe . Therefore, any shield that is more permissive than n+1 ⊔ (h,d) is unsafe, so ∗ (h, d) = d implies that ∗ is unsafe, thus ∗ (h, d) ̸= d. As n+1 and ∗ are canonical, we have n+1 (h, d) = ∗ (h, d) = d|ActSafe (last(h)) .

L. Heck et al.

F Lemma 10. Given a constructed shield = (h,d)∈J (h,d) for a finite J, (h, d) can be computed in time O(|h| · |J| · |Act|), while V (s0 ) can be computed in time O(|J| · L · |Act| · |S|), where L is the length of the longest history in J. Proof (Lemma 10). Proof that (h, d) can be computed in time O(|h| · |J| · |Act|): Suppose that J is given as a finite list. Then one can search whether (h, d) is in J by performing a linear search on the list, which takes time O(|h| · |J|). If the search fails, we need to compute the action projection, which can be done in time O(|Act|). Proof that V (s0 ) can be computed in time O(|J| · L · |Act| · |S|), where L is the length of the longest history in J: We have |J ′ | ≤ |J| + |J| · L, as each history in J has at most L prefixes. Then, one can solve the equation for V by dynamic programming on the directed acyclic graph whose nodes are the elements of J ′ . Considering the evaluation of C , this takes time O(|J| · L · |Act| · |S|). Theorem 9. Let be a safe shield constructed using Def. 15. The policy transformer T ′ as defined below, allows unsafe policies: T ′ (π)(s0 α1 s1 · · · αt st ) :=

t+1 (ht , dt ), where ht := s0 T ′ 1 (π)(s0 ) α1 s1 T ′ 2 (π)(s0 α1 s1 ) α2

dt := π(s0 α1 s1 · · · αt st ), and 0 := , t+1 := t ⊕safe

· · · αt st ,

(ht ,dt ) .

Proof (Theorem 9). Consider the MDP in Fig. 2. For the unsafe policy π = {s0 7→ 1ε , s0 εs1 7→ 1β , s0 εs2 7→ 1δ }, we have T ′ Safe (π) = π: T ′ Safe (π)(s0 ) = (

Safe ⊕safe

(s0 ,1ε ) )(s0 , 1ε ) = 1ε ,

T ′ Safe (π)(s0 εs1 ) = (

Safe ⊕safe

(s0 ,1ε ) ⊕safe

(s0 1ε εs1 ,1β ) )(s0 1ε εs1 , 1β ) = 1β ,

Safe ⊕safe

(s0 ,1ε ) ⊕safe

(s0 1ε εs2 ,1δ ) )(s0 1ε εs2 , 1δ ) = 1δ .

′

T Safe (π)(s0 εs2 ) = (

Lemma 11. Shielding an episode with any fixed constructed shield is safe. Proof (Lemma 11). This is a direct corollary of the definition of (S+).

Shields to Guarantee Probabilistic Safety in MDPs

Extended Evaluation

In this section, we provide more insight into the setup of the experiments and provide more empirical results. B.1

Evaluation Explanation

For Table 2 we report the value of reaching a bad state and the expected allowed choices for the first 50 steps (as this was the episode length we used for all of our experiments). To evaluate the shields, we construct the induced DTMC based on the shielded choices and perform model checking to obtain the results. On optimistic ( opt ) and online ( onl ) shields, this is not possible as for opt we would need to unfold every possible path while the risk is below the threshold3 and the online shield constantly changes so we cannot construct a single object for model checking. In these cases, we evaluate the shielded agent via simulations. We run one million simulation steps (for an episode length of 50, this equals to at least 20,000 completed episodes) three times and report the average value from these runs. The offline ( off ) used in the experiments was constructed on one million steps of the agent. B.2

Complete Results

This section includes the complete versions of the Tables 2 and 3, with all of the omitted results included here. Tables 5 and 6 contain the extended results for the Table 2. Table 7 reports the total runtime in seconds of the simulator with the equipped shield. B.3

Influence of Data on Construction Scalability

We report the influence of changing the number of construction steps and episode length on the construction time performance. Table 9 showcases the speedup in the number of shield queries per second for the online shield as the number of construction steps grows. Table 8 shows how the number of online shield queries per second decreases when using longer episode lengths. These results show that considering lengthy episodes is the most costly characteristic for the online shield, but even in the case where episode length 200 was considered and the runtime was slowest, the average shield query takes less than 4ms as the numbers in the table include the overhead from the simulator.

Theoretically, this is possible, but in practice this is often infeasible.

L. Heck et al.

Towards Sliding-Window Constructed Shields

Shields (Def. 3) have access to the full history. However, practical limitations provide motivation for considering shields that have access to less information. We first introduce a shield that observes the equivalence class of the history: Definition 19 (∼-Shield). Let ∼ be an equivalence relation on histories. A ∼-shield ∼ is a function Hist(M)/∼ × ∆(Act) → ∆(Act). For a history h ∈ Hist(M) and choice d ∈ ∆(Act), we write ∼ (h, d) := ∼ ([h]∼ , d). The existing safety and permissiveness guarantees remain the same. However, it is helpful to define a ∼-variant of saturated permissiveness: Guarantee (∼-P*): ∼-Saturated Permissiveness. For all π ∈ ΠM \ Allow( ), there is no safe ∼-shield ′ such that Allow( ) ∪ {π} ⊆ Allow( ′ ). We say that a history h ∈ Hist(M) is ∼-consistent with policy π if there exists a history h′ ∼ h such that h′ is consistent with π. We obtain the lattice structure by defining mix ∼ : Definition 20 (∼-History Mixing). Given a set of policies P ⊆ ΠM , the ∼-history mixing is the set mix ∼ (P ) ⊆ ΠM such that π ∈ mix ∼ (P ) if: ∀h ∈ Hist(M). h is ∼-consistent with π =⇒ (∃π ′ ∈ P. h is ∼-consistent with π ′ ). We now give an instance of ∼-shields: A sliding-window shield has access to the last n history elements. Definition 21 (Sliding-Window Shield). Given a window size n ∈ N with n ≥ 0, a sliding window-shield is a ∼n -shield, where h ∼n h′ :⇔ h|n = h′ |n and h|k := st−k dt−k αt−k+1 · · · st is the history suffix of length k, 0 ≤ k ≤ t. Now consider sliding-window shields and ∼n -saturated permissiveness. We can define a ∼n -value of shield from Def. 13 by replacing all histories with their respective equivalence classes. Note that while this construction does not necessarily go through for arbitrary equivalence relations (e.g., if the abstraction does not preserve the current state last(h), it is well-defined for ∼n . In the case of ∼n , this is a Bellman operator of a (potentially cyclic) MDP. One can then show a version of Lemma 9.

39 Shields to Guarantee Probabilistic Safety in MDPs

Table 5. Comparison of different shields. The second column reports the safety values of the unshielded agents. The other columns report the safety value of the shielded agent and the ratio of allowed actions (higher is better). For each row, the most permissive safe shields are in boldface. For shields marked with *, the results are obtained using simulations and are thus subject to a statistical imprecision.

Model

corridor

dpm

timid (.125)

greedy (.125)

Agent (value)

0.05 0.1 0.2

.000 .771 .000 .771 .000 .771

.000 .116 .000 .116 .000 .116

.000 .020 .000 .020 .000 .020

SAFE

.000 .981 .000 .981 .000 .981

.000 .771 .000 .771 .000 .771

.000 .116 .000 .116 .000 .116

.000 .020 .000 .020 .000 .020

UNSAFE

.131 .131 .131

.063 .063 .063

.479 .479 .479

=1 =1 =1

.000 .116 .000 .116 .000 .116

.000 .020 .000 .020 .125 =1

.000 .020 .000 .020 .125 .735

UNSAFE

.029 =1 .028 =1 .029 =1

.002 =1 .002 =1 .002 =1

.165 =1 .161 =1 .165 =1

.731 =1 .732 =1 .729 =1

.000 .020 .100 .408 .125 =1

.000 .020 .101 .209 .125 =1

UNSAFE

.000 .794 .000 .794 .000 .794

.000 .979 .000 .979 .000 .979

.000 .767 .000 .767 .000 .767

.000 .116 .000 .116 .000 .116

.000 .020 .000 .020 .000 .020

SAFE

∗ pess

.005 .831 .005 .831 .005 .831

.000 .979 .000 .979 .000 .979

.010 .790 .047 .839 .062 .870

.049 .134 .098 .153 .199 .190

.000 .020 .100 .406 .124 .993

.000 .020 .100 .204 .125 .936

SAFE

∗ onl

.006 .841 .006 .841 .006 .841

.000 .981 .000 .981 .000 .981

.010 .792 .050 .848 .097 .908

.050 .142 .100 .148 .200 .215

.000 .020 .100 .406 .125 .997

.000 .020 .100 .202 .125 .968

SAFE

of f

.006 .839 .037 .989 .131 =1

.000 .981 .010 .984 .063 =1

.009 .794 .044 .844 .155 .924

.000 .116 .000 .116 .000 .116

.000 .020 .000 .020 .125 .925

.000 .020 .000 .020 .125 .735

SAFE

∗ opt

random (.733)

0.01 0.05 0.2

.000 .981 .000 .981 .000 .981

.000 .798 .000 .798 .000 .798

δ+

greedy (.479)

0.01 0.05 0.2

.000 .798 .000 .798 .000 .798

timid (.063)

0.01 0.05 0.2

Safe

random (.131)

L. Heck et al. 40

Table 6. Comparison of different shields. The second column reports the safety values of the unshielded agents. The other columns report the safety value of the shielded agent and the ratio of allowed actions (higher is better). For each row, the most permissive safe shields are in boldface. For shields marked with *, the results are obtained using simulations and are thus subject to a statistical imprecision.

Model

drone

drone-b

timid (.014)

greedy (.240)

Agent (value)

0.01 0.05 0.2

.000 .160 .000 .160 .000 .160

.000 .722 .000 .722 .000 .722

.000 .554 .000 .554 .000 .554

.000 .207 .000 .207 .000 .207

SAFE

.000 .987 .000 .987 .000 .987

.000 .160 .000 .160 .000 .160

.000 .722 .000 .722 .000 .722

.000 .554 .000 .554 .000 .554

.000 .207 .000 .207 .000 .207

UNSAFE

.016 .764 .101 .764 .101 .764

.000 .987 .014 .999 .014 .999

.000 .160 .000 .160 .139 .915

.052 .839 .052 .839 .052 .839

.002 .728 .002 .728 .014 =1

.001 .211 .001 .211 .240 =1

UNSAFE

.785 =1 .782 =1 .781 =1

.015 =1 .014 =1 .015 =1

.000 .160 .052 .260 .586 .967

.270 =1 .269 =1 .269 =1

.014 =1 .014 =1 .015 =1

.161 .591 .234 .813 .242 =1

UNSAFE

.000 .762 .000 .761 .000 .761

.000 .987 .000 .987 .000 .987

.000 .160 .000 .160 .000 .160

.000 .719 .000 .721 .000 .722

.000 .558 .000 .558 .000 .557

.000 .207 .000 .207 .000 .207

SAFE

∗ pess

.010 .762 .042 .764 .044 .763

.002 .989 .002 .989 .002 .989

.000 .160 .050 .247 .197 .733

.000 .721 .000 .723 .000 .722

.009 .808 .008 .811 .009 .810

.009 .214 .049 .254 .160 .538

SAFE

∗ onl

.010 .763 .050 .765 .074 .766

.004 .990 .004 .990 .004 .990

.000 .160 .050 .256 .200 .743

.000 .722 .000 .722 .000 .722

.010 .830 .011 .855 .011 .855

.010 .218 .050 .259 .200 .656

SAFE

of f

.000 .762 .000 .762 .000 .762

.000 .987 .000 .987 .000 .987

.000 .160 .000 .160 .000 .160

.000 .722 .006 .749 .027 .812

.000 .554 .000 .554 .001 .640

.000 .208 .000 .208 .054 .239

SAFE

∗ opt

random (.962)

0.01 0.05 0.2

.000 .987 .000 .987 .000 .987

.000 .762 .000 .762 .000 .762

δ+

greedy (.912)

0.01 0.05 0.2

.000 .762 .000 .762 .000 .762

timid (.016)

0.01 0.05 0.2

Safe

random ( =1)

Shields to Guarantee Probabilistic Safety in MDPs

Table 7. Comparison of runtimes of different shields. We report the time it took to shield one million actions in seconds (including the simulation overhead). For all experiments, we used greedy agent and ν = 0.2. |M |

Safe

δ+

opt

pess

onl

off

corridor 15 dpm 797 drone 1859 drone-b 87k

373 351 377 462

454 454 340 340 386 386 454 454

536 418 555 664

528 772 383 647 429 1471 590 1106

476 447 608 552

Model

Table 8. Runtime comparison of the construction for the greedy agent with increasing number of steps used for construction. We report the average number of shield queries per second. Model

|M |

corridor 15 dpm 797 drone 1859 drone-b 87k

63k 126k 253k 500k 1.1k 1.4k 0.5k 0.8k

1.2k 1.4k 0.6k 0.9k

1.4k 1.4k 0.6k 0.9k

1.5k 1.8k 1.9k 1.4k 1.6k 1.7k 0.7k 0.7k 0.8k 0.9k 0.9k 0.9k

Table 9. Runtime comparison of the construction for the greedy agent with increasing episode length used for construction. All constructions ran for 1 million shield calls. We report the average number of shield queries per second. Model

|M |

corridor 15 dpm 797 drone 1859 drone-b 87k

75 100 200

2.0k 1.9k 1.8k 1.7k 1.4k 0.9k 2.3k 2.1k 1.6k 1.2k 1.1k 0.8k 2.2k 1.1k 0.7k 0.5k 0.4k 0.3k 1.9k 1.1k 0.9k 0.7k 0.7k 0.5k

Record · ID 175287 · SHA-256 acda79e445ea9b6c
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.