Provably Correct Training of Neural Network
Controllers Using Reachability Analysis

Consider discrete-time nonlinear dynamical systems of the form:

where the state vector $x^{(t)}\in\mathcal{X}\subset\mathbb{R}^{n}$, the control vector $u^{(t)}\in\mathcal{U}\subset\mathbb{R}^{m}$, and $t\in\mathbb{N}$. Given a feedback control law $\Psi:\mathcal{X}\rightarrow\mathcal{U}$, we use $\xi_{x_{0},\Psi}:\mathbb{N}\rightarrow\mathcal{X}$ to denote the closed-loop trajectory of (3) that starts from the state $x_{0}\in\mathcal{X}$ and evolves under the control law $\Psi$.

In this paper, our primary focus is on controlling the nonlinear system (3) with a state-feedback neural network controller $\mathcal{NN}:\mathcal{X}\rightarrow\mathcal{U}$. An $F$-layer Rectified Linear Unit (ReLU) NN is specified by composing $F$ layer functions (or just layers). A layer $l$ with $\mathfrak{i}_{l}$ inputs and $\mathfrak{o}_{l}$ outputs is specified by a weight matrix $W^{(l)}\in\mathbb{R}^{\mathfrak{o}_{l}\times\mathfrak{i}_{l}}$ and a bias vector $b^{(l)}\in\mathbb{R}^{\mathfrak{o}_{l}}$ as follows:

where the $\max$ function is taken element-wise, and $\theta^{(l)}\triangleq(W^{(l)},b^{(l)})$ for brevity. Thus, an $F$-layer ReLU NN is specified by $F$ layer functions $\{L_{\theta^{(l)}}:l=1,\dots,F\}$ whose input and output dimensions are composable: that is they satisfy $\mathfrak{i}_{l}=\mathfrak{o}_{l-1},l=2,\dots,F$. Specifically:

where we index a ReLU NN function by a list of matrices $\theta\triangleq(\theta^{(1)},\dots,\theta^{(F)})$. Also, it is common to allow the final layer function to omit the $\max$ function altogether, and we will be explicit about this when it is the case.

As a typical control task, this paper considers a reach-avoid specification $\phi$, which combines a safety property $\phi_{\text{safety}}$ for avoiding a set of obstacles $\{\mathcal{O}_{1},\ldots,\mathcal{O}_{o}\}$ with $\mathcal{O}_{i}\subset\mathcal{X}$, and a liveness property $\phi_{\text{liveness}}$ for reaching a goal region $\mathcal{X}_{\text{goal}}\subset\mathcal{X}$ in a bounded time horizon $T$. We use $\xi_{x_{0},\Psi}\models\phi_{\text{safety}}$ and $\xi_{x_{0},\Psi}\models\phi_{\text{liveness}}$ to denote a trajectory $\xi_{x_{0},\Psi}$ satisfies the safety and liveness specifications, respectively, i.e.:

Given a set of initial states $\mathcal{X}_{\text{init}}$, a control law $\Psi:\mathcal{X}\rightarrow\mathbb{R}^{m}$ satisfies the specification $\phi$ (denoted by $\Psi,\mathcal{X}_{\text{init}}\models\phi$) if all trajectories starting from the set $\mathcal{X}_{\text{init}}$ satisfy the specification, i.e., $\xi_{x,\Psi}\models\phi$, $\forall x\in\mathcal{X}_{\text{init}}$.

Given the dynamical model (3) and a reach-avoid specification $\phi=\phi_{\text{safety}}\land\phi_{\text{liveness}}$, we consider the problem of designing a NN controller with provable guarantees as described in the next problem.

While it is desirable to find the largest possible set of safe initial states $\mathcal{X}_{\text{init}}$, our algorithm will instead focus on finding an $\epsilon$ sub-optimal $\mathcal{X}_{\text{init}}$. For space considerations, the quantification of the sub-optimality in the computations of $\mathcal{X}_{\text{init}}$ is omitted.

Our approach to address the safety specification $\phi_{\text{safety}}$ is as follows:

• •

  Step 1: Capture the closed-loop behavior of the system under all CPWA controllers using a finite-state abstract model. Such abstract model can be obtained by extending current results on reachability analysis for polytopic systems (Yordanov et al.,, 2012).

• •

  Step 2: Identify a family of CPWA controllers that lead to correct behavior on the abstract model.

• •

  Step 3: Enforce the training of the NN to pick from the identified family of the CPWA controllers.

