Although the construction of a suitable LDBW reaches back to the 80s [39], not all LDBWs are suitable. Broadly speaking, the nondeterministic decisions taken in the initial part may not depend on the future—though it may depend on the state of an MDP. The example LDBW from Fig. 1 (left) satisfies the property: it can try to delay to progress to one of the accepting states to when an endcomponent in an MDP is reached that always produces a's or b's, respectively. In contrast, the LDBW from Fig. 1 (right)—which recognizes the same language will have to make the decision of seeing only a's or only b's immediately, without the option to wait for reaching an end-component. This makes it unsuitable for the use in MDPs.

**Theorem 2** [8,15,33,39]*. Suitable limit-deterministic B¨uchi automata exist for all* ω*-regular languages.*

SLDBWs—and their properties described in Definition 1—are used in the qualitative and quantitative model checking algorithms in [8,15,33,39]. The accepting end-components of the product MDPs are all using only states from the final part of the SLDBW. B¨uchi acceptance then allows for using memoryless almost sure winning strategies in the accepting end-components, while outside of accepting end-components a memoryless strategy that maximizes the chance of reaching such an end-component can be used. The distinguishing property is the guarantee that they provide the correct probability, while using a product with a general NBW would only provide a value that cannot exceed it.

#### **2.5 Linear Time Logic Objectives**

LTL (Linear Time Logic) is a temporal logic whose formulae describe a subset of the ω-regular languages, which is often used to specify objectives in humanreadable form. Translations exist from LTL to various forms of automata, including NBW, DRW, and SLDBW. Given a set of atomic propositions AP, a is an LTL formula for each a ∈ AP. Moreover, if ϕ and ψ are LTL formulae, so are ¬ϕ, ϕ ∨ ψ,X ϕ, ψ Uϕ. Additional operators are defined as abbreviations: def = a ∨ ¬a; ⊥ def = ¬; ϕ ∧ ψ def = ¬(¬ϕ ∨ ¬ψ); ϕ → ψ def = ¬ϕ ∨ ψ; F ϕ def = Uϕ; and G ϕ def = ¬F ¬ϕ. We write w |= ϕ if ω-word w over 2AP satisfies LTL formula ϕ. The satisfaction relation is defined inductively [2,24].

#### **2.6 Reinforcement Learning**

For an MDP M and an objectives *Reward*M ∈ {*Reach*(T)M, *Disct*(λ)M, *Avg*M}, the optimal reward and an optimal strategy can be computed using value iteration, policy iteration, or, in polynomial time, using linear programming [12,30]. On the other hand, for ω-regular objectives (given as DRW, SLDBW, or LTL formulae) optimal satisfaction probabilities and strategies can be computed using graph-theoretic techniques (computing accepting endcomponent and then maximizing the probability to reach states in such components) over the product structure. However, when the MDP transition/reward structure is unknown, such techniques are not applicable.

For MDPs with unknown transition/reward structure, *reinforcement learning* [37] provides a framework to compute optimal strategies from repeated interactions with the environment. Of the two main approaches to reinforcement learning in MDPs, *model-free* approaches and *model-based* approaches the former, which is asymptotically space-efficient [36], has been demonstrated to scale well [14,25,35]. In a model-free approach such as Q-learning [31,37], the learner computes optimal strategies without explicitly estimating the transition probabilities and rewards. We focus on making it possible for model-free RL to learn a strategy that maximizes the probability of satisfying a given ω-regular objective.

# **3 Problem Statement and Motivation**

Given MDP M with unknown transition structure and ω-regular objective ϕ, we seek a strategy that maximizes the probability that M satisfies ϕ.

**Fig. 2.** A grid-world example (left), a Rabin automaton for [(F Gg0) ∨ (F Gg1)] ∧ G ¬b (center), and product MDP (right).

To apply model-free RL algorithms to this task, one needs to define rewards that depend on the observations of the MDP and reflect the satisfaction of the objective. It is natural to use the product of the MDP and an automaton monitoring the satisfaction of the objective to assign suitable rewards to various actions chosen by the learning algorithm.

