Shielding Regular Safety Properties in Reinforcement Learning

We thank the reviewer for their time in constructing their review.

Re weaknesses: we point the reviewer to the experiments involving property 3 on our colour grid-world environment, in this instance there is a direct conflict between optimal reward and constraint satisfaction, this is reflected by the fact that normal Q-learning obtains the same optimal reward whereas our shielding approach obtains good reward within the constraints of the problem (i.e. Problem 4.1). Some more extended discussion of this is given in Appendix D.1. Similarly for the deep RL experiments, property 2 conflicts with the optimal reward policy and so blindly maximising reward will result in poor safety performance, this is reflected by the results in Figure 3, we refer the reviewer to Appendix D.2 for more details.

With regards to the CMDP formulation, we agree that CMDPs have limitations, particularly when one considers expected cumulative cost constraints these offer little semantic meaning in terms of safety (see lines 24-26). We consider a CMDP formulation analogous to chance constraints but for a finite horizon H, we believe that this is more appropriate in the context of safety. We cannot provide absolute guarantees (100% safety) due to the statistical error that arises from approximating the dynamics of environment and sampling from the model. We would be grateful if you could share some of the approaches that you mentioned in your review to see if we can draw some parallels to our approach.

Re questions: indeed, there are some similarities between our approach and Carr et. al., in particular, for the deep RL experiment the environment is partially observable. Our approach here is built upon approximate model-based shielding (AMBS) [1], which operates in the most permissive setting (no partial-knowledge of the POMDP transitions) and learns the dynamics of the environment with dreamer-v3. In Carr et. al. they assume access to a graph preserving approximation of the POMDP (known transitions but unknown probabilities) or a partial model, which also overapproximates the transition model of the POMDP, meaning that if there is a (non-zero probability) transition in the POMDP then it will also be in the partial model. This assumption is quite restrictive and as a result the experiments in Carr et. al. are constrained to grid-world environments where it is easy to specify a partial model. In our case, we can deploy our approach in high-dimensional visual-input settings for arbitrary regular safety properties. I would imagine coming up with a partial model for Seaquest would be near impossible given the observation space is very large. Furthermore, in Carr et. al. they consider reach avoid properties whereas we consider a more general class of safety properties (regular), although in principle these can be reduced to avoid properties on the product MDP/MC. That being said, we greatly thank the reviewer for bringing this paper to our attention. We also appreciate the reviewer for flagging some grammatical errors.

[1] Goodall, Alexander W., and Francesco Belardinelli. "Approximate Model-Based Shielding for Safe Reinforcement Learning." ECAI 2023. IOS Press, 2023. 883-890.

We would like to thank the reviewer for taking the time to construct such an insightful review.

We will clear up the questions you have, and I think this will deal with some of the weaknesses you have highlighted.

Re questions:

• When we start using neural networks or deep learning architectures like dreamer-v3 to model the environment dynamics, then most of our guarantees go out the window. However, not all is lost, as Proposition 5.5 still holds so long as the total-variation distance between the belief state representation of dreamer-v3 and the true belief state in the POMDP is upper bounded by the same quantity $\epsilon/H$, this is a bit handwavy, but essentially minimising TV distance between the belief state representation minimises an upper bound on the TV distance between the underlying state of the POMDP and this objective is directly encoded in the dreamer-v3 loss function, some of these details are described in AMBS [1] upon which our experiments are based and [2] provides a more formal proof of this upper bound.

[1] Goodall, Alexander W., and Francesco Belardinelli. "Approximate Model-Based Shielding for Safe Reinforcement Learning." ECAI 2023. IOS Press, 2023. 883-890.

[2] Gangwani, Tanmay, et al. "Learning belief representations for imitation learning in pomdps." uncertainty in artificial intelligence. PMLR, 2020.