Figure 1 conceptualizes our framework. To start with, we construct an abstract model by partitioning both the state space $\mathcal{X}$ and the set of all allowed CPWA functions $\mathcal{P}^{K}\times\mathcal{P}^{b}$. In Figure 1 (a), the state space $\mathcal{X}$ is partitioned into a set of abstract states $\mathbb{X}=\{q_{1},q_{2},q_{3},\text{obst},\text{goal}\}$ such that $\mathcal{X}=\bigcup_{q\in\mathbb{X}}q$. Similarly, the controller space $\mathcal{P}^{K}\times\mathcal{P}^{b}$ is partitioned into a set of controller partitions $\mathbb{P}=\{\mathcal{P}_{1},\mathcal{P}_{2}\}$ such that $\mathcal{P}^{K}\times\mathcal{P}^{b}=\bigcup_{\mathcal{P}\in\mathbb{P}}\mathcal{P}$ (each controller partition $\mathcal{P}\in\mathbb{P}$ represents a subset of CPWA functions). The resulting abstract model is a non-deterministic finite transition system with nodes represent abstract states in $\mathbb{X}$ and transitions are labeled by controller partitions in $\mathbb{P}$. Transitions between the abstract states are computed based on the reachable sets of the nonlinear system (3) from each abstract state $q\in\mathbb{X}$ and under every controller partition $\mathcal{P}\in\mathbb{P}$.

Based on the abstract model, we compute a function $P_{\text{safe}}$ that maps each abstract state $q\in\mathbb{X}$ to a subset of the controller partitions that are considered to be safe at the abstract state $q$, denoted by $P_{\text{safe}}(q)$. For example, in Figure 1 (b), since the transition from $q_{1}$ labeled by $\mathcal{P}_{2}$ leads to the obstacle, the controller partition $\mathcal{P}_{2}$ is unsafe at $q_{1}$, and hence $P_{\text{safe}}(q_{1})=\{\mathcal{P}_{1}\}$. Similarly, $P_{\text{safe}}(q_{2})=\{\mathcal{P}_{1},\mathcal{P}_{2}\}$. For the abstract state $q_{3}$, since both $\mathcal{P}_{1}$ and $\mathcal{P}_{2}$ can lead to the obstacle, $P_{\text{safe}}(q_{3})$ is empty, and hence $q_{3}$ is considered an unsafe abstract state. The set of initial states that can provide safety guarantee is the union of the safe abstract states, i.e., $\mathcal{X}_{\text{init}}=q_{1}\cup q_{2}$.

Using the set of safe controllers captured by $P_{\text{safe}}(q)$, it is direct to show that if a neural network gives rise to CPWA functions in $P_{\text{safe}}(q)$ at every abstract state $q\in\mathbb{X}$, then the NN satisfies the safety specifications. Therefore, to ensure the safety of the resulting trained neural network, we propose a NN weight “projection” operator to enforce that the trained NN only gives rise to the CPWA functions indicated by $P_{\text{safe}}(q)$.

Our approach to addressing the liveness specification $\phi_{\text{liveness}}$ (reaching the goal) can be summarized as follows:

• •

  Step 1: Use the abstract model to identify candidate controller partitions $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$ that can lead to satisfaction of the liveness properties.

• •

  Step 2: Train one local neural network $\text{NN}_{q}$ for each of the abstract states using either imitation learning or reinforcement learning. We take into account the knowledge of $\mathcal{P}^{\star}$ as constraints during training, and use the NN weight projection operator to ensure that the resulting NN still enjoys the safety specifications.

• •

  Step 3: Combine all the local neural networks $\text{NN}_{q}$ into a single global NN.

In the context of the example in Figure 1 (c), the controller partition $\mathcal{P}_{1}$ is assigned to both $q_{1}$ and $q_{2}$ as the candidate controller partition $\mathcal{P}^{\star}$ that may lead to the satisfaction of the liveness properties.

Next, we train one local neural network $\text{NN}_{q}$ for each abstract state, or a subset of abstract states assigned with the same controller partition as shown in Figure 1 (d). During training of the local neural networks, we project their weights to enforce that the resulting NNs only give rise to the CPWA functions belong to the assigned controller partitions $\mathcal{P}^{\star}$. Since the controller partition $\mathcal{P}^{\star}$ is chosen from the subset $P_{\text{safe}}(q)$ at every $q\in\mathbb{X}$, the resulting NN enjoys the same safety guarantees.

Finally, in Figure 1 (e), we combine the local networks trained for each abstract state into a single NN controller, with layers of fixed weights to decide which part of the NN should be activated.

