1 Introduction↩︎

Reinforcement learning (RL) [1] optimizes the behavior of an agent taking actions in an unknown environment, generally modeled as a Markov decision process (MDP). While success stories of RL have reached into key areas, such as robotics [2], game playing [3], and autonomous driving [4], safety in RL remains a major concern. In particular, state-of-the-art RL algorithms let agents explore actions unrestrictedly and will thus inevitably select potentially harmful actions [5].

This unsafe exploration problem has triggered research on shielded RL [6]. A shield is a mechanism that prevents (“shields”) RL agents from executing unsafe actions. Shields have been developed for MDPs [7], [8] as well as partially observable MDPs (POMDPs) [9]. To guarantee safety, these approaches require knowing the MDP’s transition dynamics relevant to safety. However, in typical RL problems, these dynamics are unknown. Instead, our starting assumption is to have access to some prior data on the dynamics, whether from previous executions or a simulator. One solution is to use this data to learn point estimates of the dynamics, but doing so introduces statistical errors [10] that compromise the shield’s safety guarantees. An alternative is to learn an uncertainty set around each unknown transition probability that is probably approximately correct (PAC), contains the true probability with high confidence [11], [12]. Unfortunately, existing shielding approaches are limited to models with exact probabilities and thus incompatible with such uncertainty sets and PAC bounds.

1.0.0.1 Contributions: shielding robust MDPs.

We address this gap by developing a novel shielding framework for MDPs with sets of transition probabilities, known as robust MDPs (RMDPs) [13]. An RMDP can be seen as a game between the agent, which chooses the actions, and an adversary, which chooses transition probabilities from the uncertainty sets. Intuitively, our shield prevents the agent from deploying any policy that leads to unsafe outcomes under any choice by the adversary. As is common in shielding [6], [7], we adopt linear temporal logic (LTL) as a specification language, focusing on the safety fragment for algorithmic purposes [14]. When used to constrain the agent’s policy, our shield guarantees that, regardless of the choices by the adversary, the probability of satisfying a given LTL formula meets a prescribed threshold. As depicted in 1, we can instantiate our framework to shield unknown MDPs in two steps:

1. We use sampled transitions in the environment to learn the transition probabilities of the (unknown) MDP as an RMDP with PAC guarantees, the RMDP “contains” the true MDP with a prescribed (high) confidence probability \(\delta\). As common in shielding [6], we do not need to learn all probabilities, but instead only those relevant to the safety specification.

2. Based on the learned RMDP, we construct a shield. The shield restricts the agent’s choices to a subset of probability distributions over actions. When used to constrain the actions of the agent on the true MDP, the shield guarantees that, with the same confidence probability \(\delta\), the safety LTL formula is satisfied with at least the desired threshold probability.

As a key contribution, we prove, under mild assumptions detailed in 1 2, that our shield is both sound and optimal on the RMDP: every policy admissible under the shield is safe and, conversely, every safe RMDP policy is admissible under the shield. Since the RMDP converges to the true MDP as the number of sampled transitions increases, this optimality carries over to optimality for the MDP in the limit. Thus, our shield guarantees safety on the true MDP at any point with high confidence – both during learning and execution – and is minimally restrictive to the learning agent, enabling it to converge to optimal rewards as the quality of the learned RMDP increases. We demonstrate these results empirically and, by contrast, show that state-of-the-art shielding for learned MDPs with point estimates of probabilities can violate safety.

1.0.0.2 Related work.

Safety in RL is an active area of research [5], [15], [16]. Shielding has proved to be a successful approach to block unsafe actions during training and execution [6], [8], [9], [17]–[21]. Closest to our approach is the probabilistic shielding for MDPs proposed in [7], which, however, assumes knowledge of the underlying MDP. Here, we consider the more challenging case of RMDPs and thereby shielding unknown MDPs learned as an RMDP. Existing shields on learned dynamics generally lack finite-sample guarantees by relying on, Monte Carlo sampling [22] or learned latent representations [23]. To our knowledge, the only existing RMDP shielding approach is [24], which considers RMDPs with intervals of probabilities (interval MDPs) and iteratively expands the allowed actions per state, yielding sound but overly conservative shields as a permissive policy [25].

Lagrangian approaches [26], [27] convert safety-constrained MDPs into unconstrained problems with dual variables to penalize cost violations in the reward objective. Recent works extend these ideas to robust constrained MDPs [28], [29]. While often empirically effective, these methods cannot provably guarantee safety at any time (as opposed to shields), thus limiting their use in safety-critical scenarios.

Lyapunov-based methods enforce safety by satisfying a Lyapunov decrease condition defined w.r.t. a safe baseline policy [30], [31], where guarantees depend on accurate safety critics and linearizations. In [32], Gaussian processes (GP) are used for model-based RL, but guarantees rely on the GP prior and a known Lyapunov function, which is hard to construct in practice. Finally, Dyna-style model-based RL uses rollouts on learned models to generate data for model-free agents [33]–[35], which reduces required system interactions but cannot give formal safety guarantees as shields do.

1.0.0.3 Overview.

After the preliminaries in 2, we present our shields for RMDPs in 3. We discuss the setting of shielding unknown MDPs in 4 and empirically evaluate our approach in 5. Throughout the paper, we focus on intuition for our results and instead present all rigorous details about, measure-theoretic constructions, and proofs for our results in the appendix.

2 Preliminaries↩︎

A Markov decision process (MDP) is a tuple \(\mathcal{M}=\langle S,A,P,s_\text{init},AP,L \rangle\), where \(S\) is an (in)finite set of states with initial state \(s_\text{init}\in S\); \(A\) is an (in)finite set of actions;¹ \(P \colon S\times A \to \Delta(S)\) is a transition function; \(AP\) is a finite set of atomic propositions; and \(L \colon S\to2^{AP}\) is the labeling function. We say that \(\mathcal{M}\) is an MDP with rewards if it is additionally equipped with a reward function \(R \colon S\to \mathbb{R}\). For simplicity, we may write \(P(s,a,s')\) instead of \(P(s,a)(\{s'\})\). A finite history in \(\mathcal{M}\) of length \(n\) is a finite word \(h=s_0 a_0 \cdots s_{n-1}a_{n-1}s_n \in S( A S)^n\) for some \(n\in\mathbb{N}\), and we denote its last state \(s_n\) by \(\text{last}\left(h\right)\). An infinite history \(h=s_0 a_0\cdots s_n a_n\cdots\) is defined analogously. A policy \(\pi \colon H \to \Delta(A)\) of \(\mathcal{M}\) is a mapping from the set \(H\) of finite histories to distributions over actions. Fixing a policy \(\pi\) and state \(s \in S\) induces a probability measure \(\text{prob}^{s}_{\mathcal{M},\pi}\) over histories. We write \(\text{prob}_{\mathcal{M},\pi}\) for \(\text{prob}^{s_\text{init}}_{\mathcal{M},\pi}\). For details on policies and induced probability measures, see [36], [37].

2.0.0.1 Safe linear temporal logic.

We express objectives for MDPs in linear temporal logic (LTL) [38]. Following [36], an LTL formula \(\varphi\) over the atomic propositions \(AP\) is generated by the grammar \[\varphi\Coloneqq \top \mid p \mid \neg \varphi\mid \varphi\land \varphi \mid \mathbf{X}\varphi\mid \varphi\,\mathbf{U}\, \varphi, \qquad p \in AP.\] As standard, we define \(\varphi_1 \lor \varphi_2 \mathrel{\vcenter{:}}= \neg(\neg \varphi_1 \land \neg \varphi_2)\), \(\mathbf{F}\varphi\mathrel{\vcenter{:}}= \top \,\mathbf{U}\, \varphi\), and \(\mathbf{G}\varphi\mathrel{\vcenter{:}}= \neg \mathbf{F}\neg \varphi\). A finite (resp. infinite) trace is a sequence \(\tau = b_0b_1\cdots \in \Sigma^*\) (resp. \(\Sigma^\omega\)), where the alphabet \(\Sigma = 2^{AP}\) specifies which propositions hold at each timestep. Given an (in)finite history \(h=s_0 a_0 s_1 a_1 \cdots\), we denote by \(L(h)=L(s_0)L(s_1)L(s_2)\cdots\) the (in)finite trace induced by the labeling function. The satisfaction relation \(\tau,i \models \varphi\) for a formula \(\varphi\) is defined inductively over infinite traces \(\tau = b_0 b_1\cdots\) of \(\mathcal{M}\) as \[\begin{align} {2} \tau,i &\models p &&\iff p \in b_i,\\ \tau,i &\models \neg \varphi&&\iff \tau,i \not\models \varphi,\\ \tau,i &\models \varphi_1 \land \varphi_2 &&\iff \tau,i \models \varphi_1 \text{ and } \tau,i \models \varphi_2,\\ \tau,i &\models \mathbf{X}\varphi&&\iff \tau,i+1 \models \varphi,\\ \tau,i &\models \varphi_1 \,\mathbf{U}\, \varphi_2 &&\iff \exists j \geq i \text{ such that } \tau,j \models \varphi_2 \text{ and } \tau,k \models \varphi_1 \text{ for all } i \leq k < j. \end{align}\] We write \(\tau \models \varphi\) as shorthand for \(\tau,0 \models \varphi\). An LTL formula \(\varphi\) is a safety formula [14] if every violating trace has a finite witness of violation, for every \(\tau \in \Sigma^\omega\) such that \(\tau \not\models \varphi\), there exists a finite prefix \(u \prec \tau\) (called a bad prefix) such that for every \(\rho \in \Sigma^\omega\), \(u\rho \not\models \varphi\). For every safety formula \(\varphi\), there exists a DFA that accepts exactly all bad prefixes of \(\varphi\) [36]:

The transition function extends to finite words as standard: \(\delta^*(q,ua)=\delta(\delta^*(q,u),a)\) for \(u\in\Sigma^*\), \(a\in\Sigma\). A finite word \(u \in \Sigma^*\) is accepted by DFA \(\mathcal{A}\) iff \(\delta^*(q_\text{init},u)\in F\). A specification \(\Phi=\mathbb{P}_{\geq \lambda}(\varphi)\) combines an LTL formula \(\varphi\) and a threshold \(\lambda \in [0,1]\). For a policy \(\pi\), we write \((\mathcal{M},\pi)\models \mathbb{P}_{\geq \lambda}(\varphi)\) iff \(\text{prob}_{\mathcal{M},\pi} \bigl( \{h \mid L(h)\models \varphi\} \bigr) \geq \lambda\), the probability for generating a satisfying trace is at least \(\lambda\).

2.0.0.2 Safe policy optimization.

Our goal is to compute a policy \(\pi\) that (1) maximizes the \(\gamma\)-discounted expected return \(J_{\mathcal{M}}^{\gamma}(\pi) \mathrel{\vcenter{:}}= \mathbb{E}_{\mathcal{M},\pi}^{s_\text{init}} \left[ \sum_{t=0}^{\infty} \gamma^t R(s_t) \right],\) with the expectation taken w.r.t. the probability measure \(\text{prob}^{s_\text{init}}_{\mathcal{M},\pi}\), and (2) ensures the probability of violating a safety LTL formula \(\varphi\) is below a prescribed threshold \(p \in [0,1]\). Formally, this amounts to solving the safe policy optimization problem: \[\pi^\star \in \mathop{\mathrm{arg\,max}}\nolimits_{\pi}\; J_{\mathcal{M}}^{\gamma}(\pi) \quad \text{subject to} \quad (\mathcal{M},\pi)\models \mathbb{P}_{\geq {1-p}}(\varphi).\] If the MDP \(\mathcal{M}\) is known, \(\pi^\star\) can be computed using the probabilistic shielding techniques for MDPs from [7]. Here, however, we assume that the transition function \(P\) is unknown and we only have access to samples from \(P\), rendering existing techniques inapplicable. Instead, we develop a shielding framework for RMDPs (3) and use it to shield a learned RMDP of the unknown MDP (4).

An RMDP with rewards is additionally equipped with a reward function \(R \colon S\to \mathbb{R}\). An RMDP defines a game between the agent that chooses actions via the policy \(\pi\), and an adversary \(\theta\) that chooses probability distributions in \(\mathcal{P}\). Formally, the adversary \(\theta\) is a mapping that associates every finite history \(h \in H\) to a distribution in \(\mathcal{P}(\text{last}\left(h\right), a)\) for every action \(a \in A\). Fixing an adversary \(\theta\) for \(\mathcal{M}_R\) induces a standard MDP [12], denoted by \(\mathcal{M}_R[\theta]\). We say that \(\mathcal{M}_R\) satisfies the specification \(\mathbb{P}_{\geq 1-p}(\varphi)\), denoted as \((\mathcal{M}_R,\pi)\models \mathbb{P}_{\geq 1-p}(\varphi)\), iff \((\mathcal{M}_R[\theta],\pi)\models \mathbb{P}_{\geq 1-p}(\varphi)\) for every adversary \(\theta\).

3 Probabilistic Shields for Robust MDPs↩︎

In this section, we present our shielding approach for RMDPs. We first define our general notion of shield in 3.1, instantiate it to finite RMDPs in 3.2, and show its correctness in 3.3.

3.1 Shields for RMDPs↩︎

A shield may need internal memory to remember enough about the history to determine which actions can still be taken while satisfying the specification. We encode this memory in a controllable monitor, which extends standard monitors (used in, runtime verification [39], [40]) with auxiliary actions.

We will use the auxiliary action to allocate a remaining violation budget, which records how much probability of violating the specification is still allowed over the remaining execution.

To combine an RMDP with a controllable monitor, we construct a product model based on an observation map \(\alpha \colon S \to \Xi\) from the RMDP states \(S\) into the observation space \(\Xi\) of the monitor. The product state \((s,m)\) contains both the RMDP and monitor state, and the product action \((a,u)\) consists of both an RMDP action \(a \in A\) and an auxiliary action \(u \in U\).