• If we have a generative model of the environment that we can query at any time from any state then this does break the standard RL setting and could have several implications, e.g. we could just construct an approximate MDP by sampling many times from each state and do value iteration (or similar) to get an approximate optimal policy without having to interact with the environment. To clarify, Assumption 5.2 means exactly this, we have a black box model of the true environment that we can query at any point from any state. We note that this is a weaker assumption than 5.1 (which also breaks the standard RL setting), although it is still strong. We stress that in our experiments we operate in the most permissive setting, where we don’t have the true probabilities $\mathcal{P}$ or access to a black box model of the environment. Assumption 5.2 is more of a ‘what if’ scenario, how could we still do model checking without the true probabilities $\mathcal{P}$ but with a black box model instead. We want to make it clear that in our experiments we do not have access to a black box model, or the true probabilities and we do Monte Carlo/statistical model checking with the approximate model (which is learned by experience generated from episodes of environment interaction). I think the confusion can be lifted here by understanding that we can do Monte Carlo model checking with either a black box model or with an approximate model it is not limited to either scenario. In Appendix F.2 we investigate the effect of given the shield access to the true probabilities $\mathcal{P}$ and access to sampling from $\mathcal{P}$.
• It would not be possible to check that the TV distance for the next state distribution for some $(s, a) \in S \times A$ is bounded by $\epsilon$ without knowing the actual probability of interest ($\mathcal{P}(\cdot | s, a)$), i.e. we want to know if $D_{TV}(\mathcal{P}(\cdot | s, a), \widehat{\mathcal{P}}(\cdot | s, a)) \leq \epsilon$. We can have an arbitrary high-statistical confidence $(1- \delta)$ that $D_{TV}(\mathcal{P}(\cdot | s, a), \widehat{\mathcal{P}}(\cdot | s, a)) \leq \epsilon$ holds for any given $\epsilon$, provided that the number of samples from $\mathcal{P}(\cdot | s, a)$ is large enough. This constitutes the first half of the proof of Theorem 6.5. In particular, if any state-action pair $(s, a) \in S \times A$ has been visited at least $\mathcal{O}\left(\frac{H^2|\mathcal{S}|^2}{\epsilon^2} \log\left( \frac{|\mathcal{A}||\mathcal{S}|^2}{\delta}\right)\right)$ many times then $D_{TV}(\mathcal{P}(\cdot | s, a), \widehat{\mathcal{P}}(\cdot | s, a)) \leq \epsilon$ holds with probability roughly $(1- \delta)$ up to some constants.
• I don’t think there is any significant impact of assuming that the rewards are in $[0, 1]$, most of our technical statements and proofs are only concerned with safety.

Re minor remarks:

• At a first glance there does seem to be a slight bug in Definition 3.3 but I will double check in (Baier & Katoen 2008).
• I think we tried to exclude $H=0$ here but I don’t think it matters if we use $H \in \mathbb{N}$.
• Indeed, this would be an $\omega$-automaton it might be nice to mention this, thanks for your suggestion.
• Indeed, when we are exact model checking $H$ doesn’t matter that much.
• Yes, that is correct we will make this clearer.
• Yes, I agree this is slightly confusing we will change this and use min.
• No we allow for any arbitrary regular safety properties not only bounded ones. Rather, we simply check the invariant property for a bounded lookahead horizon $H$. Under the assumption (Assumption 6.3) that $H$ is big enough to avoid irrecoverable states (Definition 6.2), then we can guarantee the satisfaction of the unbounded regular safety property for the entire episode length $T$, provided that $p_1$ is chosen appropriately, see Proposition 4.2. Note that we can’t include unbounded eventually as this would not be a safety property (rather liveness).
• We are not claiming that we can check arbitrary PCTL* formula as indeed this suffers from similar problems as LTL. Rather we are checking regular safety properties, we just use PCTL/PCTL* notation to compactly define the regular safety properties in Table 1, rather than provide the full DFA. All the properties in Table 1 are regular safety properties as we can come up with a corresponding DFA for them, we thought that the keen-eyed reader might realise that the formulas in Table 1 are in fact PCTL* formula and not PCTL and thus we tried to add some clarification here. More precise semantics and details for these properties are given in Appendix D.1.

Thank you for your remarks, we will certainly make these points clear in the updated version of our paper.

We thank the reviewer for their time in constructing their review.