We highlight that the proposed framework above always guarantees that the resulting NN satisfies the safety specification $\phi_{\text{safety}}$ thanks to the NN weight projection operator. This is reflected in Theorem 10 in Section 5.2.

On the other hand, achieving the liveness specification $\phi_{\text{liveness}}$ depends on the effort of neural network training and the quality of training data, and hence needs an extra step of formally verifying the resulting neural networks and iteratively changing the candidate controller partitions $\mathcal{P}^{\star}$ if needed. However, we argue that the resulting NN architecture is modular and is composed of a set of local networks $\text{NN}_{q}$ that are more amenable to verification. The proposed architecture leads to a direct divide-and-conquer approach in which only some of the local networks $\text{NN}_{q}$ may need to be re-trained whenever the liveness properties are not met.

In order to capture the behavior of the system (3) under all possible CPWA controllers $\Psi_{\text{CPWA}}$ in the form of (1), we construct a finite-state abstract model by discretizing both the state space and the set of all allowed CPWA functions. In particular, we partition the state space $\mathcal{X}\subset\mathbb{R}^{n}$ into a collection of abstract states, denoted by $\mathbb{X}=\{q_{1},\ldots,q_{N}\}$. The goal region $\mathcal{X}_{\text{goal}}\subset\mathcal{X}$ is represented by a single abstract state $q_{\text{goal}}\in\mathbb{X}$, and the set of obstacles $\mathbb{X}_{\text{obst}}=\bigcup_{i=1}^{o}\{q_{\text{obst}_{i}}\}$ represents each obstacle $\mathcal{O}_{i}\subset\mathcal{X}$ by an abstract state $q_{\text{obst}_{i}}\in\mathbb{X}$, $i=1,\ldots,o$. Other abstract states $q_{i}\in\mathbb{X}\setminus(\mathbb{X}_{\text{obst}}\cup\{q_{\text{goal}}\})$ represent infinity-norm balls in the state space $\mathcal{X}\subset\mathbb{R}^{n}$, and the partitioning of the state space satisfies $\mathcal{X}=\bigcup_{q\in\mathbb{X}}q$ and $\mathrm{Int}(q_{i})\cap\mathrm{Int}(q_{j})=\emptyset$ if $i\neq j$. For the interest of this paper, we consider the size of abstract states is pre-specified, by noticing that discretization techniques such as adaptive partitioning (e.g., Hsu et al., (2018)) can be directly applied in our framework. In experiments, we show results with both uniform and non-uniform partitioning of the state space.

Similarly, we partition the controller space into polytopic subsets. For simplicity of notation, we define the set of parameters $\mathcal{P}^{K\times b}\subset\mathbb{R}^{m\times(n+1)}$ be a polytope that combines $\mathcal{P}^{K}\in\mathbb{R}^{m\times n}$ and $\mathcal{P}^{b}\in\mathbb{R}^{m}$, and with some abuse of notation, we use $K_{i}(x)$ with a single parameter $K_{i}\in\mathcal{P}^{K\times b}$ to denote $K^{\prime}_{i}x_{i}+b^{\prime}_{i}$ with the pair $(K^{\prime}_{i},b^{\prime}_{i})=K_{i}$. The controller space $\mathcal{P}^{K\times b}\subset\mathbb{R}^{m\times(n+1)}$ is discretized into a collection of polytopic subsets in $\mathbb{R}^{m\times(n+1)}$, denoted by $\mathbb{P}=\{\mathcal{P}_{1},\ldots,\mathcal{P}_{M}\}$, such that $\mathcal{P}^{K\times b}=\bigcup_{\mathcal{P}\in\mathbb{P}}\mathcal{P}$ and $\mathrm{Int}(\mathcal{P}_{i})\cap\mathrm{Int}(\mathcal{P}_{j})=\emptyset$ if $i\neq j$. We call each of the subsets $\mathcal{P}_{i}\in\mathbb{P}$ a controller partition. Each controller partition $\mathcal{P}\in\mathbb{P}$ represents a subset of CPWA functions, by restricting parameters $K_{i}$ in a CPWA function to take values from $\mathcal{P}$.

In order to reason about the safety property $\phi_{\text{safety}}$, we introduce a posterior operator based on the dynamical model (3). The posterior of an abstract state $q\in\mathbb{X}$ under a controller partition $\mathcal{P}\in\mathbb{P}$ is the set of states that can be reached in one step from states $x\in q$ by using affine state feedback controllers with parameters $K\in\mathcal{P}$, i.e.:

Calculating the exact posterior of a nonlinear system is computationally daunting. Therefore, we rely on over-approximations of the posterior set denoted by $\overline{\mathrm{Post}}$.

Our abstract model is defined by using the set of abstract states $\mathbb{X}$, the set of controller partitions $\mathbb{P}$, and the posterior operator $\overline{\mathrm{Post}}$. Intuitively, an abstract state $q\in\mathbb{X}$ has a transition to $q^{\prime}\in\mathbb{X}$ under a controller partition $\mathcal{P}\in\mathbb{P}$ if the intersection between $q^{\prime}$ and $\overline{\mathrm{Post}}(q,\mathcal{P})$ is non-empty.

The computation of the posterior operator can be done by borrowing existing techniques in reachability analysis of polytopic systems (Yordanov et al.,, 2012), with the subtle difference due to the need to consider polytopic partitions of the parameter space $\mathcal{P}^{K\times b}\subset\mathbb{R}^{m\times(n+1)}$ instead of the well-studied problem of considering polytopic partitions of the input space $\mathcal{U}\subset\mathbb{R}^{m}$. We refer to the Posterior Graph $S_{\mathrm{Post}}$ as the finite-state abstract model of (3).

Once the abstract model $S_{\mathrm{Post}}$ is computed, our framework identifies a set of safe controller partitions $P_{\text{safe}}(q)\subseteq\mathbb{P}$ at each abstract state $q\in\mathbb{X}$. It is possible that the set $P_{\text{safe}}(q)$ is empty at some state $q\in\mathbb{X}$, in which case, the state $q$ is considered to be unsafe.

We first introduce the $\mathrm{Next}$ operator as follows:

We identify the set of unsafe abstract states in a recursive manner by backtracking from the set of obstacles $\mathbb{X}_{\text{obst}}$ in the posterior graph $S_{\mathrm{Post}}$:

The backtracking stops at iteration $k^{*}$ when it cannot find new unsafe states, i.e., $\mathbb{X}_{\text{unsafe}}^{k^{*}}=\mathbb{X}_{\text{unsafe}}^{k^{*}-1}$. This backtracking process ensures that the set $\mathbb{X}_{\text{unsafe}}^{k^{*}}$ includes all the abstract states that inevitably lead to the obstacles $\mathbb{X}_{\text{obst}}$ (either directly or over multiple transitions).

Then, we define the set of safe abstract states as $\mathbb{X}_{\text{safe}}\triangleq\mathbb{X}\setminus\mathbb{X}_{\text{unsafe}}^{k^{*}}$. The following proposition guarantees that there exists a controller partition assignment for each safe abstract state $q\in\mathbb{X}_{\text{safe}}$ such that collision-free can be satisfied for all times in the future.

Assume for the sake of contradiction that $\exists q\in\mathbb{X}_{\text{safe}}$, s.t. $\forall\mathcal{P}\in\mathbb{P}$, $\mathrm{Next}(q,\mathcal{P})\cap\mathbb{X}_{\text{unsafe}}^{k^{*}-1}\neq\emptyset$. Then, by the backtracking process, $q\in\mathbb{X}_{\text{unsafe}}^{k^{*}}$ which contradicts the assumption that $q\in\mathbb{X}_{\text{safe}}=\mathbb{X}\setminus\mathbb{X}_{\text{unsafe}}^{k^{*}}$. Correspondingly, the function $P_{\text{safe}}$ maps each abstract state $q\in\mathbb{X}_{\text{safe}}$ to the subset of controller partitions that can be used to force the invariance of the set $\mathbb{X}_{\text{safe}}$:

The following theorem summarizes the safety property.

It is sufficient to show that the set $\mathcal{X}_{\text{init}}=\bigcup_{q\in\mathbb{X}_{\text{safe}}}q$ is positive invariant under the controller $\Psi$ in the form of (10). In other words, for any state $x\in\mathcal{X}_{\text{init}}$, let $q\in\mathbb{X}_{\text{safe}}$ be the abstract state contains $x$, i.e., $x\in q$, then by applying any controller $K\in\mathcal{P}$ with any $\mathcal{P}\in P_{\text{safe}}(q)$, it holds that $f(x,K(x))\in\mathcal{X}_{\text{init}}$.

