Safety Verification of Model Based Reinforcement Learning Controllers
Authors: akshita gupta
Inseok Hwang
Venue:  (2021)
Keywords: Reachable set
state constraints
safety verification
model-based reinforcement learning

Abstract: Model-based reinforcement learning (RL) has emerged as a promising tool for developing controllers for real world systems (e.g., robotics, autonomous driving, etc.).  However, real systems often have constraints imposed on their state space which must be satisfied to ensure the safety of the system and its environment. Developing a verification tool for RL algorithms is challenging because the non-linear structure of neural networks impedes analytical verification of such models or controllers.  To this end, we present a novel safety verification framework for model-based RL controllers using reachable set analysis.  The proposed framework can efficiently handle models and controllers which are represented using neural networks. Additionally, if a controller fails to satisfy the safety constraints in general, the proposed framework can also be used to identify the subset of initial states from which the controller can be safely executed.

Under review as a conference paper at ICLR 2021
SAFETY VERIFICATION OF MODEL BASED REINFORCEMENT LEARNING CONTROLLERS
Anonymous authors
Paper under double-blind review
ABSTRACT
Model-based reinforcement learning (RL) has emerged as a promising tool for developing controllers for real world systems (e.g., robotics, autonomous driving, etc.). However, real systems often have constraints imposed on their state space which must be satisfied ensure the safety of the system and its environment. Developing verification tool for RL algorithms is challenging because the non- linear structure of neural networks impedes analytical verification of such models or controllers. To this end, we present a novel safety verification framework for model-based RI controllers using reachable set analysis. The proposed frame- work can efficiently handle models and controllers which are represented using neural networks. Additionally, if a controller fails to satisfy the safety constraints in general, the proposed framework can also be used to identify the subset of initial states from which the controller can be safely executed.
INTRODUCTION
One of the primary reasons for the growing application of reinforcement learning (RL) algorithms in developing optimal controllers is that RL does not assume a priori knowledge of the system dy- namics. Model-based RL explicitly learns a model of the system dynamics, from observed samples of state transitions. This learnt model is used along with planning algorithm to develop optimal controllers for different tasks. Thus, any uncertainties in the system, including environment noise, friction, air-drag etc., can also be captured by the modeled dynamics.
However, the performance of the controller directly related to how accurately the learnt model represents the true system dynamics. Due to the discrepancy between the learnt model and the true model, the developed controller can behave unexpectedly when deployed on the real physical system, e.g., land robots, UAVs, etc. (Benbrahim & Franklin 1997 Endo et al. 2008 Morimoto Doya 200Tp. This unexpected behavior may result in the violation of constraints imposed on the system, thereby violating its safety requirements (Moldovan & Abbeel, 2012). Thus, it is necessary to have a framework which can ensure that the controller will satisfy the safety constraints before it is deployed real system. This raises the primary question of interest: Given a of safety constraints imposed on the state space, how do we determine whether a given controller is safe or not?
In the literature, there have been several works that focus on the problem of ensuring safety. Most of these works incorporate safety constraints in the learning phase train controller (policy) to satisfy certain desired specifications or constraints. However, to achieve this goal, some works make strict assumptions on the complete or accurate knowledge of the system dynamics [heng & Ratifi 2020 Hasanbeig et al. 2020) which can be difficult to obtain. Further, to incorporate safety during learning, some works approximate the original problem to represent safety constraints in a tractable form (Fu et al. [Am et al. 2019). which reduces the performance of the final trained controller
[Fu et al. 2018 Briksson & Dimitrakakis 2019 Junges et al. 2016 Könighoter et al., 2020). On
the other hand, some of the works aim at finding safe controller, under the assumption of a known
baseline safe policy (Hans et al. 2008 Garcia & Fernández 2012; Berkenkamp et al. 2017 Thomas
et al., 2015: Laroche et al. 2019 Zheng & Rathifi 2020), several known safe policies (Perkins
& Barto] 2002). However, such safe policies may not be readily available in general. Alternatively,
Akametalu et al. (2014) used reachability analysis to develop safe model-based controllers, under the

---

Under review as a conference paper at ICLR 2021
assumption that the system dynamics can be modeled using Gaussian processes, i... assumption which is violated by most modern RL methods that make use of neural networks (NN) instead.
While there have been several works proposed to develop safe controllers, some of the assumptions made in these works may not be possible to realize in practice. In recent years, this limitation has drawn attention towards developing verification frameworks for RL controllers, which is the focus of this paper. The safety verification algorithm proposed in this work is a standalone framework which makes no assumptions on how the model-based RL controller is trained. It works independently of the training phase to identify the safe initial conditions for any given policy. One advantage of using a standalone verification framework is that we can deploy potentially unsafe policies on real systems, without further training, by restricting their initial conditions to only the safe states. Since verifying safety of an NN based RL controller is also related to verifying the safety of the underlying NN model (Xiang et al,, 2018b; Tran et al., 2019b; Xiang et al. 2018 8a an additional review for these methods in Appendix A.
Tran et al. 2019a), we provide
Contributions: In this work, we focus on the problem of determining whether given controller safe or not, with respect to satisfying constraints imposed on the state space. To do so, we pro- pose a novel safety verification algorithm for model-based RL controllers using, forward reachable tube analysis that can handle NN based learnt dynamics and controllers, while also being robust against modeling error. The problem of determining the reachable tube is framed as an optimal control problem using the Hamilton Jacobi (HJ) partial differential equation (PDE), whose solution computed using the level set method. The advantage of using the level set method is the fact that it can represent sets with non-convex boundaries, thereby avoiding approximation errors that most existing methods suffer from. Additionally, if a controller is deemed unsafe, we take a step further to identify if there are any starting conditions from which the given controller can be safely exe- cuted. To achieve this, a backward reachable tube is computed for the learnt model and, to the best of our knowledge, this is the first work which computes the backward reachable tube over an NN. Finally, empirical results are presented on two domains inspired by real-world applications where safety verification is critical.
2 PROBLEM SETTING
Let S R" denote the set of states and A C R" denote the set of feasible actions for the RL agent. Let So C S denote the set of bounded initial states and & := {(st, a=)) represent a trajectory generated over a finite time T, as a sequence of state and action tuples, where subscript t denotes the instantaneous time. Additionaly, let s(-) and a(-) represent a sequence of states and actions, respectively. The state constraints imposed on the system are represented as unsafe regions using bounded sets C, = c(" where C C S, Vi E 21, .p.. The true system dynamics is f(s,, a), and is unknown to the agent.
c(), given by a non-linear function f S A - IR. such that,
A model-based RL. algorithm is used to find an optimal controller æ S - A., to reach a set of target states T C S within some finite time T, while avoiding constraints C, An NN model, fo : S x A- + R" parameterized by weights 6, is trained to learn the true, but unknown, system dynamics from the observed state transition data tuples D = {(st a; ) (6)) J However, due to sampling bias, the learnt model fo may not be accurate. We assume that it is possible to estimate a bounded set D C R" such that, at any state 8 E S, augmenting the learnt dynamics fo with some D results in closer approximation of the true system dynamics at that particular state. Using this notation, we now define the problem of safety verification of given controller π (s)).
Problem 1 (Safety verification): Given set of initial states So, determine if Vso E So, all the trajectories & executed under n (8) and following the system dynamics J, satisfy the constraints C, or not.
The solution Problem 1 will only provide a binary yes or answer to whether :T(s) is safe not with respect to Sg. In the case where the policy is unsafe, a stronger result is the identification of safe initial states feafe C So from which (s) executes trajectories which always satisfy the constraints C, This problem is stated below.
2

---

Under review as a conference paper at ICLR 2021
Problem 2 (Safe initial states): Given (s), find Seafe- such that, any trajectory & executed under ((s) and following the system dynamics f. starting from any 8o E Seafe. satisfies the constraints C.
SAFETY VERIFICATION
To address Problems 1 and we use reachability analysis. Reachability analysis is an exhaustive verification technique which tracks the evolution the system states over a finite time, known as the reachable tube, from given set of initial states So (Maler 2008). If the evolution is tracked starting from Sg, then it called the forward reachable tube and is denoted as F ((T"). Analogously, if the evolution is tracked starting from C, to Sg, then it is called the backward reachable tube and is denoted as (T)
In the following sections, will formulate reachable tube problem for NN-based models and controllers, and then propose a verification framework that (a) can determine whether or not a given policy и is safe, and (b) can compute fsafe if is unsafe. To do so, there need to be answered. First, since the true system dynamics f is unknown, how can we determine a conservative bound on the modeling eπror, to augment the learnt model fe and better model the true system dynamics when evaluating a controller x? Second, how do we formulate the forward and backward reachable tube problems over the NN modeled system dynamics?
main questions that
3.1 MODEL-BASER REINFORCEMENT LEARNING
In this section, we focus on the necessary requirements for the modeled dynamics fe and discuss the estimation of the modeling error set DD. A summary of the model-based RL framework is presented in Appendix A.2 Recall that the learnt model fo is represented using NN and predicts the change in states A E IR" To learn Se. an observed data set D = ((8,, Ot, As++ 1 ) ) is first split into a training data set Dr and a validation data set D.- A supervised learning technique is then used to train fo over D, by minimizing the prediction error E N, Σ [ As where A is the change predicted by the learnt model, A the true observed change in state and N₂ = |De]- With this notation, we now formalize the following necessary assumption for this work. This assumption is required to ensure boundedness during analysis and is easily satisfied by NNs that use common activation functions like t tanh or s sigmoid (Usama & Chang 2018).
Assumption fo is Lipschitz continuous and Vj E {1,..., n). AS, [-c, cl, where |c| 00.
As mentioned earlier, the accuracy of the learnt model fe depends on the quality of data and the NN being used, thereby resulting some modeling error in the prediction of the next state. Estimating modeling errors is an active area of research and is required for several existing works on safe RL. (Akametalu et al. 2014 Gillula & Tomlin 2012), and complementary to goal. Since the primary contribution of this work is the development of reachable tube formulation for model-based controllers that use NNs, we rely on existing techniques (Moldovan
Modeling error:
et al. 2015) to estimate conservative modeling error bound. We leverage the error estimates d, A -Asدح A of fo. for the transition tuples in the validation set D. construct the upper confidence bound d+ [di, d2,... d,)) and lower confidence bound d' = [-d1, -d2, ... - d,] for d, for each state dimension. Let high-confidence bounded error set D be defined such that {d: Vi E [), d; d4 < d. We then use IT to represent the augmented learnt system dynamics
: a) + d. den
3.2 REACHABLE TUBE FORMULATION
For exhaustive verification technique continuous state and action space, it is infeasible to sample trajectories from every point in the given initial state and further, to verify whether all these trajectories satisfy the safety constraints. Therefore, reachable sets usually (approximately) rep- resented as convex polyhedrons and their evolution is tracked by pushing the boundaries of this polyhedron according to the system dynamics. However, convex polyhedrons can lead to large
3

---

Under review as a conference paper at ICLR 2021
Forward Reachable Set
Backward Reachable Set
Input: str), Dc.
Ex(-7) BRTU, ,ts).C,)
Sunsafe = B (-7) Sg
d Modiciingrrott....
8 =)
Saae Sunafe n Sp
Fx(T) FRTj. (c.)()))
Ssafe
Yes-
x(s) unsate
(R()) =
A(S) sale
C1
a(3) safe for Initial states State
Stop
Figure 1: Flowchart of the proposed safety verification algorithm. The rectangle on the left repre- sents the flow for computing the forward reachable tube (FRT), which can only state r(s) is safe or unsafe for Sp. The rectangle tube (BRT), which is invoked if I (s) is unsafe. The BRT analysis can compute the subset of safe initial states fa for (s). if such set exists.
the right presents the flow for computing the backward reachable
approximation errors, we leverage the level method (Mitchell et al. 2005 to compute the bound- aries of the reachable tube for NN-based models and controllers at every time instant. With the level set method, even non-convex boundaries of the reachable tube can be represented, thereby en- suring an accurate computation of the reachable tube (Mitchell et al. 2005). Since the non-linear, non-convex structure of NNs not suitable for analytical verification techniques, the reachability analysis gives efficient, simulation-base fore, in this subsection, we formulate the reachable tube for NN modeled system dynamics fo, but first we formally define the forward reachable tube and backward reachable tube for a policy T(s).
approach analyze the safety of the controller. There-
Forward reachable tube (FRT): It is the set of all states that can be reached from initial set Su. when the trajectories are executed under policy it (s) and system dynamics f(r) (s, a, d). The FRT computed over a finite length of time T and is formally defined as
(T( {s Ad E D, s(-) satisfies = f(()) (s, a, d), where a (s)) sto E So, T}, (2)
where to and ty denote the initial and final time of the trajectory &. respectively.
Backward reachable tube (BRT): the all states which can reach given bounded tar- get set T C R., when the trajectories & are executed under policy T(s) and system dynamics ((r) (s, a. d). The BRT is also computed for finite length of time, with the trajectories starting at time la -T and ending at time O. It is denoted as
BR(-T) = (so : Vd E D. s(-) satisfies = ffr)) (s, a, d), where a = T(s) with Sto s-T; St, E T,ty [-T.0]].
The key difference between the FRT and BRT is that, for the former, the initial set of states are known, whereas for the latter, the final of states known.
4

---

Under review as a conference paper at ICLR 2021
Outline: The flowchart of the safety verification framework proposed in this work is presented in Fig. Given a model-based policy (s), the set of initial states So and the set of constrained states Cg. the first step is to estimate the bounded set of modeling error D, as discussed in Section 3.1. Using 1 the FRT is constructed from the initial set So and it contains all the states reachable by TT()) over a finite time T. Thus, if the FRT contains any state from the unsafe region C.. ((s)
deemed unsafe. Therefore, the solution to Problem is determined by analyzing the set of intersection of the FRT with C,
{ safe if (T)T)nC. 0, π -= unsafe (R(T) + 0.
(4)
If (8) is classified as safe for the entire set Sp. then no further analysis is required. However, if (s) classified as unsafe, we proceed to compute the subset Saaee Sy of initial states for which (s) generates safe trajectories. Seafe is the solution to rrollem[and allows an unsafe policy to be deployed on a real system, with restrictions on the starting states. To this end, the BRT is computed from the unsafe region C.. to determine the set of trajectories (and states) which terminate in C,- The intersection of the BRT with So determines the set of unsafe initial states Sunsofe. To determine Sea we utilize the following properties, (a) Ssafe U Sunsafe So, and (b) Saafe Sunsofe 0, and compute
Sen = Sunsafe Ngg-
(5)
If Safee * 0. then we have identified the safe initial states for rTs), otherwise, it is concluded that there are no initial states in So from which x (8) can generate safe trajectories.
Mathematical Formulation:
This section presents the mathematical formulation to compute the BRT. The FRT can be computed with a slight modification to the BRT formulation and this dis- cussed in the end of this section.
Recall, for the BRT problem, there exists a target set T C R" which the agent has to reach in finite time, i.e., the condition on the final state is given as 8t, E T. Conventionally, for the BRT formulation, the final time ty = and the starting time ty TT where evaluating a policy (s)), the controller input is computed by the given policy as a = T(s). However,
T < co. When
following the system dynamics f(r)) in d the modeling error d is now included in the system as an adversarial input, whose value at each state is determined so as to maximize the controller's cost function. We use the HJ PDE to formulate the effect of the modeling error on the system for computing the BRT, but first we briefly review the formulation of the HJ PDE with an NN modeled system dynamics fo in the following.
For an optimal controller, we first define the cost function which the controller has to minimize. Let C(st, az) denote the running cost of the agent, which is dependent on the state and action taken at time t E [-T.0] 0]. Let g(s;,) denote the cost at the final state Sty, Then, the goal of the optimal controller is to find series of optimal actions such that
min (L C(Sr, ar )dT ((s),,a)dr a-(-)
+ {((,,))
subject to é fols. a), sty TT
where a A and fo is the NN modeled system dynamics. The above optimization problem is solved using the dynamic programming approach (Smith & Smith 1991), which based on the Principle of Optimality (Troutman) 2012). Let V(st. denote the value function of a state s at time t t [-TT, OT. such that
[."" ay)r + g( a-(+)
win J C(s,, a,),, + V($+4s o)]
(7) where 5 > O. ((,,, t) is a quantitative measure of being at a state s, described in terms of the cost required reach the goal state from s. Then, using the Taylor series expansion, V( t d) is approximated around V(s 1) in 7 to derive the HJ PDE as dV
V(st,
min
+ min VV fo(s, + C(s, = 0, dt
(8)
[4) = g(8t,);
5

---

Under review as a conference paper at ICLR 2021
where VV IR is the spatial derivative of V. Additionally, the time index has been dropped above and the dynamics constraint in ( has been included in the PDE. Equation @ is a terminal value PDE, and by solving B). we can compute the value of state V( t) at any time t.
We now discuss how the formulation in can be modified to obtain the BRT. It is noted that along with computing the value function, the formulation in also computes the optimal action a. the optimal policy π (s) is already provided. Therefore, the constraint (T) should be included problem 6 thereby avoiding the need of minimizing over actions E A in B Additionally, as discussed in Section 3.1, the NN modeled system dynamies fo may not be a good approximation of the true system dynamics f. Instead, the augmented learnt system dynamics f in used in place of fe in (8. since better models the true dynamics at a given state. However, by including f(r) in 88. the modeling error d is now included in the formulation. The modeling error E D is treated as an adversarial input which is trying to drive the system away from it's goal state by taking value which maximizes the cost function at each state. Thus, to account for this adversarial input, the formulation in is now maximized over
However, in Problems Tand 2
Lastly, the BRT problem is posed for set of states and not an individual state. Hence, efficient representation of the target set is required to propagate an entire set of trajectories at a time, as opposed to propagating individual trajectories.
Assumption The target set T C R" is closed and can be represented as the zero sublevel set of a
bounded and Lipschitz continuous function L: R + IR such that, T ((s) S 0}.
The above assumption defines a function I check whether a state lies inside or outside the target set. If T is represented using regular, well-defined geometric shape (like sphere, rectangle, cylinder, etc.), then deriving the level set function ((8) is straight forward, whereas, an irregularly shaped T can be represented as a union of several well-defined geometric shapes to derive ((8).
For the BRT problem, the goal is to determine all the states which can reach T. within a finite time. The path taken by the controller is irrelevant and only the value of the final state is used to determine any state s E (-T). From Assumption 2 the terminal condition 8t, E T can be restated as ((sr,) S O. Thus, to prevent the system from reaching T, the adversarial input d tries to maximize I(st,). ). thereby pushing St, as far away from T as possible. Therefore, the cost function in (6) is modified to J I(ss,). Additionally, any state which reach T within finite time interval 7 is included in the BRT. Therefore, if any trajectory reaches T at some ty < O, it shouldn' 't be allowed leave the set. Keeping this in mind, the BRT optimization problem can be posed as
max
min ((Stg) d(-) (E(-T.
subject to: = fs, a, d), a a= ==)(s), 1(se,) < S,
where the inner minimization over time prevents the trajectory from leaving the target set. Then, the value function for the above problem is defined as
Vn(#;, () max ((s(1))). d()
(10)
Comparing this with 7 it is observed that the value of state is longer dependent the running cost C(s,, a). This doesn't imply that the generated trajectories are not optimal w.r.t action a, because the running cost is equivalent to the negative reward function, for which rss) is already optimized. Instead, VR solely depends on whether the final state of the trajectory lies within the target not, i.e., whether or not 8t, T. Thus, the value function VR for any state is equal to ((st,), where St, is the final state of the trajectory originating at Then, the HJ PDE for the problem in ( is stated as
imesn'timmly
dVR dt
+ Min VVR(s..), 0.
Vn((i,, 1(seg);
(11)
where H max (VVn (s,
where H' represents the optimal Hamiltonian. Since we are computing the BRT, min (s, VVR(S,, (),0) ()) in the PDE above ensures that the tube grows only in the backward

---

Under review as a conference paper at ICLR 2021
0fT chrttctes and?
Gool dtilce
Ctstadee
0-
Figure 2: (Left) The environment for the safe land navigation problem. (Middle) The FRTs for both the augmented learnt model dynamics and true system dynamics classify the controller unsafe. (Right) The BRT computed from obstacles and for the given controller. Ssafe computed by the proposed BRT algorithm is compared with the ground truth (G.T.) data for the safe initial states, marked in green.
direction, thereby preventing trajectory which has reached T from leaving. In Problem (I.. the optimal action has been substituted by T(s) and the augmented learnt dynamics is used instead of fe. The Hamiltonian optimization problem can be further simplified to derive an analytical solution for the modeling error. By substituting the augmented dynamics from I the optimization problem can be re-written as
H VVn fo a) max VVR d.
(12)
Expanding VVR = [P1, .a..... Pnl T E R", the vector product VV d pıd + p2d2 + Therefore, to maximize VVR d, the disturbance control is chosen
+.... ... pr
d2
if p: >
d, = -dd
Vi 1,......
(13)
if
<
With this analytical solution, the final PDE representing the BRT is stated as
dVR + min(0, (s, VRn(s: (), 0,
dt
VR(St,, = =((st)), where H" VR (o(8,a)+((
(14)
+ |p2 +... + Pnn (dn).
The value function Vn( in represents the evolution of the target level set function back- wards in time. By finding the solution to VR in the above PDE, the level set function is determined at any time instant / [-T,-0 0), thereby determining the BRT. From the result of Theorem 2 in Mitchell je al. (2005). it is proved that the solution of VR the BRT. Thus,
14
at any time gives the zero sublevel set for
(15) The solution to VA can be computed numerically by using existing solvers for the level set method. brief note on the implementation of the algorithm is included in subsection A.3 in the Appendix.
BR(-T) = {s: VR(S,, t) - 0, tE [-r,0]]
There are a few things to note about the formulation in 14b. First, Equation 14 assumes that T is desired goal state. However, the formulation can be modified ' is an unsafe set, which case, the adversarial modeling error tries to minimize the Hamiltonian. Similarly. the input d can represent any other disturbance in the system, either adversarial or cooperative. Second, to compute the FRT, the formulation in (14) is modified from final value PDE an initial value PDE.
4 EXPERIMENTS
In our experiments, we aim to answer the following questions: (a) Can safety verification be done for an NN-based π and fo using FRT?, and (b) Can Saate be identified using BRT if deemed un- safe? To answer these questions, demonstrate results the following domains inspired by

---

Under review as a conference paper at ICLR 2021
real world safety-critical problems, where RL controllers developed using learnt model can be ap- pealing, as they can adapt to transition dynamics involving friction, air-drag, wind, etc., which might be hard to explicitly model otherwise. It is noted that since the proposed verification framework is developed for control-oriented tasks for physical systems, the state representation of such systems comprises of position, velocity and orientation data. Therefore, the state dimensions of such class of problems are typically not as large as the popular image-based OpenAl or Deepmind domains. Instead, the results are demonstrated on experimental domains which are similar the ones in prior works on safety verification of NN controllers for physical systems (Xiang et al. 2018b Xlang & Johnson 2018: Akintunde et al. 2018 2019
Safe land navigation: Navigation of ground robot in an indoor environment is a common ap- plication which requires the satisfaction of safety constraints by и to avoid collision with obstacles. For this setting, we simulate a ground robot which has continuous states and actions. The initial configuration of the domaín shown in Fig. 2 The set of initial and goal states are represented by circles and the obstacles with rectangles.
Safe aerial navigation: This domain simulates a navigation problem in an urban environment for unmanned aerial vehicle (UAV). Constraints are incorporated while training æ to ensure that collision is avoided with potential obstacles in its path. States and actions are both continuous and the initial configuration of the domain is shown in Fig E The set of initial and goal states are represented using cuboids, and the obstacles with cylinders.
To address the questions with respect to the above mentioned domains, we first train a NN based fo to estimate the dynamics using sampled transitions. This fu is then also used to learn NN based controller æ which is trained with cost function designed mitigate collisions. For brevity, only the representative results for this π are discussed here; implementation details and more experimental results are available in Appendix
Analysis:
A.5
To address the first question, the FRT is computed for both the domains over the augmented learnt dynamics /67) as shown in Fig. 2 and Fig. Additionally, for land navigation we also compute the FRT over the true system dynamics S. which serves as a way to validate the safety verification result of æ from the proposed framework. It is observed that for both the domains, FRTs deem the given policy π as wnsafe, since the FRTs intersect with one of the obstacles. Even when is learnt using a cost function designed to avoid collisions, the proposed safety verification framework successfully brings out the limitations of æ, which may have resulted due to the use of function approximations, ill-specified hyper-paramertt
convergence
local optimum, etc.
For the second question, the BRT is computed from both the obstacles for the given controller т, as shown Fig. 2 and Fig. S To estimate the accuracy of the BRT computation, we compare the computed fe and S.aff sets with the ground truth (G.T.) data generated using random samples of possible trajectorics. implying that all trajectories are safe w.r.t. obstacle 1. However, the BRT from obstacle 2 intersects with Sy and identifies the subset of initial states which are unsafe. The set of unsafe initial states computed by the BRT algorithm may not be exact, as is seen in Fig. 5 where the BRT computation over approximates fe- Such an information can be critical to safely deploy even an unsafe controller just by restricting its starting conditions.
is observed that the BRT from obstacle 1 does not intersect with So.
CONCLUSION
In this paper, we have presented a novel framework using forward and backward reachable tubes for safety verification and determination of the subset of initial states for which a given model- based RL controller always satisfies the state constraints. The main contribution of this work is the formulation of the reachability problem for neural network modeled system dynamics and the use of level set method to compute exact reachable tube by solving the Hamilton-Jacok partial differential equation, for the reinforcement learning framework, thereby minimizing approximation errors that other existing reachability methods suffer. Additionally, the proposed framework can identify the set of safe initial sets for a given policy, thereby determining the initial conditions for which even sub-optimal, unsafe policy satisfies the safety constraints.
8

---

Under review as a conference paper at ICLR 2021
Ood
1-
Figure 3: (Left) The safe aerial navigation domain. (Middle) The FRT is computed for the aug- mented learnt dynamics. For clarity in 3D, FRT with true dynamics is not plotted; instead the approximation quality can be better visualized in BRT. (Right) Comparison of Seafe computed by the proposed BRT algorithm with the ground truth data of the safe initial states, marked in green (and unsafe states marked in red), is observed that the BRT over approximates Sunsafe-
While the results from the proposed framework are promising, there still room for improvement. One of the drawbacks of using the level set method is the fact that it scales poorly with the increasing dimension of the state space. Recent progress in addressing the scalability issue includes decompo- sition of system dynamics into subsystems which can later be coupled via common states or controls (Bansal et al. 2017| Margellos & Lygeros, 201T, Chen al. 2018). Additionally, the application of reachability analysis in developing safe learning based controllers is also promising direction (Akametalu et al. 2014
Fisac et al. 2018
REFERENCES
Anayo Akametalu, Jaime Fisac, Jeremy H Gillula, Shahab Kaynama, Melanie Zeilinger, and Claire J Tomlin. Reachability safe learning with gaussian processes. In 53rd IEEE Conference on Decision and Control, pp. 1424 1431. IEEE, 2014.
Michael Akintunde, Alessio Lomuscio, Lalit Maganti, and Edoardo Pirovano. Reachability analysis for neural eevermennvir systems. In KR, pp. 184-193, 2018.
Michael E Akintunde, Andreea Kevorchian, Alessio Lomuscio, and Edoardo Pirovano. Verifica- tion of rnn-based neural agent-environment systems. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, pp. 6006-6013, 2019.
Guy Avni, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina Könighofer, and Stefan Pranger. Run-time optimization for learned controllers through quantitative games. In International Conference on Computer Aided Verification, pp. 630-649, Springer, 2019.
Somil Bansal, Mo Chen, Sylvia Herbert, and Claire J Tomlin. Hamilton-jacobi reachability: A brief overview and recent advances. In 2017 IEFF 56th Annual Conference on Decision and Control (CDC), pp. 2242-2253. IEEE, 2017.
Osbert Bastani, Yani loannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, and An- tonio Criminisi. Measuring neural net robustness with constraints. In Advances in neural infor- mation processing systems, pp. 2613-2621, 2016.
Hamid Benbrahim and Judy A Franklin. Biped dynamic walking using reinforcement learning. Roboticy and Autonomous Systems, 22(3-4):283-302, 1997.
Felix Berkenkamp, Matteo Turchetta, Angela Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. In Advances in neural information processing systems, pp. 908-918, 2017.

---

Under review as a conference paper at ICLR 2021
Mo Chen, Sylvia L Herbert, Mahesh S Vashishtha, Somil Bansal, and Claire J Tomlin. Decomposi- tion of reachable sets and tubes for class of nonlinear systems. IEEE Transactions on Automatic -3887,88588,,- 2018.
Control,
Michael G Crandall and P-L Lions. Two approximations of solutions of hamilton-jacobi equations. Mathematics of computation, 43(167):1-19, 1984.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Learning and verifi- cation of feedback control systems using feedforward neural networks. IFAC-PapersOnLinee, (16):151-156, 2018.
Souradeep Dutta, Xin Chen, and Sriram Sankaranarayanan. Reachability analysis for neural feed- back systems using regressive polynomial rule inference. Proceedings of the 22nd ACM Inter- national Conference Hybrid Systems: Computation and Control, pp. 157-168, 2019.
Gen Endo, Jun Morimoto, Takamitsu Matsubara, Jun Nakanishi, and Gordon Cheng. Learning epg- based biped locomotion with a policy gradient method: Application to a humanoid robot. The International Journal of Robotics Research, 27(2):213-228, 2008.
Hannes Eriksson and Christos Dimitrakakis. Epistemic risk-sensitive reinforcement learning. arXiv
preprint arXiv:/906.0622 06273, 2019.
Jaime F Fisac, Anayo K Akametalu, Melanie N Zeilinger, Shahab Kaynama, Jeremy Gillula, and Claire Tomlin. A general safety framework for learning-based control uncertain robotic systems. IEEE Transactions Automatic Control, 64(7):2777-2752, 2018.
Michael Fu et al. Risk-sensitive reinforcement learning: A constrained optimization viewpoint. arXiv preprint
2018.
Javier Garcia and Fernando Fernández. Safe exploration of state and action spaces in reinforcement learning. Journal of Artificial Intelligence Research, 45:515-564, 2012.
Jeremy H Gillula and Claire Tomlin. Guaranteed safe online learning via reachability: track- ing ground target using a quadrotor. In 20/2 IEEE International Conference on Robotics and Automation, pp. 2723-2730. IEEE, 2012.
Alexander Hans, Daniel SchneegaB, Anton Maximilian Schäfer, and Steffen Udluft. Safe explo- ration for reinforcement learning. In ESANN, pp. 143-148, 2008.
Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Cautious reinforcement learning with logical constraints. arXiv preprint arXiv:2002. 12156, 2020.
Chao Huang, Jiameng Fan, Wenchao Li, Xin Chen, and Qi Zhu. Reachnn: Reachability analysis of netral-network controlled systems. ACM Transactions on Embedded Computing Systems (TECS), 18(5s):1-22, 2019.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. International Conference on Computer Aided Verification, pp. 3-29. Springer, 2017.
Radoslav Ivanov, James Weimer, Rajeev Alur, George J Pappas, and Insup Lec. Verisig: veri- fying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 169-178, 2019.
Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topeu, and Joost-Pieter Katoen. Safety- constrained reinforcement learning for mdps. In International Conference on Tools and Algo- rithms for the Construction and Analysis of Systems, pp. 130 146. Springer, 2016.
Guy Katz, Clark Barrett, David I. Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex:
efficient smt solver for verifying deep neural networks. In International Conference Computer Aided Verification, pp. 97-117. Springer, 2017.
Yafim Kazak, Clark Barrett, Guy Katz, and Michael Schapira. Verifying deep-rl-driven systems. In Proceedings of the 2019 Workshop Network Meets Al & MI., pp. 83-89, 2019.
10

---

Under review as a conference paper at ICLR 2021
Bettina Könighofer, Roderick Bloem, Sebastian Junges, Nils Jansen, and Alex Serban. Safe inforcement learning using probabilistic shields. In International Conference on Concurvency Theory: 31st CONCUR 2020: Vienna, Austria (Virtual Conference). Schloss Dagstuhl-Leibniz- Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020.
Marta Z K Wiittkowsa. Safery verification for deep neural networks with provable guarantees. 2019.
Romain Laroche, Paul Trichelair, and Remi Tachet Des Combes. Safe policy improvement with baseline bootstrapping. In International Conference on Machine Learning, pp. 3652-3661. PMLR, 2019.
Oded Maler. Computing reachable sets: An introduction. Tech. rep. French National Center of Scientific Research, 2008.
Kostas Margellos and John Lygeros. Hamilton-jacobb formulation for reach-avoid differential 2011.
games. IEEE Transactions on Automatic Control,
Ian M Mitchell. A toolbox of level set methods. UBC Department of Computer Science Technical Report TR-2007-11, 2007.
Ian Mitchell, Alexandre Bayen, and Claire Tomlin. A time-dependent hamilton-jacon formu- lation of reachable sets for continuous dynamic games. IEEE Transactions on automatic control, 50(7):947-957, 2005.
Teodor Mihai Moldovan and Pieter Abbeel. Safe exploration in markov decision processes. arXiv preprint arXiv:1205.4811 2012.
Teodor Mihai Moldovan, Sergey Levine, Michael Jordan, and Pieter Abbeel. Optimism-driven exploration for nonlinear systems. In 2015 IEEE International Conference on Robotics and Au- tomation (ICRA), pp. 3239 3246. IEEE, 2015.
Jun Morimoto and Kenji Doya. Acquisition of stand-up behavior by real robot using hierarchical reinforcement learning. Robotics and Autonomous Systems, 36(1):37-51, 2001.
Stanley Osher and James A Sethian. Fronts propagating with curvature-depender speed: algorithms based hamilton-jacobi formulations. Journal of computational physics, 79(1): (2:)2-4499 49, 1988.
Stanley Osher, Ronald Fedkiw, and K Piechor. Level methods and dynamic implicit surfaces. Appl. Mech. Rev., 57(3):B15-B15, 2004.
Theodore J Perkins and Andrew G Barto. Lyapunov design for safe reinforcement learning, Journal of Machine Learning Research, 3(Dec):803-$8) 832, 2002.
Luca Pulina and Armando Tacchella. Challenging smt solvers verify neural networks. Ai Com- munications, 25(2):117-135, 2012.
James Albert Sethian. Level set methods and marching methods: evolving interfaces in compu- tational geometry, fluid mechanics, computer vision, and materials science, volume 3. Cambridge university press, 1999.
David K Smith and David K Smith. Dynamic programming: a practical introduction. Ellis Horwood New York, 1991.
Xiaowu Sun, Haitham Khedr, and Yasser Shoukry. Formal verification of neural network controlled autonomous systems. In Proceedings of the 22nd ACM International Conference Hybrid Sys- tems: Computation and Control, pp. 147-156, 2019.
Philip Thomas, Georgios Theocharous, and Mohammad Ghavamzadeh. High confidence policy improvement. In International Conference on Machine Learning, pp. 2380 2388, 2015.
toolbox. https:// cww http://s...aauacoo///////eaaatap
2019.
Tran, Feiyang Cai, Manzanas Lopez Diego, Patrick Musau, Taylor T Johnson, and Xenofon Koutsoukos. Safety verification of cyber-physical systems with reinforcement learning control. ACM Transactions Embedded Computing Systems (TECS), 18-5,):1-22, 2019a.

---

Under review as a conference paper at ICLR 2021
Booag-Dungg Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T Johnson. Parallelizable reachability analysis algorithms for feed- forward neural networks. In 2019 IEEE/ACM 7th Interationnal Conference Formal Methods in Software Engineering (FormaliSE), pp- 51-60. IERE, 2019b.
John L Troutman. Variational calculus and optimal control: optimization with elementary convexity. Springer Science Business Media, 2012.
Muhammad Usama and Dong Eui Chang. Towards robust neural networks with lipschitz continuity. In International Workshop on Digital Watermarking, pp. 373-389. Springer, 2.18.
Weiming Xiang and Taylor T Johnson. Reachability analysis and safety verification for neural network control systems. arXiv preprint 1oXiv:/805.000 1805.09944, 2018.
Weiming Xiang, Hoang-Dung Tran, and Taylor T Johnson. Output reachable set estimation and verification for multilayer neural networks. IEEE transactions on neural networks and learning systems, 29(1 (9(11)577775578 2018a.
Weiming Xiang, Hoang-Dung Tran, Joel A Rosenfeld, and Taylor T Johnson. Reachable set estima- tion and safety verification for piecewise linear systems with neural network controllers. In 2018 Annual American Control Conference (ACC), pp. 1574-1579, IEEE, 2018b.
Guoqing Yang, Guangyi Qian, Pan Lv, and Hong Li. Efficient verification of control systems with neural network controllers. In Proceedings of the 3rd International Conference on Vision, Image and Signal Processing, pp. 1-7, 2019.
Liyuan Zheng and Lillian J Ratliff. Constrained upper confidence reinforcement learning. arXiv preprint a7Xiv22001.09377, 2020.
12


Reviews:
[{"review_id": "uRqafS_kMB1", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "# Summary\n\nThe paper presents a method for safety verification of trained model-based RL agents using reachable set analysis.\nThe method allows to both analyse whether any of the start states might end in an unsafe state, via the forward reachable tube, and to determine which start states do or do not end in an unsafe state, via the backward reachable tube.\nAnother claimed contribution is the first method to calculate the backward reachable tube on NNs.\nAn experimental evaluation is performed on to navigation environments.\n\n# Comments to the Authors\n\nSafety verification is a crucial topic for the acceptance and deployment of learned methods in control systems.\nThis paper contributes a method to verify a model-based RL controller in forwards and backwards direction, given the trained controller, a set of start and goal states and the constraints, i.e. a description of the unsafe states.\n\nThe method appears sound and is presented as straightforward, which will allow adoption in future works and potentially pratical application.\nIt includes the transfer of the backward reachable tube computation to NNs, which is central to the method.\nSince it is outside my expertise, I do not verify the theoretical contributions of the paper.\n\nComing from the experimental evaluation, there are a few questions regarding the applicability of the method:\na) How would it handle dynamic environments, e.g. moving obstacles? As it is, only the deterministic trajectory of the agent appears to be evaluated.\nb) How complex is the method computationally? What are the runtimes for the given examples?\nc) In Figure 3 (right) it appears as if some green starting states are in an unsafe area. Is this a visual artifact or does the method not guarantee that all unsafe starting states are discovered (which was my impression before)?\n\nRegarding the presentation of the paper, I understand that the authors are restricted by the conference format, but I would encourage to revise the selection of material for the main paper and the appendices.\nThe related work part of the paper might be benefit from some of the extended work in the appendix and the experiments could also be described more in detail.\nAt the same time, maybe the size of the flowchart could be improved or non-crucial parts of Sec. 3.2 extracted to the appendix.\nAlso, I think it is okay to put the paper + appendix as the main PDF on openreview, which makes the appendices more accessible for the readers on this platform.", "extra_scores": {}, "extra_text": {}}, {"review_id": "mmCXVZuLafp", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "update after rebuttal: the answers were convincing, and the paper improved. \n\nSummary and Contribution\n\nThis work presents a novel approach for the safety verification of model based RL controllers. It uses a so-called reachability tube analysis to check whether unsafe states may be reached from the initial states of a (learned) model. In case unsafe states may be reached, a backward analysis determines the initial states that are safe (if they exist). Existing methods to measure potential modeling errors are taken into account. The efficacy of the method is demonstrated on two small examples.\n\n\n\nReasons for Score\n\nWith more details on the correctness, better literature study, and more experiments, the paper would be a clear accept. As of now, I see it as marginally above the acceptance threshold.\n\nStrengths\n\n- A novel method for verifying the safety of NN-based controllers\n- A framework to incorporate inherent modeling errors\n\nWeaknesses\n\n- A better comparison to related work is in order\n- The experiments are not very extensive, and it is not clear how to reproduce them.\n- The correctness and completeness of the method, as well as the concrete assumptions on the NN architecture is unclear to me. \n\nQuestions for Authors\n\n- Please compare your work to the literature listed below. What is novel, how does it relate?\n- What assumptions are being made on the neural network architecture? How can you obtain an exact and efficient method (soundness, completeness, global optima) for an potentially undecidable problem? \n- How would your method perform on state-of-the-art benchmark sets like from OpenAI or Deepmind?\n- If you assume model-based RL, and the model is already there, why can't you construct a simpler model like a Markov decision process and reason directly about safety using sound and efficient methods like value iteration or linear programming? I understand you have a continuous state space (as given by the neural network), but do the experiments/examples require such a complicated model?\n\nDetailed Comments\n\n- related work\n\nThere is large body of related work on safety of (model-based) RL which has not been cited, for instance:\n\n\n[1] Prashanth L, A., and Michael Fu. \"Risk-sensitive reinforcement learning: A constrained optimization viewpoint.\" arXiv preprint arXiv:1810.09126 (2018)\n\n[2] Zheng, Liyuan, and Lillian J. Ratliff. \"Constrained upper confidence reinforcement learning.\" arXiv preprint arXiv:2001.09377 (2020).\n\n[3] Eriksson, Hannes, and Christos Dimitrakakis. \"Epistemic Risk-Sensitive Reinforcement Learning.\" arXiv preprint arXiv:1906.06273 (2019).\n\n[4] Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen:\nSafety-Constrained Reinforcement Learning for MDPs. TACAS 2016: 130-146\n\n[5] Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, Roderick Bloem:\nSafe Reinforcement Learning Using Probabilistic Shields. CONCUR 2020: 3:1-3:16\n\n[6] Guy Avni, Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Bettina Könighofer, Stefan Pranger:\nRun-Time Optimization for Learned Controllers Through Quantitative Games. CAV (1) 2019: 630-649\n\n[7] Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:\nCautious Reinforcement Learning with Logical Constraints. AAMAS 2020: 483-491\n\n\n[8] Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening:\nLogically-Correct Reinforcement Learning. CoRR abs/1801.08099 (2018)\n\n\n- correctness and efficiency\n\nI don't really understand how you can incorporate nonconvex boundaries of the reachable tube. In any case, it should be an overapproximation. How is the efficiency of the method? How will it perform in practice? \n\n- experiments\n\nIt would be very nice to see how the method performs on well-known environments like the OpenAI safety gymn or the Deepmind safety gridworlds.\n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "XJqRD3dCZcN", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "## Summary\n\nThe authors propose a safety verification algorithm based on reachability analysis and formal methods that is applicable to dynamics models and policies that are parameterized as neural networks. \n\nI find the problem(s) clear and well-motivated in general. There are many prior works in this area from outside the machine learning community, and I'm not totally convinced that this paper provides a substantial contribution over those works. \n\n## Strengths\n\n - The problem setup is clear and well-motivated\n - The methodology seems solid\n\n## Weaknesses\n\n - The work is framed in the context of model-based RL, but since the model (including the estimate of the modeling error bound $d$) is assumed known, it would seem like this should be framed more squarely within the optimal control literature. Within this literature, there are many methods related to Safe MPC (e.g. [1], [2])  that it would seem are attempting to achieve the same objective as what is stated here. \n\n - The central issue with all of the host of works on formal methods and reachability analysis for dynamical systems is that they don't scale to complex environments or dynamics. As a result, assumptions need to made such as monotonicity (work of Del Vecchio e.g. [3] [4]). The experiments that you show are very simplistic also (low dimensional and very simple/convex geometry). Is there something about this approach which allows us to make progress in terms of scaling these methods to real world problems.  \n\n - You argue that \"Estimating modeling errors is an active area of research and is required for several existing works on safe RL (Akametalu et al., 2014; Gillula & Tomlin, 2012), and is complementary to our goal. Since the primary contribution of this work is the development of a reachable tube formulation for model-based controllers that use NNs, we rely on existing techniques (Moldovan et al., 2015) to estimate a conservative modeling error bound.\" but I find this assumption that you are given the modeling error bound diminishes the contribution of the work since everything downstream in your algorithm will be impacted by this value, which is hard to get in practice. \n\n## Minor Comments/Questions\n\n - Similar to comment above, what is a \"model-based policy\"? If you mean that it is derived from model-based RL method, why is this important?\n\n- It would seem that taking the worst case modeling error, while able to provide guarantees (subject to the accuracy of the modeling error), also results in conservatism. A comment on this in the manuscript would be nice. \n\n- Part of the novelty that is claimed here is that the dynamics and policy are parametrized by neural networks, but what is the limitation of previous works on reachability analysis that would not permit a NN model to be used?\n\n[1] Learning-based Model Predictive Control for Safe Exploration\nT Koller, F Berkenkamp, M Turchetta, A Krause\nDecision and Control (CDC), 2018 IEEE 57th Conference on\n\n[2] Safe nonlinear trajectory generation for parallel autonomy with a dynamic vehicle model\nW Schwarting, J Alonso-Mora, L Paull, S Karaman, D Rus\nIEEE Transactions on Intelligent Transportation Systems 19 (9), 2994-3008\n\n[3] M. R. Hafner and D. Del Vecchio, “Computational tools for the safety control of a class of piecewise continuous systems with imperfect information on a partial order,” SIAM J. Control Optim., vol. 49, pp. 2463–2493, 2011.\n\n[4] R. Ghaemi and D. D. Vecchio, “Control for safety specifications of systems\nwith imperfect information on a partial order,", "extra_scores": {}, "extra_text": {}}, {"review_id": "4qWH34a5y-", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary: The paper studies the problem of safety verification of model-based RL controllers in continuous action&state spaces. The paper proposes a verification method based on reachable set analysis. The proposed method either verifies the controller to be safe or identifies the subset of initial states that are safe.\n\nStrengths:\n\ni) The motivation, organization and the overall writing of the paper are clear.\n\nWeakness:\n\ni) The problem of verifying properties of NN based controllers is studied in the literature [1,2,3,4,5,6,7,8,9,10,11,12,…], which is not discussed in detail in the paper (i.e., there is a paragraph present in the supplementary material). Moreover, there are no experimental comparisons made to any of these previous works.\n\nii) The tested experimental domains are not the best representatives of the control problems motivated in the paper. They are extremely small in size and do not really require NN approximation. As such, the resulting NN architectures are very small (as seen in the supplementary materials).\n\nReferences:\n\n[1] Verisig: verifying safety properties of hybrid systems with neural network controllers, Ivanov et al. HSCC-19.\n\n[2] Learning and Verification of Feedback Control Systems using Feedforward Neural Networks, Dutta et al., 2018.\n\n[3] Reachability Analysis and Safety Verification for Neural Network Control Systems, Xiang and Johnson, arvix 2018.\n\n[4] Efficient Verification of Control Systems with Neural Network Controllers, Yang et al., ICVISP-19.\n\n[5] Verifying Deep-RL-Driven Systems, Kazak et al. NetAI-19.\n\n[6] Guarded Deep Learning using Scenario-based Modeling, Katz MODELSWARD 2020.\n\n[7] Reachability Analysis for Neural Agent-Environment Systems, Akintunde et al, KR-18.\n\n[8] Verification of RNN-Based Neural Agent-Environment Systems, Akintunde et al, AAAI-19.\n\n[9] Reachability Analysis for Neural Feedback Systems using Regressive Polynomial Rule Inference, Dutta et al., HSCC-19.\n\n[10] ReachNN: Reachability Analysis of Neural-Network Controlled Systems, Huang et al., TECS-19.\n\n[11] Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers, Xiang et al., ACC-18.\n\n[12] A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers, Julian et al., arvix, 2019.", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: # Quality: 
The paper makes a good job of presenting the proposed algorithm, which seems interesting and solid.
However, the paper fails to place the proposed approach in the larger context of the existing literature.
In addition, only qualitative results are presented, without any comparison. 
As such, it is impossible to really understand the goodness of the proposed approach.

# Clarity: 
The paper is generally well-written and clear.

# Originality:
The proposed approach is novel to the best of the reviewers and my knowledge.

# Significance of this work: 
The paper deal with a very relevant and timely topic. However, as stated by the authors themself the paper is not concerned with high-dimensional systems, which is what would really differentiate this work compared to existing literature. In addition, the paper has no quantitative results nor comparisons against previous literature, and does not evaluate any of the standard benchmarks.

# Overall:
There is disagreement from the reviewers regarding the acceptance of this paper, and the overall score is very borderline. After thoroughly reading the paper, I agree with the evaluation of Reviewer 2 and 3 regarding the lack of comparisons and thus lean towards rejection.


Decision: Reject