Re weakness 1.: Indeed, similar chance constraints have been introduced and studied in several prior works including [1] and [2]. We thank the reviewer for bringing these papers to our attention and I believe paper [2] is cited in our related work section. With regards to [1] our setting is different, we consider discrete state-action MDPs with arbitrary size and transition dynamics, in [1] they consider continuous state-action MDPs with smooth and continuous transition dynamics and the rely on empirical estimation of a CBF to guarantee safety. I could imagine coming up with a CBF for non-smooth and discrete transition dynamics might be problematic. We also consider regular safety properties rather than box-constraints on the state space. Our framework is also flexible enough to be used to effectively shield high-dimensional visual-input settings such as Atari, and thus scales well. [2] can be considered as a shielding approach and is more closely related to our work, however in [2] they assume access to an emergency reset button, most algorithms do not have this privilege. Furthermore, they also consider a problem setting that constrains the cumulative cost below a pre-defined threshold with high-probability (this is formalised in our paper as Problem 4.5), this is distinctly different to our approach that constrains the probability of just one safety-violation (or cost) in the H-step horizon. We provide an exploratory comparison between our problem setup and Problem 4.5 in Appendix G.

Re weakness 2.: To test the flexibility of our framework we first run experiments in a simple tabular setting where we could test each of the model checking paradigms (Appendix F.2), the results in the main paper corresponding to the most permissive setting (no prior model and no prior backup policy). We test with regular safety properties of increasing complexity and demonstrate the importance of using counter-factual experiences to train the backup policy (Appendix F.1). We also run experiments on Seaquest with two different regular safety properties, in total this is really 5 different problems over two different environments. In terms of baselines, we used a Lagrangian version of dreamer-v3 similar to [3], to try and solve the CMDP. Evaluating against other CMDP RL algorithms like PPO-Lag would be disingenuous as PPO-Lag is a model free algorithm (rather than model-based) and would not have the capacity of the dreamer-v3 model and would exhibit significantly slower convergence and worse performance, this is demonstrated in works [3] and [4], where the model-based algorithms dramatically outperform model-free algorithms in terms of safety.

[3] Weidong Huang, Jiaming Ji, Borong Zhang, Chunhe Xia, and Yaodong Yang. 2023. Safe DreamerV3: Safe Reinforcement Learning with World Models. arXiv preprint arXiv:2307.07176524 (2023).

[4] Yarden As, Ilnura Usmanova, Sebastian Curi, and Andreas Krause. 2022. Constrained policy optimization via bayesian world models. arXiv preprint arXiv:2201.09802 (2022).

Re Limitations: Since we consider the most permissive setting where the transition probabilities are unknown and the backup policy is not provided a priori, then we cannot obtain the same strict safety guarantees that classical shielding approaches can. This is a trade-off of course, as classical shielding approaches are restricted to small grid world problems and require a significant amount of engineering effort from one environment to the next, whereas our approach can be used mostly off-the-shelf and operate in high dimensional environments. We can only obtain safety guarantees when the model of the environment is sufficiently accurate, and the backup policy has learned a good safe strategy. However, our guarantees are only probabilistic/statistical, so we can’t make formal statements about the entire system, but we can have well placed confidence in it. Further limitations include: lack of RL convergence guarantees – this is a key open problem with the shielding paradigm in general; reliance on the backup policy to operate safely, although for most settings low reward safe behaviour can be easily learnt (think breaking to a halt in a car); finally, Assumption 6.3 which requires the model checking horizon to be sufficiently large to avoid irrecoverable states, this Assumption is similar to the one made in [5] (think breaking to a halt in a car – it only takes a finite amount of time to stop to a halt).

[5] Thomas, Garrett, Yuping Luo, and Tengyu Ma. "Safe reinforcement learning by imagining the near future." Advances in Neural Information Processing Systems 34 (2021): 13859-13869.

I appreciate the feedback from the authors. However, I still have some disagreements.

With regards to [1] our setting is different, we consider discrete state-action MDPs with arbitrary size and transition dynamics, in [1] they consider continuous state-action MDPs with smooth and continuous transition dynamics and the rely on empirical estimation of a CBF to guarantee safety. I could imagine coming up with a CBF for non-smooth and discrete transition dynamics might be problematic.