The definitions of the posterior operator (6) and the $\mathrm{Next}$ operator (7) directly yield $f(x,K(x))\in\overline{\mathrm{Post}}(q,\mathcal{P})$ and $\overline{\mathrm{Post}}(q,\mathcal{P})\subseteq\bigcup_{q^{\prime}\in\mathrm{Next}(q,\mathcal{P})}q^{\prime}$, and hence:

where $x\in q$, $q\in\mathbb{X}$, $K\in\mathcal{P}$, and $\mathcal{P}\in\mathbb{X}$ are arbitrarily chosen. Now consider an arbitrary safe abstract state $q\in\mathbb{X}_{\text{safe}}$, by Proposition 4 and the definition of $P_{\text{safe}}$ as (9), the set $P_{\text{safe}}(q)\neq\emptyset$, and for any $\mathcal{P}\in P_{\text{safe}}(q)$, it holds that:

where it uses the definition $\mathcal{X}_{\text{init}}=\bigcup_{q\in\mathbb{X}_{\text{safe}}}q$. Therefore, by (11) and (12), $f(x,K(x))\in\mathcal{X}_{\text{init}}$ for any $x\in q\in\mathbb{X}_{\text{safe}}$ and any $K\in\mathcal{P}\in P_{\text{safe}}(q)$.

By Theorem 5, the system is guaranteed to satisfy the safety specification $\phi_{\text{safety}}$ by applying any CPWA controller $\Psi_{q,\text{CPWA}}$ at each abstract sate $q\in\mathbb{X}_{\text{safe}}$, as long as the controller parameters $K_{i}$ are chosen from the safe controller partitions $\mathcal{P}\in P_{\text{safe}}(q)$. This allows us to conclude the safety guarantee provided by a NN controller if the CPWA function represented by the NN is chosen from the safe controller partitions, as we show in detail in the next subsection.

As described in Section 3, the final NN consists of several local networks $\text{NN}_{q}$ that will be trained to account for the liveness property. Nevertheless, to ensure that the safety property is met by each of the local networks $\text{NN}_{q}$, we propose a NN weight projection operator that can be incorporated in the training of these local NNs. Given a controller partition $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$, this operator projects the weights of $\text{NN}_{q}$ to ensure that the network represents a CPWA function belongs to $\mathcal{P}^{\star}$.

Consider a local network $\text{NN}_{q}$ of $F$ layers, including $F-1$ hidden layers and an output layer. The NN weight projection operator updates the weight matrix $W^{(F)}$ and the bias vector $b^{(F)}$ of the output layer to $\widehat{W}^{(F)}$ and $\widehat{b}^{(F)}$, respectively, such that the CPWA function represented by the updated local network belongs to the selected controller partition $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$ at linear regions intersecting $q$. To be specific, let the CPWA functions represented by the local network $\text{NN}_{q}$ before and after the weight projection be $\mathcal{NN}_{\theta}$ and $\mathcal{NN}_{\widehat{\theta}}$, respectively. Then, we formulate the NN weight projection operator as an optimization problem:

where by the notation (2), $\mathbb{L}_{\mathcal{NN}_{\theta}}=\{\mathcal{R}_{1},\ldots,\mathcal{R}_{L}\}$ is the set of linear regions of the CPWA function $\mathcal{NN}_{\theta}$. Consider the CPWA function $\mathcal{NN}_{\widehat{\theta}}$ is in the form of (1), where affine functions parametrized by $K_{i}\in\mathbb{R}^{m\times(n+1)}$ are associated to linear regions $\mathcal{R}_{i}$, $i=1,\ldots,L$. Then, the constraints (14) require that $K_{i}\in\mathcal{P}^{\star}$ whenever the corresponding linear region $\mathcal{R}_{i}$ intersects the abstract state $q$. As a common practice, we consider there is no ReLU activation function in the output layer. Then, the projection operator does not change the set of linear regions, i.e., $\mathbb{L}_{\mathcal{NN}_{\widehat{\theta}}}=\mathbb{L}_{\mathcal{NN}_{\theta}}$, since the linear regions of a neural network only depend on the hidden layers, while the projection operator updates the output layer weights.

The optimization problem (13)-(14) tries to minimize the change of NN outputs due to the projection, which is measured by the largest 1-norm difference between the control signals $\mathcal{NN}_{\widehat{\theta}}$ and $\mathcal{NN}_{\theta}$ across the abstract state $q$, i.e., $\underset{x\in q}{\max}\;|\!|{\mathcal{NN}_{\widehat{\theta}}(x)-\mathcal{NN}_{\theta}(x)}|\!|_{1}$. The relation between this objective function and the change of output layer weights is captured in the following proposition.

