Reachability Analysis of Neural Network Control Systems
Neural network controllers (NNCs) have shown great promise in autonomous and
cyber-physical systems. Despite the various verification approaches for neural
networks, the safety analysis of NNCs remains an open problem. Existing
verification approaches for neural network control systems (NNCSs) either can
only work on a limited type of activation functions, or result in non-trivial
over-approximation errors with time evolving. This paper proposes a
verification framework for NNCS based on Lipschitzian optimisation, called
DeepNNC. We first prove the Lipschitz continuity of closed-loop NNCSs by
unrolling and eliminating the loops. We then reveal the working principles of
applying Lipschitzian optimisation on NNCS verification and illustrate it by
verifying an adaptive cruise control model. Compared to state-of-the-art
verification approaches, DeepNNC shows superior performance in terms of
efficiency and accuracy over a wide range of NNCs. We also provide a case study
to demonstrate the capability of DeepNNC to handle a real-world, practical, and
complex system. Our tool \textbf{DeepNNC} is available at
\url{https://github.com/TrustAI/DeepNNC}.
Chi Zhang, Wenjie Ruan, Peipei Xu
# Reachability Analysis of Neural Network Control Systems

###### Abstract

Neural network controllers (NNCs) have shown great promise in autonomous and cyber-physical systems. Despite the various verification approaches for neural networks, the safety analysis of NNCs remains an open problem. Existing verification approaches for neural network control systems (NNCSs) either can only work on a limited type of activation functions, or result in non-trivial over-approximation errors with time evolving. This paper proposes a verification framework for NNCS based on Lipschitzian optimisation, called DeepNNC. We first prove the Lipschitz continuity of closed-loop NNCSs by unrolling and eliminating the loops. We then reveal the working principles of applying Lipschitzian optimisation on NNCS verification and illustrate it by verifying an adaptive cruise control model. Compared to state-of-the-art verification approaches, DeepNNC shows superior performance in terms of efficiency and accuracy over a wide range of NNCs. We also provide a case study to demonstrate the capability of DeepNNC to handle a real-world, practical, and complex system. Our tool **DeepNNC** is available at [https://github.com/TrustAI/DeepNNC](https://github.com/TrustAI/DeepNNC).

## Introduction

Neural network controllers have gained increasing interest in the autonomous industry and cyber-physical systems because of their excellent capacity of representation learning [14, 15, 16]. Compared to conventional knowledge-based controllers, learning-based NNCs not only simplify the design process, but also show superior performance in various unexpected scenarios [11, 12]. Since they have already been applied in safety-critical circumstances, including autonomous driving [13, 14, 15] and air traffic collision avoidance systems [13], verification on NNCSs plays a crucial role in ensuring their safety and reliability before their deployment in the real world. Essentially, we can achieve verification on NNCSs through estimating the system's reachable set. As Figure 1 shows, given the neural network controller, the dynamic model of the target plant, and the range \(X_{0}\) of initial states, we intend to estimate the reachable sets of the system, that is, the output range of state variables over a finite time horizon \([0,t_{n}]\). If the reachable sets \(X_{t1}\), \(X_{t2}\),... \(X_{tn}\) have _no intersection_ with the avoid set and \(X_{tn}\) reaches the goal set, we can verify that the NNCS is safe.

Compared to verification on NNCSs, verification on neural networks (NNs) is a relatively well-explored area [14, 15, 16, 17, 18, 19, 20, 21]. Representative solutions can be categorised into constraint satisfaction based approaches [13, 14] and approximation-based approaches [15, 16, 17, 18]. However, these verification approaches cannot be applied directly to NNCS. They are not workable in the scenario where the neural network is in close conjunction with other subsystems. A speciality of NNCSs is the association with control time steps. Moreover, approximation-based verification inevitably results in the accumulation of the over-approximation error with the control time evolved.

Recently, some pioneering research has emerged to verify NNCSs. They first estimate the output range of the controller and then feed the range to a hybrid system verification tool. Although both groups of tools can generate a tight estimate on their isolated models, direct combination results in a loose estimate of NNCS reachable sets after a few control steps, known as the _wrapping effect_[11].

To resolve the wrapping effect, researchers develop vari

Figure 1: NNCS verification through reachable set estimation. _We estimate the reachable sets \(X_{t1},X_{t2},X_{t3}\)..., \(X_{tn}\) at \(t_{1},t_{2},t_{3}\)..., \(t_{n}\). If all reachable sets do not intersect with the grey avoid set and \(X_{tn}\) reaches the blue goal set, the NNCS is verified to be safe._
ous methods to analyse NNCSs as a whole. Verisig [14] transforms the neural network into an equivalent hybrid system for verification, which can only work on Sigmoid activation function. NNV [13] uses a variety of set representations, e.g., polyhedra and zonotopes, for both the controller and the plant. Other researchers are inspired by the fact that the Taylor model approach can analyse hybrid systems with traditional controllers [1]. Thus, they applied the Taylor model for the verification of NNCSs. Representatives are ReachNN [10], ReachNN* [13], Versig 2.0 [14] and Sherlock [15]. However, verification approaches based on Taylor polynomials are limited to certain types of activation function. And their over-approximation errors still exist and accumulate over time.

To alleviate the above weakness, this paper proposes a novel verification method for NNCSs, called DeepNNC, taking advantage of the recent advance in Lipschitzian optimisation. As shown in Table 1, compared to the state-of-the-art NNCS verification, DeepNNC can solve linear and nonlinear NNCS with a wide range of activation functions. Essentially, we treat the reachability problem as a black-box optimisation problem and verify the NNCS as long as it is Lipschitz continuous. DeepNNC is the only model-agnostic approach, which means that access to the inner structure of NNCSs is not required. DeepNNC has the ability to work on _any Lipschitz continuous complex system_ to achieve efficient and tight reachability analysis. The contributions of this paper are summarised below:

* This paper proposes a novel framework for the verification of NNCS, called DeepNNC. It is the first model-agnostic work that can deal with a broad class of hybrid systems with linear or nonlinear plants and neural network controllers with various types of activation functions such as ReLU, Sigmoid, and Tanh activation.
* We theoretically prove that Lipschitz continuity holds on closed-loop NNCSs. DeepNNC constructs the reachable set estimation as a series of independent global optimisation problems, which can significantly reduce the over-approximation error and the wrapping effect. We also provide a theoretical analysis on the soundness and completeness of DeepNNC.
* Our intensive experiments show that DeepNNC outperforms state-of-the-art NNCS verification approaches on various benchmarks in terms of both accuracy and efficiency. On average, DeepNNC is **768 times faster** than ReachNN* [13], **37 times faster** than Sherlock [15], and **56 times faster** than Verisig 2.0 [14] (see Table 2).

## Related Work

We review the related works from the following three aspects.

**SMC-based approaches** transform the problem into an SMC problem [15]. First, it partitions the safe workspace, i.e., the safe set, into imaging-adapted sets. After partitioning, this method utilises an SMC encoding to specify all possible assignments of the activation functions for the given plant and NNC. However, it can only work on discrete-time linear plants with ReLU neural controller.

**SDP-based and LP-based approaches** SDP-based approach [16] uses a semidefinite program (SDP) for reachability analysis of NNCS. It abstracts the nonlinear components of the closed-loop system by quadratic constraints and computes the approximate reachable sets via SDP. It is limited to linear systems with NNC. LP-based approach[17] provides a linear programming-based formulation of NNCSs. It demonstrates higher efficiency and scalability than the SDP methods. However, the estimation results are less tight than SDP-based methods.

**Representation-based approaches** use the representation sets to serve as the input and output domains for both the controller and the hybrid system. The representative method is NNV [13], which has integrated various representation sets, such as polyhedron [13, 14], star sets [13] and zonotop [15]. For a linear plant, NNV can provide exact reachable sets, while it can only achieve an over-approximated analysis for a nonlinear plant.

**Taylor model based approaches** approximate the reachable sets of NNCSs with the Taylor model (TM). Representative methods are Sherlock [15] and Verisig 2.0 [14]. The core concept of the Taylor model is to approximate a function with a polynomial and a worst-case error bound. TM approximation has shown impressive results in the anal

\begin{table}
\begin{tabular}{c|c c c c c} \hline \hline  & **Plant Dynamics** & **Discrete/Continuous** & **Workable Activation Functions** & **Core Techniques** & **Model-Agnostic Solution** \\ \hline
**SMC** [15] & Linear & Discrete & ReLU & SMC encoding + solver & ✗ \\ \hline
**Verisig** [16] & Linear, Nonlinear & Discrete, Continuous & Sigmoid, Tanh & TM + Equivalent hybrid & ✗ \\ \hline
**ReachNN** [17] & Linear, Nonlinear & Discrete, Continuous & ReLU, Sigmoid, Tanh & TM+ Bernstein polynomial & ✗ \\ \hline
**Sherlock** [17] & Linear, Nonlinear & Discrete, Continuous & ReLU & TM + MILP & ✗ \\ \hline
**ReachNN*** [18] & Linear, Nonlinear & Discrete, Continuous & ReLU, Sigmoid, Tanh & TM + Bernstein polynomial & ✗ \\ \hline
**Verisig 2.0** [19] & Linear, Nonlinear & Discrete, Continuous & Tanh, Sigmoid & TM + Extrink wrapping & ✗ \\ \hline
**DeepNNC (Our work)** & Any Lipschitz & Continuous & Any Lipschitz continuous activations & \multirow{2}{*}{Lipschitz optimisation} & ✗ \\  & continuous systems & & e.g., ReLU, Sigmoid, Tanh, etc. & \\ \hline \hline \end{tabular}
\end{table}
Table 1: Comparison with existing NNCS verification methods from multiple aspects
ysis of the reachability of hybrid systems with conventional controllers [3, 13] and the corresponding tool Flow*[3] is widely applied. Verisig [12] makes use of the tool Flow*[3] by transforming the NNC into a regular hybrid system without a neural network. It proves that the Sigmoid is the solution to a quadratic differential equation and applies Flow* [3] on the reachability analysis of the equivalent system. Instead of directly using the TM verification tool, ReachNN [13], ReachNN* [13] and Verisig 2.0 [12] maintain the structure of NNCS and approximate the input and output of NNC by a polynomial and an error band, with a structure similar to the TM model. Therefore, the reachable sets of controller and plant share the same format and can be transmitted and processed in the closed loop.

Table 1 presents a detailed comparison of DeepNNC with its related work. The core technique of our method is significantly different from existing solutions, enabling DeepNNC to work on any neural network controlled system as long as it is Lipschitz continuous.

## Problem Formulation

This section first describes the NNCS model and then formulates the NNCS reachability problem. We deal with a closed-loop neural network controlled system as shown in Figure 2. It consists of two parts, a plant represented by a continuous system \(\dot{x}=f(x,u)\) and a neural network controller \(u=\sigma(y)\). The system works in a time-triggered manner with the control step size \(\delta\).

In control systems, the plant is usually modelled in the form of an ordinary differential equation (ODE). To guarantee the existence of a unique solution in ODE, the function \(f\) to model the plant is required to be Lipschitz continuous in \(x\) and \(u\)[10].

**Definition 2** (Neural Network Controller).: _The neural network controller is a k layer feedforward neural network with one or multiple types of activation functions, such as Sigmoid, Tanh, and ReLU activations, which can be defined as:_

\[\sigma(y)=\sigma_{k}\circ\sigma_{k-1}\circ...\circ\sigma_{1}(y). \tag{3}\]

As shown in Figure 2, system transmits the measurements \(y\) to the NNC, forming the control input through \(u=\sigma(y)\). The measurement function \(y=h(x)\) is usually Lipschitz continuous, and some systems use \(y=x\) for simplicity [10].

**Definition 3** (Neural Network Controlled System).: _The neural network controlled system \(\phi\) is a closed-loop system composed of a plant \(P\) and a neural network controller \(\sigma\). In a control time step, the closed-loop system is characterised as:_

\[\begin{split}\phi(x(i\delta),\Delta t)\equiv\,x(i\delta+\Delta t )\\ =x(i\delta)+\int_{i\delta}^{i\delta+\Delta t}f(x(\tau),\sigma(h(x(i \delta))))\,d\tau\end{split} \tag{4}\]

_with \(i=0,1,2,3...\), and \(\Delta t\in[0,\delta]\). For a given initial state \(x_{0}\in\mathcal{X}_{0}\) at \(t=0\) and a specified NNCS \(\phi\), the state \(x\) at time \(t\geq 0\) is denoted as \(x(t)\equiv\phi(x_{0},t)\)._

**Definition 4** (Reachable Set of NNCS).: _Given a range \(\mathcal{X}_{0}\) for initial states and a neural network controlled system \(\phi\), we define the region \(S_{t}\) a reachable set at time \(t\geq 0\) if all reachable states can be found in \(S_{t}\)._

\[\forall x_{0}\in\mathcal{X}_{0},\,\exists\,\phi(x_{0},t)\in S_{t} \tag{5}\]

It is possible that an over-approximation of reachable states exists in the reachable set. In other words, all reachable states of time \(t\) stay in \(S_{t}\), while not all states in \(S_{t}\) are reachable. Furthermore, we can formulate the estimation of the reachable set of NNCS as an optimisation problem:

**Definition 5** (Reachability of NNCS).: _Let the range \(\mathcal{X}_{0}\) be initial states \(x_{0}\) and \(\phi\) be a NNCS. The reachability of NNCS at a predefined time point \(t\) is defined as the reachable set \(S_{t}(\phi,X_{0},\epsilon)=[l,u]\) of NNCS \(\phi\) under an error tolerance \(\epsilon\geq 0\) such that_

\[\begin{split}\inf_{x_{0}\in X_{0}}\phi(x_{0},t)-\epsilon\leq l \leq\inf_{x_{0}\in X_{0}}\phi(x_{0},t)+\epsilon\\ \sup_{x_{0}\in X_{0}}\phi(x_{0},t)-\epsilon\leq u\leq\sup_{x_{0} \in X_{0}}\phi(x_{0},t)+\epsilon\end{split} \tag{6}\]

As discussed in multiple works [13, 14], the reachability problem in neural networks is extremely challenging, it is an NP-complete problem.

## Reachability Analysis via Lipschitzian Optimisation

This section presents a novel solution taking advantage of recent advances in Lipschitzian optimisation [15, 16, 17]. But before employing Lipschitzian optimisation, we need to theoretically prove the Lipschitz continuity of the NNCS.

Figure 2: Architecture of a neural network controlled system. _Neural network controller \(\delta\) takes measurements \(y\) as input and initiates the control input \(u\). The plant updates its states according to its dynamic \(\dot{x}=f(x,u)\) and generates new measurements of the states to be fed to the controller._
### Lipschitz Continuity of NNCSs

**Theorem 1** (Lipschitz Continuity of NNCS).: _Given an initial state \(X_{0}\) and a neural network controlled system \(\phi(x,t)\) with controller \(\sigma(x)\) and plant \(f(x,u)\), if \(f\) and \(\sigma\) are Lipschitz continuous, then the system \(\phi(x,t)\) is Lipschitz continuous in initial states \(\mathcal{X}_{0}\). A real constant \(K\geq 0\) exists for any time point \(t>0\) and for all \(x_{0},y_{0}\in\mathcal{X}_{0}\):_

\[\left|\phi(x_{0},t)-\phi(y_{0},t)\right|\leq K\left|x_{0}-y_{0}\right| \tag{7}\]

_The smallest \(K\) is the best Lipschitz constant for the system, denoted \(K_{best}\)._

Proof.: (sketch) The essential idea is to open the control loop and further demonstrate that the system \(\phi(x_{0},t)\) is Lipschitz continuous on \(x_{0}\). We duplicate the NNC and plant blocks to build an equivalent open-loop control system. Based on Definition 3, we have

\[\begin{split}&\left|\phi(x_{0},t)-\phi(y_{0},t)\right|\leq\left|x_ {0}-y_{0}\right|\\ +&\int_{t_{0}}^{t}\left|\,f(x(\tau),u_{x}(\tau))\ -\ f(y(\tau),u_{y}(\tau))\right|d\tau\end{split} \tag{8}\]

We add the term \(f(x(\tau),u_{y}(\tau))\ -\ f(x(\tau),u_{y}(\tau))\) to the right side and assume that the Lipschitz constant of \(f\) on \(x\) and \(u\) are \(L_{u}\) and \(L_{x}\) and the Lipschitz constant of NN as \(L_{n}\), we can transform Equation (8) to the following form:

\[\begin{split}&\left\|\phi(x_{0},t)-\phi(y_{0},t)\right\|\leq\\ &\left(L_{u}L_{n}(t-t_{0})+1\right)\left\|x_{0}-y_{0}\right\|+L_{ x}\int_{t_{0}}^{t}\left\|\,x(\tau)-y(\tau)\ \right\|\ d\tau.\end{split} \tag{9}\]

Based on Gronwall's theory of integral inequality (Gronwall, 1919), we further have the following equation:

\[\begin{split}&\left\|\phi(x_{0},t)-\phi(y_{0},t)\right\|\leq \left(L_{u}L_{n}(t-t_{0})+1\right)\left\|x_{0}-y_{0}\right\|e^{L_{x}(t-t_{0})}.\end{split} \tag{10}\]

Hence, we have demonstrated the Lipschitz continuity of the closed-loop system on its initial states with respect to the time interval \([0,\delta]\). We repeat this process through all the control steps and prove the Lipschitz continuity of NNCSs on initial states. See **Appendix-A1** for a detailed proof. 

Footnote 1: All appendixes of this paper can be found at [https://github.com/TrustAI/DeepNNC/blob/main/appendix.pdf](https://github.com/TrustAI/DeepNNC/blob/main/appendix.pdf)

Based on Theorem 1, we can easily have the following lemma about the local Lipschitz continuity of the NNCS.

**Lemma 1** (Local Lipschitz Continuity of NNCS).: _If NNCS \(\phi(x,t)\) is Lipschitz continuous throughout \(X_{0}\), then it is also locally Lipschitz continuous in its sub-intervals. There exists a real constant \(k_{i}\geq 0\) for any time point \(t>0\), and \(\forall x_{0},y_{0}\in[a_{i},a_{i+1}]\subset X_{0}\), we have \(\left\|\phi(x_{0},t)-\phi(y_{0},t)\right\|\leq k_{i}\left\|x_{0}-y_{0}\right\|\)._

Based on Lemma 1, we develop a fine-grained strategy to estimate local Lipschitz constants, leading to faster convergence in Lipschitz optimisation.

### Lipschitzian Optimisation

In the reachability analysis, the primary aim is to provide the lower bound \(R\) of the minimal value \(\phi(x),x\in X_{0}\). We achieve tighter bounds by reasonably partitioning the initial input region \(X_{0}\) and evaluating the points at the edges of the partition. The pseudocode of the algorithm can be found in **Appendix-B**. Here, we explain the partition strategy and the construction of \(R\) in the \(k\)-th iteration.

1. We sort the input sub intervals \(D_{0},D_{1},D_{2}...D_{n}\), with \(D_{i}=[a_{i},a_{i+1}]\). In the first iteration, we only have one sub interval with \(D_{0}=X_{0}=[a_{0},a_{1}]\).
2. We evaluate the system output \(\phi_{i}=\phi_{t}(a_{i})\) at the edge points \(a_{0},...a_{n}\), and define \(R_{i}\) as the character value of the interval \(D_{i}\) with the corresponding input \(x_{i}^{R}\): \[R_{i}=\frac{\phi_{i}+\phi_{i+1}}{2}+l_{i}\frac{a_{i}-a_{i+1}}{2}\] (11) \[x_{i}^{R}=\frac{\phi_{i}-\phi_{i+1}}{2l_{i}}+\frac{a_{i+1}+a_{i}}{2}.\] (12) Both \(R_{i}\) and \(x_{i}^{R}\) are determined by the information of the edge point and local Lipschitz constant \(l_{i}\).
3. We search for the interval with a minimum character value and minimal evaluated edge points: \[\begin{split}& R_{min}^{k}=\min\{R_{0},...,R_{n}\},\ j=\arg\min\{R_{0},...,R_{n}\}\\ & D_{j}=[a_{j},a_{j+1}],\ \hat{\phi}_{min}^{k}=\min\{\phi_{0},\phi_{1},...\phi_{n}\}.\end{split}\] (13) If \(\hat{\phi}_{min}^{k}-R_{min}^{k}\leq\epsilon\), the optimisation terminates, and we return \(R_{j}\) for the lower bound. Otherwise, we add a new edge point \(a_{new}=x_{j}^{R}\) to divide \(D_{j}\).

As illustrated in Figure 3, with blue points as edges and red points indicating the characteristic value \(R\). Both \(R_{min}^{k}\) and \(\hat{\phi}_{min}^{k}\) are approaching the real minimum value \(\phi_{min}\). The optimisation ends when \(\hat{\phi}_{min}^{k}-R_{min}^{k}\leq\epsilon\), which implies \(R_{min}^{k}\leq\phi_{min}\leq R_{min}^{k}+\epsilon\)

To extend the above strategy into a multi-dimensional case, we use the nested optimisation scheme to solve the problem in a recursive way.

\[\min_{x\in[p_{i},q_{i}]^{n}}\ \phi(x)=\min_{x_{1}\in[p_{1},q_{1}]}\ \cdots\min_{x_{n}\in[p_{n},q_{n}]}\phi(x_{1},...,x_{n}) \tag{14}\]

w

Figure 3: Demonstration of the optimisation process: \(|\hat{\phi}_{min}^{k}-R_{min}^{k}|\)_decreases with iteration \(k\), optimisation converges when \(|\hat{\phi}_{min}^{k}-R_{min}^{k}|<\epsilon\)_
We define the \(d\)-th level optimisation sub-problem,

\[w_{d}(x_{1},...,x_{d})=\min_{x_{d+1}\in[p_{d+1},q_{d+1}]}w_{d+1}(x_{1},...,x_{d+1}) \tag{15}\]

and for \(d=n\), \(w_{n}(x_{1},...,x_{n})=\phi(x_{1},x_{2},...,x_{n})\). Thus, we have \(\min_{x\in[p_{i},q_{i}]^{n}}\ \ \phi(x)=\min_{x_{1}\in[p_{i},q_{1}]}\phi_{1}(x_{1})\) which is actually a one-dimensional optimisation problem.

### Convergence Analysis

We discuss the convergence analysis in two circumstances, i.e., one-dimensional problem and multidimensional problem. In the one-dimensional problem,we divide the sub-interval \(D_{j}=[a_{j},a_{j+1}]\) into \(D^{1}_{new}=[a_{j},x_{j}^{R}]\) and \(D^{2}_{new}=[x_{j}^{R},a_{j+1}]\) in the \(k\)-th iteration. The new character value \(R^{1}_{new}-R_{j}=l_{j}\frac{a_{j+1}-x_{j}^{R}}{2}-\frac{\phi_{j+1}-\phi(x_{j} ^{R})}{2}>0\), \(R^{2}_{new}-R_{j}=l_{j}\frac{x_{j}^{R}-a_{j}}{2}-\frac{\phi(x_{j}^{R})-\phi_{j} }{2}>0\). Since \(R^{1}_{min}=\min\{R_{0},...R_{n}\}\setminus\{R_{j}\}\cup\{R^{1}_{new},R^{2}_{ new}\}\), we confirm that \(R^{k}_{min}\) increases strictly monotonically and is bounded.

In the multidimensional problem, the problem is transformed to a one-dimensional problem with nested optimisation. We introduce Theorem 2 for the inductive step.

**Theorem 2**.: _In optimisation, if \(\forall x\in\mathbb{R}^{d}\), \(\lim_{k\rightarrow\infty}R^{k}_{min}=\inf_{x\in[a,b]^{d}}\phi(x)\) and \(\lim_{i\rightarrow\infty}(\hat{\phi}^{k}_{min}-R^{k}_{min})=0\) are satisfied, then \(\forall x\in\mathbb{R}^{d+1}\), \(\lim_{k\rightarrow\infty}R^{k}_{min}=\inf_{x\in[a,b]^{d+1}}\phi(x)\) and \(\lim_{k\rightarrow\infty}(\hat{\phi}^{k}_{min}-R^{k}_{min})=0\) hold._

Proof.: (sketch) By the nested optimisation scheme, we have

\[\min_{x\in[a_{i},b_{i}]^{d+1}}\phi(x)=\min_{x\in[a,b]}W(x);\ \ W(x)=\min_{y\in[a_{i},b _{i}]^{d}}\phi(x,y) \tag{16}\]

Since \(\min_{y\in[a_{i},b_{i}]^{d}}\phi(x,y)\) is bounded by an interval error \(\epsilon_{\mathbf{y}}\), then we have \(|W(x)-W^{*}(x)|\leq\epsilon_{\mathbf{y}},\forall x\in[a,b]\), where \(W^{*}(x)\) is the accurate evaluation of the function.

For the inaccurate evaluation case, we have \(W_{min}=\min_{x\in[a,b]}W(x)\), \(R^{k}_{min}\) and \(\widehat{W}^{k}_{min}\). The termination criteria for both cases are \(|\widehat{W}^{k}_{min}-R^{k}_{min}|\leq\epsilon_{x}\) and \(|\widehat{W}^{k*}_{min}-R^{k}_{min}|\leq\epsilon_{x}\), and \(w^{*}\) represents the ideal global minimum. Based on the definition of \(R^{k}_{min}\), we have \(w^{*}-R^{k}_{min}\leq\epsilon_{\mathbf{y}}+\epsilon_{x}\). By analogy, we get \(\widehat{W}^{k}_{min}-w^{*}\leq\epsilon_{\mathbf{y}}+\epsilon_{x}\). Thus, the accurate global minimum is bounded. Theorem 2 is proved. See **Appendix C** for a detailed proof. 

### Estimation of Lipschitz Constant

To enable a fast convergence of the optimisation, we need to provide a Lipschitz constant for NNCS. As we aim for a model-agnostic reachability analysis for NNCSs, we further propose two practical variants to estimate the Lipschitz constant for a black-box NNCS.

Dynamic Estimation of Global Lipschitz ConstantIn the optimisation process, the entire input range \(X\) of the function \(\phi_{t}(x)\) is divided into limited sub-intervals \(D_{0},D_{1},D_{2}...D_{n}\), where \(D_{i}=[a_{i},a_{i+1}]\). We update the global Lipschitz constant \(L\) according to the interval partitions:

\[L=r\cdot max\bigg{|}\frac{\phi_{t}(a_{i+1})-\phi_{t}(a_{i})}{a_{i+1}-a_{i}} \bigg{|} \tag{17}\]

To avoid an underestimate of \(L\), we choose \(r>1\) and have

\[\lim_{j\rightarrow\infty}r\cdot\max_{i=1,...,j-1}\bigg{|}\frac{\phi_{t}(a_{i+ 1})-\phi_{t}(a_{i})}{a_{i+1}-a_{i}}\bigg{|}=r\cdot\sup_{a\in X}\frac{d\phi_{t }}{da}>K_{best}. \tag{18}\]

The dynamic update of \(L\) will approximate the best Lipschitz constant of the NNCS.

Local Lipschitz Constant EstimationAn alternative to improve efficiency is the adoption of the local Lipschitz constant \(l_{i}\). We adopt the local adjustment (Sergeyev 1995) for local Lipschitz estimation, which considers not only global information, but also neighbourhood intervals. For each sub-interval, we introduce \(m_{i}\)

\[m_{i}=|\phi_{t}(a_{i+1})-\phi_{t}(a_{i})|/|a_{i+1}-a_{i}|,M=\max\ m_{i} \tag{19}\]

We calculate sub-interval sizes \(d_{i}\) and select the largest \(D\).

\[d_{i}=|a_{i+1}-a_{i}|\,,D=\max\ d_{i} \tag{20}\]

Equation (21) estimates the local Lipschitz constant.

\[l_{i}=r\cdot\max\left\{m_{i-1},m_{i},m_{i+1},M\cdot d_{i}/D\right\} \tag{21}\]

It balances the local and global information. When the sub-interval is small, that is, \(M\cdot d_{i}/D\to 0\), \(l_{i}\) is decided by local information.

\[\lim_{d_{i}\to D}l_{i}=r\cdot max\left\{m_{i-1},m_{i},m_{i+1}\right\}=r \cdot\sup_{a\in[a_{i},a_{i+1}]}\frac{d\phi_{t}}{da}>k_{i}^{best}\]

When the subinterval is large, that is, \(d_{i}\to D\), local information is not reliable. \(l_{i}\) is determined by global information.

\[\lim_{d_{i}\to D}l_{i}=r\cdot M=r\cdot\sup_{a\in X}\frac{d\phi_{t}}{da}>K_{ best}>k_{i}^{best} \tag{22}\]

Local Lipschitz constants provide a _more accurate_ polyline approximation to the original function, leading to faster convergence.

### Soundness and Completeness

**Theorem 3** (Soundness).: _Given a box-constrained initial input range \(X_{0}\) and a dangerous set \(S_{a}\), the verification of an NNCS via DeepNNC is sound anytime. DeepNNC can return an overestimation \(S\) of the real reachable set \(X\) at any iteration, even it has not reached the convergence._

Proof.: When we interrupt the optimisation at any iteration \(k\), lower bound \(R^{k}_{min}\) is returned for verification. We assume that the real minimal value \(\phi_{min}\) is located in the

Figure 4: \(X_{0}\) is the initial state set and \(S_{d}\) is the avoid set. DeepNNC can return an overestimation \(S_{any}\) in any iteration. Verification is sound but not complete by \(S_{any}\), and Verification is both sound and complete by \(S_{\epsilon\to 0}\).
sub-interval \([a_{i},a_{i+1}]\), i.e. \(\phi_{min}=\phi(x_{min})\) with \(x_{min}\in[a_{i},a_{i+1}]\).

\[R_{i}-\phi_{min}=\frac{\phi_{i}+\phi_{i+1}}{2}-l_{i}\frac{a_{i}-a_ {i+1}}{2}-\phi_{min}\] \[= \frac{\phi_{i}-\phi_{min}}{2}+l_{i}\frac{a_{i}-x_{min}}{2}+\frac{ \phi_{min}-\phi_{i+1}}{2}+l_{i}\frac{x_{min}-a_{i+1}}{2}\leq 0 \tag{23}\]

Thus, \(R_{min}^{k}-\phi_{min}\leq R_{i}-\phi_{min}\leq 0\) holds. When using \(R_{min}^{k}\) to estimate the output range \(S_{any}\), \(R_{min}^{k}\leq\phi_{min}\) ensures \(X\subset S_{any}\), where \(X\) is the real reachable set. Given an avoid set \(S_{d}\), if \(S_{any}\cap S_{d}=\emptyset\), then \(X\cap S_{d}=\emptyset\), the NNCS is safe. Thus, the approach DeepNNC is sound. 

**Theorem 4** (Completeness).: _Given a box-constrained initial input range \(X_{0}\) and a dangerous set \(S_{d}\), verification via DeepNNC is complete only when optimisation reaches convergence with the overestimation error \(\epsilon\to 0\)._

Proof.: As demonstrated in the convergence analysis, with iteration number \(k\rightarrow\infty\) the optimisation can achieve convergence with error \(\epsilon\to 0\). In such circumstances, the lower bound \(R_{min}^{k}\rightarrow\phi_{min}\) results in an estimation \(S_{\epsilon\to 0}\to X_{0}\) with ignorable estimation error. If \(S_{\epsilon\to 0}\cap S_{d}\neq\emptyset\), then \(X\cap S_{d}\neq\emptyset\), the NNCS is not safe. 

## Experiments

We first compare DeepNNC with some state-of-the-art baselines. We then analyse the influences of parameter \(k_{max}\) and \(\epsilon\). Finally, we provide a case study on an airplane model. An additional case study of an adaptive cruise control system is presented in **Appendix D**.

### Comparison with State-of-the-art Methods

We test DeenNNC and baseline methods on six benchmarks. See **Appendix-E** for the details of the benchmarks. We compare our method with ReachNN* [12], Sherlock [10] and Versig 2.0 [2] in terms of efficiency. Regarding the accuracy comparison, we compare our method with Verisig [2] instead of Sherlock [10], since the results of Sherlock loose fast with the increase of control steps.

The time consumption of different approaches for estimating the reachable set at a predefined time is demonstrated in Table 2 and Figure 5. Our method can be applied to all benchmarks and has relatively better efficiency, especially for low-dimensional problems.
ing of the control timestep and the simulated trajectories (red). Reachable sets of DeepNNC (blue) can cover the trajectories with a small overestimation error.

### Impact of \(\epsilon\) and \(k_{max}\)

Two parameters \(\epsilon\) and \({}_{max}k\) are involved in our approach. \(\epsilon\) indicates the allowable error, and \(k_{max}\) represents the maximum number of iterations in each dimension. The iteration stops either when the difference of upper bound (red square) and lower bound (blue square) is smaller than \(\epsilon\) or the iteration number in one dimension reaches \(k_{max}\). In Figure 8, we fix \(\epsilon=0.0005\) and change \(k_{max}=3,5,10,10000\). The estimation becomes tighter with the larger iteration number. In Figure 9 we study the influence of \(\epsilon\) by fixing the maximum iteration number \(k_{max}=10^{4}\) and changing \(\epsilon=0.5,0.05,0.005,0.0005\). The accuracy of the estimate increases with smaller \(\epsilon\).

### Case Study: Flying Airplane

We analyse a complex control system of a flying airplane, which is a benchmark in ARCH-COMP21 (Johnson et al., 2021). The system contains 12 states \([x,y,z,u,v,w,\alpha,\beta,\gamma,r,p,q]\) and the technical details are in **Appendix-F**. Initial states are \(x=y=z=r=p=q=0,[u,v,w,\alpha,\beta,\gamma]=[0,1]^{6}\). The goal set is \(y\in[-0.5,0,5]\) and \([\alpha,\beta,\gamma]=[-1,1]^{3}\) for \(t<2s\). The controller here takes an input of 12 dimensions and generates a six-dimensional control input \(F_{x},F_{y},F_{z},M_{x},M_{y},M_{z}\). For simplicity, we choose a small subset of the initial input \([u,v,w,\alpha,\beta,\gamma]=[0.9,1]^{6}\), the estimated reachable sets of \(\alpha\) and \(y\) in the time range \([0s,2s]\) are presented in figure 10 (a). Both \(\alpha\) and \(y\) are above the safe range. Figure 10 shows the reachable set of \(\alpha\) and \(\gamma\), which is also above the safe region. The airplane NNCS is unsafe.

## Conclusion

We develop an NNCS verification tool, DeepNNC, that is applicable to a wide range of neural network controllers, as long as the whole system is Lipschitz-continuous. We treat NNCS verification as a series of optimisation problems, and the estimated reachable set bears a tight bound even in a long control time horizon. The efficiency of DeepNNC is mainly influenced by two factors, the Lipschitz constant estimation and the dimension of the input. For the first, we have adopted dynamic local Lipschitzian optimisation to improve efficiency. Regarding the high-dimensional reachability problem, a possible solution is to transform the high-dimension problem into a one-dimensional problem using a space-filling curve (Lera and Sergeyev, 2015). This idea can be explored in future work.

Figure 8: Reachable sets of B3 with ReLU at \(t=0.01s\), 0.1s, 0.2s, 0.4s, 1s, 3s, 6s, with \(\epsilon=0.0005\) and (a) \(k_{max}=3\); (b) \(k_{max}=5\); (c) \(k_{max}=10\); (d) \(k_{max}=10^{4}\)

Figure 6: Reachable sets at a predefined time point estimated by different approaches. The estimated reachable set at a time point is a polygon. The size of the area of the reachable set indicates the precision of the estimation results.

Figure 7: (a)B1 Sigmoid (b) B2 Sigmoid (c) B5 Sigmoid (d) B5 Tanh. Red trajectories are the simulated results. Blue reachable sets are generated from our approach. The yellow and green reachable sets are from the baseline methods.
## Acknowledgements

This work is supported by Partnership Resource Fund of ORCA Hub via the UK EPSRC under project [EP/R026173/1].