This is not true for the reviewer. CBF tries to solve a QP problem (optimization) or reduce loss function (learning-based) with a given dynamic model and can pick an action from the action sets to ensure forward invariance and safety. One can always learn this dynamic model with ML/neural network to do so in the unknown environment settings. And there is no fundamental difference between continuous and discrete settings. Even, a discrete setting is simpler as your optimization variable is reduced to a finite set.

As for the experiments, the ML paper is expected to provide comprehensive experimental studies to show the effectiveness, especially for (Safe) RL community, as training RL is fundamentally unstable and varying.

Given these, I would keep my current score as final.

Thanks for taking the time to construct a response.

I will try to add some clarity as I think the part of the rebuttal you highlighted is not perfectly worded.

I agree that in general discrete settings are easier to deal with than continuous settings. However, there are still some fundamental differences between the scope of our setup and the scope of paper [1]. In [1] the authors assume that the transition dynamics are smooth and continuous, and able to be modelled as an SDE. As a result the authors of [1] also explicitly state that their approach cannot handle hybrid dynamics (joint discrete and continuous dynamics) or discontinuous jump dynamics present in mujoco and safety gym (a popular safe RL benchmark). This has the following consequences:

• The approach in [1] cannot be used to check arbitrary regular safety properties (only invariant properties), if we were to construct the product MDP between the approximated SDE and automaton, this would be a hybrid system (continuous dynamics + discrete transitions in the automaton) which [1] cannot deal with.
• In the deep RL experiments we use Approximate Model-based Shielding (AMBS) [2] (and dreamer-v3) as the backbone of our approach, AMBS has been shown to work effectively for safety gym (see [3]) which the approach in [1] cannot.
• In the deep RL experiments the environment is partially observable and the observation space is discrete but very high-dimensional (approximately 100,000 observations and 32,000 states), in our original statement/rebuttal we claimed that it would be very challenging to learn a smooth and continuous SDE from these dynamics as they are discrete and discontinuous and it is not clear how the approach of [1] might deal with partial observability.

[1] Wang, Yixuan, et al. "Enforcing hard constraints with soft barriers: Safe reinforcement learning in unknown stochastic environments." International Conference on Machine Learning. PMLR, 2023.

[2] Goodall, Alexander W., and Francesco Belardinelli. "Approximate Model-Based Shielding for Safe Reinforcement Learning." ECAI 2023. IOS Press, 2023. 883-890.

[3] Goodall, Alexander W., and Francesco Belardinelli. "Leveraging Approximate Model-based Shielding for Probabilistic Safety Guarantees in Continuous Environments." Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems. 2024.

With regards to our experiments, our paper is a hybrid theoretical and experimental paper, thus we dedicated an equal amount of time in rigorously proving the technical details of our paper and conceiving adequate experimental settings to test our approach.

We thank the reviewer for their time in constructing their review.

Re summary: one minor inconsistency, the backup policy is not necessarily pre-trained, in our experiments the backup policy is trained online with RL to minimise cost, although our framework is flexible enough to allow for a pre-trained/handcrafted backup policy.

Re weaknesses: The goal of our paper is to present a flexible framework for shielding RL policies w.r.t regular safety properties. A precise description of the problem setting is provided in Section 3. In particular, we consider discrete state and action MDPs augmented with a set of atomic propositions and corresponding labelling function – in line with standard model checking formalisms. The problem setup is then precisely described as a CMDP, see Problem 4.1, which introduces a new type of constraint, the (probabilistic) step-wise bounded regular safety property constraint. If you have examples of how our exact problem setup has been studied before we would very grateful if you could share them with us, so that we can improve our paper.

The shield can be used during training and deployment, and we make no distinction between the two settings, this is justified as follows: a key property of shielding is that even after training with a shield the shield still needs to be put in place during deployment of the agent, see [1]. This is unavoidable for us and so the performance of the agent at the end of training will reflect the performance of the agent during deployment (assuming the agent is deployed in the same environment as in training). Solving the problem of mismatch between the training environment and the deployment environment is beyond the scope of our paper.

[1] Alshiekh, Mohammed, et al. "Safe reinforcement learning via shielding." Proceedings of the AAAI conference on artificial intelligence. Vol. 32. No. 1. 2018.