Intuitively, choosing action \((a,u)\) in state \((s,m)\) of the product RMDP means that the next RMDP state \(s' \in S\) is given by \(\mathcal{P}(s,a)\), and the next monitor state is \(m' = \zeta(m,\alpha(s'),u)\). 4 extends the usual product between an MDP \(\mathcal{M}\) and a DFA \(\mathcal{A}\), used in model checking [36] and shielding [6], with auxiliary actions. Indeed, this usual product can be recovered with \(\mathcal{M}\otimes_{L} \mathcal{A}\), where \(L\) is the labeling function of the MDP, and the DFA is identified with its associated monitor as in 1.

We can now define our notion of a shield. In a nutshell, a shield specifies, for every observation and monitor state, which randomized choices over (RMDP and auxiliary) actions are allowed.

The shield in 5 is defined over an observation space \(\Xi\), rather than directly over the full state space \(S\). This feature, in particular, allows us to construct shields on a safety abstraction of the RMDP [6]. Let \(\mathcal{M}_R=\langle S,A,\mathcal{P},s_\text{init},AP,L \rangle\) be an RMDP, let \(\mathfrak S=(\mathcal{D},\Gamma)\) be a shield over \((\Xi,A_\Xi)\), and let \(\alpha \colon S \to \Xi\) be an observation map. We say that the shield \(\mathfrak S\) acts on \((\mathcal{M}_R,\alpha)\) if \(A_{\Xi}=A\). As visualized in 2, at runtime, the shield observes only the abstract state \(\xi = \alpha(s)\) and monitor state \(m\), and enforces the agent to select a randomized choice over actions contained in \(\Gamma(\xi,m)\).

3.2 A Shield for Finite RMDPs↩︎

We now instantiate the general shield from 5 to finite RMDPs. Throughout this section, we assume we are given an RMDP \(\mathcal{M}_R\) with finite sets \(S\) and \(A\). Inspired by [7], our construction uses a robust upper bound on the probability of reaching a bad state, formalized as follows.

In our case, the states \(U\) correspond to violating a given safety LTL formula \(\varphi\). This violating set is defined as \(S \times F\) on the product \(\mathcal{M}_R\otimes_L \mathcal{A}\) between the RMDP \(\mathcal{M}_R\) and DFA \(\mathcal{A}=\langle Q,2^{AP},q_\text{init},\delta,F \rangle\) that recognizes the bad prefixes of \(\varphi\). Thus, we use an \((\mathcal{M}_R\otimes_L\mathcal{A}, S \times F)\)-inductive value function \(\beta \colon S \times Q \to [0,1]\). Intuitively, \(\beta(s,q)\) is an upper bound on the probability of violating \(\varphi\) in state \((s,q)\) under an optimal policy and worst-case adversary. To enforce the probability threshold \(p \in [0,1]\), we thus require that \(\beta(s_\text{init},q_\text{init}) \leq p\). Furthermore, we define \(\mathcal{V}_\beta=\prod\nolimits_{(s,q)\in S\times Q} \left[ \beta(s,q),1 \right].\) Each \(v \in \mathcal{V}_\beta\) assigns an admissible violation budget \(v(s,q) \in [0,1]\) to every product state \((s,q)\).

Intuitively, \(\Gamma\) contains those distributions \(\overline{\rho}\) such that the worst-case expected next budget remains below the current budget \(y\). Since the initial budget is at most \(p\), every policy allowed by the shield keeps the worst-case probability of reaching \(S \times F\) (and thus of a bad prefix) at most \(p\).

3.3 Sound and Optimal Shields on Safety Abstractions↩︎

We now analyze the guarantees of the shield from 7. In this section, we return to the setup in 2, where \(\mathcal{M}_R\) may be an infinite RMDP but the observation space \(\Xi\) is finite. Thus, we in fact analyze the shield \(\mathfrak S(\mathcal{M}_R/\alpha,\mathcal{A},\beta)\) for the finite safety abstraction \(\mathcal{M}_R/\alpha\), which is defined as the standard quotient (see 15 in App. 7). Yet, the shield is deployed on the (non-abstracted) RMDP \(\mathcal{M}_R\), so we need to reason about policies on \(\mathcal{M}_R[\overline{\theta}] \otimes_\alpha \mathcal{D}\) for different adversaries \(\overline{\theta}\), on the product of the induced MDP \(\mathcal{M}_R[\overline{\theta}]\) and the monitor \(\mathcal{D}\), relative to the abstraction map \(\alpha\).

We say that a shield is realizable if, after following any compliant policy up to time \(t\), there always exists a continuation policy that is compliant under every adversary.

As a final ingredient for defining soundness and optimality, we need to project policies \(\overline{\pi}\) on \(\mathcal{M}_R\otimes_\alpha \mathcal{D}\) onto the original RMDP \(\mathcal{M}_R\). Intuitively, the projected policy \(\overline{\pi}^\downarrow\) is obtained from \(\overline{\pi}\) by ignoring the monitor component, at each history, it selects actions according to the marginal distribution induced by \(\pi\) over product histories consistent with that history (see 23 for a formal definition).

We now state the main results of this section. Recall \(\mathcal{M}_R\) is an RMDP equipped with a finite safety abstraction \(\alpha:S\to\Xi\), defining the quotient RMDP \(\mathcal{M}_R/\alpha = \langle \Xi,A_\alpha,\mathcal{P}_\alpha,\xi_\text{init},AP,L_\alpha \rangle\). Also, let \(\Phi=\mathbb{P}_{\ge 1-p}(\varphi)\), let \(\mathcal{A}=\langle Q,2^{AP},q_\text{init},\delta,F \rangle\) recognize the bad prefixes of \(\varphi\), and let \(\beta:\Xi\times Q\to[0,1]\) be an \(((\mathcal{M}_R/\alpha)\otimes_{L_\alpha}\mathcal{A},\Xi\times F)\)- inductive value function such that \(\beta(\xi_\text{init},q_\text{init})\le p\).

We say an RMDP \(\mathcal{M}_R\) is conditionally deterministic w.r.t. abstraction \(\alpha\) if every reachable abstract history determines a unique concrete history, for every abstract history \(\widehat h_t=\xi_0a_0\xi_1a_1\cdots a_{t-1}\xi_t\) with \(\xi_0=\alpha(s_\text{init})\), there is at most one concrete history \(h_t=s_0a_0s_1a_1\cdots a_{t-1}s_t\) such that \(s_0=s_\text{init}\), \(\alpha(s_i)=\xi_i\) for all \(i\le t\), and \(h_t\) has positive probability under some adversary of \(\mathcal{M}_R\). We remark that this assumption is trivially satisfied if the safety abstraction \(\alpha\) is the identity. As another example, this assumption is satisfied by the Pacman environment used for our experimental evaluation in Section 5. This assumption is needed for 2 because an optimal safe policy might otherwise induce different safety-relevant behaviors on different concrete states associated with the same abstract history, in which case it might become impossible to certify the safety of that safe optimal policy without some further knowledge of the dynamics of the concrete MDP.

1 2 show that the shield in 7 is sound and approximately optimal, respectively. Furthermore, if the value function \(\beta\) used to define the shield is equal to the exact least fixed point \(\beta^\infty\), then our shield is (exactly) optimal, as long as the corresponding return is well-defined.

4 Shielding Unknown MDPs via Learned RMDPs↩︎

We use the shielding approach from 3 to shield unknown finite MDPs learned as an RMDP. A common approach to learning an unknown (finite) MDP is to estimate transition probabilities from samples and represent the resulting uncertainty via intervals [41]–[45]. For each state-action \((s,a)\) and next state \(s'\), we construct an interval \([\check{P}(s,a,s'), \hat{P}(s,a,s')] \subseteq [0,1]\) and define the uncertainty set \[\mathcal{P}(s,a) = \left\{ \mu \in \Delta(S) \;:\; \forall s' \in S,\; \mu(s') \in [\check{P}(s,a,s'), \hat{P}(s,a,s')] \right\}.\] Suppose that, for a fixed pair \((s,a)\), we obtain \(N_{s,a}\) samples from \(P(s,a)\), out of which \(N_{s,a,s'}\) led to a transition to \(s'\). For any confidence budget \(\tau\in (0,1)\), the Clopper-Pearson confidence interval [46] provides a probably approximately correct (PAC) estimator of the unknown probability \(P(s,a,s')\): \[\mathbb{P}\big\{ P(s,a,s') \in [\check{P}(s,a,s'), \hat{P}(s,a,s')] \big\} \ge 1 - \tau,\] which is defined via the inverse CDF of the beta distribution \(\mathrm{Beta}(\alpha, \nu)\), denoted by \(\mathrm{Beta}^{-1}(\cdot; \alpha, \nu)\): \[\begin{align} \check{P}(s,a,s') &= \begin{cases} 0, & N_{s,a,s'} = 0,\\ \mathrm{Beta}^{-1}(\tfrac{\tau}{2};\,\, N_{s,a,s'},\, N_{s,a}-N_{s,a,s'}+1), \,\,\,\,\,\,\,\,\,\, & \text{otherwise}, \end{cases} \\[0.0em] \hat{P}(s,a,s') &= \begin{cases} 1, & N_{s,a,s'} = N_{s,a},\\ \mathrm{Beta}^{-1}(1-\tfrac{\tau}{2};\,\, N_{s,a,s'}+1,\, N_{s,a}-N_{s,a,s'}), & \text{otherwise}. \end{cases} \end{align}\] By repeating this procedure for every state-action pair, we obtain the transition function \(\mathcal{P}\) for an RMDP such that \(\mathbb{P}\left\{ P \in \mathcal{P}\right\} \geq 1-\psi\cdot \tau,\) with \(\psi\leq |S|^2 \cdot |A|\) the number of transitions in the MDP.

In our experiments, we either assume that (a) the graph of the MDP (and thus \(\psi\)) is known, or (b) the graph of the MDP is unknown, but the minimum probability \(p_\text{min}\) is known (and \(\psi= |S|^2 \cdot |A|\)).

4.0.0.1 Shielding unknown MDPs.

Finally, we use our approach from 3 to shield a learned RMDP \(\widehat{\mathcal{M}}\), representing an unknown MDP \(\mathcal{M}= \langle S,A,P,s_\text{init},AP,L,R \rangle\) equipped with a safety abstraction \(\alpha \colon S\to\Xi\) into a finite set \(\Xi\). We write \(\mathcal{M}/\alpha = \langle \Xi,A_\alpha,P_\alpha,\xi_\text{init},AP,L_\alpha \rangle\) for the quotient MDP (cf. 15), \(\Phi=\mathbb{P}_{\ge 1-p}(\varphi)\) is a specification, and \(\mathcal{A}\) is a DFA for the bad prefixes of \(\varphi\). In the following, we assume we have learned a finite RMDP such that the true \(P_\alpha\) is contained in the learned set \(\widehat\mathcal{P}\), \(P_\alpha(\xi,a)\in\widehat{\mathcal{P}}(\xi,a)\) \(\,\forall (\xi,a) \in \Xi \times A_\alpha\). In practice, this holds with probability \(\geq 1-\psi\cdot \tau\), so this confidence level carries over to 3 4 below.

Let \(\widehat\beta:\Xi\times Q\to[0,1]\) be an \((\widehat{\mathcal{M}}\otimes_{L_\alpha}\mathcal{A},\Xi\times F)\)-inductive value function such that \(\widehat\beta(\xi_\text{init},q_\text{init})\le p\). Then, the shield \(\mathfrak S(\widehat{\mathcal{M}},\mathcal{A},\widehat\beta)\) computed on the learned RMDP \(\widehat\mathcal{M}\) is sound for the unknown MDP \(\mathcal{M}\):

We now present our optimality results, which bound the gap in expected return between the optimal policy under the shield \(\mathfrak S(\widehat{\mathcal{M}},\mathcal{A},\widehat\beta)\), and the optimal safe policy on the true MDP \(\mathcal{M}\). These bounds depend on the total variation abstraction error \(\eta \mathrel{\vcenter{:}}= \sup_{(\xi,a) \in \Xi \times A_\alpha} \sup_{\widehat P\in\widehat{\mathcal{P}}(\xi,a)} \mathrm{TV}(P_\alpha(\xi,a),\widehat P)\), the least fixed points \(\widehat\beta^\infty\) and \(\beta^\infty\) of the Bellman operators \(\mathcal{B}_{\widehat{\mathcal{M}}\otimes_{L_\alpha}\mathcal{A}}^{\Xi\times F}\) and \(\mathcal{B}_{(\mathcal{M}/\alpha)\otimes_{L_\alpha}\mathcal{A}}^{\Xi\times F}\) as in 6, and the parameter \(q_\text{min} = \frac{p_\text{min}\left(\mathcal{M}\right) \cdot p_\text{min}(\widehat\mathcal{M})}{p_\text{min}(\mathcal{M}/\alpha)}\), where \(p_\text{min}(\cdot)\) denotes the minimum transition probability of the respective model. Finally, let \(H_{\max}\) be a uniform upper bound on the expected hitting time to either a bad automaton state or a safe absorbing component, taken over all deterministic \(\mathcal{A}\)-memory policies and all transitions in \(\widehat\mathcal{P}\). As a conservative bound, we may take \(H_{\max}= \frac{|S| \cdot |Q|}{ (q_\text{min})^{|S| \cdot |Q|}}\).

In 4, we again use optimality as per 11 and define \(\widehat\epsilon_\beta \mathrel{\vcenter{:}}= \frac{ \|\widehat\beta-\widehat\beta^\infty\|_\infty }{ \|\widehat\beta-\widehat\beta^\infty\|_\infty + p-\widehat\beta(\xi_\text{init},q_\text{init}) }\) for brevity. To ensure the denominator of \(\epsilon_{\widehat \beta}\) is nonzero, we assume \(\widehat\beta(\xi_\text{init},q_\text{init}) < p\), which in turn implies there exists a policy \(\pi_{\mathrm{sl}}\) and a constant \(\kappa>0\) such that \(\inf_{\widehat\theta} \mathrm{prob}_{\widehat{\mathcal{M}}[\widehat\theta],\pi_{\mathrm{sl}}}(\varphi) \ge 1-p+\kappa.\)

The bounds in 4 separate three sources of suboptimality. First, \(\epsilon_{\widehat\beta}\) comes from using the inductive certificate \(\widehat\beta\) instead of the exact robust fixed point \(\widehat\beta^\infty\). Second, the terms with \(\eta\) quantify the mismatch between the learned RMDP and the true abstraction \(\mathcal{M}/\alpha\). Third, the additional term \(\gamma^T\) in the discounted case is the price of switching after \(T\) steps to a robustly safe Slater policy; increasing \(T\) reduces this switching cost but increases the finite-horizon model error term \(T\eta\).

5 Experimental Evaluation↩︎

We implement our shielding approach and perform numerical experiments to demonstrate our approach for safe reinforcement learning on unknown MDPs via shielding learned RMDPs.

5.0.0.1 Implementation.

Our shielding pipeline for unknown MDPs consists of three steps: (1) Learn an RMDP from sampled transitions; (2) Construct a shield on the learned RMDP; and (3) Run policy optimization with the shield active. We assume access to a simulator of the underlying MDP \(\mathcal{M}\), but crucially do not know its transition function \(P\). For step (1), we use this simulator (in fact, a simulator of the safety abstraction only suffices) to sample transitions for every state-action pair and learn an RMDP \(\widehat\mathcal{M}\) as described in 4 that is correct wrt a specified confidence \(\delta \in (0,1)\). For (2), we run robust value iteration [11], [48] on the product RMDP \(\widehat\mathcal{M}\otimes_L \mathcal{A}\) to compute an inductive value function \(\beta\) (cf. 6) to construct the shield as per 7. For (3), we use reinforcement learning on the MDP simulator with the action space restricted to \(A^{\mathfrak S}(s,m)=\Gamma(\alpha(s),m)\). This space \(A^{\mathfrak S}(s,m)\) is convex and can thus be given by its extremal points. In fact, the set of violation budgets \(\mathcal{V}_\beta\) that satisfy condition 2 in 7 has finitely many extremal points, allowing us to represent and optimize over the shielded action space (see 10.1 for details). In practice, we optimize the policy with PPO [49] and implement a heuristic for choosing the auxiliary actions, described in 10.1.

5.0.0.2 Experimental setup.

We conduct experiments comparing our contributions (cases 3 and 4 below) against two baselines that use state-of-the-art probabilistic shielding for MDPs (cases 1 and 2):

1. Known MDP (MDP). This baseline assumes full knowledge of the true MDP transition probabilities and uses the probabilistic shielding from [7] directly on the exact model. This baseline provides a reference for safety and performance under full knowledge of the MDP.

2. MLE-based Shielding (MLE). This baseline applies the probabilistic shielding from [7] on a learned MDP with maximum-likelihood estimates (MLEs) of the transition probabilities. While this approach often achieves strong reward performance, the lack of uncertainty modeling prevents theoretical guarantees and can lead to unsafe behavior.

3. RMDP Shield with Known Support (Kno). The MDP is unknown and is learned as an RMDP with PAC guarantees, but the graph of the true MDP is known in advance.

4. RMDP Shield with Unknown Support (Unk). Same as setting 3, but the graph of the true MDP is unknown and must instead be learned based on a given minimum transition probability \(p_\text{min}\) as part of the RMDP learning, as described in 1.

We compare these four cases on two variants of three environments: Media Streaming, Color Bomb Gridworld, and Pacman (see 10.2 for detailed descriptions). We learn each RMDP with an overall confidence level of \(0.95\), taking between \(10\)–\(20\,000\) samples per distribution \(P(s,a)\) in the MDP simulator (except for the MDP baseline, which does not use sampling). For each configuration, we report two evaluation metrics: (1) expected discounted reward (rew) is the average episodic return, and (2) specification satisfaction probability (sat) is the empirical probability that an evaluation rollout satisfies the safety specification on 15 episodes. The experiments are run on a server running Ubuntu 24.04.4 LTS, with an Intel Core i7-10700K CPU, 32 GB of RAM, and NVIDIA GeForce RTX 3080 GPU with 10 GB VRAM. The code to reproduce our results is provided in the supplementary material. Our implementation builds upon the MASA library [50], for the PPO algorithm.

5.0.0.3 Discussion.

3 summarizes our experimental results, reporting the averaged metrics (rew and sat) during training as a function of the sample size for each environment. Learning curves showing the evolution of these metrics are deferred to 10.2 to avoid clutter. Finally, all experiments are averaged over three random seeds, and shaded regions show the standard deviation. The MDP baseline corresponds to a perfect-information setting and therefore remains constant across all sample sizes.

First, we observe that Kno and Unk cannot always be evaluated for small sample sizes, as illustrated by Pacman Slippery. In particular, for too low sample sizes, the learned uncertainty sets \(\mathcal{P}(s,a)\) of the RMDP are too large to construct a shield that satisfies the required satisfaction probability of \(1-p\). Increasing the sample size yields tighter sets \(\mathcal{P}(s,a)\), thereby mitigating this issue. For Unk, we additionally need at least a certain minimum number of samples from each distribution \(P(s,a)\) of the MDP to learn the graph structure, as described in 1.

Despite these sampling requirements, 3 shows that the claimed safety probability of \(1-p\) is indeed satisfied empirically by our robust shields (Kno and Unk). As the number of samples increases, the uncertainty sets become progressively tighter, reducing the conservativeness of the robust shield and allowing the methods to achieve increasingly higher expected rewards while maintaining safety. By contrast, the MLE shield frequently fails to satisfy the required safety threshold for small to moderate sample sizes, despite often achieving strong reward performance, in the Pacman environment. The reason is that MLE does not explicitly model uncertainty in the learned probabilities and thus cannot provide safety guarantees.

Overall, our results highlight a trade-off between the data used to learn the RMDP and the shield’s conservatism. For small sample sizes, our robust methods lead to suboptimal rewards, while the specification satisfaction probability remains well above the required threshold. This conservatism is a typical limitation of robust methods, which rely on worst-case reasoning leading to loose bounds for small sample budgets [51], [52]. Nevertheless, as the sample size grows, the learned RMDP becomes a tighter approximation to the true MDP, yielding results close to the baseline with a fully known MDP.

6 Conclusion↩︎

We presented a novel shielding approach for robust MDPs (RMDPs). Our shielding approach is sound and (approximately) optimal and can be used to shield unknown MDPs learned as an RMDP. By using existing sampling methods for learning transition probabilities with PAC guarantees, we construct shields that, with high confidence, ensure safety while remaining minimally restrictive. Our experiments confirmed that, while conservative for small sample sizes, our robust shields guarantee probabilistic safety, whereas shields constructed for MDPs with maximum likelihood estimates do not. In the future, we plan to extend our approach to robust shielding of stochastic games and investigate more sophisticated RMDP learning techniques to reduce the required sample sizes.

7 Extended Preliminaries↩︎

For a standard Borel space \(X\), we write \(\Delta(X)\) for the set of probability measures on \(X\), equipped with the evaluation \(\sigma\)-algebra. When \(X\) is endowed with a Polish topology generating its Borel \(\sigma\)-algebra, we equip \(\Delta(X)\) with the corresponding weak topology; its Borel \(\sigma\)-algebra coincides with the evaluation \(\sigma\)-algebra. For any set-valued map \(f\colon E\to 2^F\), we let \(\operatorname{Gr}(f)\) denote the graph of f, the set \(\{(x,y)\mid x\in E, y\in f(x)\}\).

7.1 Markov Decision Processes↩︎

A Markov Decision Process (MDP) is a tuple \(\mathcal{M}=\langle S,A,P,s_\text{init},AP,L \rangle\), where \(S\) is a standard Borel space of states; \(A\) is a mapping \(A\colon S\to 2^{\mathsf A}\) where \(\mathsf A\) is a standard Borel space of actions, that defines for each \(s\in S\) the actions \(A(s)\) enabled in \(s\), and such that \(\operatorname{Gr}(A)\) is Borel; the transition function \(P \colon \operatorname{Gr}(A) \to \Delta(S)\) is a measurable map; \(s_\text{init}\in S\) is the initial state; \(AP\) is a finite set of atomic propositions equipped with the discrete \(\sigma\)-algebra; and \(L\colon S\to2^{AP}\) is a measurable labeling function. We say that \(\mathcal{M}\) is an MDP with rewards if it is additionally equipped with a measurable reward function \(R\colon \operatorname{Gr}(A)\to \mathbb{R}\). For simplicity, we may write \(P(s,a,s')\) instead of \(P(s,a)(\{s'\})\) when \(\{s'\}\) is measurable. A finite path or history in \(\mathcal{M}\) is a finite word \(h=s_0 a_0 \cdots s_{n-1}a_{n-1}s_n\) in \(S(\mathsf A S)^n\) for some \(n\in\mathbb{N}\) such that \(a_i\in A(s_i)\) for \(i\in \{0,\ldots,n-1\}\). The length of a history \(h=s_0 a_0 \cdots s_{n-1}a_{n-1}s_n\) is \(n\), and we denote its last state \(s_n\) by \(\text{last}\left(h\right)\). An infinite path or infinite history \(h=s_0 a_0\cdots s_n a_n\cdots\) is defined analogously.

For \(n\in\mathbb{N}\), let \(H_n\) be the space of histories of length \(n\), equipped with the trace \(\sigma\)-algebra induced by the product \(\sigma\)-algebra of \(S\times (\mathsf A \times S)^n\) on \(H_n\). A policy of \(\mathcal{M}\) is a sequence \(\pi=(\pi_n)_{n\ge 0}\), where each \(\pi_n\) is a measurable map from \(H_n\) to \(\Delta(\mathsf A)\) such that \(\pi_n(h)(A(\text{last}\left(h\right)))=1\) for any \(h\in H_n\). We denote \(\pi_n(h)(E)\) by \(\pi(E\mid h)\). We write \(\mathrm{HR}\) for the general class of history-dependent randomized policies. A policy \(\pi\in\mathrm{HR}\) is memoryless deterministic if there exists a measurable map \(d\colon S\to\mathsf A\) such that \(d(s)\in A(s)\) for every \(s\in S\), and for every finite history \(h\), \(\pi(\cdot\mid h)=\mathrm{Dirac}\left(d(\text{last}\left(h\right))\right)\). We write \(\mathrm{MD}\) for the class of memoryless deterministic policies. In the rest of the paper, the policies considered are in \(\mathrm{HR}\) unless stated otherwise.

Fixing a policy \(\pi\) and an initial state \(s \in S\) induces a probability measure \(\text{prob}^{s}_{\mathcal{M},\pi}\) over paths of the MDP \(\langle S,A,P,s,AP,L \rangle\). We write \(\text{prob}_{\mathcal{M},\pi}\) for \(\text{prob}^{s_\text{init}}_{\mathcal{M},\pi}\). For details on policies and induced probability measures, see [36], [37].

7.2 Safe Linear Temporal Logic↩︎

We consider objectives for MDPs expressed in linear temporal logic (LTL). Following [36], an LTL formula \(\varphi\) over the atomic propositions \(AP\) is generated by the grammar \[\varphi::= \top \mid p \mid \neg \varphi\mid \varphi\land \varphi \mid \mathbf{X}\varphi\mid \varphi\,\mathbf{U}\, \varphi, \qquad p \in AP.\] As usual, we define \(\varphi_1 \lor \varphi_2 \mathrel{\vcenter{:}}= \neg(\neg \varphi_1 \land \neg \varphi_2)\), \(\mathbf{F}\varphi\mathrel{\vcenter{:}}= \top \,\mathbf{U}\, \varphi\), and \(\mathbf{G}\varphi\mathrel{\vcenter{:}}= \neg \mathbf{F}\neg \varphi\). A finite (resp. infinite) trace is a sequence \(\tau = b_0 b_1\cdots \in \Sigma^*\) (resp. \(\Sigma^\omega\)), where the alphabet \(\Sigma = 2^{AP}\) specifies which propositions hold at one instant. Given an (in)finite path \(h=s_0 a_0 s_1 a_1 \cdots\), we denote by \(L(h)=L(s_0)L(s_1)L(s_2)\cdots\) the (in)finite trace induced by the labeling function. The satisfaction relation \(\tau,i \models \varphi\) for a formula \(\varphi\) is defined inductively over infinite traces \(\tau = b_0 b_1\cdots\) of \(\mathcal{M}\) as \[\begin{align} {2} \tau,i &\models p &&\iff p \in b_i,\\ \tau,i &\models \neg \varphi&&\iff \tau,i \not\models \varphi,\\ \tau,i &\models \varphi_1 \land \varphi_2 &&\iff \tau,i \models \varphi_1 \text{ and } \tau,i \models \varphi_2,\\ \tau,i &\models \mathbf{X}\varphi&&\iff \tau,i+1 \models \varphi,\\ \tau,i &\models \varphi_1 \,\mathbf{U}\, \varphi_2 &&\iff \exists j \geq i \text{ such that } \tau,j \models \varphi_2 \text{ and } \tau,k \models \varphi_1 \text{ for all } i \leq k < j. \end{align}\] We write \(\tau \models \varphi\) as shorthand for \(\tau,0 \models \varphi\). An LTL formula \(\varphi\) is a safety formula [14] if every violating trace has a finite witness of violation, for every \(\tau \in \Sigma^\omega\) such that \(\tau \not\models \varphi\), there exists a finite prefix \(u \prec \tau\) (called a bad prefix) such that for every \(\rho \in \Sigma^\omega\), \(u\rho \not\models \varphi\). For every safety formula \(\varphi\), there exists a DFA that accepts exactly all bad prefixes of \(\varphi\):

The transition function extends to finite words in the standard way: \(\delta^*(q,ua)=\delta(\delta^*(q,u),a)\) for \(u\in\Sigma^*\) and \(a\in\Sigma\). A finite word \(u \in \Sigma^*\) is accepted by the DFA \(\mathcal{A}\) iff \(\delta^*(q_\text{init},u)\in F\).

A specification \(\Phi=\mathbb{P}_{\geq p}(\varphi)\) combines an LTL formula \(\varphi\) and a threshold \(p \in [0,1]\). For a state \(s\in S\) and policy \(\pi\), we write \((\mathcal{M},\pi,s)\models \mathbb{P}_{\geq p}(\varphi)\) iff \(\text{prob}^{s}_{\mathcal{M},\pi} \bigl( \{h \mid L(h)\models \varphi\} \bigr) \geq p\), the probability for generating a trace satisfying \(\varphi\) is at least \(p\). When \(s=s_\text{init}\), we simply write \((\mathcal{M},\pi)\models \mathbb{P}_{\geq p}(\varphi)\).

7.3 Robust MDPs and Safety Abstractions↩︎

Robust MDPs (RMDPs) extend MDPs with sets of transition probabilities [13].

We say that \(\mathcal{M}_R\) is an RMDP with rewards if, additionally, it is equipped with a measurable reward function. An RMDP defines a game between the agent that chooses actions via the policy \(\pi\), and an adversary \(\theta\) that chooses probability distributions in \(\mathcal{P}\). Formally, an adversary for an RMDP \(\mathcal{M}_R\) is a sequence \(\theta=(\theta_n)_{n\in\mathbb{N}}\), where each \(\theta_n\) assigns to every history \(h\in H_n\) and every action \(a\in A(\text{last}\left(h\right))\) a measure \(\theta_n(h,a)\in\mathcal{P}(\text{last}\left(h\right),a)\), and is measurable as a map \((h,a)\mapsto\theta_n(h,a)\). Fixing an adversary \(\theta\) induces an MDP on the history space \(H=\bigsqcup_{n\in\mathbb{N}}H_n\), whose enabled actions at \(h\in H\) are \(A(\text{last}\left(h\right))\), and whose transition kernel is given by \[P_\theta(h,a)(E) = \theta_n(h,a) \bigl(\{s'\in S: h a s'\in E\}\bigr), \qquad h\in H_n.\] We denote this history MDP by \(\mathcal{M}_R[\theta]\). For an RMDP \(\mathcal{M}_R\) and a policy \(\pi\), we write \(\mathcal{M}_R,\pi\models\Phi\) if, for every adversary \(\theta\) of \(\mathcal{M}\), \(\mathcal{M}_R[\theta],\pi\models\Phi\).

We could directly define a shield on the RMDP \(\mathcal{M}_R\), but often, parts of the state space are unimportant for the satisfaction of the safety formula \(\varphi\). Thus, we follow the common approach of defining a shield on a safety-relevant abstraction of the model [6], defined as follows.

Intuitively, condition 1 requires that all states \(s,s' \in S\) mapping to the same abstract state have the same label and enabled actions, and condition 2 that these states induce the same sets of transition probabilities under the abstraction map. Since \(\alpha\) is surjective and refines the labeling, the induced labeling map \(L_\alpha\colon \Xi\to 2^{AP}\) is well-defined by \(L_\alpha(\xi)=L(s)\) for any \(s\in\alpha^{-1}(\{\xi\})\).

8 Probabilistic Shields for Robust MDPs↩︎

In this appendix, we present all extended definitions, results, and proofs for our RMDP shielding approach from 3.

8.1 Shields for RMDPs↩︎

In this section, we formally define the notion of shield for an RMDP and how it constrains the action choices when deployed on an RMDP. We first define the notion of controllable monitor.

For simplicity, we identify DFAs and their associated controllable monitor. Recall that, for any measurable map \(T\colon X\to Y\) and any measure \(\mu\) on \(X\), the pushforward of \(\mu\) by \(T\) is the measure \(\mu\circ T^{-1}\) on \(Y\) defined by \((\mu\circ T^{-1})(E)=\mu(T^{-1}(E))\) for every measurable set \(E\subseteq Y\).

An observation map for a state space \(S\) is a measurable map \(\alpha\colon S\to\Xi\) into the observation space \(\Xi\) of a controllable monitor.

The above lemma allows us to define the product of an RMDP and a controllable monitor.

We now state our general definition of a shield, which extends 5 from the main paper with the necessary measurability requirements.

8.2 A Shield for Finite RMDPs↩︎

The robust Bellman operator \(\mathcal{B}_{\mathcal{M}_R}^{U}\) acts on functions \(f\in [0,1]^S\) as \[\left(\mathcal{B}_{\mathcal{M}_R}^{U}(f)\right)(s) = \begin{cases} 1, & \text{ if } s\in U,\\[1mm] \displaystyle \inf_{a\in A(s)}\;\sup_{\mu\in\mathcal{P}(s,a)} \mathbb{E}_{s'\sim \mu} \left[f(s')\right], & \text{otherwise.} \end{cases}\]

In the following, we let \(\mathcal{M}_R=\langle S,A,\mathcal{P},s_\text{init},AP,L,R \rangle\) with \(A\colon S\to 2^{\mathsf A}\) be a finite RMDP, we let \(p\in [0;1]\) be a safety threshold, and we let \(\Phi=\mathbb{P}_{\geq 1-p}(\varphi)\) be a probabilistic safety LTL formula. We let \(\mathcal{A}=\langle Q,2^{AP},q_\text{init},\delta,F \rangle\) be a DFA recognizing the bad prefixes of \(\varphi\). We additionally let \(\beta\) be an \((\mathcal{M}_R\otimes_{L}\mathcal{A},S\times F)\)-inductive value function such that \(\beta(s_\text{init},q_\text{init}) \leq p\). Finally, we let \(\mathcal{V}_\beta=\prod_{(s,q)\in S\times Q}[\beta(s,q),1]\).

8.3 Realizability, Soundness and Optimality↩︎

For any RMDP \(\mathcal{M}_R=\langle S,A,\mathcal{P},s_\text{init},AP,L \rangle\) with \(A\colon S\to 2^{\mathsf A}\) and monitor observation map \(\alpha\), we say that a shield \(\mathfrak S=(\mathcal{D},\Gamma)\) over \((\Xi,A_\Xi)\) with \(A_{\Xi}\colon \Xi \to 2^{\mathsf A_\Xi}\) acts on \((\mathcal{M},\alpha)\) if \(\mathsf A=\mathsf A_{\Xi}\), and if \(A(s)=A_\Xi(\alpha(s))\) for all \(s\in S\).

If \(\theta\) is an adversary of the RMDP \(\mathcal{M}_R\), we denote by \(\theta^\otimes\) the canonical adversary of the product RMDP \(\mathcal{M}_R\otimes_\alpha\mathcal{D}\) induced by \(\theta\), which is defined as follows. For a product history \(\overline{h}_t\) ending in \((s,m)\), and for a product action \((a,u)\in A(s)\times U\), let \(T_{m,u}\colon S\to S\times M\) be defined by \[T_{m,u}(s') = \bigl(s',\zeta(m,\alpha(s'),u)\bigr).\] Then \[\theta^\otimes_t(\overline{h}_t,(a,u)) = \theta_t(\overline{h}_t^\downarrow,a)\circ T_{m,u}^{-1}.\] A distribution \(\rho\in\Delta(\mathsf A\times U)\) is compliant with \(\mathfrak S\) at a product history \(\overline{h}_t\) ending in \((s,m)\) if \[\rho\in\Gamma(\alpha(s),m).\]

Let \(\overline{\pi}\) be an HR policy on \(\mathcal{M}_R\otimes_\alpha\mathcal{D}\). We say that \(\overline{\pi}\) is compliant with \(\mathfrak S\) up to time \(t\) under the adversary \(\theta\) of \(\mathcal{M}_R\) if \[\mathrm{prob}_{(\mathcal{M}_R\otimes_\alpha\mathcal{D})[\theta^\otimes],\overline{\pi}} \left[ \forall k<t,\; \overline{\pi}(\cdot\mid\overline{H}_k) \in \Gamma(\alpha(S_k),M_k) \right] = 1,\] where \(\overline{H}_k\) is the product history up to time \(k\), and \((S_k,M_k)\) is its last product state.

We say that \(\overline{\pi}\) is compliant with \(\mathfrak S\) up to time \(t\) if it is compliant up to time \(t\) under every adversary \(\theta\) of the base RMDP \(\mathcal{M}_R\). Finally, \(\overline{\pi}\) is compliant with \(\mathfrak S\) if it is compliant up to time \(t\) for every \(t\in\mathbb{N}\).

We use the following concatenation notation for history-dependent randomized policies. Let \(t\in\mathbb{N}\), and let \(\overline{\pi}^-\) and \(\overline{\pi}^+\) be policies on \(\mathcal{M}_R\otimes_\alpha\mathcal{D}\). We define \(\overline{\pi}^-\star_t\overline{\pi}^+\) as the policy that follows \(\overline{\pi}^-\) for the first \(t\) decision times and then follows \(\overline{\pi}^+\). Formally, for every augmented history \(\overline{h}_k\) of length \(k\), \[(\overline{\pi}^-\star_t\overline{\pi}^+)(\cdot\mid \overline{h}_k) = \begin{cases} \overline{\pi}^-(\cdot\mid \overline{h}_k), & k<t,\\[1mm] \overline{\pi}^+(\cdot\mid \overline{h}_k), & k\ge t. \end{cases}\]

Similarly, if \(\overline{\theta}^-\) and \(\overline{\theta}^+\) are adversaries of \(\mathcal{M}_R\otimes_\alpha\mathcal{D}\), we write \(\overline{\theta}^-\star_t\overline{\theta}^+\) for the adversary defined by \[(\overline{\theta}^-\star_t\overline{\theta}^+)_k (\overline{h}_k,\overline{a}) = \begin{cases} \overline{\theta}^-_k(\overline{h}_k,\overline{a}), & k<t,\\ \overline{\theta}^+_k(\overline{h}_k,\overline{a}), & k\ge t. \end{cases}\]

Given a history \(\overline{h}_t=((s_0,m_0),(a_0,u_0),\dots,(a_{t-1},u_{t-1}),(s_t,m_t))\) of \(\mathcal{M}_R\otimes_{\alpha} \mathcal{D}\), its projection onto \(\mathcal{M}_R\) is the history \(\overline{h}_t^{\downarrow}=(s_0,a_0,s_1,a_1,\dots,s_{t-1},a_{t-1},s_t)\).

For two policies \(\pi\) and \(\pi'\) on an RMDP \(\mathcal{M}_R\), and for an adversary \(\theta\) of \(\mathcal{M}_R\), we write \(\pi\equiv_{\theta}\pi'\) if they induce the same probability measure on infinite state-action paths under \(\theta\), \(\mathrm{prob}_{\mathcal{M}_R[\theta],\pi} = \mathrm{prob}_{\mathcal{M}_R[\theta],\pi'}\).

For two policies \(\pi\) and \(\pi'\) on an RMDP \(\mathcal{M}_R\), we write \(\pi\equiv\pi'\) if, for every adversary \(\theta\) of \(\mathcal{M}_R\), \(\pi\equiv_{\theta}\pi'\).

For any two measures \(\mu,\nu\) over a measurable space \((X,\mathcal{F})\), we denote by \(\mathrm{TV}(\mu,\nu)\) their total variation distance, \(\mathrm{TV}(\mu,\nu) = \sup_{A\in\mathcal{F}} |\mu(A)-\nu(A)|\).

For any standard Borel spaces of states \(S\) and actions \(A\), for any \(\gamma\in(0,1)\), we let \(\Omega=(SA)^{\omega}\) equipped with the \(\sigma\)-algebra \(\mathcal{F}_\Omega\) generated by cylinder sets. The discounted Hamming distance on \(\Omega\) is the distance \(d_{\gamma}\) such that, for any two words \(h=s_0a_0s_1a_1\cdots\) and \(h'=s'_0a'_0s'_1a'_1\cdots\), we have \[d_\gamma(h,h') = (1-\gamma)\sum_{t=0}^{\infty}\gamma^t \mathbf{1}\!\left\{(s_t,a_t)\neq (s_t',a_t')\right\}.\]

The discounted Hamming distance is a metric on \(\Omega\), and it satisfies \(0\le d_\gamma(h,h')\le 1\). Given two probability measures \(\mu,\nu\) on \(\Omega\), a coupling of \(\mu\) and \(\nu\) is a probability measure \(\xi\) on \(\Omega\times\Omega\) whose first marginal is \(\mu\) and second marginal is \(\nu\). We denote by \(\Gamma(\mu,\nu)\) the set of all such couplings. We define the \(1\)-Wasserstein distance associated to \(d_{\gamma}\) as the distance \(W_{1,\gamma}\) on \(\Delta(\Omega,\mathcal{F}_\Omega)\) such that \[W_{1,\gamma}(\mu,\nu) = \inf_{\xi\in\Gamma(\mu,\nu)} \int_{\Omega\times\Omega} d_\gamma(h,h')\,\xi(dh,dh').\]

For any RMDP \(\mathcal{M}_R\), and any two policies \(\pi,\pi'\) over \(\mathcal{M}_R\), we define \[\mathrm{TV}_{\mathcal{M}_R}(\pi,\pi') = \sup_{\theta} \mathrm{TV}\!\left( \mathrm{prob}_{\mathcal{M}_R[\theta],\pi}, \mathrm{prob}_{\mathcal{M}_R[\theta],\pi'} \right),\] and, for \(\gamma\in(0,1)\), \[W_{1,\gamma}^{\mathcal{M}_R}(\pi,\pi') = \sup_{\theta} W_{1,\gamma}\!\left( \mathrm{prob}_{\mathcal{M}_R[\theta],\pi}, \mathrm{prob}_{\mathcal{M}_R[\theta],\pi'} \right),\] where the suprema range over all adversaries \(\theta\) of \(\mathcal{M}_R\).

The notion of \(\mathcal{C}\)-completeness is equivalent to \(\mathcal{C}\)-\(0\)-\(\mathrm{TV}\)-completeness, and also to \(\mathcal{C}\)-\(0\)-\(W_{1,\gamma}\)-completeness.

In the rest of the section, we let \(\mathcal{M}_R\) be an RMDP equipped with a finite safety abstraction \(\alpha\colon S\to\Xi\), we let \(\langle \Xi,\mathsf A,A_\alpha,\mathcal{P}_\alpha,\xi_\text{init},AP,L_\alpha \rangle=\mathcal{M}_R/\alpha\), we let \(\Phi=\mathbb{P}_{\ge 1-p}(\varphi)\), we let \(\mathcal{A}=\langle Q,2^{AP},q_\text{init},\delta,F \rangle\) recognize the bad prefixes of \(\varphi\), and \(\beta\colon \Xi\times Q\to[0,1]\) be an \(((\mathcal{M}_R/\alpha)\otimes_{L_\alpha}\mathcal{A},\Xi\times F)\)- inductive value function such that \(\beta(\xi_\text{init},q_\text{init})\le p\).

We proceed with proving the optimality results. In what follows, we let \(\beta^{\infty}\) be the lowest fixed point of \(\mathcal{B}_{(\mathcal{M}_R/\alpha)\otimes_{L_{\alpha}}\mathcal{A}}^{\Xi\times F}\). Furthermore, we say that an RMDP \(\mathcal{M}_R\) is conditionally deterministic w.r.t an abstraction \(\alpha\) if every reachable abstract history determines a unique concrete history. More precisely, for every abstract history \(\widehat h_t=\xi_0a_0\xi_1a_1\cdots a_{t-1}\xi_t\) with \(\xi_0=\alpha(s_\text{init})\), there is at most one concrete history \(h_t=s_0a_0s_1a_1\cdots a_{t-1}s_t\) such that \(s_0=s_\text{init}\), \(\alpha(s_i)=\xi_i\) for all \(i\le t\), and \(h_t\) has positive probability under some adversary of \(\mathcal{M}_R\). When such a concrete history exists, we denote its last state by \(\chi(\widehat h_t)=s_t\).

Notice that by Lemma 5, the above theorem implies that the shield \(\mathfrak S(\mathcal{M}_R/\alpha,\mathcal{A},\beta)\) is \(\mathrm{HR}\)-\(\epsilon\)-\(W_{1,\gamma}\)-complete over \((\mathcal{M}_R,\alpha)\) for \(\Phi\) as well.

By Lemma 7, we have the following.

9 Probabilistic Shielding for Unknown MDPs↩︎

In this appendix, we present all extended definitions, results, and proofs for our shielding approach for unknown MDPs, learned as RMDP from 4.

Throughout, we suppose that \(\mathcal{M}=\langle S,A,P,s_\text{init},AP,L,R \rangle\) is an MDP equipped with a finite abstraction \(\alpha\colon S\to\Xi\), we let \(\mathcal{M}/\alpha = \langle \Xi,A_\alpha,P_\alpha,\xi_\text{init},AP,L_\alpha \rangle\) by its quotient, we suppose that \(\Phi=\mathbb{P}_{\geq 1-p}(\varphi)\) is a probabilistic safety LTL formula, that \(\mathcal{A}=\langle Q,2^{AP},q_\text{init},\delta,F \rangle\) is a DFA recognizing the bad prefixes of \(\varphi\), and that \(\widehat{\mathcal{M}}=(\Xi,A_\alpha,\widehat{\mathcal{P}},\xi_\text{init},AP,L_\alpha,R_\alpha)\) is an RMDP with \(P_\alpha\in \widehat{\mathcal{P}}\). Furthermore, we suppose that \(\widehat \beta\) is an \((\widehat{\mathcal{M}}\otimes_{L_\alpha}\mathcal{A},\Xi\times F)\)-inductive value function such that \(\widehat\beta(\xi_\text{init},q_\text{init})\leq p\).

9.1 Soundness of the Shield for Unknown MDPs↩︎

We first prove the soundness result from 3.

9.2 \(\mathrm{TV}\)-Completeness of the Shield for Unknown and Finite MDPs↩︎

In the following, we use policies with randomized memory. Formally, a memory-based randomized policy (MBR policy) on an RMDP \(\mathcal{M}_R\) is specified by a standard Borel memory space \(\mathsf Z\), an initial memory distribution \(\lambda\in\Delta(\mathsf Z)\), a measurable action-selection kernel \[\sigma\colon S\times\mathsf Z\to\Delta(\mathsf A),\] and a measurable memory-update kernel \[\upsilon\colon \mathsf Z\times S\times\mathsf A\times S\to\Delta(\mathsf Z),\] such that \(\sigma(s,z)(A(s))=1\) for all \((s,z)\in S\times\mathsf Z\). Such a policy is executed as follows. First, an initial memory state \(z_0\sim\lambda\) is sampled. At time \(t\), after observing the current state \(s_t\) and holding memory \(z_t\), the controller samples \[a_t\sim\sigma(s_t,z_t).\] After the next state \(s_{t+1}\) is generated by the measure selected by the adversary, the memory is updated according to \[z_{t+1}\sim \upsilon(\cdot\mid z_t,s_t,a_t,s_{t+1}).\]

Although MBR policies are useful as compact representations, in our setting, they do not induce more state-action path laws than HR policies. Indeed, every MBR policy admits an adversary-uniform HR realization.

Bernoulli mixtures of policies are a special case of MBR policies. Let \(\Pi^0\) and \(\Pi^1\) be two policies on the same RMDP, and let \(\varepsilon\in[0,1]\). We write \[(1-\varepsilon)\Pi^0\oplus\varepsilon\Pi^1\] for the policy that first samples \(Z\in\{0,1\}\) with \(\Pr(Z=1)=\varepsilon\), and then follows \(\Pi^Z\) for the whole execution. We call \(\oplus\) an external mixture. It should not be confused with the combination of policies that, at each history, independently randomizes between the action distributions of \(\Pi^0\) and \(\Pi^1\).

We now define the policy class used in the following completeness theorem. Throughout this paragraph, \(\mathcal{M}\) is finite. Let \(\mathfrak D_{\mathcal{A}}(\mathcal{M})\) be the finite set of maps \(d\colon S\times Q\to\mathsf A\) such that \(d(s,q)\in A(s)\) for every \((s,q)\in S\times Q\).

For every \(\lambda\in\Delta(\mathfrak D_{\mathcal{A}}(\mathcal{M}))\), let \(\Pi_\lambda\) be the MBR policy:

• memory space \(\mathsf Z=\mathfrak D_{\mathcal{A}}(\mathcal{M})\times Q,\)

• initial memory distribution \(\lambda\otimes\mathrm{Dirac}\left(q_\text{init}\right),\)

• action-selection kernel \(\sigma(s,(d,q))=\mathrm{Dirac}\left(d(s,q)\right),\) and

• memory-update kernel \(\upsilon(\cdot\mid(d,q),s,a,s') = \mathrm{Dirac}\left((d,\delta(q,L(s')))\right).\)

Thus \(\Pi_\lambda\) first samples a deterministic map \(d\), keeps it fixed for the whole execution, and uses the DFA state as finite memory. Furthermore, we define \[\mathcal{C}_{\mathcal{A}}(\mathcal{M}) = \left\{ \Pi_\lambda^\flat: \lambda\in\Delta(\mathfrak D_{\mathcal{A}}(\mathcal{M})) \right\},\] where \(\Pi_\lambda^\flat\) denotes the HR realization of \(\Pi_\lambda\) from Lemma 9.

In the rest of this section, we assume that the MDP \(\mathcal{M}\) is finite, and that \(\widehat{\mathcal{M}}\) is graph-preserving. We define the minimum transition probability parameter \(\underline p_{\min}\) as \[\underline p_{\min} \mathrel{\vcenter{:}}= \min\left\{ \inf_{\mu\in\widetilde{\mathcal{P}}(s,a)}\mu(s') \;\middle|\; s\in S,\;a\in A(s),\;P(s,a,s')>0 \right\}.\] Furthermore, we define \(N=|S| \cdot |Q|\), \(H_{\max}=\frac{N}{\underline p_{\min}^{\,N}}\), and \[\eta=\sup_{(\xi,a)\in \Xi\times A_\alpha(\xi)} \sup_{\widehat P(\xi,a)\in \widehat{\mathcal{P}}(\xi,a)} \mathrm{TV}(P_\alpha(\xi,a),\widehat{P}(\xi,a)).\]

We assume in the following that there exists a policy \(\pi_{\mathrm{sl}}\) on \(\widehat{\mathcal{M}}\) and a constant \(\kappa>0\) such that \[\inf_{\widehat\theta} \mathrm{prob}_{\widehat{\mathcal{M}}[\widehat\theta],\pi_{\mathrm{sl}}}(\varphi) \ge 1-p+\kappa.\] We identify \(\pi_{\mathrm{sl}}\) with its lift to the concrete state space via \(\alpha\).

9.3 \(W_{1,\gamma}\)-Completeness of the Shield for Unknown MDPs↩︎

We now prove a \(W_{1,\gamma}\)-completeness result. In contrast to the \(\mathrm{TV}\)-completeness theorem above, this result does not require a uniform hitting-time bound. Instead, we only compare the true MDP and the conditional lift over a finite horizon \(T\).

Let \(\widehat{\beta}^{\infty}\) be the least fixed point of \(\mathcal{B}_{\widehat{\mathcal{M}}\otimes_{L_\alpha}\mathcal{A}}^{\Xi\times F}\). Let \(\beta^\infty\) be the least fixed point of \(\mathcal{B}_{(\mathcal{M}/\alpha)\otimes_{L_\alpha}\mathcal{A}}^{\Xi\times F}\). We define \(\Delta_\infty = \|\widehat{\beta}^{\infty}-\beta^\infty\|_\infty\). Since \(\alpha\) is an exact safety abstraction, the least bad-reachability value on the concrete product \(\mathcal{M}\otimes_{L}\mathcal{A}\) is the lift of \(\beta^\infty\), namely \((s,q)\mapsto \beta^\infty(\alpha(s),q)\).

Since the learned product RMDP is finite, choose a policy \(\widehat\pi^\star\) on \(\widehat{\mathcal{M}}\otimes_{L_\alpha}\mathcal{A}\) such that, for every \((\xi,q)\in\Xi\times Q\), \[\sup_{\widehat\theta} \mathrm{prob}_{\widehat{\mathcal{M}}[\widehat\theta],\widehat\pi^\star}^{(\xi,q)} \left[\left\{ h\mid h\models \mathbf{F}(\Xi\times F)\right\} \right] \le \widehat{\beta}^{\infty}(\xi,q).\] We identify \(\widehat\pi^\star\) with its lift to the concrete state space through \(\alpha\).

For an HR policy \(\pi\) on \(\mathcal{M}\) and \(T\in\mathbb{N}\), let \(\pi^{(T)}\) be the policy that follows \(\pi\) for the first \(T\) decision times and then follows the lifted policy \(\widehat\pi^\star\) forever.

9.4 Optimality Results↩︎

We now derive optimality guarantees presented in 4 from the completeness results above. The \(W_{1,\gamma}\)-result already applies to all HR policies. For the \(\mathrm{TV}\)-result, which was proved only for the class \(\mathcal{C}_{\mathcal{A}}(\mathcal{M})\), we first recall that this class is sufficient to attain the optimal value of the finite undiscounted safe policy optimization problem under standard total-reward assumptions.

We are now ready to state our two final optimality results, as presented in 4. The first follows directly from combining Theorem 9, Lemma 16, and Lemma 7.

The following result follows directly from combining Theorem 10 and Lemma 7.

10 Details for Experiments↩︎

10.1 Implementation Details↩︎

In this appendix, we further detail the implementation of our shielding pipeline, in particular, for step (3) of running policy optimization with the shield active. Recall that the transition function \(P\) of the true MDP \(\mathcal{M}\) is unknown, but we instead have access to a simulator. Thus, enabling the shield means that we obtain a shielded simulator MDP \(\overline{\mathcal{M}}^{\mathfrak S} \left(\overline{S},A^{\mathfrak S},P^{\mathfrak S},\overline{s_\text{init}},AP,\overline{L}\right)\), obtained from the restriction of policy distributions allowed by the shield. More precisely, \(\overline{\mathcal{M}}^{\mathfrak S}\) is the MDP with same set of states, labels, labelling, and rewards as \(\mathcal{M}\otimes_{\alpha} \mathcal{D}\), but with action space \(A^{\mathfrak S}(s,m)=\Gamma(\alpha(s),m)\), and probability transition function \[\overline{P}^{\mathfrak S}((s,m),\rho)(E) = \int_{\mathsf A\times U} \overline{P}((s,m),(a,u))(E)\, \rho(d(a,u)).\] Given the definition of \(\Gamma\), the space \(A^{\mathfrak S}(s,m)\) is convex, and, for optimization purposes, \(A^{\mathfrak S}(s,m)\) can be taken as its extremal points. Furthermore, since \(\Gamma(\alpha(s),m)\) is defined over \(\overline{\mu}\in\Delta(\mathsf A\times\mathcal{V}_\beta)\) by a single scalar inequality, an extremal point of \(A^{\mathfrak S}(s,m)\) is always a mixture of at most two Dirac distributions over \(A\times U\). In addition, for a fixed action distribution \(\mu\) over two actions \(a\) and \(a'\), the set of all auxiliary actions \((v,v')\) that satisfy compliance with the shield is a convex polytope itself. More precisely, for any action distribution \(\mu\), the set of all possible auxiliary actions for every base action \(a\) that satisfy compliance with the shield is the set \(\mathcal{V}_{\lambda}(\xi,q,y)\) of all \((v_a)_{a\in A_\alpha(\xi)} \in \mathcal{V}_\beta^{A_\alpha(\xi)}\) such that \[\sum_{a\in A_\alpha(\xi)} \mu(a)\sup_{\mu\in\mathcal{P}_\alpha(\xi,a)} \mathbb{E}_{\xi'\sim\mu} \left[ v_a\bigl(\xi',\delta(q,L_\alpha(\xi'))\bigr) \right] \le y.\]

As a consequence, since we still assume the the quotient \(\mathcal{M}/\alpha\) is finite, the \(\mathcal{V}_\beta^{A_\alpha(\xi)}\) has finitely many extremal points. Thus, we can restrict the action space of \(\overline{\mathcal{M}}^{\mathfrak S}\) to

1. the choice of two actions, of a trade-off \(\lambda\in [0;1]\) between those two action, inducing a distribution \(\mu\) over actions, and

2. the choice of an extremal point of \(\mathcal{V}_{\lambda}(\xi,q,y)\).

In practice, we optimize with PPO [49] over \(\overline{\mathcal{M}}^{\mathfrak S}\), we leave the choice of the trade-off \(\lambda\) to the actor, and implement the following heuristic for the choice of the extremal point of \(\mathcal{V}_{\lambda}(\xi,q,y)\).

10.1.0.1 Auxiliary action heuristic.

We describe the heuristic used to choose the auxiliary actions after the actor has selected a mixed base action. Fix a shield state \((\xi,q,y)\), and let \(\lambda\in\Delta(A_\alpha(\xi))\) be the action distribution selected by the actor. In principle, a compliant shielded action may assign an action-dependent continuation certificate \((v_a)_{a\in A_\alpha(\xi)}\in\mathcal{V}_{\widehat\beta}^{A_\alpha(\xi)}\) satisfying \[\sum_{a\in A_\alpha(\xi)} \lambda(a) \sup_{\widehat\mu\in\widehat{\mathcal{P}}(\xi,a)} \mathbb{E}_{\xi'\sim\widehat\mu} \left[ v_a\bigl(\xi',\delta(q,L_\alpha(\xi'))\bigr) \right] \le y .\] Rather than optimizing over this full polytope, our implementation uses a single shared continuation certificate \(v\in\mathcal{V}_{\widehat\beta}\) for all actions in the support of \(\lambda\). This is conservative but simplifies the shielded action parametrization. Starting from the baseline certificate \(\widehat\beta\), we distribute the available residual budget uniformly by considering the one-dimensional family \[v_m(\xi',q') = \min\{\widehat\beta(\xi',q')+m,1\}, \qquad m\ge 0.\] We then choose the largest margin \(m\) preserving one-step robust feasibility: \[m^\star = \sup \left\{ m\ge 0: \sum_{a\in A_\alpha(\xi)} \lambda(a) \sup_{\widehat\mu\in\widehat{\mathcal{P}}(\xi,a)} \mathbb{E}_{\xi'\sim\widehat\mu} \left[ v_m\bigl(\xi',\delta(q,L_\alpha(\xi'))\bigr) \right] \le y \right\}.\] The auxiliary action used by the shield is \(v_{m^\star}\), i.e. we take \(v_a=v_{m^\star}\) for every action \(a\) in the support of \(\lambda\). If \(m=0\) is already infeasible, then the proposed action distribution \(\lambda\) is not compatible with the shield; in that case the implementation falls back to a precomputed safe distribution witnessing the inductiveness of \(\widehat\beta\).

For finite RMDPs, the map \[m\mapsto \sum_{a\in A_\alpha(\xi)} \lambda(a) \sup_{\widehat\mu\in\widehat{\mathcal{P}}(\xi,a)} \mathbb{E}_{\xi'\sim\widehat\mu} \left[ v_m\bigl(\xi',\delta(q,L_\alpha(\xi'))\bigr) \right]\] is monotone and piecewise affine. Its breakpoints occur only when a coordinate \(\widehat\beta(\xi',q')+m\) reaches \(1\). We therefore compute \(m^\star\) by sorting these saturation breakpoints and scanning the corresponding affine pieces. On the first segment where the robust expectation reaches the budget \(y\), \(m^\star\) is obtained by solving a one-dimensional affine equation. If the robust expectation remains below \(y\) after all coordinates have saturated, then all continuation thresholds can be set to \(1\).

10.2 Additional Experimental Results↩︎

This section reports the full experimental results for each environment considered in the main paper.

10.2.0.1 Environments.

We now provide a description of the environments used to evaluate our approach. These environments have been used in prior work, and their behavior remains unchanged unless stated otherwise. In particular, we consider two variants of the Media Streaming environment, two variants of the Colour Bomb Gridworld, as well as Pacman and its variant, Pacman Slippery, in which the agent may execute slippery actions.

Overall, this results in a total of six environments. For brevity, we provide a detailed description only for the general version of each environment family (three environments in total), while the corresponding variants differ only in the aspects mentioned above.

• Media streaming. The agent manages a data buffer of size \(20\). Packets leave the buffer according to a Bernoulli process with rate \(\mu_{\textit{out}}=0.7\). At each timestep, the agent chooses between two actions \(A=\{\textit{slow},\textit{fast}\}\), which add packets according to Bernoulli rates \(\mu_{\textit{slow}}=0.1\) and \(\mu_{\textit{fast}}=0.9\), respectively. The reward objective is to minimise outage time: the agent receives reward \(-1\) whenever the buffer is empty and \(0\) otherwise. Safety is governed by a counter \(c_t\) recording the number of times the fast action has been used, capped at \(C+1\), with \(C=\lfloor T/2\rfloor\) and \(T=100\). We use the probabilistic safety constraint \[\mathbb{P}_{\geq 0.5} \left( \mathbf{G}(c_t \leq C) \right).\] The environment has \(20 \times 52 = 1040\) states, corresponding to the buffer level and the capped fast-action counter. A related benchmark has been considered in [53].

• Media streaming - Alternative. We also consider a stochastic-safety variant of the media-streaming environment. The buffer dynamics and reward function are the same as above, but safety is governed by a danger level \(d_t\), initialised at \(0\) and capped at \(D_{\max}+1\), where \(D_{\max}=20\). We use the safety constraint \[\mathbb{P}_{\geq 0.5} \left( \mathbf{G}(d_t \leq D_{\max}) \right).\] Under the slow action, the danger level decreases by one with probability \(0.5\), remains unchanged with probability \(0.1\), and increases by one with probability \(0.4\). Under the fast action, the danger level increases by one with probability \(0.8\), remains unchanged with probability \(0.1\), and decreases by one with probability \(0.1\). Thus, the fast action improves the buffer more reliably but tends to increase the probability of entering unsafe states, while the slow action is safer on average but does not guarantee that danger decreases. The full observation is \((d_t,b_t,t)\), giving \(22 \times 20 \times 101 = 44440\) possible observations. Since the buffer affects reward but not safety, the shield uses the abstraction \((d_t,t)\), which has \(22 \times 101 = 2222\) states.

• Colour bomb gridworld. The agent operates in a \(15\times 15\) gridworld, with discrete actions \(A=\{\textit{left},\textit{right},\textit{down},\textit{up},\textit{stay}\}\). Outside the medic states, the intended action is executed with probability \(0.9\), while with probability \(0.1\) the agent slips uniformly to one of the other actions. In medic states, the dynamics are deterministic. The environment contains wall cells, bomb cells, medic cells, and coloured goal regions. At the beginning of each episode, the initial state is sampled uniformly from a fixed set of start states. The agent receives reward \(+1\) upon entering any coloured goal region and reward \(0\) otherwise; after reaching such a goal region, the process is reset to a uniformly sampled start state. The base gridworld has \(15^2=225\) states. We consider the probabilistic safety constraint \[\mathbb{P}_{\geq 0.5} \left( \mathbf{G}\,\neg\mathsf{bomb} \right),\] and an LTL-safety variant \[\mathbb{P}_{\geq 0.99} \left( \mathbf{G} \left( \mathsf{bomb} \Rightarrow \mathbf{F}_{\leq 10} \left( \mathsf{medic} \wedge \mathbf{X}\mathsf{medic} \right) \right) \right).\] The LTL property is represented by a \(22\)-state safety automaton, so the product MDP used by the shield has \(225\times 22 = 4950\) states. A related gridworld has been used in [6].

• Pacman and slippery Pacman. We consider a Pacman-with-coins environment on a \(7\times 10\) map. The environment contains one Pacman agent, one ghost, walls, and collectible coins, with reward \(+1\) obtained when Pacman visits a cell containing an uncollected coin. The full coin-augmented state is combinatorial: the map has \(28\) free cells, giving up to \(2^{28}\) possible coin configurations for each agent–ghost configuration. For shielding, we use a safety abstraction that discards the coins and retains only the positions and directions of Pacman and the ghost. This abstraction has \(4624\) states. The ghost dynamics are stochastic: the ghost chooses an available action directed toward Pacman with probability \(0.4\), and otherwise randomises uniformly over the other available actions with total probability \(0.6\). We use the safety specification \[\mathbb{P}_{\geq 1-p} \left( \mathbf{G}(\mathrm{loc}_{\mathrm{Pacman}} \neq \mathrm{loc}_{\mathrm{Ghost}}) \right),\] where \(p=0.05\) for Pacman and \(0.5\) for Pacman slippery. We also evaluate a slippery variant on the same map and with the same \(4624\)-state safety abstraction. In this variant, the requested Pacman action is executed with probability \(0.9\), while with probability \(0.1\) one of the other actions is executed uniformly at random. The task is to collect as many coins as possible while satisfying the probabilistic safety specification of avoiding the ghost throughout the episode. Similar environments were considered in [6], [7].

We use the shorthand labels MDP, MLE, Kno, and Unk in all plots to indicate the four different cases described in 5.

10.2.0.2 Evaluation metrics.

We report two evaluation metrics:

• Expected discounted reward (rew): the average episodic return, corresponding to an empirical estimate of \(J^\gamma_M(\pi)\).

• Specification satisfaction probability (sat): the empirical probability that a rollout satisfies the specification.

When learning curves are shown, we additionally report the corresponding training-time quantities rew and sat. For each environment, we provide two groups of plots:

1. learning curves over training steps, shown for each sample size (the specific number that changes across the various environments represents the minimum number of samples needed for Unk);

2. averaged performance as a function of sample size.

10.2.0.3 Colour bomb gridworld

10.2.0.4 Colour bomb gridworld – LTL goal

10.2.0.5 Pacman

10.2.0.6 Pacman Slippery

10.2.0.7 Media Streaming

10.2.0.8 Media Streaming – Alternative

References↩︎

---

1. For notational simplicity, we assume every action is enabled in every state (see App. 7 for the case without this restriction).↩︎

2. An RMDP \(\mathcal{M}_R\) is graph-preserving if each induced MDP \(\mathcal{M}_R[\theta]\) has the same graph. For \(\widehat\mathcal{M}\), we can ensure graph-preservation (with the specified confidence budget) by using sufficiently many samples to satisfy 1.↩︎