In the above proposition, by following the notation of layer functions (4), we use a single function $h:\mathbb{R}^{n}\rightarrow\mathbb{R}^{\mathfrak{o}_{F-1}}$ to represent all the hidden layers:

where $\mathfrak{o}_{F-1}$ is the number of neurons in the $(F-1)$-layer (the last hidden layer). We denote by $\mathbb{L}_{\mathcal{NN}_{\theta}\cap q}$ the intersected regions between the linear regions in $\mathbb{L}_{\mathcal{NN}_{\theta}}$ and the abstract state $q$, i.e.:

and denote by $\mathrm{Vert}(\mathbb{L}_{\mathcal{NN}_{\theta}\cap q})$ the set of all vertices of regions in $\mathbb{L}_{\mathcal{NN}_{\theta}\cap q}$, i.e., $\mathrm{Vert}(\mathbb{L}_{\mathcal{NN}_{\theta}\cap q})\triangleq\bigcup_{\mathcal{R}\in\mathbb{L}_{\mathcal{NN}_{\theta}\cap q}}\ \mathrm{Vert}(\mathcal{R})$. {pf} The function $\mathcal{NN}_{\theta}$ can be written as $\mathcal{NN}_{\theta}(x)=W^{(F)}h(x)+b^{(F)}$, and after the change of output layer weights, $\mathcal{NN}_{\widehat{\theta}}(x)=\widehat{W}^{(F)}h(x)+\widehat{b}^{(F)}$. Then,

where (19) directly follows the form of $\mathcal{NN}_{\theta}$ and $\mathcal{NN}_{\widehat{\theta}}$, (20) takes the absolute value of each term before summation and uses the fact that the hidden layer outputs $h(x)\geq 0$. We notice that when $h$ is restricted to each linear region of $\mathcal{NN}_{\theta}$, (20) is a linear program whose optimal solution is attained at extreme points. Therefore, in (21), the maximum can be taken over a finite set of all the vertices of linear regions in $\mathbb{L}_{\mathcal{NN}_{\theta}\cap q}$.

Proposition 6 proposes a direct way to design the intended projection operator. It implies that minimizing the right hand side of the inequality (15) will minimize the upper bound on the change in the control signal due to the projection operator. To that end, given a controller partition $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$, let $\Pi_{\mathcal{P}^{\star}}$ be the NN weight projection operator that updates the output layer weights of $\text{NN}_{q}$ as $\widehat{W}^{(F)},\widehat{b}^{(F)}=\Pi_{\mathcal{P}^{\star}}(\mathcal{NN}_{\theta})$. In order to minimize the change of NN outputs due to the projection, we minimize its upper bound in (15). Accordingly, we write the NN weight projection operator $\Pi_{\mathcal{P}^{\star}}$ as the following optimization problem:

A direct question is related to the computational complexity of the proposed projection operator $\Pi_{\mathcal{P}^{\star}}$. This is addressed in the following proposition.

Using the epigraph form of the problem (22)-(23), we can write it in the equivalent form:

The inequality (24) is affine since the hidden layer function $h$ is known and does not depend on the optimization variables. The number of inequalities in (24) is finite since the set of vertices $\mathrm{Vert}(\mathbb{L}_{\mathcal{NN}_{\theta}\cap q})$ is finite. To see the constraint (27) is affine, consider the CPWA function $\mathcal{NN}_{\widehat{\theta}}:x\mapsto\widehat{W}^{(F)}h(x)+\widehat{b}^{(F)}$, which is represented by the NN with the output layer weights $\widehat{W}^{(F)}$, $\widehat{b}^{(F)}$, and the hidden layer function $h$. Since $h$ restricted to each linear region $\mathcal{R}_{i}\in\mathbb{L}_{\mathcal{NN}_{\theta}}$ is a known affine function, the parameter $K_{i}$ (coefficients of $\mathcal{NN}_{\widehat{\theta}}$ restricted to $\mathcal{R}_{i}$) affinely depends on $\widehat{W}^{(F)}$ and $\widehat{b}^{(F)}$.

Finally, the following result shows the safety guarantee provided by applying the projection operator $\Pi_{\mathcal{P}^{\star}}$ during training of the neural network controller.

The proof directly follows Theorem 5 and the constraints (23) in the NN weight projection operator.

As a practical issue, it is often desirable to have the trained NNs be safe or close to safe even before the weight projection, and thus the projection operator $\Pi_{\mathcal{P}^{\star}}$ does not or only slightly modifies the NN weights without compromising performance. To reduce the effect of projection, our algorithm alternates the training and projection, and uses the safe controller partitions $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$ as constraints to bias the training.