More readable figures are provided in Appendix D.1 and D.2.

Re presentation: We very clearly state the assumptions of the different model-checking paradigms at the beginning of Section 5, each paradigm corresponds to different levels of prior knowledge available, see the global Author Rebuttal for more details. Rather than hone in on the specifics we demonstrate the flexibility of our framework in the tabular setting (where Q-learning is used) and the deep RL setting where Dreamer-v3 is used for both RL and dynamics learning. We thank the reviewer for the spelling and grammatical errors they picked up on.

Re question 1.: The aim of our paper is to present a flexible framework, as such the choice of RL algorithm and dynamics learning depends on the actual environment. In our experiments, we considered tabular RL the obvious choice here is to use tabular Q-learning for task and backup policy optimisation and maximum likelihood to construct the approximate transition probabilities. For the deep RL setting we considered Seaquest (a high-dimensional visual-input Atari game), we opted for dreamer-v3 for both policy optimisation and dynamics learning. For continuous control settings one might consider, for example, TD3 for RL and Gaussian process to model the system dynamics.

Re question 2.: The approximate model is updated with transition tuples $(s’, s, a)$ collected during interaction with the environment. If the agent violates the regular property (enters an accepting state), the experience from this interaction is incorporated in the approximate model, so that the next time the agent is in a similar situation they can more accurately estimate the probability of a safety-violation. In the case of our deep RL approach based on dreamer-v3 we refer the reviewer to AMBS [2] upon which our solution is built.

[2] Goodall, Alexander W., and Francesco Belardinelli. "Approximate Model-Based Shielding for Safe Reinforcement Learning." ECAI 2023. IOS Press, 2023. 883-890.

Re question 3.: Indeed, the types of statistical bounds that we use suffer from the problem of rare events. This issue is exacerbated by the fact that our framework constructs an approximate model of the environment dynamics from experience, if there is a very rare and catastrophic event that we might want to avoid we might never see it during training and be unaware of it and unable to accurately predict the probability of it happening. I believe that such events require special consideration depending on the intended domain. For self-driving cars, we might have to augment our dataset with rare catastrophic experiences. We could then use sampling strategies like importance sampling to try and better understand the risk of these rare events.

Re question 4.: We simply require that the TV distance between the true MC $P(\cdot | s)$ and the approximate MC $\widehat{P}(\cdot | s)$ is bounded by $\epsilon/H$ for all states $s \in S$. This is stated in assumption 5.3. This is all we need to guarantee that we can model check with the approximate model and obtain the same statistical guarantees. So, an arbitrary approximation error of $\alpha$ contributes an error of $\alpha * H$ to the approximation error of the reachability probability, proof details are outlined in Appendix C.4.

Re question 5.: We discuss this in some detail in Appendix D. The main hyperparameter of the colour gridworld environment is the $p$ hyperparameter which corresponds to the level of stochasticity of the environment, for larger $p$ the probability threshold $p_1$ may need to be more permissive to learn a policy with high reward, although in principle any $p_1$ could be used (although you might get a low reward policy). Further experimentation is also detailed in Appendix F.

Re limitations: We believe that our work is transformative at the very least and presents a novel framework for shielding and guaranteeing the safety of RL agents w.r.t an interesting class of safety properties. We provide an extensive literature review which should make it clear where our work lies in the safe RL literature.

We would like to thank the reviewer for their extensive review.

Re weakness 1.: In our paper we consider the most permissive setting where no prior knowledge about the transition probabilities is required. We only require that there is a labelling function defined over the state space of the MDP and that the safety property is a regular safety property given as a DFA. In Section 5 we introduce 3 model checking paradigms, namely exact model checking that assumes the transition probabilities are known (as in previous work), Monte Carlo/statistical model checking with a black box model and model checking with an approximate model of the transition probabilities. As is stated in Proposition 5.5 we can obtain an epsilon-approximate estimate for the corresponding reachability probability in the product MC, either by exact model checking or by statistical model checking with the approximate model, to verify the validity of this statement we refer the reviewer to Appendix C.5 which contains the full proof. The goal of our paper is to develop a framework (or meta-algorithm) that is flexible enough so that it can operate in each paradigm, including the most permissive setting where the approximate model is learned from experience (i.e. no prior knowledge). We stress that these guarantees are probabilistic or analogously PAC as we rely on Hoeffding/Bernstein type bounds for both statistical model checking (Proposition 5.4) and learning the transition probabilities (Theorem 6.5).