Sadigh *et al.* [32] were the first to apply model-free RL to a qualitativeversion of this problem, i.e., to learn a strategy that satisfies the property with probability 1. For an MDP M and a DRW Aϕ of index k, they formed the product MDP M×Aϕ with k different "Rabin" reward functions ρ1,...,ρk. The function ρi corresponds to the Rabin pair (B× i , G× i ): it assigns a fixed negative reward −R− < 0 to all edges in B× i and a fixed positive reward R+ > 0 to all edges in G× i . [32] claimed that if there exists a strategy satisfying an ω-regular objective ϕ with probability 1, then there exists a Rabin pair i, discount factor λ∗ ∈ [0, 1[, and suitably high ratio R∗, such that for all λ ∈ [λ∗, 1[ and R−/R+ ≥ R∗, any strategy maximizing λ-discounted reward for the MDP (M×Aϕ, ρi) also satisfies the ω-regular objective ϕ with probability 1. Using Blackwell-optimality theorem [19], a paraphrase of this claim is that if there exists a strategy satisfying an ω-regular objective ϕ with probability 1, then there exists a Rabin pair i and suitably high ratio R∗, such that for all R−/R+ ≥ R∗, any strategy maximizing expected average reward for the MDP (M×Aϕ, ρi) also satisfies the ω-regular objective ϕ with probability 1. This approach has two faults, the second of which also affects approaches that replace DRWs with LDBWs [16,17].

**Fig. 3.** A grid-world example. The arrows represent actions (left). When action b is performed, Cell 2 is reached with probability p and Cell 1 is reached with probability 1 − p, for 0 <p< 1. Deterministic B¨uchi automaton for ϕ = (G ¬b) ∧ (G F g) (center). The dotted transition is the only accepting transition. Product MDP (right).

*Example 1 (Two Rabin Pairs).* Consider the MDP given as a simple grid-world example shown in Fig. 2. Each cell (state) of the MDP is labeled with the atomic propositions that are true there. In each cell, there is a choice between two actions rest and go. With action rest the state of the MDP does not change. However, with action go the MDP moves to the other cell in the same row with probability p, or to the other cell in the same column with probability 1−p. The initial cell is (0, 0).

The specification is given by LTL formula ϕ = [(F Gg0) ∨ (F Gg1)] ∧ G¬b. A DRW that accepts ϕ is shown in Fig. 2. The DRW has two accepting pairs: (B0, G0) and (B1, G1). The table besides the automaton gives, for each transition, its label and the B and G sets to which it belongs.

The optimal strategy that satisfies the objective ϕ with probability 1 chooses go in Cell (0, 0) and chooses rest subsequently. However, for both Rabin pairs, the optimal strategy for expected average reward is to maximize the probability of reaching one of the (0, 1), safe or (1, 0), safe states of the product and stay there forever. For the first accepting pair the maximum probability of satisfaction is 1 2−p , while for the second pair it is 1 1+p .

*Example 2 (DBW to Expected Average Reward Reduction).* This counterexample demonstrates that even for deterministic B¨uchi objectives, the problem of finding an optimal strategy satisfying an objective may not be reduced to the problem of finding an optimal average strategy. Consider the simple grid-world example of Fig. 3 with the specification ϕ = (G ¬b)∧(G F g), where atomic proposition b (blue) labels Cell 1 and atomic proposition g (green) labels Cells 2 and 3. Actions enabled in various cells and their probabilities are depicted in the figure.

The strategy from Cell 0 that chooses Action a guarantees satisfaction of ϕ with probability 1. An automaton with accepting transitions for ϕ is shown in Fig. 3; it is a DBW (or equivalently a DRW with one pair (B,G) and B = ∅).

The product MDP is shown at the bottom of Fig. 3. All states whose second component is trap have been merged. Notice that there is no negative reward since the set B is empty. If reward is positive and equal for all accepting transitions, and 0 for all other transitions, then when p > 1/2, the strategy that

**Fig. 4.** Adding transitions to the target in the augmented product MDP.

maximizes expected average reward chooses Action b in the initial state and Action e from State (2, safe). Note that, for large values of λ, the optimal expected average reward strategies are also optimal strategies for the λ-discounted reward objective. However, these strategies are not optimal for ω-regular objectives.

Example 1 shows that one cannot select a pair from a Rabin acceptance condition ahead of time. This problem can be avoided by the use of B¨uchi acceptance conditions. While DBWs are not sufficiently expressive, SLDBWs express all ω-regular properties and are suitable for probabilistic model checking. In the next section, we show that they are also "the ticket" for model-free reinforcement learning, because they allow us to maximize the probability of satisfying an ω-regular specification by solving a reachability probability problem that can be solved efficiently by off-the-shelf RL algorithms.

# **4 Model-Free RL from Omega-Regular Rewards**

We now reduce the model checking problem for a given MDP and SLDBW to a reachability problem by slightly changing the structure of the product: We add a target state t that can be reached with a given probability 1 − ζ whenever visiting an accepting transition of the original product MDP.

Our reduction avoids the identification of winning end-components and thus allows a natural integration to a wide range of model-free RL approaches. Thus, while the proofs do lean on standard model checking properties that are based on identifying winning end-components, they serve as a justification not to consider them when running the learning algorithm. In the rest of this section, we fix an MDP M and an SLDBW A for the ω-regular property ϕ.

**Definition 2 (Augmented Product).** *For any* ζ ∈]0, 1[*, the* augmented MDP Mζ *is an MDP obtained from* M×A *by adding a new state* t *with a self-loop to the set of states of* M×A*, and by making* t *a destination of each accepting transition* τ *of* M×A *with probability* 1 − ζ*. The original probabilities of all other destinations of an accepting transition* τ *are multiplied by* ζ*.*

An example of an augmented MDP is shown in Fig. 4. With a slight abuse of notation, if σ is a strategy on the augmented MDP Mζ , we denote by σ also the strategy on M×A obtained by removing t from the domain of σ.

We let pσ s (ζ) denote the probability of reaching t in Mζ σ when starting at state s. Notice that we can encode this value as the expected average reward in the following rewardful MDP (Mζ , ρ), where we set the reward function ρ(t, a)=1 for all a ∈ A and ρ(s, a) = 0 otherwise. For any strategy σ, the probability pσ s (ζ) and the reward of σ from s in (Mζ , ρ) are the same. We also let aσ s be the probability that a run that starts from s in (M×A)σ is accepting.

**Lemma 1.** *If* σ *is a positional strategy on* Mζ *, then, for every state* s *of the Markov chain* (M×A)σ*, the following holds:*

*Proof.* (1) holds as there are no accepting transition in a rejecting BSCC of (M×A)σ, and so t cannot be reached when starting at s in Mζ σ. (2) holds because t (with its self-loop) is the only BSCC reachable from s in Mζ . In other words, t (with its self-loop) and the rejecting BSCCs of (M×A)σ are the only BSCCs in Mζ σ. (3) then follows, because the same paths lead to a rejecting BSCCs in (M×A)σ and Mζ σ, while the probability of each such a path is no larger—and strictly smaller iff it contains an accepting transition—than in Mζ σ. (4) holds because, if pσ s (ζ) = 1, then t (with its self-loop) is the only BSCC reachable from s in Mζ σ. Thus, there is no path to a rejecting BSCC in Mζ σ, and therefore no path to a rejecting BSCC in (M×A)σ.

**Lemma 2.** *Let* σ *be a positional strategy on* Mζ *. For every state* s *of* Mζ *, we have that* limζ↑1 pσ s (ζ) = aσ s *.*

*Proof.* As shown in Lemma 1(3) for all ζ, we have pσ s (ζ) ≥ aσ s . For a coarse approximation of their difference, we recall that (M×A)σ is a finite Markov chain. The expected number of transitions taken before reaching a BSCC from s in (M×A)σ is therefore a finite number. Let us refer to the—no larger expected number of accepting transitions taken before reaching a BSCC when starting at s in (M×A)σ as fσ s . We claim that aσ s ≥ pσ s (ζ) − (1 − ζ) · fσ s . This is because the probability of reaching a rejecting BSCC in (M×A)σ is at most the probability of reaching a rejecting BSCC in Mζ σ, which is at most 1−pσ s (ζ), plus the probability of moving on to t from a state that is not in any BSCC in (M×A)σ, which we are going to show next is at most fσ s · (1 − ζ).

First, a proof by induction shows that (1 − ζk) ≤ k(1 − ζ) for all k ≥ 0. Let P σ s (ζ,k) be the probability of generating a path from s with k accepting transitions before t or a node in some BSCC of (M×A)σ is reached in Mζ σ. The probability of seeing k accepting transitions and not reaching t is at least ζk. Therefore, probability of moving to t from a state not in any BSCC is at most

$$\sum\_{k} P\_s^{\sigma}(\zeta, k)(1 - \zeta^k) \le \sum\_{k} P\_s^{\sigma}(\zeta, k)k \cdot (1 - \zeta) \le f\_s^{\sigma} \cdot (1 - \zeta).$$

The proof is now complete.

This provides us with our main theorem.

**Theorem 3.** *There exists a threshold* ζ ∈]0, 1[ *such that, for all* ζ>ζ *and every state* s*, any strategy* σ *that maximizes the probability* pσ s (ζ) *of reaching the sink in* Mζ *is (1) an optimal strategy in* M×A *from* s *and (2) induces an optimal strategy for the original MDP* M *from* s *with objective* ϕ*.*

*Proof.* We use the fact that it suffices to study positional strategies, and there are only finitely many of them. Let σ1 be an optimal strategy of M×A, and let σ2 be a strategy that has the highest likelihood of creating an accepting run among all non-optimal memoryless ones. (If σ2 does not exist, then all strategies are equally good, and it does not matter which one is chosen.) Let δ = aσ1 s −aσ2 s .

Let fmax = maxσ maxs fσ s , where σ ranges over positional strategies only, and fσ s is defined as in Lemma 2. We claim that it suffices to pick ζ ∈]0, 1[ such that (1 − ζ ) · fmax < δ. Suppose that σ is a positional strategy that is optimal in Mζ for ζ>ζ , but is not optimal in M×A. We then have

$$a\_s^\sigma \le p\_s^\sigma(\zeta) \le a\_s^\sigma + (1 - \zeta)f\_s^\sigma < a\_s^\sigma + \delta \le a\_s^{\sigma\_1} \le p\_s^{\sigma\_1}(\zeta),$$

where these inequalities follow, respectively, from: Lemma 1(3), the proof of Lemma 2, the definition of ζ , the assumption that σ is not optimal and the definition of δ, and the last one from Lemma 1(3). This shows that pσ s (ζ) < pσ1 s (ζ), i.e., σ is not optimal in Mζ ; a contradiction. Therefore, any positional strategy that is optimal in Mζ for ζ>ζ is also optimal in M×A.

Now, suppose that σ is a positional strategy that is optimal in M×A. Then the probability of satisfying ϕ in M when starting at s is at least1 aσ s . At the same time, if there was a strategy for which the probability of satisfying ϕ in M is > aσ s , then the property of A to be an SLDBW (Definition 1) would guarantee the existence of strategy σ for which aσ- s > aσ s ; a contradiction with the assumption that σ is optimal. Therefore any positional strategy that is optimal in M×A induces an optimal strategy in M with objective ϕ.

**Corollary 1.** *Due to Lemma 1(4),* M *satisfies* ϕ *almost surely if and only if the sink is almost surely reachable in* Mζ *for all* 0 <ζ< 1*.*

Theorem 3 leads to a very simple model-free RL algorithm. The augmented product is not built by the RL algorithm, which does not know the transition structure of the environment MDP. Instead, the observations of the MDP are used by an *interpreter* process to compute a run of the objective automaton. The interpreter also extracts the set of actions for the learner to choose from. If the automaton is not deterministic and it has not taken the one nondeterministic transition it needs to take yet, the set of actions the interpreter provides to the learner includes the choice of special "jump" actions that instruct the automaton to move to a chosen accepting component.

1 This holds for all nondeterministic automata that recognize the models of ϕ: an accepting run establishes that the path was a model of ϕ.

When the automaton reports an accepting transition, the interpreter gives the learner a positive reward with probability 1 − ζ. When the learner actually receives a reward, the training episode terminates. Any RL algorithm that maximizes this probabilistic reward is guaranteed to converge to a policy that maximizes the probability of satisfaction of the ω-regular objective.

# **5 Experimental Results**

We implemented the construction described in the previous sections in a tool named Mungojerrie [11], which reads MDPs described in the PRISM language [21], and ω-regular automata written in the HOA format [1,9]. Mungojerrie builds the augmented product Mζ , provides an interface for RL algorithms akin to that of [5] and supports probabilistic model checking. Our algorithm computes, for each pair (s, a) of state and action, the maximum probability of satisfying the given objective after choosing action a from state s by using offthe-shelf, temporal difference algorithms. Not all actions with maximum probability are part of positional optimal strategies—consider a product MDP with one state and two actions, a and b, such that a enables an accepting self-loop, and b enables a non-accepting one: both state/action pairs are assigned probability 1. In b's case, because choosing b once—or a finite number of times—does not preclude acceptance. Since the probability values alone do not identify a pure optimal strategy, Mungojerrie computes an optimal mixed strategy, uniformly choosing all maximum probability actions from a state.

The MDPs on which we tested our algorithms [26] are listed in Table 1. For each model, the numbers of decision states in the MDP, the automaton, and the product MDP are given. Next comes the probability of satisfaction of the objective for the strategy chosen by the RL algorithm as computed by the model checker (which has full access to the MDP). This is followed by the estimate of the probability of satisfaction of the objective computed by the RL algorithm and the time taken by learning. The last six columns report values of the hyperparameters when they deviate from the default values: ζ controls the probability of reward, is the exploration rate, α is the learning rate, and tol is the tolerance for probabilities to be considered different. Finally, ep-l controls the episode length (it is the maximum allowed length of a path in the MDP that does contain an accepting edge) and ep-n is the number of episodes. All performance data are the averages of three trials with Q-learning. Rewards are undiscounted, so that the value of a state-action pair computed by Q-learning is a direct estimate of the probability of satisfaction of the objective from that state when taking that action.

Models twoPairs and riskReward are from Examples 1 and 2, respectively. Model deferred is discussed later. Models grid5x5 and trafficNtk are from [32]. The three "windy" MDPs are taken from [37]. The "frozen" examples are from [27]. Some ω-regular objectives are simple reachability requirements (e.g., frozenSmall and frozenLarge). The objective for the othergrid models is to collect three types of coupons, while incurring at most one of two types of penalties. In doublegrid two agents simultaneously move across the grid.

The objective for slalom is given by the LTL formula G(p → X G¬q) ∧ G(q → X G¬p). For model rps1 the strategy found by RL is (slightly) suboptimal. The difference in probability of 0.01 is explained by the existence of many strategies of nearly identical values. Model mutual [7,15,34] describes the mutual exclusion protocol of Pnueli and Zuck [29]. Though large, this model is easy for learning.

Figure 5 illustrates how increasing the parameter ζ makes the RL algorithm less sensitive to the presence of transient (not in an end-component) accepting transitions. Model deferred consists of two chains of states: one, which the agent choses with action a, has accepting transitions throughout, but leads to an end-component that is not accepting. The other chain, selected with action b, leads to an accepting end-component, but has no other accepting transitions. There are no other decisions in the model; hence only two strategies are possible, which we denote by a and b, depending on the action chosen.

**Fig. 5.** Model deferred and effect of ζ on it.

The curve labeled pa in Fig. 5 gives the probability of satisfaction under strategy a of the MDP's objective as a function of ζ as computed by Q-learning. The number of episodes is kept fixed at 20, 000 and each episode has length 80. Each data point is the average of five experiments for the same value of ζ.

For values of ζ close to 0, the chance is high that the sink is reached directly from a transient state. Consequently, Q-learning considers strategies a and b equally good. For this reason, the probability of satisfaction of the objective, pϕ, according to the strategy that mixes a and b, is computed by Mungojerrie's model checker as 0.5. As ζ approaches 1, the importance of transient accepting transitions decreases, until the probability computed for strategy a is no longer considered to be approximately the same as the probability of strategy b. When that happens, pϕ abruptly goes from 0.5 to its true value of 1, because the pure strategy b is selected. The value of pa continues to decline for larger values of ζ until it reaches its true value of 0 for ζ = 0.9999. Probability pb, not shown in the graph, is 1 throughout.

The change in value of pϕ does not contradict Theorem 3, which says that pb = 1 > pa for all values of ζ. In practice a high value of ζ may be needed to reliably distinguish between transient and recurrent accepting transitions in numerical computation. Besides, Theorem 3 suggests that even in the almostsure case there is a meaningful path to the target strategy where the likelihood of satisfying ϕ can be expected to grow. This is important, as it comes with the promise of a generally increasing quality of intermediate strategies.

#### **6 Conclusion**

We have reduced the problem of maximizing the satisfaction of an ω-regular objective in a MDP to reachability on a product graph augmented with a sink state. This change is so simple and elegant that it may surprise that it has not been used before. But the reason for this is equally simple: it does not help in a model checking context, as it does not remove any analysis step there. In a reinforcement learning context, however, it simplifies our task significantly. In previous attempts to use suitable LDBW [4], the complex part of the model checking problem—identifying the accepting end-components—is still present. Only after this step, which is expensive and requires knowledge of the structure of the underlying MDP, can these methods reduce the search for optimal satisfaction to the problem of maximizing the chance to reach those components. Our reduction avoids the identification of accepting end-components entirely and thus allows a natural integration with a wide range of model-free RL approaches.

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Verifiably Safe Off-Model Reinforcement Learning**

Nathan Fulton(B) and Andr´e Platzer

Computer Science Department, Carnegie Mellon University, Pittsburgh, USA<EMAIL_ADDRESS>
**Abstract.** The desire to use reinforcement learning in safety-critical settings has inspired a recent interest in formal methods for learning algorithms. Existing formal methods for learning and optimization primarily consider the problem of constrained learning or constrained optimization. Given a single correct model and associated safety constraint, these approaches guarantee efficient learning while provably avoiding behaviors outside the safety constraint. Acting well given an accurate environmental model is an important pre-requisite for safe learning, but is ultimately insufficient for systems that operate in complex heterogeneous environments. This paper introduces verification-preserving model updates, the first approach toward obtaining formal safety guarantees for reinforcement learning in settings where multiple possible environmental models must be taken into account. Through a combination of inductive data and deductive proving with design-time model updates and runtime model falsification, we provide a first approach toward obtaining formal safety proofs for autonomous systems acting in heterogeneous environments.

# **1 Introduction**

The desire to use reinforcement learning in safety-critical settings has inspired several recent approaches toward obtaining formal safety guarantees for learning algorithms. Formal methods are particularly desirable in settings such as selfdriving cars, where testing alone cannot guarantee safety [22]. Recent examples of work on formal methods for reinforcement learning algorithms include justified speculative control [14], shielding [3], logically constrained learning [17], and constrained Bayesian optimization [16]. Each of these approaches provide formal safety guarantees for reinforcement learning and/or optimization algorithms by stating assumptions and specifications in a formal logic, generating monitoring conditions based upon specifications and environmental assumptions, and then

This research was sponsored by the Defense Advanced Research Projects Agency (DARPA) under grant number FA8750-18-C-0092. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government or any other entity.

leveraging these monitoring conditions to constrain the learning/optimization process to a known-safe subset of the state space.

Existing formal methods for learning and optimization consider the problem of constrained learning or constrained optimization [3,14,16,17]. They address the question: assuming we have a single accurate environmental model with a given specification, how can we learn an efficient control policy respecting this specification?

Correctness proofs for control software in a single well-modeled environment are necessary but not sufficient for ensuring that reinforcement learning algorithms behave safely. Modern cyber-physical systems must perform a large number of subtasks in many different environments and must safely cope with situations that are not anticipated by system designers. These design goals motivate the use of reinforcement learning in safety-critical systems. Although some formal methods suggest ways in which formal constraints might be used to inform control even when modeling assumptions are violated [14], none of these approaches provide formal safety guarantees when environmental modeling assumptions are violated.

Holistic approaches toward safe reinforcement learning should provide formal guarantees even when a single, a priori model is not known at design time. We call this problem *verifiably safe off-model learning*. In this paper we introduce a first approach toward obtaining formal safety proofs for off-model learning. Our approach consists of two components: (1) a model synthesis phase that constructs a set of candidate models together with provably correct control software, and (2) a runtime model identification process that selects between available models at runtime in a way that preserves the safety guarantees of all candidate models.

Model update learning is initialized with a set of models. These models consist of a set of differential equations that model the environment, a control program for selecting actuator inputs, a safety property, and a formal proof that the control program constrains the overall system dynamics in a way that correctly ensures the safety property is never violated.

Instead of requiring the existence of a single accurate initial model, we introduce *model updates* as syntactic modifications of the differential equations and control logic of the model. We call a model update *verification-preserving* if there is a corresponding modification to the formal proof establishing that the modified control program continues to constrain the system of differential equations in a way that preserves the original model's safety properties.

Verification-preserving model updates are inspired by the fact that different parts of a model serve different roles. The continuous portion of a model is often an assumption about how the world behaves, and the discrete portion of a model is derived from these equations and the safety property. For this reason, many of our updates inductively synthesize ODEs (i.e., in response to data from previous executions of the system) and then deductively synthesize control logic from the resulting ODEs and the safety objective.

Our contributions enabling verifiably safe off-model learning include: **(***1***)** A set of verification preserving model updates (VPMUs) that systematically update differential equations, control software, and safety proofs in a way that preserves verification guarantees while taking into account possible deviations between an initial model and future system behavior. **(***2***)** A reinforcement learning algorithm, called model update learning (μlearning), that explains how to transfer safety proofs for a set of feasible models to a learned policy. The learned policy will actively attempt to falsify models at runtime in order to reduce the safety constraints on actions. These contributions are evaluated on a set of hybrid systems control tasks. Our approach uses a combination of program repair, system identification, offline theorem proving, and model monitors to obtain formal safety guarantees for systems in which a single accurate model is not known at design time. This paper fully develops an approach based on an idea that was first presented in an invited vision paper on Safe AI for CPS by the authors [13].

The approach described in this paper is model-based but does not assume that a single correct model is known at design time. Model update learning allows for the possibility that all we can know at design time is that there are many feasible models, one of which might be accurate. Verification-preserving model updates then explain how a combination of data and theorem proving can be used at design time to enrich the set of feasible models.

We believe there is a rich space of approaches toward safe learning in-between model-free reinforcement learning (where formal safety guarantees are unavailable) and traditional model-based learning that assumes the existence of a single ideal model. This paper provides a first example of such an approach by leveraging inductive data and deductive proving at both design time and runtime.

The remainder of this paper is organized as follows. We first review the logical foundations underpinning our approach. We then introduce verificationpreserving model updates and discuss how experimental data may be used to construct a set of explanatory models for the data. After discussing several model updates, we introduce the μlearning algorithm that selects between models at runtime. Finally, we discuss case studies that validate both aspects of our approach. We close with a discussion of related work.

# **2 Background**

This section reviews existing approaches toward safe on-model learning and discusses the fitness of each approach for obtaining guarantees about off-model learning. We then introduce the specification language and logic used throughout the rest of this paper.

Alshiekh et al. and Hasanbeig et al. propose approaches toward safe reinforcement learning based on Linear Temporal Logic [3,17]. Alshiekh et al. synthesize monitoring conditions based upon a safety specification and an environmental abstraction. In this formalism, the goal of off-model learning is to systematically expand the environmental abstraction based upon both design-time insights about how the system's behavior might change over time and based upon observed data at runtime. Jansen et al. extend the approach of Alshiekh et al. by observing that constraints should adapt whenever runtime data suggests that a safety constraint is too restrictive to allow progress toward an over-arching objective [20]. Herbert et al. address the problem of safe motion planning by using offline reachability analysis of pursuit-evasion games to pre-compute an overapproximate monitoring condition that then constrains online planners [9,19].

The above-mentioned approaches have an implicit or explicit environmental model. Even when these environmental models are accurate, reinforcement learning is still necessary because these models focus exclusively on safety and are often nondeterministic. Resolving this nondeterminism in a way that is not only safe but is also effective at achieving other high-level objectives is a task that is well-suited to reinforcement learning.

We are interested in how to provide formal safety guarantees even when there is not a single accurate model available at design time. Achieving this goal requires two novel contributions. We must first find a way to generate a robust set of feasible models given some combination of an initial model and data on previous runs of the system (because formal safety guarantees are stated with respect to a model). Given such a set of feasible models, we must then learn how to safely identify which model is most accurate so that the system is not over-constrained at runtime.

To achieve these goals, we build on the safe learning work for a single model by Fulton et al. [14]. We choose this approach as a basis for verifiably safe learning because we are interested in safety-critical systems that combine discrete and continuous dynamics, because we would like to produce explainable models of system dynamics (e.g., systems of differential equations as opposed to large state machines), and, most importantly, because our approach requires the ability to systematically modify a model together with that model's safety proof.

Following [14], we recall Differential Dynamic Logic [26,27], a logic for verifying properties about safety-critical hybrid systems control software, the ModelPlex synthesis algorithm in this logic [25], and the KeYmaera X theorem prover [12] that will allow us to systematically modify models and proofs together.

Hybrid (dynamical) systems [4,27] are mathematical models that incorporate both discrete and continuous dynamics. Hybrid systems are excellent models for safety-critical control tasks that combine the discrete dynamics of control software with the continuous motion of a physical system such as an aircraft, train, or automobile. Hybrid programs [26–28] are a programming language for hybrid systems. The syntax and informal semantics of hybrid programs is summarized in Table 1. The continuous evolution program is a continuous evolution along the differential equation system x *i* = θ*i* for an arbitrary duration within the region described by formula F.

*Hybrid Program Semantics.* The semantics of the hybrid programs described by Table 1 are given in terms of transitions between states [27,28], where a state s assigns a real number s(x) to each variable x. We use st to refer to the value of a term t in a state s. The semantics of a program α, written α, is the set of pairs (s1, s2) for which state s2 is reachable by running α from state s1. For example, x := t1 ∪ x := t2 is:

$$\{ (s\_1, s\_2) \mid s\_1 = s\_2 \text{ except } s\_2(x) = s\_1 \lbrack \!\lbrack t\_1 \rbrack \rbrack \} \cup \{ \!\lbrack (s\_1, s\_2) \rbrack \mid s\_1 = s\_2 \text{ except } s\_2(x) = s\_1 \lbrack \!\lbrack t\_2 \rbrack \rbrack \}$$

**Table 1.** Hybrid programs

for a hybrid program α and state s where α(s) is set of all states t such that (s, t) ∈ α.

*Differential Dynamic Logic.* Differential dynamic logic (dL) [26–28] is the dynamic logic of hybrid programs. The logic associates with each hybrid program α modal operators [α] and α, which express state reachability properties of α. The formula [α]φ states that the formula φ is true in *all* states reachable by the hybrid program α, and the formula αφ expresses that the formula φ is true after *some* execution of α. The dL formulas are generated by the grammar

$$\phi ::= \theta\_1 \sim \theta\_2 \mid \neg \phi \mid \phi \land \psi \mid \phi \lor \psi \mid \phi \to \psi \mid \forall x \phi \mid \exists x \phi \mid [\alpha] \phi \mid \langle \alpha \rangle \phi$$

where θ*i* are arithmetic expressions over the reals, φ and ψ are formulas, α ranges over hybrid programs, and is a comparison operator =, =, ≥, >, ≤, <. The quantifiers quantify over the reals. We denote by s |= φ the fact that formula φ is true in state s; e.g., we denote by s |= [α]φ the fact that (s, t) ∈ α implies t |= φ for all states t. Similarly, φ denotes the fact that φ has a proof in dL. When φ is true in every state (i.e., valid) we simply write |= φ.

*Example 1 (Safety specification for straight-line car model).*

$$\underbrace{v \ge 0 \land A > 0}\_{\text{initial condition}} \to \left[ \left( \underbrace{a := A \cup a := 0}\_{c \, trl} \right) ; \underbrace{\{p' = v, \, v' = a\}}\_{\text{plant}} \right)^\* ] \underbrace{v \ge 0}\_{\text{post cond.}}$$

This formula states that if a car begins with a non-negative velocity, then it will also always have a non-negative velocity after repeatedly choosing new acceleration (A or 0), or coasting and moving for a nondeterministic period of time.

Throughout this paper, we will refer to sets of actions. An **action** is simply the effect of a loop-free deterministic discrete program without tests. For example, the programs a:=A and a:=0 are the actions available in the above program. Notice that **actions** can be equivalently thought of as mappings from variables to terms. We use the term action to refer to both the mappings themselves and the hybrid programs whose semantics correspond to these mappings. For an action u, we write u(s) to mean the effect of taking action u in state s; i.e., the unique state t such that (s, t) ∈ u.

*ModelPlex.* Safe off-model learning requires noticing when a system deviates from model assumptions. Therefore, our approach depends upon the ability to check, at runtime, whether the current state of the system can be explained by a hybrid program.

The KeYmaera X theorem prover implements the ModelPlex algorithm [25]. For a given dL specification ModelPlex constructs a correctness proof for monitoring conditions expressed as a formula of quantifier-free real arithmetic. The monitoring condition is then used to extract provably correct monitors that check whether observed transitions comport with modeling assumptions. ModelPlex can produce monitors that enforce models of control programs as well as monitors that check whether the model's ODEs comport with observed state transitions.

ModelPlex *controller monitors* are boolean functions that return false if the controller portion of a hybrid systems model has been violated. A *controller monitor* for a model {ctrl; plant}∗ is a function cm : S×A→ B from states S and actions A to booleans B such that if cm(s, a) then (s, a(s)) ∈ ctrl. We sometimes also abuse notation by using controller monitors as an implicit filter on A; i.e., cm : S→A such that a ∈ cm(s) iff cm(s, a) is true.

ModelPlex also produces *model monitors*, which check whether the model is accurate. A *model monitor* for a safety specification φ → [α∗]ψ is a function mm : S×S → B such that (s0, s) ∈ α if mm(s0, s). For the sake of brevity, we also define mm : S×A×S → B as the model monitor applied after taking an action (a ∈ A) in a state and then following the plant in a model of form α ≡ ctrl; plant. Notice that if the model has this canonical form and if if mm(s, a, a(s)) for an action a, then cm(s, a(s)).

The KeYmaera X system is a theorem prover [12] that provides a language called Bellerophon for scripting proofs of dL formulas [11]. Bellerophon programs, called tactics, construct proofs of dL formulas. This paper proposes an approach toward updating models in a way that preserves safety proofs. Our approach simultaneously changes a system of differential equations, control software expressed as a discrete loop-free program, and the formal proof that the controller properly selects actuator values such that desired safety constraints are preserved throughout the flow of a system of differential equations.

# **3 Verification-Preserving Model Updates**

A *verification-preserving model update* (VPMU) is a transformation of a hybrid program accompanied by a proof that the transformation preserves key safety properties [13]. VPMUs capture situations in which a model and/or a set of data can be updated in a way that captures possible runtime behaviors which are not captured by an existing model.

**Definition 1 (VPMU).** *A* verification-preserving model update *is a mapping which takes as input an initial* dL *formula* ϕ *with an associated Bellerophon tactic* e *of* ϕ*, and produces as output a new* dL *formula* ψ *and a new Bellerophon tactic* f *such that* f*is a proof of* ψ*.*

Before discussing our VPMU library, we consider how a set of feasible models computed using VPMUs can be used to provide verified safety guarantees for a family of reinforcement learning algorithms. The primary challenge is to maintain safety with respect to all feasible models while also avoiding overly conservative monitoring constraints. We address this challenge by falsifying some of these models at runtime.

# **4 Verifiably Safe RL with Multiple Models**

VPMUs may be applied whenever system designers can characterize likely ways in which an existing model will deviate from reality. Although applying model updates at runtime is possible and sometimes makes sense, model updates are easiest to apply at design time because of the computational overhead of computing both model updates and corresponding proof updates. This section introduces model update learning, which explains how to take a set of models generated using VPMUs at design time to provide safety guarantees at runtime.

Model update learning is based on a simple idea: begin with a set of *feasible models* and act safely with respect to all feasible models. Whenever a model does not comport with observed dynamics, the model becomes infeasible and is therefore removed from the set of feasible models. We introduce two variations of μlearning: a basic algorithm that chooses actions without considering the underlying action space, and an algorithm that prioritizes actions that rule out feasible models (adding an *eliminate* choice to the classical explore/exploit tradeoff [32]).

All μlearning algorithms use monitored models; i.e., models equipped with ModelPlex controller monitors and model monitors.

**Definition 2 (Monitored Model).** *A monitored model is a tuple* (m, cm, mm) *such that* m *is a* dL *formula of the form*

$$\mathtt{init} \to [\{\mathtt{ctx1}; \mathtt{p1ant}\}^\*] \mathtt{safe}$$

*where* ctrl *is a loop-free program, the entire formula* m *contains exactly one modality, and the formulas* cm *and* mm *are the control monitor and model monitor corresponding to* m*, as defined in Sect. 2.*

Monitored models may have a continuous action space because of both tests and the nondeterministic assignment operator. We sometimes introduce additional assumptions on the structure of the monitored models. A monitored model over a finite action space is a monitored model where {t : (s, t) ∈ ctrl} is finite for all s ∈ S.

Model update learning, or μlearning, leverages verification-preserving model updates to maintain safety while selecting an appropriate environmental model. We now state and prove key safety properties about the μlearning algorithm.

**Definition 3 (**μ**learning Process).** *A learning process* P*M for a finite set of monitored models* M *is defined as a tuple of countable sequences* (*U*, *S*,*Mon*) *where U are actions in a finite set of actions* A *(i.e., mappings from variables to values), elements of the sequence S are states, and Mon are monitored models with Mon*0 = M*. Let* specOK*m*(*U*, *S*, i) ≡ mm(*Si*−1, *Ui*−1, *Si*) → cm(*Si*, *Ui*) *where* cm *and* mm *are the monitors corresponding to the model* m*. Let* specOK *always return true for* i = 0*.*

*A* μ*learning process is a learning process satisfying the following additional conditions: (a) action availability: in each state Si there is at least one action* u *such that for all* m ∈ *Moni,* u ∈ specOK*m*(*U*, *S*, i)*, (b) actions are safe for all feasible models: Ui*+1 ∈ {u ∈ A | ∀(m, cm, mm) ∈ *Moni*, cm(*Si*, u)}*, (c) feasible models remain in the feasible set: if* (ϕ, cm, mm) ∈ *Moni and* mm(*Si*, *Ui*, *Si*+1) *then* (ϕ, cm, mm) ∈ *Moni*+1*.*

Note that μlearning processes are defined over an environment E : A×S → S that determines the sequences **U** and **S**1, so that **S***i*+1 = E(**U***i*, **S***i*). In our algorithms, the set **Mon***i* never retains elements that are inconsistent with the observed dynamics at the previous state. We refer to the set of models in **Mon***i* as the set of feasible models for the i th state in a μlearning process.

Notice that the safe actions constraint is not effectively checkable without extra assumptions on the range of parameters. Two canonical choices are discretizing options for parameters or including an effective identification process for parameterized models.

Our safety theorem focuses on time-aware μlearning processes, i.e., those whose models are all time-aware; similarly, a *finite action space* μ*learning process* is a μlearning process in which all models m ∈ M have a finite action space. The basic correctness property for a μlearning process is the safe reinforcement learning condition: the system never takes unsafe actions.

**Definition 4 (**μ**learning process with an accurate model).** *Let* P*M* = (*S*, *U*,*Mon*) *be a* μ*learning process. Assume there is some element* m∗ ∈ *Mon*0 *with the following properties. First,*

$$m^\* \equiv (\mathtt{init}\_m \to [\{\mathtt{ctx1}\_m; \mathtt{p1ant}\_m\}^\*] \mathtt{safe}).$$

*Second,* m∗*. Third,* (s, u(s)) ∈ ctrl*m implies* (u(s), E(u, s)) ∈ plant *for a mapping* E : S×A → S *from states and actions to new states called environment. When only one element of Mon*0 *satisfies these properties we call that element* m∗ *the* distinguished *and/or* accurate *model and say that the process* P*M is* accurately modeled with respect to E*.*

We will often elide the environment E for which the process P*M* is accurate when it is obvious from context.

**Theorem 1 (Safety).** *If* P*M is a* μ*learning process with an accurate model, then Si* |= safe*for all* 0 <i< |*S*|*.*

1 Throughout the paper, we denote by **S** a specific sequence of states and by S the set of all states.

Listing 1.1 presents the μlearning algorithm. The inputs are: **(***a***)** A set M of models each with an associated function m.models : S×A×S → B that implements the evaluation of its model monitor in the given previous and next state and actions and a method m.safe : S×A→ B which implements evaluation of its controller monitor, **(***b***)** an action space A and an initial state init ∈ S, **(***c***)** an environment function env : S×A→ S×R that computes state updates and rewards in response to actions, and **(***d***)** a function choose : ℘(A) → A that selects an action from a set of available actions and update updates a table or approximation. Our approach is generic and works for any reinforcement learning algorithm; therefore, we leave these functions abstract. It augments an existing reinforcement learning algorithm, defined by update and choose, by restricting the action space at each step so that actions are only taken if they are safe with respect to *all* feasible models. The feasible model set is updated at each control set by removing models that are in conflict with observed data.

The μlearning algorithm rules out incorrect models from the set of possible models by taking actions and observing the results of those actions. Through these experiments, the set of relevant models is winnowed down to either the distinguished correct model m∗, or a set of models M∗ containing m∗ and other models that cannot be distinguished from m∗.

#### **Listing 1.1.** The basic *µ*learning algorithm

```
def μlearn(M,A,init,env,choose,update):
  s_pre = s_curr = init
  act = None
  while(not done(s_curr)):
    if act is not None:
      M = {m ∈ M : m.models(s_pre,act,s_curr)}
    avail = {a ∈ A : ∀ m ∈ M, m.safe(s_curr, a)}
    act = choose(avail)
    s_pre = s_curr
    (s_curr, reward) = env(s_curr, act)
    update(s_pre, act, s_curr, reward)
```
#### **4.1 Active Verified Model Update Learning**

Removing models from the set of possible models relaxes the monitoring condition, allowing less conservative and more accurate control decisions. Therefore, this section introduces an active learning refinement of the μlearning algorithm that prioritizes taking actions that help rule out models m ∈ M that are not m∗. Instead of choosing a random safe action, μlearning prioritizes actions that differentiate between available models. We begin by explaining what it means for an algorithm to perform good experiments.

**Definition 5 (Active Experimentation).** *A* μ*learning process with an accurate model* m∗ *has* locally active experimentation *provided that: if Moni* > 1 *and there exists an action* a *that is safe for all feasible models (see Definition 3) in state* s*i such that taking action* a *results in the removal of* m *from the model set*2*, then* |*Moni*+1| < |*Moni*|*. Experimentation is* er*-*active *if the following conditions hold: there exists an action* a *that is safe for all feasible models (see Definition 3) in state* s*i, and taking action* a *resulted in the removal of* m *from the model set, then* |*Moni*+1| < |*Moni*| *with probability* 0 < er< 1*.*

**Definition 6 (Distinguishing Actions).** *Consider a* μ*learning process* (*U*, *S*,*Mon*) *with an accurate model* m∗ *(see Definition 4). An action* a distinguishes m from m∗ *if* a = *Ui,* m ∈ *Moni and* m ∈ *Moni*+1 *for some* i > 0*.*

The *active* μ*learning algorithm* uses model monitors to select distinguishing actions, thereby performing active experiments which winnow down the set of feasible models. The inputs to active-μlearn are the same as those to Listing 1.1 with two additions: **(***1***)** models are augmented with an additional prediction method p that returns the model's prediction of the next state given the current state, a candidate action, and a time duration. **(***2***)** An elimination rate er is introduced, which plays a similar role as the classical explore-exploit rate except that we are now deciding whether to insist on choosing a good experiment. The active-μlearn algorithm is guaranteed to make some progress toward winnowing down the feasible model set whenever 0 < er < 1.

**Theorem 2.** *Let* P*M* = (*S*, *U*,*Mon*) *be a finite action space* μ*learning process with an accurate model* m∗*. Then* m∗ ∈ *Moni for all* 0 ≤ i ≤ |*Mon*|*.*

**Theorem 3.** *Let* P*M be a finite action space* er*-active* μ*learning process under environment* E *and with an accurate model* m∗*. Consider any model* m ∈ *Mon*0 *such that* m = m∗*. If every state* s *has an action* a*s that is safe for all models and distinguishes* m *from* m∗*, then* lim*i*→∞ *Pr*(m ∈ *Moni*)=1*.*

**Corollary 1.** *Let* P*M* = (*S*, *U*,*Mon*) *be a finite action space* er*-active* μ*learning process under environment* E *and with an accurate model* m∗*. If* each *model* m ∈ *Mon*0 \ {m∗} *has in each state* s *an action* a*s that is safe for all models and distinguishes* m *from* m∗*, then Mon converges to* {m∗} *a.s.*

Although locally active experimentation is not strong enough to ensure that P*M* eventually converges to a minimal set of models3, our experimental validation demonstrates that this heuristic is none-the-less effective on some representative examples of model update learning problems.

# **5 A Model Update Library**

So far, we have established how to obtain safety guarantees for reinforcement learning algorithms given a set of formally verified dL models. We now turn

2 We say that taking action *ai* in state *si* results in the removal of a model *m* from

the model set if *m* ∈ **Mon***i* but *m* ∈ **Mon***i*+1. 3 *x* ≥ 0 ∧ *t* = 0 → [{{?*t* = 0; *x* := 1 ∪ *x* := 0}; {*x* = *F, t* = 1}}∗] *x* ≥ 0 with the parameters *F* = 0*, F* = 5*,* and *F* = *x* are a counter example [10, Section 8.4.4].

our attention to the problem of generating such a set of models by systematically modifying dL formulas and their corresponding Bellerophon tactical proof scripts. This section introduces five generic model updates that provide a representative sample of the kinds of computations that can be performed on models and proofs to predict and account for runtime model deviations4.

The simplest example of a VPMU instantiates a parameter whose value is not known at design time but can be determined at runtime via system identification. Consider a program p modeling a car whose acceleration depends upon both a known control input accel and parametric values for maximum braking force −B and maximum acceleration A. Its proof is

$$\mathsf{i m}\mathtt{p}\mathtt{1yR}(1);\mathsf{i}\mathtt{o}\mathtt{op}(\mathtt{pos}-\mathtt{obsPos}>\frac{\mathtt{ve1}^2}{2B},1);\mathsf{o}\mathtt{o}\mathtt{A}11(\mathtt{master})$$

This model and proof can be updated with concrete experimentally determined values for each parameter by uniformly substituting the variables B and A with concrete values in both the model and the tactic.

The **Automatic Parameter Instantiation** update improves the basic parameter instantiation update by automatically detecting which variables are parameters and then constraining instantiation of parameters by identifying relevant initial conditions.

The **Replace Worst-Case Bounds with Approximations** update improves models designed for the purpose of safety verification. Often a variable occurring in the system is bounded above (or below) by its worst-case value. Worst-case analyses are sufficient for establishing safety but are often overly conservative. The approximation model update replaces worst-case bounds with approximate bounds obtained via series expansions. The proof update then introduces a tactic on each branch of the proof that establishes our approximations are upper/lower bounds by performing.

Models often assume perfect sensing and actuation. A common way of robustifying a model is to add a piecewise constant noise term to the system's dynamics. Doing so while maintaining safety invariants requires also updating the controller so that safety envelope computations incorporate this noise term. The **Add Disturbance Term** update introduces noise terms to differential equations, systematically updates controller guards, and modifies the proof accordingly.

Uncertainty in object classification is naturally modeled in terms of sets of feasible models. In the simplest case, a robot might need to avoid an obstacle that is either static, moves in a straight line, or moves sinusoidally. Our generic model update library contains an update that changes the model by making a static point (x, y) dynamic. For example, one such update introduces the equations {x = −y, y = −x} to a system of differential equations in which the variables x, y do not have differential equations. The controller is updated so that any statements about separation between (a, b) and (x, y) require global separation of (a, b) from the circle on which (x, y) moves. The proof is also updated by

4 Extended discussion of these model updates is available in [10, Chapters 8 and 9].

prepending to the first occurrence of a differential tactic on each branch with a sequence of differential cuts that characterize circular motion.

Model updates also provide a framework for characterizing algorithms that combine model identification and controller synthesis. One example is our synthesis algorithm for systems whose ODEs have solutions in a decidable fragment of real arithmetic (a subset of linear ODEs). Unlike other model updates, we do not assume that any initial model is provided; instead, we learn a model (and associated control policy) entirely from data. The **Learn Linear Dynamics** update takes as input: (1) data from previous executions of the system, and (2) a desired safety constraint. From these two inputs, the update computes a set of differential equations odes that comport with prior observations, a corresponding controller ctrl that enforces the desired safety constraint with corresponding initial conditions init, and a Bellerophon tactic prf which proves init → [{ctrl; odes}∗]safe . Computing the model requires an exhaustive search of the space of possible ODEs followed by a computation of a safe control policy using solutions to the resulting ODEs. Once a correct controller is computed, the proof proceeds by symbolically decomposing the control program and solving the ODEs on each resulting control branch. The full mechanism is beyond the scope of this paper but explained in detail elsewhere [10, Chapter 9].

*Significance of Selected Updates.* The updates described in this section demonstrate several possible modes of use for VPMUs and μlearning. VPMUS can update existing models to account for systematic modeling errors (e.g., missing actuator noise or changes in the dynamical behavior of obstacles). VPMUs can automatically optimize control logic in a proof-preserving fashion. VPMUS can also be used to generate accurate models and corresponding controllers from experimental data made available at design time, without access to any prior model of the environment.

# **6 Experimental Validation**

The μlearning algorithms introduced in this paper are designed to answer the following question: given a set of possible models that contains the one true model, how can we *safely* perform a set of experiments that allow us to efficiently discover a minimal safety constraint? In this section we present two experiments which demonstrate the use of μlearning in safety-critical settings. Overall, these experiments empirically validate our theorems by demonstrating that μlearning processes with accurate models do not violate safety constraints.

Our simulations use a conservative discretization of the hybrid systems models, and we translated monitoring conditions by hand into Python from ModelPlex's C output. Although we evaluate our approach in a research prototype implemented in Python for the sake of convenience, there is a verified compilation pipeline for models implemented in dL that eliminates uncertainty introduced by discretization and hand-translations [7].

**Adaptive Cruise Control.** Adaptive Cruise Control (ACC) is a common feature in new cars. ACC systems change the speed of the car in response to the changes in the speed of traffic in front of the car; e.g., if the car in front of an ACC-enabled car begins slowing down, then the ACC system will decelerate to match the velocity of the leading car. Our first set of experiments consider a simple linear model of ACC in which the acceleration set-point is perturbed by an unknown parameter p; i.e., the relative position of the two vehicles is determined by the equations pos rel = velrel, vel rel = accrel.

In [14], the authors consider the collision avoidance problem when a noise term is added so that vel rel = paccrel. We are able to outperform the approach in [14] by combining the **Add Noise Term** and **Parameter Instantiation** updates; we outperform in terms of both avoiding unsafe states and in terms of cumulative reward. These two updates allow us to insert a multiplicative noise term p into these equations, synthesize a provably correct controller, and then choose the correct value for this noise term at runtime. Unlike [14], μlearning avoids all safety violations. The graph in Fig. 1 compares the Justified Speculative Control approach of [14] to our approach in terms of cumulative reward; in addition to substantially outperforming the JSC algorithm of [14], μlearning also avoids 204 more crashes throughout a 1,000 episode training process.

**Fig. 1.** Left: The cumulative reward obtained by Justified Speculative Control [14] (green) and *µ*learning (blue) during training over 1,000 episodes with each episode truncated at 100 steps. Each episode used a randomly selected error term that remains constant throughout each episode but may change between episodes. Right: a visualization of the hierarchical safety environment. (Color figure online)

**A Hierarchical Problem.** Model update learning can be extended to provide formal guarantees for hierarchical reinforcement learning algorithms [6]. If each feasible model m corresponds to a subtask, and if all states satisfying termination conditions for subtask m*i* are also safe initial states for any subtask m*j* reachable from m*i*, then μlearning directly supports safe hierarchical reinforcement learning by re-initializing M to the initial (maximal) model set whenever reaching a termination condition for the current subtask.

We implemented a variant of μlearning that performs this re-initialization and validated this algorithm in an environment where a car must first navigate an intersection containing another car and then must avoid a pedestrian in a crosswalk (as illustrated in Fig. 1). In the crosswalk case, the pedestrian at (ped*x*, ped*y*) may either continue to walk along a sidewalk indefinitely or may enters the crosswalk at some point between c*min* ≤ ped*y* ≤ c*max* (the boundaries of the crosswalk). This case study demonstrates that safe hierarchical reinforcement learning is simply safe μlearning with safe model re-initialization.

### **7 Related Work**

Related work falls into three broad categories: safe reinforcement learning, runtime falsification, and program synthesis.

Our approach toward safe reinforcement learning differs from existing approaches that do not include a formal verification component (e.g., as surveyed by Garc´ıa and Fern´andez [15] and the SMT-based constrained learning approach of Junges et al. [21]) because we focused on *verifiably* safe learning; i.e., instead of relying on oracles or conjectures, constraints are derived in a provably correct way from formally verified safety proofs. The difference between verifiably safe learning and safe learning is significant, and is equivalent to the difference between verified and unverified software. Unlike most existing approaches our safety guarantees apply to both the learning process and the final learned policy.

Section 2 discusses how our work relates to the few existing approaches toward *verifiably* safe reinforcement learning. Unlike those [3,14,17,20], as well as work on model checking and verification for MDPs [18], we introduce an approach toward verifiably safe off-model learning. Our approach is the first to combine model synthesis at design time with model falsification at runtime so that safety guarantees capture a wide range of possible futures instead of relying on a single accurate environmental model. Safe off-model learning is an important problem because autonomous systems must be able to cope with unanticipated scenarios. Ours is the first approach toward verifiably safe off-model learning.

Several recent papers focus on providing safety guarantees for model-free reinforcement learning. Trust Region Policy Optimization [31] defines safety as monotonic policy improvement, a much weaker notion of safety than the constraints guaranteed by our approach. Constrained Policy Optimization [1] extends TRPO with guarantees that an agent nearly satisfies safety constraints during learning. Br´azdil et al. [8] give probabilistic guarantees by performing a heuristic-driven exploration of the model. Our approach is model-based instead of model-free, and instead of focusing on learning safely without a model we focus on identifying accurate models from data obtained both at design time and at runtime. Learning concise dynamical systems representations has one substantial advantage over model-free methods: safety guarantees are stated with respect to an explainable model that captures the safety-critical assumptions about the system's dynamics. Synthesizing explainable models is important because safety guarantees are always stated with respect to a model; therefore, engineers must be able to understand inductively synthesized models in order to understand what safety properties their systems do (and do not) ensure.

Akazaki et al. propose an approach, based on deep reinforcement learning, for efficiently discovering defects in models of cyber-physical systems with specifications stated in signal temporal logic [2]. Model falsification is an important component of our approach; however, unlike Akazaki et al., we also propose an approach toward obtaining more robust models and explain how runtime falsification can be used to obtain safety guarantees for off-model learning.

Our approach includes a model synthesis phase that is closely related to program synthesis and program repair algorithms [23,24,29]. Relative to work on program synthesis and repair, VPMUs are unique in several ways. We are the first to explore *hybrid* program repair. Our approach combines program verification with mutation. We treat programs as *models* in which one part of the model is varied according to interactions with the environment and another part of the model is systematically derived (together with a correctness proof) from these changes. This separation of the dynamics into inductively synthesized models and deductively synthesized controllers enables our approach toward using programs as representations of dynamic safety constraints during reinforcement learning.

Although we are the first to explore hybrid program repair, several researchers have explored the problem of synthesizing hybrid systems from data [5,30]. This work is closely related to our **Learn Linear Dynamics** update. Sadraddini and Belta provide formal guarantees for data-driven model identification and controller synthesis [30]. Relative to this work, our **Learn Linear Dynamics** update is continuous-time, synthesizes a computer-checked correctness proof but does not consider the full class of linear ODEs. Unlike Asarin et al. [5], our full set of model updates is sometimes capable of synthesizing nonlinear dynamical systems from data (e.g., the static → circular update) and produces computer-checked correctness proofs for permissive controllers.

# **8 Conclusions**

This paper introduces an approach toward verifiably safe off-model learning that uses a combination of design-time verification-preserving model updates and runtime model update learning to provide safety guarantees even when there is no single accurate model available at design time. We introduced a set of model updates that capture common ways in which models can deviate from reality, and introduced an update that is capable of synthesizing ODEs and provably correct controllers without access to an initial model. Finally, we proved safety and efficiency theorems for active μlearning and evaluated our approach on some representative examples of hybrid systems control tasks. Together, these contributions constitute a first approach toward verifiably safe off-model learning.

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Correction to: WAPS: Weighted and Projected Sampling

Rahul Gupta, Shubham Sharma, Subhajit Roy, and Kuldeep S. Meel

Correction to: Chapter "WAPS: Weighted and Projected Sampling" in: T. Vojnar and L. Zhang (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, LNCS 11427, https://doi.org/10.1007/978-3-030-17462-0\_4

In the version of this paper that was originally published, there was an error in the acknowledgement at the bottom of the first page. "AI Singapore Grant [R-252-000- A16-490]" was mentioned instead of "National Research Foundation Singapore under its AI Singapore Programme [Award Number: AISG-RP-2018-005]". This has now been corrected.

The updated version of this chapter can be found at https://doi.org/10.1007/978-3-030-17462-0\_4

# Author Index

Abate, Alessandro II-247 Amparore, Elvio Gilberto II-285 André, Étienne II-211 Arcak, Murat II-265 Baarir, Souheib I-135 Babar, Junaid II-303 Bakhirkin, Alexey II-79 Barbon, Gianluca I-386 Basset, Nicolas II-79 Becker, Nils I-99 Belmonte, Gina I-281 Beneš, Nikola II-339 Biere, Armin I-41 Bisping, Benjamin I-244 Blanchette, Jasmin Christian I-192 Bläsius, Thomas I-117 Blicha, Martin I-3 Bloemen, Vincent II-211 Bodden, Eric II-393 Bozga, Marius II-3 Bozzano, Marco I-379 Brain, Martin I-79 Brim, Luboš II-339 Bruintjes, Harold I-379 Bunte, Olav II-21 Butkova, Yuliya II-191 Castro, Pablo F. II-375 Cauchi, Nathalie II-247 Češka, Milan II-172 Chen, Taolue I-155 Chen, Yu-Fang I-365 Christakis, Maria I-226 Ciancia, Vincenzo I-281 Ciardo, Gianfranco II-285, II-303 Cimatti, Alessandro I-379 Cruanes, Simon I-192

D'Argenio, Pedro R. II-375 Dawes, Joshua Heneage II-98 de Vink, Erik P. II-21 Demasi, Ramiro II-375 Donatelli, Susanna II-285

Eles, Petru I-299 Enevoldsen, Søren I-316 Esparza, Javier II-154 Fox, Gereon II-191 Franzoni, Giovanni II-98 Friedrich, Tobias I-117 Fulton, Nathan I-413 Ganjei, Zeinab I-299 Gao, Pengfei I-155 Gligoric, Milos I-174 Govi, Giacomo II-98 Groote, Jan Friso II-21 Guldstrand Larsen, Kim I-316 Gupta, Aarti I-351 Gupta, Rahul I-59 Hahn, Christopher II-115 Hahn, Ernst Moritz I-395 Hartmanns, Arnd I-344 Hasuo, Ichiro II-135 Heizmann, Matthias I-226 Henrio, Ludovic I-299

Hermann, Ben II-393 Heule, Marijn J. H. I-41 Huang, Bo-Yuan I-351 Hyvärinen, Antti E. J.   I-99 Sun, Xuechao I-365 Sun, Youcheng I-79 Sutton, Andrew M. I-117

Tentrup, Leander II-115 Tonetta, Stefano I-379 Trivedi, Ashutosh I-395 Turrini, Andrea I-365

Urabe, Natsuki II-135

van de Pol, Jaco II-58, II-211 van Dijk, Tom II-58 Veanes, Margus I-372 Vukmirović, Petar I-192

Wan, Tiki I-372 Wang, Kaiyuan I-174 Wang, Qi II-40 Wang, Wenxi I-174 Wesselink, Wieger II-21 Widder, Josef II-357

Wijs, Anton I-21, II-21 Willemse, Tim A. C. II-21 Wojtczak, Dominik I-395 Wüstholz, Valentin I-226

Xie, Hongyi I-155 Xu, Eric I-372 Xu, Junnan I-365

Yamada, Akihisa I-262

Zamani, Majid II-265 Zhang, Hongce I-351 Zhang, Jun I-155 Zhang, Min II-40 Zuleger, Florian II-319, II-357