We show the provably safe training of each local network $\text{NN}_{q}$ in Algorithm 1. Similar to a projected gradient algorithm, Algorithm 1 alternates the training (Line 3 in Algorithm 1) and the NN weight projection (Line 5 in Algorithm 1) up to a pre-specified maximum iteration max_iter. The training approach Constrained-Train (Line 3 in Algorithm 1) can be any imitation learning or reinforcement learning algorithm, with some extra constraints required by the safe controller partition $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$. In the imitation learning setting, we use $\{(x,u)\}$ to denote the collection of training data generated by an expert, where each state $x\in\mathcal{X}$ is associated with an input label $u\in\mathbb{R}^{m}$. The approach Constrained-Train requires that all the training data satisfy $u=K(x)$ and $K\in\mathcal{P}^{\star}$. Similarly, in the reinforcement learning setting, we assign high reward to the explored state-action pairs $(x,u)$ that satisfy $u=K(x)$ and $K\in\mathcal{P}^{\star}$.

To guarantee that the trained neural networks are safe, Algorithm 1 identifies the set of linear regions $\mathbb{L}_{\mathcal{NN}_{\theta}}$ (Line 4 in Algorithm 1) and projects the neural network weights by solving the linear program (22)-(23) (Line 5 in Algorithm 1). The solved weights $\widehat{W}^{(F)}$, $\widehat{b}^{(F)}$ are then used to replace the currently trained output layer weights $W^{(F)}$, $b^{(F)}$ (Line 6 in Algorithm 1), and the largest possible change of the NN’s outputs is bounded by (15). Thanks to the training approach Constrained-Train takes the constraints required by $\mathcal{P}^{\star}$ into consideration, and the problem (22)-(23) tries to minimize the change of NN outputs due to the projection, we observe in our experiments that the projection operator usually does not change the trained NN weights much. Indeed, in the result section, we show that the trained NNs perform well even with just a single projection at the end (i.e., $\text{max\_iter}=1$).

Among all the safe controller partitions in $P_{\text{safe}}(q)$, we assign one of them $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$ to each abstract state $q\in\mathbb{X}_{\text{safe}}$, by taking into account the liveness specification $\phi_{\text{liveness}}$. The liveness property requires that the nonlinear system (3) can reach the goal $\mathcal{X}_{\text{goal}}\subset\mathcal{X}$ by using the trained NN controller. Unlike the safety property which can be enforced using the projection operator $\Pi_{\mathcal{P}^{\star}}$, achieving the liveness property depends on practical issues, such as the amount of training data and the effort spent on training the NNs. To that end, we show that the safety guarantee provided by our algorithm does not impede training NNs to satisfy the liveness property by using standard learning techniques.

Since the posterior graph $S_{\mathrm{Post}}$ over-approximates the behavior of the system, a transition from the abstract state $q$ to $q^{\prime}$ in $S_{\mathrm{Post}}$ does not guarantee that every state $x\in q$ can reach $q^{\prime}$ in one step. Therefore, we introduce a predecessor operator to capture the liveness property. The predecessor of an abstract state $q^{\prime}\in\mathbb{X}$ under a controller partition $\mathcal{P}\in\mathbb{P}$ is defined as the set of states that can reach $q^{\prime}$ in one step by using an affine state feedback controller with some parameter $K\in\mathcal{P}$:

The predecessor operator can be computed using backward reachability analysis of polytopic systems (Yordanov et al.,, 2012). We then introduce the predecessor graph:

Notice that in the construction of $S_{\mathrm{Pre}}$, we restrict transition labels to the safe controller partitions $\mathcal{P}\in P_{\text{safe}}(q)$ at each state $q\in\mathbb{X}_{\text{safe}}$. Let $\mathcal{T}_{\mathrm{Pre}}$ be the set of all trajectories over the predecessor graph $S_{\mathrm{Pre}}$, then we use $\pi_{X}^{(t)}:\omega\mapsto q$ to denote the map from a trajectory $\omega\in\mathcal{T}_{\mathrm{Pre}}$ to the abstract state $q$ at time step $t$ in $\omega$, and use $\pi_{L}^{(t)}:\omega\mapsto l$ to denote the map from $\omega\in\mathcal{T}_{\mathrm{Pre}}$ to the label $l\in 2^{\mathbb{P}}$ associated to the transition from $\pi_{X}^{(t)}(\omega)$ to $\pi_{X}^{(t+1)}(\omega)$. By extending the formulation of specification to the abstract state space, a trajectory $\omega$ in $S_{\mathrm{Pre}}$ satisfies the reach-avoid specification $\phi$, denoted by $\omega\models\phi$, if $\omega$ reaches the goal state $q_{\text{goal}}$ in $T$ steps. Similar to the notation introduced in the posterior graph, we define a $\mathrm{Next}$ operator in the predecessor graph:

At each abstract state $q\in\mathbb{X}_{\text{safe}}$, our objective is to choose the candidate controller partition $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$ that can lead most of the states $x\in q$ to the goal. To that end, we restrict our attention to the trajectories in $S_{\mathrm{Pre}}$ that progress towards the goal. That is, let $|\omega|$ be the length of a trajectory $\omega\in\mathcal{T}_{\mathrm{Pre}}$, and $\mathrm{Dist}:\mathbb{X}_{\text{safe}}\rightarrow\mathbb{N}$ map a state $q\in\mathbb{X}_{\text{safe}}$ to the length of the shortest trajectory from the state $q$ to the goal in the predecessor graph $S_{\mathrm{Pre}}$. Then, we use $\mathcal{T}^{\prime}_{\mathrm{Pre}}\subseteq\mathcal{T}_{\mathrm{Pre}}$ to denote the subset of trajectories that lead to the goal:

Now we can define the subset of abstract states that progress towards the goal from abstract state $q$ under controller partition $\mathcal{P}$, denoted by $\mathcal{Q}_{q,\mathcal{P}}\subseteq\mathrm{Next}(q,\mathcal{P})$, as the set of abstract states along trajectories $\omega\in\mathcal{T}^{\prime}_{\mathrm{Pre}}$ that satisfy the given specification:

Then, the intersection between the abstract state $q$ and the predecessors of abstract states $q^{\prime}\in\mathcal{Q}_{q,\mathcal{P}}$ under the controller partition $\mathcal{P}$, i.e.:

measures the portion of states $x\in q$ that progress towards the goal by applying input $u=K(x)$ with $K\in\mathcal{P}$ at the current step. Then, our algorithm assigns each abstract state $q\in\mathbb{X}_{\text{safe}}$ with the controller partition $\mathcal{P}^{\star}\in P_{\text{safe}}(q)$ corresponding to the maximum volume of $\mathcal{I}_{q,\mathcal{P}}$, i.e. $\mathcal{P}^{\star}=\underset{\mathcal{P}\in P_{\text{safe}}(q)}{\text{argmax}}\mu(\mathcal{I}_{q,\mathcal{P}})$, where $\mu$ is the Lebesgue measure of $\mathbb{R}^{n}$. Indeed, and as mentioned in Section 3.3, such procedure only ranks the available choices of controller partitions and one may need to iterate over the remaining choices using the same heuristic above.

The final step of our framework is to combine all the local networks $\text{NN}_{q}$ into one global NN controller. Figure 2 (a) shows the overall structure of the global NN controller obtained by combining modules $[\text{NN}_{q}]_{\mathfrak{M}}$ corresponding to the local networks $\text{NN}_{q}$. As input to the NN controller, the state $x\in\mathcal{X}$ is fed into all the local networks, and the output of the NN controller is the summation of all the local network outputs. In the figures, we show a single output for simplicity, but it can be easily extended to multiple outputs (indeed, even in the figures, $u$ and $u_{q}$ can be thought as vectors in $\mathbb{R}^{m}$, and the summation and product operations correspond to vector addition and scalar multiplication, respectively).

Each module $[\text{NN}_{q}]_{\mathfrak{M}}$ consists of two parts: logic and ReLU NN. The logic component decides whether the current state $x$ is in the abstract state $q$ associated with $[\text{NN}_{q}]_{\mathfrak{M}}$, and outputs $1$ if the answer is affirmative, $0$ otherwise. The ReLU network $\text{NN}_{q}$ is trained for this abstract state $q$ using Algorithm 1. By multiplying the outputs of the logic and the ReLU NN, output of the module $[\text{NN}_{q}]_{\mathfrak{M}}$ is identical to the output of the ReLU NN if $x\in q$, and zero otherwise. Figure 2 (b) is an example of the module $[\text{NN}_{q}]_{\mathfrak{M}}$ for an arbitrary abstract state $q\subset\mathbb{R}^{2}$ given by $0\leq x_{1}\leq 2$ and $0\leq x_{2}\leq 2$.