Re safety guarantees during learning: Before the model is sufficiently accurate and the backup policy has converged then there are no safety guarantees, this is semi-implied by Theorem 6.5 and the preceding assumption statements. However, as a consequence we can operate in with no prior knowledge.

Re weakness 2.: The results provided in the main paper are obtained under the most permissive setting (no prior model and backup policy), you can find a comparison with each of the model checking paradigms in Appendix F.2, we also clearly state on line 369: “For example, we show that we don't lose much by using Monte Carlo model checking as opposed to exact model checking with the `true' probabilities”. This is reflected in the results in Appendix F.2. We might expect to lose some safety performance when operating in the most permissive setting, however since the environment is small, we are able to quickly learn an accurate model of the transition probabilities, and we can learn a safe backup policy quickly with counterfactual experiences and the cost function in Definition 4.3. For the deep RL experiments we were unable to provide a similar comparison as the observation/state space is too large and transition probabilities can’t be modelled in a compact way.

Re weakness 3.: This was one of the main difficulties of writing this paper, we wanted the paper to be self-contained and accessible to a general audience that is not necessarily familiar with model checking. In particular, we introduce labelled MDP and MC which are a necessary formalisms for model checking, we introduce PCTL to provide standard notation for defining our safety properties later in the paper and to provide probabilistic semantics, we then introduce regular safety properties, DFA and the product MC which we also feel as necessary to fully grasp what is going on. In total this part of the paper spans little over 1.5 pages which we do not find as unreasonable, the fact our main contributions only start on page 5 is perhaps skewed by the fact that we provide the related work earlier in the paper. The definitions interleaved throughout the rest of the paper are necessary and non-standard (Problem 4.1 and Definition 4.3).

Re minor comments: Proposition 4.2 is not too difficult to see, although the proof requires a union bound and we thought it necessary to be precise and provide this proof in Appendix C. We thank you for your other comments and we will take these into consideration.

Re question 1.: As stated in (Re weakness 2.) the evaluation of different assumption on prior knowledge is presented in appendix F.2. See also (Re weakness 2.) for my comments on this.

Re question 2.: No, unlike Carr et al. we don’t explicitly need the topology of the MDP to learn a model, see my response to reviewer 5beW where I highlight the differences between our approach and Carr et al. In the most general setting, we can assume every state is reachable from every other state and we can simply learn the probability vector for each state-action pair using maximum likelihood, this is reflected by the strong dependence on $|S|$ in Theorem 6.5. If we know something about the topology of the MDP, e.g. how many successor states there are or the graphical structure of the MDP then the MDP can certainly be more quickly learnt. This is briefly discussed in the main body of the paper (lines 336-337).

Re question3.: We try and break the mould of classical shielding approaches that assume knowledge of the transition dynamics or safety dynamics (or a partial model Carr et al.), this means we lose strict safety guarantees. This is a trade-off of course, by operating in the most permissive setting which assumes no prior knowledge we are not constrained to small grid world environments - we can operate in high dimensional environments, and we minimise the amount of prior engineering effort required when deploying in a new environment. We can only obtain safety guarantees when the model of the environment is sufficiently accurate, and the backup policy has learned a good safe strategy. Further limitations include lack of convergence guarantees (an open problem with the shielding paradigm), reliance on the backup policy, etc. see more limitations provided in the author rebuttal above.

Re limitations: the relation between our problem setting and real-world considerations could be discussed in the opening paragraphs.

Thanks for your response.

Re learning an MDP model: We note that there are several approaches to safe RL that aim to learn a dynamics model/model of the MDP or similar. Some of these have been highlighted by other reviewers and include [1-2], shielding approaches that learn a model of the MDP inlcude [3-4], other approaches based on formal methods/LTL constraints include [5-6], methods adapted to high-dimensional visual-input environments like Atari and safety gym include [7-8]. Many of these approaches can be classified as model-based which have been shown to have demonstrably better performance in terms of cumulative safety violations when compared with model-free algorithms (e.g. PPO-LAG, TRPO-LAG, CPO), see [7-8]

[1] Wang, Yixuan, et al. "Enforcing hard constraints with soft barriers: Safe reinforcement learning in unknown stochastic environments." International Conference on Machine Learning. PMLR, 2023.

[2] Wachi, Akifumi, et al. "Safe exploration in reinforcement learning: A generalized formulation and algorithms." Advances in Neural Information Processing Systems 36 (2024).

[3] Goodall, Alexander W., and Francesco Belardinelli. "Approximate Model-Based Shielding for Safe Reinforcement Learning." ECAI 2023. IOS Press, 2023. 883-890.

[4] He, Chloe, Borja G. León, and Francesco Belardinelli. "Do androids dream of electric fences? safety-aware reinforcement learning with latent shielding." arXiv preprint arXiv:2112.11490 (2021).

[5] Hasanbeig, Mohammadhosein, Alessandro Abate, and Daniel Kroening. "Cautious Reinforcement Learning with Logical Constraints." Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems. 2020.

[6] Hammond, Lewis, et al. "Multi-Agent Reinforcement Learning with Temporal Logic Specifications." Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems. 2021.

[7] As, Yarden, et al. "Constrained policy optimization via bayesian world models." arXiv preprint arXiv:2201.09802 (2022).

[8] Huang, Weidong, et al. "Safe dreamerv3: Safe reinforcement learning with world models." arXiv preprint arXiv:2307.07176 (2023).

Re quickly learning an accurate model and backup policy: we quickly ran our colour gridworld experiments again and plotted the total number of state-action pairs that satisfy Assumption 5.3 throughout training. We also plotted the total number of $p_1$-recoverable states w.r.t the backup policy (during training), in this plot we provide the maximum number of $p_1$-recoverable states verified by the PRISM model checker. Unfortunately there is not a way to share these plots with you at this time, however we observed the following general trends:

• For property 1 the total number of $p_1$-recoverable states (backup policy) converges to the maximum idenitfied by PRISM within 2 epsiodes (~2000 environment steps). For property 2 and 3 the total number of $p_1$-recoverable states does not reach the maximum identified by PRISM and converges to a number slightly less after around 40 epsiodes (~40000 environment steps), this is because the exploration strategy is limited, if we don't explore every state-action pair infinitely often then Q learning does not necessarily guarantee us the optimal policy, in practice we really just require that the states with high probability under the task policy state distribution are $p_1$-recoverable with the backup policy.
• For the total number of accurate state-action pairs, we see that this steadily increases and once the task policy has converged it plateus as the state distribution induced by the task policy remains the same. Ideally we would like all state action pairs to satisfy Proposition 5.3, however this is again limited by the exploration strategy - once the task policy has converged there are many state-action pairs we will not see, in practice we really just require the safety critical state-action pairs to be accurate in our model. We will include these details in a revised version of our paper.

Re dropping the assumption of knowing the topology of the MDP: in general if the topology of the MDP is unknown then we can assume that every state is reachable from every other state. Let $v(s, a)$ denote the total number of times that $(s,a)$ had been observed and let $v(s', s, a)$ denote the total number of times that $(s,a) \to s'$ has been observed. We start by initializing the visit counts $v(s, a)= |S|$ and $v(s', s, a)=1$. The maximum likelihood probability of $s'$ given $(s, a)$ is simply $\widehat{\mathcal{P}}(s' | s, a) = v(s', s, a)/v(s,a)$ giving us the intial probability vector $\widehat{\mathcal{P}}(\cdot | s, a) = [1/|S|, ..., 1/|S|]$. Every time we see a transition $(s,a) \to s'$ we update the corresponding visit counts $v(s, a) += 1$ and $v(s', s, a) += 1$, we then use Hoeffding's to bound the difference between our maximum likelihood estimate and the true probability $\mathcal{P}(s' | s, a)$. Exact details are given in Appendix C.5.