Neural Abstraction-Based Controller Synthesis and Deployment

Rupak Majumdar

Mahmoud Salamati

Sadegh Soudjani

Newcastle University
United Kingdom

Abstraction-based techniques are an attractive approach for synthesizing correct-by-construction controllers to satisfy high-level temporal requirements.
A main bottleneck for successful application of these techniques is the memory requirement, both during controller synthesis (to store the abstract transition relation)
and in controller deployment (to store the control map).

We propose memory-efficient methods for mitigating the high memory demands of the abstraction-based techniques using neural network representations.

To perform synthesis for reach-avoid specifications, we propose an on-the-fly algorithm that
relies on compressed neural network representations of the forward and backward dynamics of the system.
In contrast to usual applications of neural representations, our technique maintains soundness of the end-to-end process.
To ensure this, we correct the output of the trained neural network such that the corrected output representations are sound with respect to the finite abstraction.

For deployment, we provide a novel training algorithm to find a neural network representation of the synthesized controller
and experimentally show that the controller can be correctly represented as a combination of a neural network and
a look-up table that requires a substantially smaller memory.

We demonstrate experimentally that our approach significantly reduces the memory requirements of abstraction-based methods.
We compare the performance of our approach with the standard abstraction-based synthesis on several models.
For the selected benchmarks,
our approach reduces the memory requirements respectively for the synthesis and deployment by a factor of $1.31\times 10^5$ and  $7.13\times 10^3$ on average, and up to $7.54\times 10^5$ and $3.18\times 10^4$.
Although this reduction is at the cost of increased off-line computations to train the neural networks,
all the steps of our approach are parallelizable and can be implemented on machines with higher number of processing units to reduce the required computational time.
This article appears as part of the ESWEEK-TECS special issue and was presented in the International Conference on Embedded Software (EMSOFT), 2023.

We consider the problem of formal controller synthesis and deployment for safety-critical systems.
Abstraction-based techniques are an attractive approach for synthesizing controllers to satisfy high-level temporal requirements. Finite abstractions are generally constructed using discretization. A main bottleneck for successful application of these techniques is their high memory demands during both controller synthesis and deployment.
In this work, we propose memory-efficient methods for mitigating the high memory demands of the abstraction-based techniques.
For synthesis, we propose an on-the-fly method that

relies on compressed neural network representations of the forward and backward dynamics of the system.

We correct the output of the trained neural network such that the corrected output representations are sound with respect to the finite abstraction.

We show how to use the corrected neural representations to perform synthesis on the fly for reach-avoid specifications.

For deployment, we provide a novel training algorithm to find a neural network representation of the synthesized controller and experimentally show that the controller can be correctly represented as a combination of a neural network and a look-up table that requires a substantially smaller memory.

Our synthesis and deployment algorithms use the compact corrected neural representations of the abstraction and the controller, thus significantly reduce the memory requirements of the abstraction-based methods.

We compare the performance of our approach with the standard abstraction-based synthesis on several vehicle models.

For the selected benchmarks,
our approach reduces the memory requirements respectively for the synthesis and deployment by a factor of $1.91\times 10^4$ and  $220$ on average, and up to $7.54\times 10^5$ and $1.12\times 10^4$. Although this reduction is at the cost of increased off-line computations,
all the steps of our approach are parallelizable and can be implemented on machines with higher number of processing units to reduce the required computational time.

We consider the formal controller synthesis and deployment problems for safety-critical systems. The ultimate goal of synthesis is to compute a controller which provides formal guarantee for satisfaction of the given specification under the presence of bounded non-determinism in the underlying dynamics. The goal of deployment is to implement the synthesized controller into the physical controller such that the required guarantee is maintained. In order to synthesize a correct-by-construction controller, one attractive solution is to use symbolic controller synthesis methods such as abstraction-based controller design (ABCD) technique, which relies on a finite abstraction of the system. One main bottleneck for application of ABCD is its high memory demands during both synthesis and deployment phases. Synthesis is high memory demanding, because size of the abstraction increases exponentially with the dimension of the state space. Therefore, for most of the real-world systems size of the abstraction, which is used during the synthesis, would become huge. Deployment is high memory demanding because the computed controller is essentially a look-up table containing list of the valid actions for every point within the set of discrete states.

In this work, we propose memory efficient methods for mitigating the high memory demand for both of the synthesis and deployment steps.
For synthesis, we propose an on-the-fly method,

which relies on compressed representations for the forward-in-time and backward-in-time dynamics. For a given state and input pair, these representations produce tight over-approximations
for the $\ell_\infty$ balls containing the corresponding (discrete) set of successors and predecessors. We consider neural networks as the structure for the  representations, and train them under the appropriate setting. We correct the output of the trained neural networks, so that the corrected output representations are sound with respect to the given finite abstraction.

Once the representation are computed, we plug them into our on-the-fly synthesis algorithm to solve the given instance of reachability problem.
Since our synthesis algorithm uses the compact representation functions instead of the full abstraction, we can significantly lower the space complexity of the synthesis process.
For deployment, we propose a novel formulation for training a neural network based representation of the synthesized symbolic controller and experimentally show that the trained representation can predict correct actions on a large portion of state set. For the small set of states at which the trained representation cannot produce the correct action, we store the corresponding set of states and actions in the form of a small look-up table. Therefore, we end up saving a lot of space by storing a representation plus a very small look-up table instead of the huge look-up table corresponding to the original controller.
All steps of our algorithms are parallelizable and hence we can gain more speed-ups by running our methods over machines with higher number of processing units. We evaluate the performance of our method using several vehicle models and show that it is effective in significantly reducing the memory requirements. For the selected benchmarks, our method reduces the space requirements for the synthesis and deployment by $3956$ and  $220$ times on average, respectively.

<concept_desc>Theory of computation Abstraction</concept_desc>
<concept_desc>Computing methodologies Representation of mathematical functions</concept_desc>
<concept_desc>Computing methodologies Computational control theory</concept_desc>

[300]Theory of computation Abstraction
[300]Computing methodologies Representation of mathematical functions
[500]Computing methodologies Computational control theory

§ INTRODUCTION

Designing controllers for safety-critical systems with formal correctness guarantees has been studied extensively in the past two decades,
with applications in robotics, power systems, and medical devices <cit.>.
Abstraction-based controller design (ABCD) has emerged as an approach that can algorithmically construct
a controller with formal correctness guarantees on systems with non-linear dynamics and
bounded adversarial disturbances <cit.>
and complex behavioral specifications.
ABCD schemes construct a finite abstraction of a dynamical system that has continuous state and input spaces, and solve
a two-player graph game on the abstraction.
When the abstraction is related to the original system through an appropriate behavioral relation (alternating bisimulation or feedback refinement <cit.>),
the winning strategy of the graph game can be refined to a controller for the original system.
Finite abstractions can be computed analytically when the system dynamics are known and certain Lipschitz continuity properties hold.
Even when the system dynamics are unknown, one can use data-driven methods to learn finite abstractions that are correct with respect to a
given confidence <cit.>.

A main bottleneck of ABCD is the memory requirement, both in representing the finite abstract transition relation and in representing the controller.
First, the state and input spaces of the abstraction grow exponentially with the system and input dimensions, respectively,
and the size of the abstract transition relation grows quadratically with the abstract states and linearly with the input states.
While symbolic encodings using BDDs can be used, in practice, the transition relation very quickly exceeds the available RAM.
Memory-efficient methods sometimes exploit the analytic description of the system dynamics or growth bounds <cit.>, but these techniques
are not applicable when the finite abstractions are learned directly from sampled system trajectories,
or when a compact analytical expression of the growth bound is not available.
Second, the winning strategy in the graph game is extracted as a look-up table mapping winning states to one or more available inputs.
Thus, the controller representation is also exponential in the system dynamics.
Such controllers cannot be deployed on memory-constrained embedded systems.

In this work, we address the memory bottleneck using approximate, compressed, representations of the transition relation and the controller map using neural networks.

We learn an approximate representation of the abstract transition relation as a neural network with a fixed architecture.
In contrast to the predominant use of neural networks to learn a generalization of an unknown function through sampling, we train the network on the entire data set
(the transition relation or the controller map) offline.
We store the transitions on disk, and train our networks in batch mode by bringing blocks of data into the RAM as needed.
The trained network is small and fits into RAM.
Since the training of the network minimizes error but does not eliminate it, we apply a correction to the output to ensure that the representation is
sound with respect to the original finite abstraction, i.e., every trajectory in the finite abstraction is preserved in the compressed representation.
We propose an on-the-fly synthesis approach that works directly on the corrected representation of the forward and backward dynamics of the system.
Although we present our results with respect to reach-avoid specifications, our approach can be generalized to other classes of properties and problems
(e.g., linear temporal logic specifications <cit.>) in which the solution requires the computation of  the set of predecessors and successors in the underlying transition system.

Similarly, we store the winning strategy as a look-up table mapping states to sets of valid inputs on disk and propose a novel training algorithm to find a
neural network representation of the synthesized controller.
The network is complemented with a look-up table that provides “exceptions” in which the network deviates from the winning strategy.
We experimentally demonstrate that a controller can be correctly represented as a combination of a neural network and a look-up table that requires a substantially smaller memory than
the original representation.

An important aspect of our approach is that, instead of using neural networks for learning an unknown data distribution, we train them over the entire data domain.
Therefore, in contrast to many other applications wherein neural networks provide function representation and generalization over the unseen data,
we are able to provide formal soundness guarantees for the performance of the trained neural representations over the whole dataset.

Our compression scheme uses additional computation to learn a compressed representation and avoid the memory bottleneck.
In our implementation, the original relations are stored on the hard drive and
data batches are loaded sequentially into the RAM to perform the training.
Hard drives generally have much higher memory sizes compared to the RAM, but reading data from the hard drive takes much longer.
However, data access during training is predictable and we can perform prefetching to hide the latency.
During the synthesis, the trained corrected neural representations fit into the RAM.
In contrast, a disk-based synthesis algorithm does not have predictable disk access patterns and is unworkable.
Similarly, the deployed controller only consists of the trained compact representation and (empirically) a small look-up table,
which can be loaded into the RAM of the controlling chip for the real-time operation of the system.

We evaluate the performance of our approach on several examples of different difficulties and show that it is effective in reducing the memory requirements at
both synthesis and deployment phases.
For the selected benchmarks, our method reduces the space requirements of synthesis and deployment respectively by factors of $1.31\times 10^5$ and  $7.13\times 10^3$ in average, and up to $7.54\times 10^5$ and $3.18\times 10^4$,

compared to the abstraction-based method that requires storing the full transition system. Moreover, we empirically show that, unlike other encodings, the memory requirement of our method is not affected by the system dimension on the considered benchmarks.

In summary, our main contributions are:

* Proposing a novel and sound representation scheme for compressing finite transition systems using the expressive power of neural networks;

* Proposing a novel on-the-fly controller synthesis method using the corrected neural network representations of forward and backward dynamics;

* Proposing an efficient scheme for compressing the controller computed by abstraction-based synthesis methods;

* Demonstrating significant reduction in the memory requirements by orders of magnitude through a set of standard benchmarks. [
Our implementations are available online at <https://github.com/msalamati/Neural-Representation>.

The rest of this paper is organized as follows. After a brief discussion of related works, we give a high-level overview of our proposed approach in Subsec. <ref>.
The preliminaries and the problem statements are given in Sec. <ref>.
We provide the details of our synthesis and deployment algorithms in Sec. <ref> and <ref>, respectively.
In Sec <ref>, we provide experimental results of applying our approach to several examples.
We state the concluding remarks in Sec. <ref>.

§.§ Related Work

Synthesis via reinforcement learning.
The idea of using neural networks as function approximators to represent tabular data for synthesis purposes has been used in different fields such as reinforcement learning (RL) literature and aircraft collision avoidance system design. RL algorithms try to find an optimal control policy by iteratively guiding the interaction between the agent and the environment modeled as a Markov decision process <cit.>. When the space of the underlying model is finite and small, q-tables are used to represent the required value functions and the policy. When the space is large and possibly uncountable, such finite q-tables are replaced with neural networks as function approximators. Convergence guarantees that hold with the q-table representation <cit.> are not valid for non-tabular setting <cit.>. A similar behavior is observed in our setting: we lose the correctness guarantees in our approach without correcting the output of the neural network representations of the transition systems and the tabular controller.

Neural-aided controller synthesis. Constructing neural network representations of the dynamics of the control system and using them for synthesis is studied in specific application domains including the design of unmanned airborne collision avoidance systems <cit.>. The central idea of <cit.> is to start from a large look-up table representing the dynamics, train a neural network on the look-up table, and use it in the dynamic programming for issuing horizontal and vertical advisories. Several techniques are used to reduce the storage requirement since the obtained score table—that is the table mapping every discrete state-input pair into the associated score—becomes huge in size (hundreds of gigabytes of floating numbers). Since simple techniques such as down sampling and block compression <cit.>,
are unable to achieve the required storage reduction, Julian et al. have shown that deep neural networks can successfully approximate the score table <cit.>. However, as in the RL controller synthesis, there is no guarantee that the control input computed using the neural representation matches the one computed using the original score table. In contrast, our corrected neural representations are guaranteed to produce formally correct controllers.

Reactive synthesis.
Binary decision diagrams (BDDs) are used extensively in the reactive synthesis literature to represent the underlying transition systems
<cit.>. While BDDs are compact enough for low-order dynamical systems, recent synthesis tools such as SCOTS v2.0
<cit.> have already migrated into the non-BDD setting in order to avoid the large runtime overheads. In fact, motivated by reducing the required memory foot print, the current trend is to synthesize controllers in a non-BDD on the fly to eliminate the need for storing the transition system <cit.>. These memory-efficient methods exploit the analytic description of the system dynamics or growth bounds. In contrast, our technique
is applicable also to the case where the finite abstractions are learned directly from the sampled system trajectories,
i.e., when no compact analytical expression of the dynamics and growth bounds are available.

Verifying systems with neural controllers.
An alternative approach developed for safety-critical systems is to use neural networks as a representation of the controller and learn the controller using techniques such as reinforcement learning and data-driven predictive control <cit.>.
In this approach, the controller synthesis stage does not provide any safety guarantee on the closed loop system, i.e., on the feedback connection of the neural controller and the physical system. Instead, the safety of the closed-loop system is verified a posteriori for the designed controller.

Ivanov et al. have considered dynamical systems with sigmoid-based neural network controllers, used the fact that
sigmoid is the solution to a quadratic differential equation to transform the composition of the system and the neural controller into an equivalent hybrid system, and studied reachability properties of the closed-loop system by utilizing existing reachability computation tools for hybrid systems <cit.>.

Huang et al. have considered dynamical systems with Lipschitz continuous neural controllers and used Bernstein polynomials for approximating the input-output model of the neural network <cit.>.

Development of formal verification ideas for closed-loop systems with neural controllers has led into emergence of dedicated tools such as NNV <cit.> and POLAR <cit.>. While these methods provide guarantees on closed-loop control system with neural controllers, they can only consider finite horizon specifications for a given set of initial states. In contrast, we consider controllers that are synthesized for infinite horizon specifications.

Minimizing the memory foot print for symbolic controllers. Girard et al. have proposed a method to reduce the memory needed to store safety controllers by determinizing them, i.e., choosing one control input per state such that an algebraic decision diagram (ADD) representing the control law is minimized <cit.>. Zapreev et al. have provided two methods based on greedy algorithms and symbolic regression to reduce the redundancy existing in the controllers computed by the abstraction-based methods <cit.>. Both of the ADD scheme in <cit.> and the BDD-based scheme in <cit.> have the capability to determinize the symbolic controller and reduce its memory foot print. However, the computed controller still suffers from the additional runtime overhead of the ADD/BDD encoding.

Further, as mentioned by the authors of <cit.>, their regression-based method is not able to represent the original controller with high accuracy. In contrast, our tool produces real-valued representations for symbolic controllers and can (additionally) be computed on top of the simplified version found by either of the methods proposed in <cit.>.

Compressed representations for model predictive controllers (MPCs).
Hertneck et al. have proposed a method to train an approximate neural controller representing the original robust (implicit) MPC satisfying the given specification <cit.>. While reducing the online computation time is the main motivation in implicit MPCs, minimizing the memory foot print is the main objective in explicit MPCs. Salamati et al. have proposed a method which is based on solving an optimization to compute a memory-optimized controller with mixed-precision coefficients used for specifying the required coefficients <cit.>. Our method considers a different class of controllers that can fulfill infinite horizon temporal specifications.

§.§ Overview of the Proposed Approach

In this subsection, we provide a high-level description of our approach for both synthesis and deployment.

Graphical description of the proposed scheme for compressing finite abstractions

Corrected neural representations. Fig. <ref>
gives a pictorial description of the steps for computing a corrected neural network representation. Given a finite abstraction $\bar\Sigma$ that corresponds to the forward dynamics of the system and stored on the hard drive, we first compute the transition system $\bar\Sigma_B$ corresponding to the backward dynamics. Next, we extract the input-output training datasets  $\ds_F$ and $\ds_B$ respectively from the forward and backward systems, and store them on the hard drive. Each data point contains one state-input pair and the characterization of $\ell_\infty$ ball for the corresponding reachable set. We train two neural networks $\NN_F$ and $\NN_B$ such that they represent compressed input-output surrogates for the datasets $\ds_F$ and $\ds_B$, respectively. Finally, we compute the soundness errors $\eFb$ and $\eBb$ which correspond to the difference between the output of $\NN_F$ and $\NN_B$ and the respective values in $\ds_F$ and $\ds_B$, calculated over all of the state-input pairs. We use the computed errors $\eFb$ and $\eBb$ in order to construct the corrected neural representations $R_F$ and $R_B$. We will get memory savings by using $R_F$ and $R_B$ instead of $\bar\Sigma$ and $\bar\Sigma_B$, respectively.

Graphical description of the proposed synthesis scheme

Synthesis. Fig. <ref> gives a pictorial description of our proposed synthesis algorithm for a reach-avoid specification with the target set  $\goal$ and obstacle set $\avoid$ as subsets of the state space. Let $W_0\subseteq \Xb$ represents a discrete under-approximation of the target set $\goal$.
We initialize the winning set as $L=W_0$, the controller as $C=\emptyset$, and the set of state-input pairs that must be added to the controller as $\Gamma_{0}=\emptyset$. In each iteration, we compute the set of new states that belong to the winning set and update the controller accordingly, until no new state is added to $L$. To this end, we first use $R_B$ and its corresponding soundness error $e_B$ to compute a set of candidates $S_i$ out of which some belong to $L$ and it is guaranteed that there will be no winning state outside of $S_{i}$ in the $i^{th}$ iteration.
We use $R_F$ and its corresponding soundness error $e_F$ to compute the set of new winning states $W_{i+1}\subseteq S_i$. We also compute the set of control inputs for every new winning state and compute the corresponding set of state-input pairs $\Gamma_{i+1}$ that must be added to the controller.

Finally, if $W_{i}=\emptyset$, we terminate the computations as we already have computed the winning set $L$ and the controller $C$. Otherwise, we add the new winning set of states and state-input pairs, respectively, into the overall winning set ($L\leftarrow L\cup W_{i+1}$) and the controller ($C\leftarrow C\cup\Gamma_{i+1}$), and repeat the steps in the next iteration.

Graphical description of the proposed scheme for compressing

Deployment.Fig. <ref>
shows our method for compressing controllers that are obtained from abstraction-based approaches. In the first step, we collect the training dataset $\ds_C$ and reformat it to become appropriate for our specific formulation of a classification problem. Each data point contains one state and an encoding of the corresponding set of control inputs.

We then train a neural network $\NN_C$ on the data with the loss function designed for this specific classification problem. Finally, we find all the states at which the output label generated by $\NN_C$ is invalid, and store the corresponding state-input pair in a look-up table, denoted by $\hat C$. We experimentally show that $\hat C$ only contains a very small portion of state-input pairs.

Graphical description of the proposed scheme for compressing the controller

§ PRELIMINARIES

§.§ Notation

We denote the set of integer numbers and natural numbers including zero by $\ints$ and $\nats$, respectively.
We use the notation $\reals$ and $\reals_{>0}$ to denote respectively the set of real numbers and the set of positive real numbers.
We use superscript $n>0$ with $\reals$ and $\reals_{>0}$ to denote the Cartesian product of $n$ copies of $\reals$ and $\reals_{>0}$ respectively. For a vector $\boldsymbol a \in \reals^d$, we denote its $i^{th}$ component, element-wise absolute value and $\ell_2$ norm by $\boldsymbol a(i)$, $|\boldsymbol a|$ and $\|\boldsymbol a\|$, respectively. For a pair of vectors $\boldsymbol a,\boldsymbol b\in\reals^d$, $\llbracket \boldsymbol{a},\boldsymbol{b}\rrbracket$ denotes the hyper-rectangular set $[\boldsymbol{a}(1),\boldsymbol{b}(1)]\times\dots\times[\boldsymbol{a}(d),\boldsymbol{b}(d)]$. Further, given $\boldsymbol{c}\in\reals^d$, $\boldsymbol{c}+\llbracket\boldsymbol{a},\boldsymbol{b}\rrbracket$ is another hyper-rectangular set which is shifted compared to $\llbracket\boldsymbol{a},\boldsymbol{b}\rrbracket$ to the extent determined by $\boldsymbol{c}$. Similarly, for a vector $\boldsymbol \eta\in\reals^d$ and a pair of vectors $\boldsymbol a,\boldsymbol b\in\reals^d$, for which $\boldsymbol a = \alpha \boldsymbol\eta$, $\alpha\in \ints$ and $\boldsymbol b=\beta\boldsymbol\eta$, $\beta\in\ints$, we define
$\llbracket \boldsymbol{a},\boldsymbol{b}\rrbracket_{\boldsymbol\eta}=\prod_{i=1}^d A_i$,
where $A_i=\set{ \gamma\boldsymbol\eta(i)\mid\gamma\in \ints, \;\alpha\leq \gamma\leq \beta}.$

Given $\boldsymbol c\in \mathbb{R}^n$ and $\boldsymbol \varepsilon\in \mathbb{R}_{>0}^{n}$, the ball with center $c$ and radius $\boldsymbol\varepsilon$ in $\mathbb{R}^n$ is denoted by
$\ball_{\boldsymbol\varepsilon}(\boldsymbol c)\coloneqq \set{\xb \in \mathbb{R}^n \mid  |\xb-\boldsymbol c|\leq \boldsymbol\varepsilon }$. For two integers $a,b\in\ints$, we define $[a;b]=\set{c\in \ints\mid a\leq c \leq b}$.

Let $A$ be a finite set of size $|A|$. The empty set is denoted by $\emptyset$. When $A$ inherits a coordinate structure, i.e., when its members are vectors on the Euclidean space, $A(i)$ denotes the projection of set $A$ onto its $i^{th}$ dimension.
Further, we use the notation $A^\infty$ to denote the set of all finite and infinite sequences formed using the members of $A$. Our control tasks are defined using a subset of Linear Temporal Logic (LTL).
In particular, we use the until operator $\mathcal{U}$.
Let $p$ and $q$ be subsets of $\reals^n$ and $\rho=(\xb_0,\xb_1,\dots)$ be an infinite sequence of elements from $\reals^n$.  We write $\rho\models p\mathcal{U}q$ if there exists
$i\in\mathbb{N}$ s.t. $\xb_i\in q$ and $\xb_j\in p$ for all $0\leq j<i$.
For the detailed syntax and semantics of LTL, we refer to <cit.> and references therein.

§.§ Control Systems

We consider the class of continuous-state continuous-time control systems characterized by the tuple $\Sigma = (X, U, W, f)$, where
$X\subset \reals^n$ is the compact state space,

$U\subset\reals^m$ is the compact input space, and
$W\subset\reals^n$ is the disturbance space being a compact hyper-rectangular set of disturbances which is symmetric with respect to the origin (i.e., for every $\boldsymbol w\in W$ also it is the case that $-\boldsymbol w\in W$).
The vector field $f: X \times U \rightarrow X$ is such that $f(\cdot, u)$ is locally Lipschitz for all $u\in U$.
The evolution of the state of $\Sigma$ is characterized by the differential inclusion

\begin{equation}
\label{eq:ODE}
\dot x(t)\in f(x(t),u(t))+W.
\end{equation}

Given a sampling time $\tau>0$, an initial state $x_0\in X$, and a constant input $u\in U$, define the continuous-time trajectory $\zeta_{x_0, u}$
of the system on the time interval $[0, \tau]$ as an absolutely continuous function $\zeta_{x_0,u}: [0, \tau] \rightarrow X$ such that $\zeta_{x_0,u}(0) = x_0$, and
$\zeta_{x_0,u}$ satisfies the differential inclusion $\dot{\zeta}_{x_0,u}(t) \in f(\zeta_{x_0,u}(t), u) + W$ for almost all $t\in [0,\tau]$.
Given $\tau$, $x_0$, and $u$, we define $\Sol(x_0, u, \tau)$ as the set of all $x\in X$ such that there is a continuous-time trajectory
$\zeta_{x_0,u}$ with $\zeta(\tau) = x$.
A sequence $x_0,x_1,x_2, \ldots$ is a time-sampled trajectory for a continuous control system if $x_0\in X$ and for each $i\geq 0$, we have
$x_{i+1} \in \Sol(x_i, u_i, \tau)$ for some $u_i \in U$.

In this work, we consider two characterizations for control systems: (i) a continuous characterization represented as differential inclusion systems, and (ii)  a discrete characterization represented as finite-state transition systems.

Continuous control systems.
We consider the class of continuous-state continuous-time control systems characterized by the tuple $\Sigma_c = (X, U, W_c, f_c)$, where
$X\subset \reals^n$ is the state space,

$U\subset\reals^m$ is the input space, and
$W_c\subset\reals^n$ is the disturbance space being a compact hyper-rectangular set of disturbances which is symmetric with respect to the origin (i.e., for every $\boldsymbol w\in W_c$ also it is the case that $-\boldsymbol w\in W_c$).
The vector field $f_c: X \times U \rightarrow X$ is such that $f_c(\cdot, u)$ is locally Lipschitz for all $u\in U$.
The evolution of the state of $\Sigma_c$ is characterized by the differential inclusion

\begin{equation}
\label{eq:ODE}
\dot x(t)\in f_c(x(t),u(t))+W_c.
\end{equation}

Given a sampling time $\tau>0$, an initial state $x_0\in X$, and a constant input $u\in U$, define the continuous-time trajectory $\zeta_{x_0, u}$
of the system on the time interval $[0, \tau]$ as an absolutely continuous function $\zeta_{x_0,u}: [0, \tau] \rightarrow X$ such that $\zeta_{x_0,u}(0) = x_0$, and
$\zeta_{x_0,u}$ satisfies the differential inclusion $\dot{\zeta}_{x_0,u}(t) \in f_c(\zeta_{x_0,u}(t), u) + W_c$ for almost all $t\in [0,\tau]$.
Given $\tau$, $x_0$, and $u$, we define $\Sol(x_0, u, \tau)$ as the set of all $x\in X$ such that there is a continuous-time trajectory
$\zeta_{x_0,u}$ with $\zeta(\tau) = x$.
A sequence $x_0,x_1, \ldots$ is a time-sampled trajectory for a continuous control system if $x_0\in X$ and for each $i\geq 0$, we have
$x_{i+1} \in \Sol(x_i, u_i, \tau)$ for some $u_i \in U$.

Given a continuous-time nonlinear dynamical system described with the tuple $(X, U, W_c, f_c)$ as above and a sampling time $\tau>0$, there exist techniques to construct
a discrete-time control system $\Sigma = (X, x_\init, U, W, f)$ such that every time-sampled trajectory of the continuous-time system is
also a trajectory of $\Sigma$.
We omit the details of the construction; see, e.g., <cit.>.

Given a continuous-time nonlinear dynamical system with the tuple $(X, U, W_c, f_c)$ as above and a sampling time $\tau$, there exist techniques to construct
a discrete-time control system $\Sigma = (X, x_\init, U, W, f)$ such that every time-sampled trajectory of the continuous-time system is
also a trajectory of $\Sigma$.
We omit the details of the construction; see, e.g., <cit.>.

A trajectory of $\Sigma$ is a finite or infinite sequence $x_0, x_1, \ldots \in X^\infty$
such that $x_0 \in X$ and for each $i\geq 0$, there is an $u_i\in U$ and $w_i \in W$ such that
$x_{i+1} = f(x_i, u_i) + w_i$.
A trajectory is nominal if $w_i = 0$ for all $i\geq 0$.

In this note, we consider discrete-time dynamical systems with compact hyper-rectangular state and input spaces $X\subset \reals^n$, $U\subset\reals^m$, whose dynamics are given in the form of the difference inclusions

\begin{equation}\label{eq:sys_dynamics}
\xb_{i+1}\in f(\xb_i, \ub_i)+W,
\end{equation}

where $\xb_i\in X$ and $\ub_i\in U$ are the state, input vectors at the current time step and $\xb_{i+1}\subset X$ denotes the updated state vector at the next time-step. Further, the mapping $f\colon\reals^n\times\reals^m\rightarrow\reals^n$ defines the nominal dynamics of the system at every time-step and $W\subset \reals^n$ represents the compact hyper-rectangular set of disturbances which is symmetric with respect to the origin (i.e., for every $\boldsymbol w\in W$ also it is the case that $-\boldsymbol w\in W$).

Note that the discrete-time dynamics can be derived from a continuous-time dynamics by specifying a sampling time $\tau>0$. For the sake of conciseness, we denote every discrete-time control system using the tuple $\Sigma=(X,\xb_\init,U,W,f,\tau)$, where $\xb_\init\in X$ represents an initial state. The sampling time $\tau$ is included to emphasize that the nominal dynamics $f$ and disturbance set $W$ are derived from the original continuous-time system $\Sigma_c=(X,\xb_\init,U,W_c,f_c)$ with respect to $\tau$.

A trajectory of $\Sigma$ is a finite or infinite sequence $\xb_0, \xb_1, \ldots \in X^\infty$
such that $\xb_0 = x_{\init}$ and for each $i\geq 0$, there is an $\ub_i\in U$ and $\boldsymbol w_i \in W$ such that
$\xb_{i+1} = f(\xb_i, \ub_i) + \boldsymbol w_i$.
A trajectory is nominal if $\boldsymbol w_i = 0$ for all $i\geq 0$.
Intuitively, a control system represents a (possibly nonlinear) dynamical system with control inputs form $U$
and disturbances from the set $W$.

§.§ Finite Abstractions

In order to satisfy a temporal specification on the trajectories of the system, it is generally needed to over-approximate the dynamics of the system with a finite discrete-time model.

In this work, we consider discrete-state discrete-time control systems. We denote state and input spaces of a control system by $X\subset \reals^n$ and $U\subset\reals^m$, respectively. In case an analytical model for the underlying control system is not given, one common approach is to store the set of transitions for each pair of quantized state and input value.

Let $\Xb\subset X$ and $\Ub\subset U$ be the finite sets of states and inputs, computed by (uniformly) quantizing the compact state and input spaces $X$ and $U$ using the  rectangular discretization partitions of size $\etab_x\in\reals^n_{>0}$ and $\etab_u\in\reals^m_{>0}$, respectively.

A finite abstraction associated with the dynamics in Eq. (<ref>)
is characterized by the tuple $ \bar\Sigma\colon(\Xb, \Ub, T_F)$, where $T_F\subseteq\Xb\times \Ub \times \Xb$ denotes the system's forward-in-time transition system. The transition system $T_F$ is defined such that

\begin{align*}
&(\xbb,\ubb,\xbb')\in T_F\Leftrightarrow\exists (\xb,\ub,\xb')\in \ball_{\frac{\etab_x}{2}}(\xbb)\times \ball_{\frac{\etab_u}{2}}(\ubb)\times \ball_{\frac{\etab_x}{2}}(\xbb')\;\text{s.t.}\;
\xb'\in\Sol(\xb,\ub,\tau).
\end{align*}

When the dynamics in Eq. (<ref>) are known and satisfy the required Lipschitz continuity condition, the finite abstraction can be constructed using the method proposed in <cit.>. For systems with unknown dynamics, data-driven schemes for learning finite abstractions can be employed <cit.>.
By abusing the notation, we denote the reachable set for a state-input pair $(\xbb,\ubb)\in\Xb\times\Ub$ by $T_F(\xbb,\ubb)=\set{\xbb'\in\Xb\mid \xbb'\in \Sol(\xbb,\ubb,\tau)}$.
We assume that the reachable sets take hyper-rectangular form, meaning that for every $\xbb\in \Xb$, $\ubb\in\Ub$ the corresponding reachable set $H=T_F(\xbb,\ubb)$ can be rewritten as $H=\prod_{i=1}^n H(i)$, where $H(i)$ corresponds to the projection of the set $H$ onto its $i^{th}$ coordinate. Otherwise, in case that $H$ is not hyper-rectangular, it is over-approximated by $\prod_{i=1}^n H(i)$.
Note that $\bar\Sigma$ can in general correspond to a non-deterministic control system, i.e., $|T_F(\xbb,\ubb))|>1$ for some $\xbb\in\Xb, \ubb\in\Ub$.

Given $\bar\Sigma$, one can easily compute the characterization of the backward-in-time dynamics as

\begin{equation}\label{eq:BW_sys}\bar\Sigma_B=(\Xb,\Ub,T_B),\; T_B=\set{(\xbb,\ubb,\xbb')\in\Xb\times\Ub\times\Xb\mid(\xbb',\ubb,\xbb)\in T_F}.
\end{equation}

A trajectory of $\bar\Sigma$ is a finite or infinite sequence $\xb_0, \xb_1,\xb_2, \ldots \in \Xb^\infty$,
such that for each $i\geq 0$, there is a control input $\ubb_i\in \Ub$ such that
$(\xb_i,\ubb_i,\xb_{i+1}) \in T_F$.

The operator $\Pre(\cdot)$ acting on sets $P\subseteq\Xb$ is defined as

\begin{align*}
&\Pre(P)=\{\xbb\in \Xb \mid \exists \ubb\in\Ub\;s.t.\; T_F(\xbb,\ubb)\subseteq P\}.
\end{align*}

Finally, to compute an over-approximating set of the discrete states that have overlap with a hyper rectangular set $\llbracket\boldsymbol x_{lb}, \boldsymbol x_{ub}\rrbracket$, we define the (over-approximating) quantization mapping as

\begin{equation*}
\bar K(\boldsymbol x_{lb}, \boldsymbol x_{ub}) = \set{\bar{\boldsymbol x}'\in \bar X\mid \llbracket\bar{\boldsymbol x}'-\boldsymbol{\eta_x}/2, \bar{\boldsymbol x}'+\boldsymbol{\eta_x}/2\rrbracket\cap \llbracket\boldsymbol x_{lb}, \boldsymbol x_{ub}\rrbracket\neq \emptyset}.
\end{equation*}

Similarly, the under-approximating quantization mapping is defined as

\begin{equation*}
\ubar K(\boldsymbol x_{lb}, \boldsymbol x_{ub}) = \set{\bar{\boldsymbol x}'\in \bar X\mid \llbracket\bar{\boldsymbol x}'-\boldsymbol{\eta_x}/2, \bar{\boldsymbol x}'+\boldsymbol{\eta_x}/2\rrbracket\subseteq \llbracket\boldsymbol x_{lb}, \boldsymbol x_{ub}\rrbracket}.
\end{equation*}

To compute  the transition system for a given control system, we need to over-approximate reachable sets. Let $\beta\colon \reals^n\times U\rightarrow\reals_{>0}$ be a growth bound function (e.g., the one introduced in <cit.>) and $\boldsymbol r=\beta(\etab_x/2,\ubb)$.
The over-approximation of trajectories started in the cell centered at $\xbb\in \Xb$ applying the control $\ubb\in \Ub$ is defined as

\begin{equation}
\Gamma^f(\xbb, \ubb) = (\xb_{lb}, \xb_{ub}) = (-\boldsymbol r+f(\xbb,\ubb), \boldsymbol r+f(\xbb,\ubb))
\end{equation}

To compute list of the cells which have overlap with $\Gamma^f(\xbb, \ubb)$, the quantization mapping is defined as

\begin{equation}
K(\xb_{lb}, \xb_{ub}) = \set{\xbb'\in \Xb\mid \llbracket\xbb'-\etab_x/2, \xbb'+\etab_x/2\rrbracket\cap \llbracket\xb_{lb}, \xb_{ub}\rrbracket\neq \set{}}.
\end{equation}

Using the monolithic approach, we have

\begin{equation}\label{eq:TS_def}
T = \set{(\xbb,\ubb, \xbb')\in\Xb\times \Ub\times \Xb\mid  \xbb'\in K(-\boldsymbol r+f(\boldsymbol s), \boldsymbol r+f(\boldsymbol s)}.
\end{equation}

Given a set $P\subseteq\Xb$, the operators $\Post(\cdot)$ and $\Pre(\cdot)$ can be computed in the following way:

\begin{equation}
\Post(P)=\set{\xbb'\in \bar X\mid \exists \xbb\in P, \ubb\in\Ub\;s.t.\; (\xbb,\ubb,\xbb')\in T},
\end{equation}

\begin{align}
&\Pre(P)=\{\xbb\in \Xb \mid \Post(\xbb)\subseteq P\}.
\end{align}

An open-loop controller for $\Sigma=(X,\xb_\init,U,f,W)$ over a time interval $[0;N_p]$ with $N_p\in\nats$
is a function $C\colon [0;N_p]\to U$.
The open-loop is obtained when we connect $C$ with $\Sigma$ serially,

denoted by $C \triangleright \Sigma$.
The set of trajectories of the open-loop system $C\triangleright\Sigma$ consists of all finite trajectories
$\xb_0, \xb_1, \ldots,\xb_{N_p}$ such that $\xb_0 = \xb_\init$ and for all $i \in [0; N_p-1]$, we have $\xb_{i+1} = f(\xb_i, C(i)) + \boldsymbol w_i$ for some $\boldsymbol w_i \in W$.

§.§ Controllers

For a finite abstraction $\bar\Sigma=(\Xb,\Ub,T_F)$, a feedback controller is denoted by $C\subseteq\Xb\times\Ub$. The set of valid control inputs at every state $\xbb\in\Xb$ is defined as $C(\xbb)\coloneq \set{\ubb\in\Ub\mid(\xbb,\ubb)\in C}$.
We denote the feedback composition of $\bar\Sigma$ with $C$ as $C\parallel\bar\Sigma$. For an initial state $\xbb^\ast\in\Xb$, the set of trajectories of $C\parallel\bar\Sigma$ having length $k\in\nats$ is the set of sequences $\xbb_0,\xbb_1,\xbb_2,\dots,\xbb_{k-1}$, s.t. $\xbb_0=\xbb^\ast$, $\xbb_{i+1}\in T_F(\xbb_i,\ubb_i)$ and $\ubb_i\in C(\xbb_i)$ for $i\in[0;k-2]$.

§.§ Neural Networks

A neural network $\NN(\boldsymbol\theta,\cdot)\colon \reals^d\rightarrow\reals^q$ of depth $v\in\nats$ is a parameterized function which transforms an input vector $\boldsymbol a\in\reals^d$ into an output vector $\boldsymbol b\in\reals^q$, and is constructed by the forward combination of $v$ functions as follows:

\NN(\boldsymbol\theta,\boldsymbol a)=G_v(\boldsymbol\theta_v,G_{v-1}(\boldsymbol\theta_{v-1},\ldots,G_2(\boldsymbol\theta_2,G_1(\boldsymbol\theta_1,\boldsymbol a)))),

$\boldsymbol\theta=(\boldsymbol\theta_1,\dots,\boldsymbol\theta_v)$ and
$G_i(\boldsymbol{\theta}_i,\cdot)\colon \reals^{p_{i-1}}\rightarrow \reals^{p_{i}}$ denotes the $i^{th}$ layer of $\NN$
parameterized by $\boldsymbol\theta_i$ with $p_0=d$, $p_i\in \nats$ for $i\in[1;v]$ and $p_v=q$. The $i^{th}$ layer of the network, $i\in[1;v]$, takes an input vector in $\reals^{p_{i-1}}$ and transforms it into
an output representation in $\reals^{p_i}$ depending on the value of parameter vector
$\boldsymbol \theta_i$ and type of the used activation function in $G_i$. During the training phase of the network, the set of parameters $\boldsymbol{\theta}$ is learned over the training set which consists of a number of input-output pairs $\{(\boldsymbol a_k,\boldsymbol b_k)\mid k=1,2,\ldots,N\}$,
in order to achieve the highest performance with respect to an appropriate metric such as mean squared error. For a trained neural network, we drop its dependence on the parameters $\boldsymbol\theta$. In this paper, we characterize a neural network of depth $v$ using its corresponding list of layer sizes, i.e., $(p_1,p_2,\ldots,p_v)$, and the type of the activation function used, e.g., hyperbolic tangent, Rectified Linear Unit (ReLU), etc.

Neural networks can be used for both regression and classification tasks. In a regression task, the goal is to predict a numerical value given an input, whereas, a classification task requires predicting the correct class label for a given input. In order to measure performance of the trained neural network, we consider prediction error. Note that prediction error is different from the metrics such as mean squared error (MSE) which are used during the training phase for defining the objective function for the training. The prediction error for regression and classification tasks is defined differently. For our regression tasks, we define the prediction error for a trained neural network $\NN$ over a training set $\{(\boldsymbol a_k,\boldsymbol b_k)\mid k=1,2,\ldots,N\}$ as

$$\boldsymbol e=\max_{k\in[1;N]}|\NN(\boldsymbol a_k)-\boldsymbol b_k|.$$

In this paper, we consider the classification tasks wherein there may exist more than one valid class label for each input. Therefore, the training set would be of the form $\{(\boldsymbol a_k,\boldsymbol b_k)\mid k=1,2,\ldots,N\}$, where $b_k\in\{0,1\}^q$
and $\boldsymbol b_k(i)=1$ iff $i\in[1;q]$ corresponds to a valid label at $\boldsymbol a_k$.
Since the number of valid labels for each input can be different, we define the prediction error of a trained classifier $\NN$ in the following way:

$$err=\frac{|\set{k\in[1;N]\mid \boldsymbol b_k(i)=0\;\text{with }   i=argmax(\NN(\boldsymbol a_k))}|}{N}.$$

For a given neural network $\NN$ with the training set $\{(\boldsymbol a_k,\boldsymbol b_k)\mid k=1,2,\ldots,N\}$, we define the continuity index as

\begin{equation}\label{eq:cont_idx}
\alpha_\NN =  \max_{1\leq i,j\leq N,\;i\neq j}\frac{\|\NN(\boldsymbol a_i) -\NN( \boldsymbol a_j)\|}{\|a_i-a_j\|}.
\end{equation}

§.§ Problem Statement

We now consider the controller synthesis problem for finite abstractions
w.r.t. a reach-avoid specification.

Let $\goal, \avoid \subseteq X, \goal\cap\avoid =\emptyset$ be the set of states representing the target and unsafe spaces, respectively.
The winning domain for the finite abstraction $\bar\Sigma=(\Xb,\Ub,T_F)$ is the set of states $\xbb^\ast\in\Xb$ such that there exists a feedback controller $C$ such that all trajectories of $C\parallel\bar \Sigma$, which are started at $\xbb^\ast$, satisfy the given specification $\Phi$. $\xbb_0=\xbb^\ast,\xbb_1,\xbb_2,\dots\models\Phi$.
The aim is to find the set of the winning states $L$ together with a feedback controller $C$ such that $C\parallel \bar\Sigma$ satisfies the reach-avoid specification $\Phi $. To compute the winning domain and the controller, one can use the methods from reactive synthesis. For many of interesting control systems, size of $T_F$ in the finite abstraction becomes huge. This restricts the application of reactive-synthesis-based methods for computing the controller. Therefore, we are looking for a method which uses compressed surrogates of $T_F$ to save memory. In particular, we want to train two corrected neural surrogates, i.e., neural network representations whose output is corrected to maintain the soundness property: $R_F$ for the forward-in-time dynamics and $R_B$ for the backward-in-time dynamics.

Continuous control systems $\Sigma_c=(X,U,W_c,f_c)$, sampling time $\tau>0$ and specification $\Phi=\lnot\avoid\,\mathcal{U}\,\goal$.

Outputs: Winning domain $L$ and a feedback controller $C$ for $\Sigma_c$ such that $C\parallel\Sigma_c$ realizes $\Phi$.

Inputs: Finite abstraction $\bar\Sigma=(\Xb,\Ub,T_F)$, and specification $\Phi=\lnot\avoid\,\mathcal{U}\,\goal$.

Outputs: Corrected neural representations $R_F$ and $R_B$,
winning domain $L$ and  a feedback controller $C$ for $\bar\Sigma$ such that $C\parallel\bar\Sigma$ realizes $\Phi$.

Inputs: Control systems $\Sigma^i=(X^i,x_\init^i,U^i,W^i,f^i)$, $i\in [1;N]$, and the global specification $\Phi=\lnot\avoid\,\mathcal{U}\,\goal$.

Parameters: A robustness margin $\varepsilon\in \reals^n_{>0}$.

Output: Local feedback controllers $\set{C^i}$ for $\set{\Sigma^i}$, $i\in [1;N]$, such that $\set{C^i}\parallel \set{\Sigma^i}$ realizes $\Phi$.

It is important to notice that any solution for this problem is required to provide a formal guarantee on the satisfaction of $\Phi$,
i.e., the reach-avoid specification $\Phi$ must be satisfied under any disturbance affecting the control systems.

Let $C\in \Xb\times \Ub$ be the computed controller for the abstraction $\bar\Sigma$ such that $C\parallel\bar\Sigma$ realizes a given specification $\Phi$. The size of this controller can be large due to the large number of discrete state and inputs. For deployment purposes, we would like to compute a corrected neural controller $\hat C\coloneqq \Xb\rightarrow\Ub$ s.t. $\hat C\parallel \bar\Sigma$ realizes $\Phi$.

Inputs: Controller $C$ computed for the discrete control system $\bar\Sigma$, and specification $\Phi$ s.t. $C\parallel\bar\Sigma$ realizes $\Phi$.

Outputs: A corrected neural controller $\hat C$
such that $\hat C\parallel\bar\Sigma$ realizes $\Phi$.

§ SYNTHESIS

One approach to formally synthesize controllers for a given specification is to store the transition system corresponding to quantization of the state and input spaces, and to use the methods from reactive synthesis to design a controller. However, the memory required to store these transition systems increases exponentially with the number of state variables, which causes a memory blow-up for many real-world systems.
In this section, we propose our memory-efficient algorithm for synthesizing controllers to satisfy reach-avoid specifications for finite abstractions and reach-avoid specifications. Our method requires computation of corrected neural representations for the finite abstraction. Computation of these representations is discussed in Sec. <ref>. Later, in Sec. <ref>, we show how our synthesis method makes use of the computed representations.

§.§ Corrected Neural Representations for Finite Abstractions

Let $\bar\Sigma=(\Xb,\Ub,T_F)$ be a finite abstraction. In this section, we show that

$T_F$ can be approximated by some generator functions. In particular, we show how to compute generator functions $R_F\colon \Xb\times\Ub\rightarrow\reals^n\times\reals^n_{\geq 0}$ and $R_B\colon\Xb\times\Ub\rightarrow\reals^n\times\reals^n_{\geq 0}$ which can produce characterization of an $\ell_\infty$ ball corresponding to the over-approximation of forward- and backward-in-time reachable sets, respectively, for every state-input pair picked from $\Xb\times\Ub$.

§.§ Continuous control systems

If the vector field $f_c$ corresponding to the nominal dynamics of the continuous system $\Sigma_c$ is given, we can easily get the desired compact representation. Since the ultimate goal is to solve a given reach-avoid problem, we have to discretize the state and input space so that we can use the methods from reactive synthesis. However, for continuous systems, our method would not require computation and storing of the complete transition system. Having the set of discrete state-input pairs, we can apply the nominal dynamics $f(\xbb, \ubb)$ and a properly selected growth bound function $\beta(\xbb,\ubb)$ to compute the center and radius of the disc over-approximating the reachable set for every pair $\xbb, \ubb\in \Xb\times \Ub$. Note that depending on the selected over-approximation method, the growth-bound function may or may not be a function of both state and input. For example, the method introduced in <cit.> suggests using a growth-bound function which is only a function of control inputs for fixed state discretization parameter $\etab_x$. The nominal (discrete-time) dynamics would be $f(\xbb,\ubb)=\xbb+\int_{0}^{\tau}f_c(\xb(h),\ubb)dh$ and $\beta(\bar x,\bar u)$ can take the form introduced in <cit.>. So, for continuous control systems, we have

\begin{equation}\label{eq:FW_model_RF}
R_F(\xbb,\ubb)=((f(\xbb, \ubb), \beta(\xbb,\ubb)).
\end{equation}

Similarly, for the backward dynamics we have:

\begin{equation}\label{eq:BW_model_RB}
R_B(\xbb,\ubb)=(-f(\xbb, \ubb), \beta^-(\xbb,\ubb)),
\end{equation}

where $\beta^-(\cdot,\cdot)$ corresponds to the growth-bound for the backward dynamics.

§.§ Discrete control systems

Regression-based compression algorithm for finite abstractions

$f(\cdot,\cdot)$, $X$, $U$, $N_p$, $\boldsymbol \epsilon$ $\etab_x$, $\etab_u$, $\beta(\cdot, \cdot)$, $\lambda$
Use ALTRO to compute a nominal trajectory $\rho\colon[0;N_p]\rightarrow X$ s.t. $\rho(0)=\xb_\init$ and $\rho(N_p)\approx \xb_f$

Discretize $X$ and $U$ using $\etab_x$ and $\etab_u$ to get $\Xb$ and $\Ub$

$\Xro\leftarrow\Xro\cup\llbracket \rho(t)-\epsilon,\rho(t)+\epsilon\rrbracket$

$\Xrob\leftarrow\Xrob\cup(\Xb\cap K(\llbracket \rho(t)-\epsilon,\rho(t)+\epsilon\rrbracket))$

Forward dynamics $\bar\Sigma$ and learning rate $\lambda$
Compute backward dynamics $\bar\Sigma_B$ and the datasets $\ds_F$ and $\ds_B$ using Eqs. (<ref>), (<ref>), and (<ref>)

Train neural networks $\NN_F$ on the dataset $\ds_F$ and train $\NN_B$ on $\ds_B$ using the learning rate $\lambda$

Compute the soundness errors $\eFb$ and $\eBb$ using Eq. (<ref>)

Compute the final corrected representations $R_F$ and $R_B$ using Eqs. (<ref>) and (<ref>)

corrected neural representations $R_F$ and $R_B$

Our aim is  to use the expressive power of neural networks to represent the behavior of $\bar \Sigma$ such that the memory requirements significantly decrease.

Comparing the set of successor states in the transition system $T_F$ and its representation $T_F^N$. We have
$\boldsymbol c=c_F(\xbb,\ubb)$,
$r_F(\xbb,\ubb) = [\boldsymbol r(1),\boldsymbol r(2)]^\top$,
$\boldsymbol c'=\NN_F^c(\xbb,\ubb)$
$\NN_F^r(\xbb,\ubb) = [\boldsymbol r'(1),\boldsymbol r'(2)]^\top$.

Our compression scheme is summarized in Alg. <ref>. We first compute the backward-in-time system $\bar\Sigma_B$ using Eq. (<ref>).
We then calculate the over-approximating $\ell_\infty$ ball for every state-input pair. Let $c_F(\xbb,\ubb)\in X$ and $r_F(\xbb,\ubb)\in\reals_{\geq 0}^n$ characterize the tightest $\ell_\infty$ ball such that

$$(\xbb,\ubb,\xbb')\in T_F\Leftrightarrow \|\xbb'-c_F(\xbb,\ubb)\|_{\infty}\leq r_F(\xbb,\ubb)-\etab_x/2.$$

This is illustrated in Fig. <ref> in two-dimensional space for a given state-input pair $(\xbb,\ubb)$. The dotted red rectangle corresponds to the hyper-rectangular reachable set.

The center $c_F(\xbb,\ubb)$ and radius $r_F(\xbb,\ubb)$ are computed using the lower-left and upper-right corners of the reachable set denoted, respectively, by $g_{FL}(\xbb,\ubb)$ and $g_{FU}(\xbb,\ubb)$. Then, we have
$c_F(\xbb,\ubb)=(g_{FU}(\xbb,\ubb)+g_{FL}(\xbb,\ubb))/2$ and $r_F(\xbb,\ubb)=(g_{FU}(\xbb,\ubb)-g_{FL}(\xbb,\ubb))/2+\etab_x/2$.

At the end of the first step we have computed and stored the dataset

\begin{equation}\label{eq:FW_ds}
\ds_F=\set{((\xbb, \ubb), (c_F(\xbb, \ubb), r_F(\xbb,\ubb)))\mid \xbb\in \Xb, \ubb\in \Ub}.
\end{equation}

Note that every data-point in $\ds_F$ consists of two pairs: one specifies a state-input pair $(\xbb,\ubb)$ and the other one characterizes the center and radius corresponding to the over-approximating $\ell_\infty$ disc $(c_F(\xbb, \ubb), r_F(\xbb,\ubb))$. Similarly, we need to store another dataset corresponding to the backward dynamics. First, we define $c_B(\xbb,\ubb)\in X$ and $r_B(\xbb,\ubb)\in\reals_{\geq 0}^n$ characterizing the tightest $\ell_\infty$ ball such that

$$(\xbb,\ubb,\xbb')\in T_B\Leftrightarrow \|\xbb'-c_B(\xbb,\ubb)\|_{\infty}\leq r_B(\xbb,\ubb)-\eta_x/2.$$

The dataset corresponding to the backward dynamics is of the following form

\begin{equation}\label{eq:BW_ds}
\ds_B=\set{((\xbb, \ubb), (c_B(\xbb, \ubb), r_B(\xbb,\ubb)))\mid \xbb\in \Xb, \ubb\in \Ub}.
\end{equation}

The regression-based configuration used in compression of abstractions. The input to the neural network includes state-input pair $(\xbb,\ubb)$, and the output includes the pair $(c,r)$ corresponding to the center and radius of the rectangular reachable set, respectively.
Right: The classification-based representation of finite abstractions. The representation receives a state-input pair $(\xbb,\ubb)$. In the output, $\boldsymbol y_{lb}$ and $\boldsymbol y_{ub}$ correspond to the lower-left and upper-right corners for the rectangular reachable set.

The configuration used in compression of abstractions. The input to the neural network includes state-input pair $(\xbb,\ubb)$, and the output includes the pair $(c,r)$ corresponding to the center and radius of the rectangular reachable set, respectively.

The size of $\ds_F$ and $\ds_B$ grows exponentially with the dimension of state space. Hence, we store both the datasets $\ds_F$ and $\ds_B$ (potentially) into the hard drive. Next, we take the datasets $\ds_F$ and $\ds_B$, for which we train neural networks $\NN_F$ and $\NN_B$, taking the state-input pairs $(\xbb,\ubb)$ as input and $(c_F(\xbb,\ubb),r_F(\xbb,\ubb))$
as output, and try to find an input-output mapping minimizing
mean squared error (MSE). For systems with state and input spaces of dimensions $n$ and $m$, the input and output layers of both neural networks are of sizes $n+m$ and $2n$, respectively. The configuration of the neural networks which we used is illustrated in Fig. <ref>. During training, we load batches of data from $\ds_F$ and $\ds_B$, which are stored on the the hard drive, into the RAM. We use the stochastic gradient descent (SGD) method to minimize MSE.

As mentioned earlier, in contrast to the usual applications wherein neural networks are used to represent an unknown distribution, we have the full dataset and require computing representations which are sound with respect to the input dataset.

A sound representation for the given finite abstractions produces reachable sets that include $T_F(\xbb,\ubb)$ for every state-input pair $(\xbb,\ubb)$. For instance, the solid green rectangle in Fig. <ref> contains the set of reachable states corresponding to $\NN_F(\xbb,\ubb)$ and contains the set of states included in the dotted red rectangle, i.e.,  $T_F(\xbb,\ubb)$. Therefore, we can say that the representation $\NN_F$ is sound for the pair $(\xbb,\ubb)$.

In order to guarantee soundness, we need to compute the maximum error induced during the training process among all the training data points. To that end, we go over all the state-input pairs (which are stored on the hard drive) and compute the maximum error in approximating the centers of the $\ell_\infty$ balls, denoted by $\eFb^c, \eBb^c$ and radius $\eFb^r, \eBb^r$ corresponding to the forward and backward representations:

\begin{align*}\label{eq:FW_soundness_err_center}
\eFb^c&=\max_{\xbb\in\Xb,\ubb\in\Ub}|c_F(\xbb,\ubb)-\NN_F^c(\xbb,\ubb)|,\quad \eFb^r=\max_{\xbb\in\Xb,\ubb\in\Ub}|r_F(\xbb,\ubb)-\NN_F^r(\xbb,\ubb)|.
\end{align*}

Similarly, for the backward dynamics,

\begin{align*}
\eBb^c&=\max_{\xbb\in\Xb,\ubb\in\Ub}|c_B(\xbb,\ubb)-\NN_B^c(\xbb,\ubb)|,\quad \eBb^r=\max_{\xbb\in\Xb,\ubb\in\Ub}|r_B(\xbb,\ubb)-\NN_B^r(\xbb,\ubb)|.
\end{align*}

We define

\begin{equation}\label{eq:FW_soundness_err}
\eFb=\eFb^c+\eFb^r,\quad \eBb=\eBb^c+\eBb^r,
\end{equation}

and use the errors $\eFb$ and $\eBb$ to compute the corrected representations $R_F$ and $R_B$, corresponding to $\NN_F$ and $\NN_B$, as described next. Let $R_F^c$ and $R_F^r$ correspond to the center and radius components of $R_F$. Similarly, $R_B^c$ and $R_B^r$ correspond to the center and radius components of $R_B$. For state-input pair $(\xbb,\ubb)\in\Xb\times \Ub$, we define

\begin{align}\label{eq:R_F}
R_F^c(\xbb,\ubb)&=\NN_F^c(\xbb,\ubb),\quad R_F^r(\xbb,\ubb)=\NN_F^r(\xbb,\ubb)+\eFb,
\end{align}

for the forward dynamics, and

\begin{align}\label{eq:R_B}
R_B^c(\xbb,\ubb)&=\NN_B^c(\xbb,\ubb),\quad R_B^r(\xbb,\ubb)=\NN_B^r(\xbb,\ubb)+\eBb,
\end{align}

for the backward dynamics.

Let us define the forward transition system computed using the trained neural network as follows

\begin{align}\label{eq:TS_NN_F}
T_F^N = &\{(\xbb,\ubb, \xbb')\!\in\!\Xb\!\times\! \Ub\!\times\! \Xb\!\mid\!\xbb'\!\in\! \bar K(\NN_F^c(\xbb, \ubb)\!-\!\NN_F^r(\xb, \ubb)\!-\!\eFb,\NN_F^c(\xbb, \ubb)\!+\!\NN_F^r(\xbb, \ubb)\!+\!\eFb)\},
\end{align}

where $\NN_F^c(\cdot, \cdot)$, $\NN_F^r(\cdot, \cdot)$ denote the components of the output of $\NN_F(\cdot, \cdot)$ corresponding to the center and radius of disc, respectively. Similarly, we can define the transition system $T_B^N$ corresponding to the backward dynamics as follows

\begin{align}\label{eq:TS_NN_B}
T_B^N = &\{(\xbb,\ubb, \xbb')\!\in\!\Xb\!\times\! \Ub\!\times\! \Xb\!\mid\!\xbb'\!\in\! \bar K(\NN_B^c(\xbb, \ubb)\!-\!\NN_B^r(\xbb, \ubb)\!-\!\eBb,\NN_B^c(\xbb, \ubb)\!+\!\NN_B^r(\xbb, \ubb)\!+\!\eBb)\}.
\end{align}

The following lemma states that we can use the trained neural networks to compute sound transition systems for both forward and backward dynamics. However, our synthesis approach does not require the computation of $T_F^N$ and $T_B^N$ and only uses the compressed representations $\NN_F$ and $\NN_B$.

Transition systems $T_F^N$ and $T_B^N$ computed by (<ref>) and (<ref>) are sound for $T_F$ and $T_B$, i.e., we have $T_F\subseteq T_F^N$ and $T_B\subseteq T_B^N$.

By definition, we have that $\llbracket-\boldsymbol r+f(\xbb,\ubb), \boldsymbol r+f(\xbb,\ubb)\rrbracket\subseteq \llbracket\NN_B^c(\xbb, \ubb)-\NN_B^r(\xbb \ubb)-\eBb,\NN_B^c(\xbb, \ubb)+\NN_B^r(\xbb, \ubb)+\eBb\rrbracket$. This gives $T\subseteq T_N$.

To reduce the level of conservativeness, we require that $T_F^N$ and $T_B^N$ do not contain too many additional edges compared to $T_F$ and $T_B$. The mismatch rate of the forward and backward dynamics are defined as

\begin{equation*}\label{eq:mismatch_rate_FW_BW}
d_F\coloneq \frac{|T_F^N\setminus T_F|}{|T_F|}, \quad d_B\coloneq \frac{|T_B^N\setminus T_B|}{|T_B|}.
\end{equation*}

If the trained representations are accurate, the mismatch rate is low, which results in a less restrictive representation.

The method proposed in this section formulates the computation of the representations as a regression problem, wherein the representative neural networks are supposed to predict the center and radius corresponding to $\ell_\infty$ reachable sets.
In Sec. <ref>, we describe a classification-based formulation for compressing finite abstractions, wherein the representative neural networks are supposed to predict the vectorized indices corresponding to the lower-left and upper-right corners of the reachable set. We experimentally show that this second formulation, while being more memory demanding, provides a less conservative representation compared to the formulation discussed in this section.

Having the trained neural networks representing the forward and backward dynamics, and computed the networks' corresponding soundness errors we finish the compression procedure.

Illustration for the configuration used for the classification-based representations of the abstraction. The neural network takes a state $\xbb$ and a control input $\ubb$ and computes the coordinates of the lower-left and upper-right corner points characterizing the corresponding reachable set $\llbracket\boldsymbol x_{lb}, \boldsymbol x_{ub}\rrbracket$.

The classification-based representation of finite abstractions. The representation receives a state-input pair $(\xbb,\ubb)$. In the output, $\boldsymbol y_{lb}$ and $\boldsymbol y_{ub}$ correspond to the lower-left and upper-right corners for the rectangular reachable set.

§.§ Classification-Based Computation of Representations for Finite Abstractions

We proposed in Sec. <ref> a formulation for training neural networks that can guess at any given state-input pair the center and radius of a hyper-rectangular over-approximation of the reachable states. This guess is then corrected using the computed soundness errors. A nice aspect of this formulation is that we only need to store the trained representations and their corresponding soundness errors. However, the result of using the soundness errors to correct the output values produced by the neural networks may give a very conservative over-approximation of the reachable sets, even when the trained representations have a very good performance on a large subset of the state-input pairs, since the soundness errors must be computed over all state-input pairs.

Computing classification-based representations of finite abstractions

Forward dynamics $\bar\Sigma$ and learning rate $\lambda$
Compute backward dynamics $\bar\Sigma_B$ and the datasets $\ds_F$ and $\ds_B$ using Eqs. (<ref>), (<ref>), and (<ref>)

Train neural networks $\NN_F$ and $\NN_B$ on the datasets $\ds_F$ and $\ds_B$ using the learning rate $\lambda$

Compute the set of misclassified state-input pairs $E_F$ and $E_B$ as in Eq. (<ref>)

Compute the set of transitions $\tilde{\NN}_F$ and $\tilde{\NN}_B$ associated with $E_F$ and $E_B$ as in  Eq. (<ref>)

Compute the corrected neural representations $R_F$, $R_B$ using Eqs. (<ref>), (<ref>)

$R_F$, $R_B$

In this section, we provide an alternative formulation for computing a compressed representation of a given abstraction. Intuitively, our idea is to train neural network representations which can guess for any given state-input pair the vectorized indices corresponding to the lower-left and upper-right corner points of the hyper-rectangular reachable set. The architecture of the representation is shown in Fig. <ref>. As illustrated, for every state-input pair $(\xbb,\ubb)\in \Xb\times \Ub$, the output of the representation gives
the lower-left and upper-right corners of the rectangular set that is reachable by taking the control input $\ubb$ at the state $\xbb$.

Illustration of the classification-based representation of finite abstractions.
The representation receives a state-input pair $(\xbb,\ubb)$. In the output, $\boldsymbol y_{lb}$ and $\boldsymbol y_{ub}$ correspond to the lower-left and upper-right corners for the rectangular reachable set.

Alg. <ref> describes our classifier-based compression scheme for finite abstractions.

We first compute the backward system $\bar\Sigma_B$ using Eq. (<ref>). We then compute the training datasets for both the forward and backward systems $\bar\Sigma$ and $\bar\Sigma_B$. For
$\bar\Sigma$, let $g_{FU}\colon\Xb\times\Ub\rightarrow \Xb$ and $g_{FL}\colon\Xb\times\Ub\rightarrow \Xb$ denote the mappings from the state-input pair $(\xbb,\ubb)\in\Xb\times\Ub$ into the corresponding upper-right and lower-left corners of the rectangular reachable set from $(\xbb,\ubb)$. We define
$z_F\colon \Xb\times \Ub\rightarrow\{0,1\}^{2\sum_{i=1}^n|\Xb(i)|}$ with $|\Xb(i)|$ being the cardinality of the projection of $\Xb$ along the $i^{\text{th}}$ axis and $z_F(\xbb,\ubb)(l)=1$ if and only if

\begin{align*}
& l=2\sum_{k=1}^{i-1}|\Xb(k)|+\Ixi(g_{FL}(\xbb,\ubb)(i)) \text{ or } l=2\sum_{k=1}^{i-1}|\Xb(k)|+|\Xb(i)|+\Ixi(g_{FU}(\xbb,\ubb)(i)),
\end{align*}

for some $i\in\{1,2,\ldots,n\}$. The indexing function $\Ixi\colon \Xb(i)\rightarrow [1;|\Xb(i)|]$ maps every element of $\Xb(i)$ into a unique integer index in the interval $[1;|\Xb(i)|]$.

The training dataset for $\bar\Sigma$ is defined as

\begin{equation}
\label{eq:FW_ds_cls}
\ds_F\coloneq
\{(\xbb,\ubb, z_F(\xbb,\ubb)) \,|\, \xbb\in\Xb \text{ and }\ubb\in \Ub\}.
\end{equation}

Intuitively, each element of the dataset $\ds_F$ contains a state-input pair $(\xbb,\ubb)$ and a vector $\boldsymbol h\in \{0,1\}^{2\sum_{i=1}^n|\Xb(i)|}$ that has $1$ only at the entries corresponding to $\Ixi(g_{FL}(\xbb,\ubb)(i))$ and $\Ixi(g_{FU}(\xbb,\ubb)(i))$ for $i\in\{1,2,\ldots,n\}$.

Similarly, we define
$z_B\colon \Xb\times \Ub\rightarrow\{0,1\}^{2\sum_{i=1}^n|\Xb(i)|}$ for $\bar\Sigma_B$ such that $z_B(\xbb,\ubb)(l)=1$ if and only if

\begin{align*}
& l=2\sum_{k=1}^{i-1}|\Xb(k)|+\Ixi(g_{BL}(\xbb,\ubb)(i))\text{ or } l=2\sum_{k=1}^{i-1}|\Xb(k)|+|\Xb(i)|+\Ixi(g_{BU}(\xbb,\ubb)(i)),
\end{align*}

for some $i\in\{1,2,\ldots,n\}$.
The training dataset for the backward dynamics is also defined similarly as

\begin{equation}
\label{eq:BW_ds_cls}
\ds_B\coloneq
\{(\xbb,\ubb, z_B(\xbb,\ubb)) \,|\, \xbb\in\Xb \text{ and }\ubb\in \Ub\}.
\end{equation}

Once the training datasets are ready, we train the neural networks $\NN_F$ and $\NN_B$  respectively on the datasets $\ds_F$ and $\ds_B$. Note that the output layer of $\NN_F$ and $\NN_B$ will be a vector of size $2\sum_{i=1}^n|\Xb(i)|$, while the final output of the representations are of size $2n$ (cf. Fig. <ref>). These final outputs give an approximation of the coordinates of the lower-left and upper-right corners of the reachable set corresponding to the pair $(\xbb,\ubb)$.

Note that, because $\Xb$ was computed by equally partitioning over $X$, both the indexing function $\Ixi$ and its inverse can be implemented in a memory-efficient way using  and  operators.
We then evaluate the performance of the trained neural networks $\NN_F$ and $\NN_B$.

Let $\rho_{FL}(\xbb,\ubb)$ and $\rho_{FU}(\xbb,\ubb)$ denote respectively the estimated lower-left and upper-right corners of the reachable set estimated by $\NN_F$. Define $\rho_{BL}(\xbb,\ubb)$ and $\rho_{BU}(\xbb,\ubb)$ similarly for $\NN_B$, and let the set of misclassified state-input pairs be

\begin{align}
E_F&\coloneq \{(\xbb,\ubb)\in\Xb\times\Ub\mid\ T_F(\xbb,\ubb)\setminus \llbracket \rho_{FL}(\xbb,\ubb), \rho_{FU}(\xbb,\ubb)\rrbracket_{\eta_x}\neq \emptyset\}\nonumber\\
E_B&\coloneq\{(\xbb,\ubb)\in\Xb\times\Ub\mid\ T_B(\xbb,\ubb)\setminus \llbracket \rho_{BL}(\xbb,\ubb), \rho_{BU}(\xbb,\ubb)\rrbracket_{\eta_x}\neq \emptyset\}.\label{eq:miss}
\end{align}

The soundness error of $\NN_F$ and $\NN_B$ can be considered as their misclassification rate:

\begin{equation}\label{eq:cls_soundness_errors}
err_F\coloneq\frac{|E_F|}{|\Xb\times\Ub|} \quad\text{ and }\quad err_B\coloneq\frac{|E_B|}{|\Xb\times\Ub|}.
\end{equation}

For the misclassified
pairs in $E_F$ and $E_B$, we extract the related transitions in the abstraction:

\begin{align}\label{eq:TS_to_be_stored}
\tilde{\NN}_F & \!\coloneq\!\set{(\xbb,\ubb,\xbb')\!\mid\! (\xbb,\ubb)\!\in\! E_F,\xbb'\!\in\! T_F(\xbb,\ubb)},
\tilde{\NN}_B  \!\coloneq\!\set{(\xbb,\ubb,\xbb')\!\mid\! (\xbb,\ubb)\in E_B,\xbb'\!\in\! T_B(\xbb,\ubb)}\!.\!
\end{align}

Finally, we correct the output of neural network representations to maintain soundness

\begin{align}
\label{eq:R_F_def_cls}
\begin{cases}
\llbracket\rho_{FL}(\xbb,\ubb),\rho_{FU}(\xbb,\ubb)\rrbracket_{\eta_x}\!\!\!\! &\text{if}\; (\xbb,\ubb)\!\notin\! E_F\\
\tilde{\NN}_F(\xbb,\ubb)  &\text{if}\;(\xbb,\ubb)\!\in\! E_F,
\end{cases}\\
\label{eq:R_B_def_cls}
\begin{cases}
\llbracket\rho_{BL}(\xbb,\ubb),\rho_{BU}(\xbb,\ubb)\rrbracket_{\eta_x} \!\!\!\! &\text{if}\; (\xbb,\ubb)\!\notin\! E_B\\
\tilde{\NN}_B(\xbb,\ubb) &\text{if}\;(\xbb,\ubb)\!\in\! E_B.
\end{cases}
\end{align}

Note that these corrected neural representations are memory efficient only if the misclassification rates are small, i.e., the size of $E_F$ and $E_B$ are small compared with $\Xb\times\Ub$.

The following lemma states that, similar to the regression-based formulation, using the classification-based formulation, we can train sound representations for both forward and backward dynamics.

Let $T_F^N$ and $T_B^N$ be the transition systems computed by (<ref>) and (<ref>). Then, we have $T_F\subseteq T_F^N$ and $T_B\subseteq T_B^N$.

§.§ On-the-Fly Synthesis

Controller synthesis algorithm

Set $W_0\subseteq \Xb$ and the corrected neural representations $R_F$ and $R_B$
Initialize $C\leftarrow \emptyset$,  $P_0\leftarrow W_0$, $\Gamma_0\leftarrow \emptyset$ and $i\leftarrow 0$

$W_i\neq \emptyset$
Compute the candidate pool $S_{i}$ using Eq. (<ref>)

Compute the set of new winning states $W_{i+1}$ using Eq. (<ref>) and add them to the winning set ($P_{i+1}\leftarrow P_i\cup W_{i+1}$)

Compute the set of new state-input pairs $\Gamma_{i+1}$ using Eq. (<ref>) and add them to the controller ($C\leftarrow C\cup \Gamma_{i+1}$)

$i\leftarrow i+1$
$L\leftarrow P_{i}$

Controller $C$ and its winning set $L$

In the previous subsection, we described the computation of the compressed representations corresponding to the forward and backward dynamics for finite abstractions.
In this subsection, we use these representations in order to synthesize formally correct controllers.

Our synthesis procedure is provided in Alg. <ref>. It takes the representations $R_F$ and $R_B$ to synthesize a controller which fulfills the given reach-avoid specification.

$$W_0=\set{\xbb\in\Xb\mid \llbracket\xbb-\boldsymbol{\eta_x}/2, \xbb+\boldsymbol{\eta_x}/2\rrbracket\subseteq \goal}$$

be a discrete under-approximation of the target set $\goal$. We take $W_0$ as the input and perform a fixed-point computation to solve the given reach-avoid game. We initialize the winning set and controller with $P_0=W_0$ and $C=\emptyset$, and in each iteration, we add the new winning set of states and state-input pairs, respectively, into the overall winning set and the controller, until no new state is found ($W_{i+1}=\emptyset$).

Let $W_i$ be the set of new winning states in the beginning of the $i^{th}$ iteration. Further, we denote the set of winning states in the beginning of the $i^{th}$ iteration by $P_i=\bigcup_{k=0}^i W_k$. In every iteration, for every $\xbb\in W_i$ and $\ubb\in \Ub$, we compute the backward over-approximating $\ell_\infty$ ball and discretize it to get the candidate pool $S_{i}$ defined as

\begin{equation}\label{eq:candid_pool}
S_i\coloneq \bigcup_{\ubb\in \Ub} Y_i(\ubb),
\end{equation}

\begin{align*}
&Y_{i}(\ubb)\coloneq\bigcup_{\xbb\in W_i}(\Xb\cap
\bar K(R_B^c(\xbb, \ubb)-R_B^r(\xbb, \ubb),R_B^c(\xbb, \ubb)+R_B^r(\xbb, \ubb))),
\end{align*}

where $R_B^c(\cdot, \cdot)$, $R_B^r(\cdot, \cdot)$ denote the components of the output of $R_B(\cdot, \cdot)$ corresponding to the center and radius of the $\ell_\infty$ ball, respectively.
Note that we compute the candidate pool by running $R_B$ over $W_i$ instead of $P_i$. This is computationally beneficial, because $|W_i|\leq |P_i|$. Next lemma shows that $S_i$ includes the whole set of new winning states $W_{i+1}$.

Let the set of candidates $S_{i}$ be as defined in Eq. (<ref>). Then, we have $W_{i+1}\subseteq S_{i}$ for all $i\geq 0$.

We prove this lemma by contradiction. Suppose that $W_{i+1}\not\subseteq S_i$. Then there exists at least one $\xbb^\ast\in W_{i+1}\setminus S_i$. Since $\xbb^\ast\in W_{i+1}$, we know that there exists at least one $\ubb^\ast\in\Ub$ such that $T_f(\xbb^\ast,\ubb^\ast)\subseteq P_i$ and $\xbb^\ast\notin P_i$. Moreover, since $\xbb^\ast\notin S_i$, by Eq. (<ref>) we get $T_f(\xbb^\ast,\ubb^\ast)\cap W_i=\emptyset$.
So, $T_f(\xbb^\ast,\ubb^\ast)\subseteq P_i\setminus W_i=P_{i-1}$. This gives $\xbb^\ast\in P_i$, which is a contradiction. This completes the proof.

Now, we can use $R_F$, which represents the forward transition system, in order to choose the legitimate candidates out of $S_{i}$ and add the new ones to $W_{i+1}$.

$$A=\set{\xbb\in\Xb\mid \llbracket\xbb-\boldsymbol{\eta_x}/2, \xbb+\boldsymbol{\eta_x}/2\rrbracket\cap \avoid\neq \emptyset}$$

be a discrete over-approximation over the set of obstacles.
The next lemma states that we can use the representation $R_F$ to compute $W_{i+1}$.

The set of states added to the winning set in the $i^{th}$ step can be computed as
\begin{align}\label{eq:NN_post}
&W_{i+1} =\{\xbb\in S_{i}\mid \exists \ubb\in\Ub\; s.t.\bar K(R_F^c(\xbb, \ubb)-R_F^r(\xbb, \ubb),R_F^c(\xbb, \ubb)+R_F^r(\xbb, \ubb))\subseteq P_i
\}\setminus (P_i\cup A).
\end{align}

To prove the first part, notice that for any state $\xbb\notin S_{i+1}$ we know $\Post(\xbb)\cap W_i=\emptyset$ and hence $\xbb\notin \Pre(W_i)$, because $S_{i+1}$ is a superset of the set of states which are reachable from $W_i$ under the backward-in-time dynamics. Therefore, $\xbb\in W_{i+1}\setminus S_{i+1}$ implies that $\Post(\xbb)\subseteq (L\setminus W_i)$, and $\xbb\notin L\cup\avoid$. For $i=0$, we have $L\setminus W_i=\emptyset$ and for $i>0$, one can notice that $\Post(\xbb)\subseteq (L\setminus W_i)$ implies that $\xbb\in L$ (contradiction for every $i\geq 0$). This completes the proof of the first part.

To prove this lemma, we denote $G=\{\xbb\in S_{i}\mid \exists \ubb\in\Ub\; s.t.\;\bar K(R_F^c(\xbb, \ubb)-R_F^r(\xbb, \ubb),R_F^c(\xbb, \ubb)+R_F^r(\xbb, \ubb))\subseteq P_i
\}\setminus (P_i\cup A)$, and show $W_{i+1}\subseteq G$ and $G\subseteq W_{i+1}$. The second direction ($G\subseteq W_{i+1}$) holds by definition. To prove the first direction ($W_{i+1}\subseteq G$), we note that $G\subseteq  S_{i}$ and further, by the result of Lemma. <ref>, we have $W_{i+1}\subseteq S_{i}$. Assume $W_{i+1}\not\subseteq G$. Then there should exist at least one $\xbb^\ast\in W_{i+1}\setminus G$. Note that $\xbb^\ast\in S_{i}\setminus G$. Since $\xbb^\ast\in S_i$, we get that there exists at least one $\ubb^\ast\in\Ub$ for which $T_F(\xbb^\ast,\ubb^\ast)\subseteq W_i$. Also, because $\xbb^\ast\notin G$, we have $T_F(\xbb^\ast,\ubb^\ast)\not\subseteq W_i$, which is a contradiction. Therefore, $W_{i+1}\subseteq G$. Hence the proof ends.

In each iteration, we calculate $\Gamma_i$, which is the set of new state-input pairs that must be added into the controller, and is defined as

\begin{align}\label{eq:controller_added_pairs}
\Gamma_{i+1}=&\{(\xbb,\ubb)\mid
\xbb\in W_{i+1},\;\bar{K}(R_F^c(\xbb, \ubb)-R_F^r(\xbb, \ubb),R_F^c(\xbb, \ubb)+R_F^r(\xbb, \ubb))\subseteq P_i	\}.
\end{align}

Finally, If $W_{i+1}=\emptyset$, we can terminate the computations as we already have computed the winning set and the controller. Otherwise, we add $W_i$ and $\Gamma_i$ into the overall winning set ($P_{i+1}\leftarrow P_i\cup W_{i+1} $) and controller ($C\leftarrow C\cup \Gamma_{i+1} $)  and restart the depicted process.

§.§ Accelerating synthesis for continuous control systems

It should pointed out that although our proposed synthesis method does not require storing huge transition systems into the memory, it adds to the runtime. Specifically, in each iteration of fixed point computation, $\mathcal O(|W_i\setminus L|^2\times |\Uh|)$ operations are required. For continuous control systems, we can use open-loop planning to reduce the on-the-fly computations in each iteration and hence speed-up the synthesis process. Given an initial state $x_\init\in X$ and a goal state $x_f\in X$, one can use standard techniques to compute a nominal trajectory $\rho:[0;N]\rightarrow X$ of length $N$ such that $\rho[0]=x_\init$ and $\rho[N]\approx x_f$. This computation is reffered to as open-loop planning and only takes the nominal dynamics ($\dot x(t)=f_c(x(t),u(t))$) into account. To generate nominal trajectories, we use the method introduced in <cit.> which introduces a fast and scalable tool named ALTRO (see Appendix <ref>).
Having the nominal trajectory $\rho$ computed, we can modify the state space such that it is only limited to the $\epsilon-$tube around the nominal trajectory.

§ DEPLOYMENT

Once the controller $C$ is computed such that $C\parallel \bar\Sigma$ realizes the given specification $\Phi$, we need to deploy $C$ onto an embedded controller platform, e.g., a microcontroller. Since such embedded controller platforms generally have
a small on-board memory, we would like to minimize the size of the stored controller.

We define the set of valid control inputs corresponding to $\xbb$ as $C(\xbb)=\set{\ubb\mid(\xbb,\ubb)\in C}$. The approach we proposed for finding representations for the finite abstractions may not work, since
we are not allowed to over-approximate $C(\xbb)$, and thus the set of valid control inputs is not representable as a compact $\ell_\infty$ ball described by its center and radius.

The following example illustrates a disconnected $C(\xbb)$, which cannot be represented by an $\ell_\infty$ ball.

Left: Illustration of a disconnected set of valid control inputs. Right: The configuration used in compression of controllers. Given a state $\xbb$, the representation produces a corresponding control input $\ubb$.

Illustration of a disconnected set of valid control inputs.

Illustration of a disconnected set of valid control inputs

The configuration used in compression of controllers. Given a state $\xbb$, the representation produces a corresponding control input $\ubb$.

Consider a vehicle which can only move along the $\boldsymbol x$ axis as shown in Fig. <ref>. Let the set of speeds for this vehicle be $\Ub=\set{\pm i\mid i\in \nats^{\leq 3}}$, where each $i\in \Ub$ determines the distance the vehicle jumps in the right and left directions in every time-point, corresponding to the positive and negative values, respectively. Starting from the white middle box, in order to not hitting the red colored obstacle states, the set of valid control inputs would be $\Ub\setminus\set{0,\;\pm1}$, which is a disjoint set and cannot be characterized by, for instance, a single $\ell_\infty$ ball.

Consider a system with one-dimensional state and input spaces ($n=m=1$). Fig. <ref> illustrates the set of transitions starting from the white middle box ($\xbb=0$). Let the boxes with green check mark and red cross mark correspond to the target and obstacle states and $C$ be the controller for the corresponding reach-avoid specification. Then, we have $\set{(0,2),(0,3),(0,-2),(0,-3)}\subseteq C$ and $C(0)=\set{-2,-3,2,3}$. It is clear that $C(0)$ is a disconnected set, which is not characterizable by an $\ell_\infty$ ball.

The configuration used in compression of controllers. Given a state $\xbb$, the representation produces a corresponding control input $\ubb$.

In contrast to the symbolic regression method proposed in <cit.>, we formulate the controller compression problem as a classification task, that is, we train a neural network which assigns every state to a list of scores over the set of control inputs, and picks the control input with the highest score. The configuration of the neural network is illustrated in Fig. <ref>. The justification for our formulation is that any representation for the controller can only perform well if it is trained over a dataset which respects the continuity property, i.e., neighboring states are not mapped into control input values which are very different from each other. A representation that respects the continuity property corresponds to a low continuity index (see Eq. (<ref>)). During the training phase, we keep all the valid control inputs and let the training process to choose which value respects the continuity property more, by minimization of the cost function. Therefore, our formulation automatically takes care of the redundancy problem by mapping a neighborhood in the state space into close-in-value control inputs to respect the continuity requirement of the trained representation. The reason that our formulation does not correspond to a standard classification setting is that during the training phase a non-uniform number of  labels (corresponding to the control input values in the output stage of the neural network) per input (corresponding to the state values at the input layer of the neural network) are considered as valid, while we only will consider one label—corresponding to the highest score—as the trained representation's choice during the runtime.

In order to formulate the problem of finding a neural-network-based representation for the controller as a regression problem, first the training data must be pre-processed such that the continuity property is respected, i.e., the set of valid control-inputs per each state is pruned so that neighboring states are mapped to close-in-value control inputs. However, this pre-processing is time consuming and does not work efficiently in practice (see, e.g., <cit.>).

Compression algorithm for the controller

Controller $C$, learning rate $\lambda$
Compute the dataset $\ds_C$ using Eq. (<ref>)

Train the neural network $\NN_C$ on the dataset $\ds_C$ using the learning rate $\lambda$

Compute the set of state-input pairs  $\tilde C$ using Eq. (<ref>)

Compute $\hat C$ using Eq. (<ref>)

Corrected neural representation $\hat C$

Alg. <ref> summarizes the proposed procedure for computing a compressed representation for the original controller.
In the first step, we need to store the training set

\begin{align}\label{eq:cont_ds}
\ds_C =\{(\xbb,\boldsymbol h(\xbb))\mid &(\xbb,\ubb)\in C \Leftrightarrow \boldsymbol h(\xbb)(\Iu(\ubb))=1,\;(\xbb,\ubb)\notin C \Leftrightarrow \boldsymbol h(\xbb)(\Iu(\ubb))=0\},
\end{align}

where $\Iu\colon U\rightarrow [1;|\Ub|]$ is an indexing function for the control set $\Ub$, which assigns every value in $\Ub$ into a unique integer in the interval $[1;|\Ub|]$. Intuitively, each point in the dataset $\ds_C$ contains a state $\xbb\in L$ and a vector $\boldsymbol h(\xbb)$ which is of length $|\Ub|$ and has ones at the entries corresponding to the valid control inputs and zeros elsewhere.

Once the training dataset is ready, we can train a neural network $\NN_C$ which takes $\xbb\in\Xb$ as input and approximates $\Iu^{-1}(argmax(\boldsymbol h(\xbb)))$ in the output, where $\Iu^{-1}(\cdot)$ denotes the inverse of the indexing function used in Eq. (<ref>).

Note that the output layer of $\NN_C$ has to be of size $|\Ub|$ and for every $\xbb\in L$,
we consider the value  $\Iu^{-1}(argmax(\NN_C(\xb)))$ as the final control input assigned by $\NN_C$ to the state $\xbb$. Moreover, because $\Ub$ was computed by equally partitioning over $U$, both the indexing function $\Iu$ and its inverse can be implemented in a memory-efficient way using  and  functions.

Once the neural network $\NN_C$ is trained, we evaluate its performance
by finding all the states $\xbb$ at which using $\NN_C$ produces an invalid control input, i.e.,

$$E=\set{\xbb\in L\mid \Iu^{-1}(argmax(\NN_C(\xbb)))\notin C(\xbb)}.$$

The misclassification rate of the trained classifier $\NN_C$ is defined as:

\begin{equation}\label{eq:err_C}
\end{equation}

In order to maintain the guarantee provided by the original controller $C$, it is very important to correct the output of the trained representation, so that it outputs a valid control input at every state. In case the misclassification rate is small, we can store $\NN_C$ together with $\tilde{C}$, where

\begin{equation}\label{eq:cont2nd_to_be_stored}
\tilde C =\set{(\xbb,\ubb)\mid \xbb\in E,\;\ubb\in C(\xbb)}.
\end{equation}

The final deployable controller $\hat C$ consists of both $\NN_C$ and $\tilde C$, and is defined as

\begin{equation}
\label{eq:C_hat_def}
\hat C(\xbb)\coloneq \left\{
\begin{array}{lr}
\Iu^{-1}(argmax(\NN_C(\xbb)))\quad \text{if}\; \xbb\notin E\\
\tilde{C}(\xbb)\qquad\qquad\qquad\qquad\; \text{if}\;\xbb\in E.
\end{array}\right.
\end{equation}

Let $\hat C$, as defined in Eq. (<ref>), be the representation for the original correct-by-construction controller $C$ computed by solving the Prob. <ref>, i.e., $C\parallel \bar\Sigma$ realizes a given specification $\Phi$. Then, we have that $\hat C\parallel \bar \Sigma$ satisfies $\Phi$ as well.

Let $\hat C$ be as defined in Eq. (<ref>). The winning domain of both $\hat C\parallel \bar\Sigma$ and $C\parallel \bar\Sigma$ for satisfying a specification $\Phi$ is the same.

Our deployment method preserves soundness.
The input to our deployment approach is a formally guaranteed controller computed by any abstraction-based method. We train a neural representation that maps the states to a control input. This control input is valid for majority of the states. For the states that the control input is not valid, we keep the set of valid control inputs from the original controller and store them as a small look-up table. Therefore, the final corrected neural controller in Eq. (<ref>) is sound with respect to the original controller.

§ EXPERIMENTAL EVALUATION

Catalog of models used to generate the finite abstractions in this paper.

2*Case-study   2*Dynamical model    4cConfiguration (1)   4|cConfiguration (2)
$X$   $U$   $\eta_x$   $\eta_u$   $X$   $U$   $\eta_x$   $\eta_u$

1*2D car    2*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\end{bmatrix}\in\begin{bmatrix}\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2$   $[-1,1]^2$   2*$\begin{bmatrix}0.05\\0.05\end{bmatrix}$   2*$\begin{bmatrix}0.23\\0.23\end{bmatrix}$   $[0,10]^2$   $[-2,2]^2$   2*$\begin{bmatrix}0.025\\0.025\end{bmatrix}$   2*$\begin{bmatrix}0.23\\0.23\end{bmatrix}$
$(\xb(1),\xb(2))$- position
$(\ub(1),\ub(2))$- speed   $\tau=0.4$, $W=[-0.025,0.025]^2$

1*3D car    3*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\end{bmatrix}\in\begin{bmatrix}\ub(1)\cos(\xb(3))\\\ub(1)\sin(\xb(3))\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   3*$\begin{bmatrix}0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-1.5,1.5]\times$   3*$\begin{bmatrix}0.1\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6, 1.6]$            $[-\pi, \pi]$   $[-1, 1]$

$\xb(3)$- angle

$\ub(1)$- speed

$\ub(2)$- turn rate   $\tau=0.3$, $W=\set{\textbf 0}$

1*4D car    4*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\\\dot \xb(4)\end{bmatrix}\in\begin{bmatrix}\xb(4)\cos(\xb(3))\\\xb(4)\sin(\xb(3))\\\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-2,2]^2$   4*$\begin{bmatrix}0.05\\0.05\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6,1.6]\times$            $[-\pi,\pi]\times$

$\xb(3)$- angle      $[-1,1]$            $[-1,1]$

$\xb(4)$- speed

$\ub(1)$- turn rate

$\ub(2)$- acceleration control   $\tau=0.5$, $W=\set{\textbf 0}$

1*5D car    4*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\\\dot \xb(4)\\\dot\xb(5)\end{bmatrix}\in\begin{bmatrix}\xb(4)\cos(\xb(3))\\\xb(4)\sin(\xb(3))\\\xb(5)\\\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-2,2]^2$   4*$\begin{bmatrix}0.05\\0.05\\0.1\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6,1.6]\times$            $[-\pi,\pi]\times$

$\xb(3)$- angle      $[-1,1]\times $            $[-1,1]\times$

$\xb(4)$- speed speed      $[-1,1]$            $[-1,1]$

$\xb(4)$- turn rate

$\ub(1)$- acceleration

$\ub(2)$- angular acceleration    $\tau=0.5$, $W=\set{\textbf 0}$

Experimental results for continuous control systems.

Case-study    $|\Xb|\times|\Ub|$   $L$   $M$   $T$

2D car     810000      10000     <1     2.23

3D car     451584       9216     <1     3.09

4D car     4967424       97251     <1     461.75

5D car     54641664       2688     <1     OOT

4*90RSS    2D car     234090      6120     <1     1.39

3D car     245000       4546     <1     2.76

4D car    612500       20962     <1     31.13

5D car     3062500       14006     <1     98.75

4*90SCOTS    2D car     810000       10000     4100     0.22

3D car     451584       9216     5303     0.21

4D car     4967424       97251     113559     3.48

5D car     54641664       128245     3478460    62.58

Experimental results.

Case-study   $N_p$   $\epsilon$   $|\Xb|\times|\Ub|$   $|\Xb_\rho|\times|\Ub|$   $\eFb$   $\eBb$   $L$   $M_C$   $M_D$   $T_{C}$   $T_D$

1*02D car*     $10$   $\begin{bmatrix}0.4\\0.4\end{bmatrix}$   $8.10\times10^5$    $2.34\times10^5$     $\begin{bmatrix}0.028\\ 0.021\end{bmatrix}$     $\begin{bmatrix}0.019\\ 0.021\end{bmatrix}$    $1896$   $116$   $48922$   $13.93$   $0.002$

1*03D car     $40$   $\begin{bmatrix}0.4\\0.4\\0.4\end{bmatrix}$    $1.21\times10^7$    $3.52\times10^6$    $\begin{bmatrix}0.013\\0.016\\ 0.008\end{bmatrix}$      $\begin{bmatrix}0.014\\0.019\\0.011\end{bmatrix}$    $5713$   $224$   $1293196$   $87.42$   $0.251$

1*04D car     $20$   $\begin{bmatrix}0.4\\0.4\\0.4\\0.4
\end{bmatrix}$    $2.13\times10^8$    $1.58\times10^7$    $\begin{bmatrix}0.011\\0.016\\0.015\\ 0.014\end{bmatrix}$     $\begin{bmatrix}0.014\\0.014\\0.017\\ 0.012\end{bmatrix}$    $31415$   $384$   $7473416$   $784.81$   $15.1$

Experimental results for discrete control systems.

Regression-based method               Classification-based method

Case-study   $\eFb$   $\eBb$   $\M_T$   $\M_F+\M_B$   $\mathcal T$   $err_F$   $err_B$   $\mathcal M_T$    $\mathcal M_F+\mathcal M_B$    $\mathcal T$

1*02D car    $\begin{bmatrix}0.041\\ 0.027\end{bmatrix}$    $\begin{bmatrix}0.076\\ 0.069\end{bmatrix}$   $4100$   $488$   $42.27$   $0.09$   $0.08$   $120$   $21.2$

1*03D car    $451584$     $\begin{bmatrix}0.057\\ 0.054\\ 0.039\end{bmatrix}$      $\begin{bmatrix}0.360\\ 0.343\\ 0.217\end{bmatrix}$   $5303$   $488$   $41.74$

1*04D car    $4967424$    $\begin{bmatrix}0.093\\ 0.099\\ 0.089\\ 0.085\end{bmatrix}$     $\begin{bmatrix}0.413\\ 0.407\\ 0.224\\ 0.227\end{bmatrix}$   $7473416$   $488$   $682.366$

Controller synthesis results for discrete control systems.

Case-study   $|\Xb|\times|\Ub|$   $\eFb$   $\eBb$   $\M_T$   $\M_F+\M_B$   $\mathcal T$

1*02D car    $810000$   $\begin{bmatrix}0.041\\ 0.027\end{bmatrix}$    $\begin{bmatrix}0.076\\ 0.069\end{bmatrix}$   $4100$   $488$   $42.27$

1*03D car    $451584$     $\begin{bmatrix}0.057\\ 0.054\\ 0.039\end{bmatrix}$      $\begin{bmatrix}0.360\\ 0.343\\ 0.217\end{bmatrix}$   $5303$   $488$   $41.74$

1*04D car    $4967424$    $\begin{bmatrix}0.093\\ 0.099\\ 0.089\\ 0.085\end{bmatrix}$     $\begin{bmatrix}0.413\\ 0.407\\ 0.224\\ 0.227\end{bmatrix}$   $2.23\times 10^7$   $488$   $682.366$

Catalog of models used to generate the finite abstractions in Sec. <ref>.

2*Case study   2*Dynamics of the model    4cConfiguration (1)   4|cConfiguration (2)
$X$   $U$   $\eta_x$   $\eta_u$   $X$   $U$   $\eta_x$   $\eta_u$

1*2D car    2*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\end{bmatrix}\in\begin{bmatrix}\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2$   $[-1,1]^2$   2*$\begin{bmatrix}0.05\\0.05\end{bmatrix}$   2*$\begin{bmatrix}0.23\\0.23\end{bmatrix}$   $[0,10]^2$   $[-2,2]^2$   2*$\begin{bmatrix}0.025\\0.025\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$
$(\xb(1),\xb(2))$- position
$(\ub(1),\ub(2))$- speed   $\tau=0.4$, $W=[-0.025,0.025]^2$

1*3D car    3*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\end{bmatrix}\in\begin{bmatrix}\ub(1)\cos(\xb(3))\\\ub(1)\sin(\xb(3))\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   3*$\begin{bmatrix}0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-1.5,1.5]\times$   3*$\begin{bmatrix}0.1\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.23\\0.23\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6, 1.6]$            $[-\pi, \pi]$   $[-1, 1]$

$\xb(3)$- angle

$\ub(1)$- speed

$\ub(2)$- turn rate   $\tau=0.3$, $W=\set{\textbf 0}$

1*4D car    4*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\\\dot \xb(4)\end{bmatrix}\in\begin{bmatrix}\xb(4)\cos(\xb(3))\\\xb(4)\sin(\xb(3))\\\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-2,2]^2$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6,1.6]\times$            $[-\pi,\pi]\times$

$\xb(3)$- angle      $[-1,1]$            $[-1,1]$

$\xb(4)$- speed

$\ub(1)$- turn rate

$\ub(2)$- acceleration control   $\tau=0.5$, $W=\set{\textbf 0}$

1*5D car    4*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\\\dot \xb(4)\\\dot\xb(5)\end{bmatrix}\in\begin{bmatrix}\xb(4)\cos(\xb(3))\\\xb(4)\sin(\xb(3))\\\xb(5)\\\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-2,2]^2$   4*$\begin{bmatrix}0.1\\0.1\\0.1\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6,1.6]\times$            $[-\pi,\pi]\times$

$\xb(3)$- angle      $[-1,1]\times $            $[-1,1]\times$

$\xb(4)$- speed      $[-1,1]$            $[-1,1]$

$\xb(5)$- turn rate

$\ub(1)$- acceleration

$\ub(2)$- angular acceleration    $\tau=0.5$, $W=\set{\textbf 0}$

1*Inverted pendulum    2*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\end{bmatrix}\in\begin{bmatrix}\xb(2)\\\frac{g}{L}\sin(\xb(1))+ \frac{1}{mL^2}\ub(1)\end{bmatrix}+W$   $[-\pi,\pi]\times$   $[-1,1]$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$   1*$\begin{bmatrix}0.3\end{bmatrix}$   $[-\pi,\pi]\times$   $[-1,1]$   2*$\begin{bmatrix}0.1\\0.1\end{bmatrix}$   1*$\begin{bmatrix}0.3\end{bmatrix}$

$\xb(1)$- angle      $[-2,2]$            $[-2,2]$

$\xb(2)$- angular velocity

$\ub(1)$- torque   $L=g$, $m=\frac{8}{g^2}$

$\tau=0.05$, $W=\set{\textbf 0}$

1*TORA    4*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot\xb(3)\\\dot\xb(4)\end{bmatrix}\in\begin{bmatrix}\xb(2)\\-\xb(1)+0.1\sin(\xb(3))\\\xb(4)\\\ub(1)\end{bmatrix}+W$   $[-2,2]^4$   $[-1,1]$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\end{bmatrix}$   1*$\begin{bmatrix}0.3\end{bmatrix}$   $[-2,2]^4$   $[-1,1]$   4*$\begin{bmatrix}0.1\\0.1\\0.1\\0.1\end{bmatrix}$   1*$\begin{bmatrix}0.3\end{bmatrix}$

$\xb(3)$- angle

$\xb(4)$- angular velocity

$\ub(1)$- torque   $\tau=0.5$, $W=\set{\textbf 0}$

The results of regression-based controller synthesis  for finite abstractions.

Case study   $|\Xb|\times|\Ub|$   $\eFb$   $\eBb$   $d_F$   $d_B$   $\M_T$ (kB)   $\M_F+\M_B$  (kB)   $\mathcal T_c$ (min)   $\mathcal T_s$ (min)

1*02D car    $810000$   $\begin{bmatrix}1.02\times 10 ^{-2}\\ 1.58\times 10 ^{-2}\end{bmatrix}$    $\begin{bmatrix}2.81\times 10 ^{-2}\\ 1.17\times 10 ^{-2}\end{bmatrix}$   $6.81\times 10^{-1}$   $9.64\times 10^{-1}$   $7.76\times 10^4$   $488$   $68.58$   $8.55$

1*03D car    $451584$     $\begin{bmatrix}2.05\times10^{-2}\\ 2.19\times10^{-2}\\ 2.26\times10^{-2}\end{bmatrix}$      $\begin{bmatrix}2.48\times10^{-2}\\ 1.76\times10^{-2}\\ 2.32\times10^{-2}\end{bmatrix}$   $7.11\times 10^{-1}$   $7.85\times 10^{-1}$   $1.35\times 10 ^5$   $488$   $65.46$    $14.50$

1*04D car    $4967424$    $\begin{bmatrix}1.71\times10^{-2}\\ 2.40\times10^{-2}\\ 1.62\times10^{-2}\\1.96\times10^{-2}\end{bmatrix}$      $\begin{bmatrix}2.05\times10^{-2}\\ 1.54\times10^{-2}\\ 1.35\times10^{-2}\\1.25\times10^{-2}\end{bmatrix}$   $4.24\times 10^{-1}$   $2.87\times 10^{-1}$   $5.58\times 10^6$   $488$   $446.23$   $20.55$

1*05D car    $30735936$    $\begin{bmatrix}1.41\times10^{-2}\\ 1.18\times10^{-2}\\ 1.97\times10^{-2}\\2.22\times10^{-2}\\1.93\times10^{-2}\end{bmatrix}$      $\begin{bmatrix}2.11\times10^{-2}\\ 1.79\times10^{-2}\\ 1.13\times10^{-2}\\1.65\times10^{-2}\\2.45\times10^{-2}\end{bmatrix}$   $5.34\times 10^{-1}$   $4.25\times 10^{-1}$   $ 3.64\times 10^8 (OOM)$   $488$   $3025.14$   $312.15$

1*0Inverted pendulum    $17360$   $\begin{bmatrix} 2.53\times 10 ^{-2}\\ 3.44\times 10 ^{-2}\end{bmatrix}$    $\begin{bmatrix}2.31\times 10 ^{-2}\\ 2.97\times 10 ^{-2}\end{bmatrix}$   $6.50\times 10^{-1}$   $5.61\times 10^{-1}$   $2.27\times 10^4$   $488$   $68.58$   $4.18$

1*0TORA    $1433531$   $\begin{bmatrix} 2.53\times 10 ^{-2}\\ 2.67\times 10 ^{-2}\\2.39\times 10 ^{-2}\\2.24\times 10 ^{-2}\end{bmatrix}$    $\begin{bmatrix}2.21\times 10 ^{-2}\\ 2.57\times 10 ^{-2}\\ 1.88\times 10 ^{-2}\\ 3.03\times 10 ^{-2}\end{bmatrix}$   $4.34\times 10^{-1}$   $4.15\times 10^{-1}$   $1.57\times 10^7$   $488$   $241.48$   $166.16$

The results of classifier-based controller synthesis for finite abstractions.

Case study   $|\Xb|\times|\Ub|$   $err_F$   $err_B$   $d_F$   $d_B$   $\M_T$ (kB)   $\M_F+\M_B$ (kB)   $\mathcal T_c$ (min)   $\mathcal T_s$ (min)

1*02D car    $810000$   $2.75\times 10^{-2}$    $3.27\times 10^{-2}$   $2.65\times 10^{-2}$   $2.93\times 10^{-2}$   $7.76\times 10^4$   $1.33\times 10^4$   $68.58$   $10.71$

1*03D car    $451584$     $2.71\times 10^{-4}$      $2.21\times 10^{-6}$   $3.71\times 10^{-5}$   $9.47\times 10^{-7}$   $1.35\times 10 ^5$   $1.91\times 10 ^4$   $50.74$    $12.11$

1*04D car    $4967424$    $6.24\times 10^{-4}$      $0$   $2.84\times 10^{-4}$   $0$   $5.58\times 10^6$   $2.37\times 10^4$   $565.13$   $24.58$

1*05D car    $30735936$    $3.41\times 10^{-5}$      $5.33\times 10^{-8}$   $3.21\times 10^{-5}$   $2.19\times 10^{-8}$   $3.64\times 10^8 (OOM)$   $3.27\times 10^4$   $3421.21$   $215.88$

1*0Inverted pendulum    $17360$    $6.03\times 10^{-2}$      $5.85\times 10^{-2}$   $0$   $0$   $2.27\times 10^4$   $2.08\times 10^4$   $8.21$   $8.33$

1*0TORA    $1433531$    $1.27\times 10^{-1}$     $1.26\times 10^{-1}$   $1.55\times 10^{-1}$   $1.48\times 10^{-1}$   $1.57\times 10^7$   $2.38\times10^4$   $234.87$   $159.75$

We evaluate the performance of our proposed algorithms
several control systems. Dynamics of our control systems are listed in Tab. <ref>.
We used configurations (1) and (2) in Tab. <ref>, respectively, for evaluating our methods for synthesis and deployment.

We construct the transition system in all the case studies using the sampling approach in <cit.>. This approach generates $T_F$ using sampled trajectories while providing confidence on the correctness of $T_F$.

Our experiments were performed on a cluster with Intel Xeon E7-8857 v2 CPUs (32 cores in total) at 3GHz, with 100GB of RAM.
For training neural networks, we did not use a distributed implementation as we found that distributing the process across GPUs actually decelerates the process. However, for the rest of our compression and synthesis algorithms, we used a distributed implementation.

We considered the $\ell_\infty$ ball centered at $(4,4)$ with the radius $0.8$ over the Euclidean plane as the target set for the multi-dimensional car examples, $[-0.5,0.5]\times[-1,1]$ for the inverted pendulum example, and $[-1,1]^4$ for the TORA example.
To evaluate our
corrected neural method described in Subsec. <ref>,
we set the list of neuron numbers in different layers as $(n+m,20,40,30,2n)$, select the activation functions to be hyperbolic tangent, and set the learning rate to be $\lambda=0.001$. As discussed in
Subsec. <ref>, the corrected neural representations for finite abstractions can also be constructed by solving a classification problem.
To evaluate this method, we set the list of neuron numbers in different layers for both $\NN_F$ and $\NN_B$ as $(n+m,40,160,160,160,160,160,160,160,160,500,800,2\sum_{i=1}^n|\Xb(i)|)$, select the activation functions to be ReLU, and set the learning rate to be $\lambda=0.0001$.

We used stochastic gradient descent method with the corresponding learning rate for training the neural networks <cit.>. Tabs. <ref> and <ref> illustrate the synthesis results related to our experiments for finite abstractions, using the regression-based and classification-based methods, respectively.
Although we used the same neural network structure for all the examples, soundness errors take small values that are bounded by $3.44\times10^{-2}$ as the maximum of $\eFb$ and $\eBb$ in the regression-based method, and by
$1.27\times 10^{-1}$ as the maximum of $err_F$ and $err_B$ in the classification-based method. Moreover, memory requirement of our proposed regression-based and classification-based methods at higher dimensions remains almost constant while the size of the transition system increases exponentially (see the illustration shown in Fig. <ref> (Left) for the multi-dimensional car case studies).
Further, we notice that the regression-based method results in higher mismatch rates $d_F$ and $d_B$ compared to the classification-based method: on average, $5.87\times 10^{-1}$ versus $3.03\times 10^{-2}$ for $d_F$, and $6.15\times 10^{-1}$ versus $2.96\times 10^{-2}$ for $d_B$ (see the illustration shown in Fig. <ref> (Right) for the multi-dimensional car case studies).
Therefore, using the classification-based method, while being sound, produces a smaller graph, which is less restrictive for the synthesis purpose.

Most importantly, memory requirement using both our approaches is way less  than the memory needed to store the original (forward) transition system ($\M_F+\M_B<<\M_T$).
Regression-based method reduces the memory requirements by a factor of $1.31\times 10^5$ and up to $7.54\times 10^5$. However, the classification-based method reduces the memory requirements by
a factor of $2.01\times 10^3$ and up to $1.12\times 10^4$.
This shows that the regression-based method requires less memory compared to the classification-based method.

Left: Memory requirement of different methods for storing transition systems of multi-dimensional cars (cf. Tab. <ref>) in logarithmic scale. Right: Distribution of total graph mismatch rate ($d_F+d_B$) for our proposed methods in logarithmic scale.

Deployment.Tab. <ref> lists our experimental results for compressing the symbolic controllers. For $\NN_C$,
we set the list of neuron numbers in different layers for both $\NN_F$ and $\NN_B$ as $(n,20,80,80,80,80,80,160,|\Ub|)$, select the activation functions to be rectified linear unit (ReLU), and set the learning rate to be $\lambda=0.0001$. It can be noticed that $err_C$ is very small for all the examples. Therefore, we only need to store a very small portion of $C$ in addition to $\NN_C$.
As it can be observed in Tab. <ref>, our method has been successful in computing representations which are very accurate and compact-in-size ($\M_{\hat C}<<\M_C$).

The results of controller compression.

Case study   $|C|$   $err_C$   $\M_C$ (kB)   $\M_{\hat C} (kB)$   $\mathcal T$ (min)

1*02D car    $2.15
\times 10 ^ 6$   $1.85\times 10^{-5}$    $2.75\times 10 ^5$
$1.21\times 10 ^3$   $6.31$

1*03D car    $2.87\times 10 ^6$   $2.16\times 10^{-3}$    $4.65\times 10 ^5$

$1.05\times 10 ^3$   $19.14$

1*04D car     $9.35 \times 10^7$   $3.63\times10^{-2}$    $2.24\times 10^6$

$1.35\times 10^3$   $39.48$

1*05D car     $1.69 \times 10^9$   $4.51\times10^{-3}$    $4.71\times 10^7$

$1.48\times 10^3$   $201.86$

1*0Inverted pendulum     $8.16 \times 10^5$   $1.08\times10^{-3}$    $7.83\times 10^4$

$8.92\times 10^2$   $7.51$

1*0TORA     $4.78 \times 10^7$   $3.78\times10^{-4}$    $7.65\times 10^6$

$8.92\times 10^2$   $113.97$

Parametrization. Our approach requires selecting the hyperparameters of the training process and choosing the structure of the neural networks. We have performed several experiments to select the hyperparameters of the training (e.g., the learning rate, epoch number, and batch size). Regarding the structure of the neural networks, we have explored different choices such as the type of the activation functions (hyperbolic tangent, ReLU, etc.), number of neurons per layer, and the depth. Increasing the complexity of the neural network, by increasing the number of neurons per layer or depth, leads to a better performance.
Note that the neural networks employed in our setting are not supposed to make any generalization over unseen data. Therefore, our approach does not suffer from over-parametrization of the neural networks. We have demonstrated this in Fig. <ref> by providing the error as a function of the depth of the neural representation for the 3D car example. The error always decreases by increasing the depth of the neural representation. Therefore, the structure of the neural representations can be selected for having an acceptable accuracy within a given time bound for the training process.

Demonstrating the effect of increasing the depth of the neural representation on the norm of the soundness error $\eFb$ (cf. Eq. (<ref>)) for regression-based controller synthesis (Left), the soundness error $err_F$ (cf. Eq. (<ref>)) for classification-based controller synthesis (Middle), and the misclassification rate (cf. Eq. (<ref>)) for deployment (Right). The experiments are performed on the 3D car example.

§ DISCUSSION AND CONCLUSIONS

In this paper, we
considered abstraction-based methods for controller synthesis to satisfy high-level temporal requirements. We addressed the (exponentially large) memory requirements of these methods in both synthesis and deployment.
Using the expressive power of neural networks,
we proposed memory-efficient methods to compute compressed representations for both forward and backward dynamics of the system. With focus on reach-avoid specifications, we showed how to perform synthesis using corrected neural representations of the system.

We also proposed a novel formulation for finding compact corrected neural representations of the controller to reduce the memory requirements in deploying the controller. Finally, we evaluated our approach on multiple case studies, showing reduction in memory requirements by orders of magnitude, while providing formal correctness guarantees.

Extension to more general specifications.Our approach is based on computing an under-approximation of $\Pre$ and over-approximation of $\Post$ operators. Therefore, it can be applied to any synthesis problem whose solution is characterized based on these operators. This means our approach can be applied to control synthesis for other linear temporal logic specifications including safety, Büchi, and Rabin objectives.

Reusability of the computed representations.
Our approach computes the corrected neural representations that is sound on the whole state space. These representations can be used for any other problem defined over the same finite abstraction.

Application to systems with known analytical model.Our approach is efficient in providing compact representations for a given finite abstraction at the cost of increasing the off-line computational time. This is regardless of constructing the finite abstraction using model-based methods or (correct) data-driven methods. Model-based on-the-fly synthesis methods will utilize numerical solutions of differential equations when the analytical model of the system is known with available bounds on the continuity properties of the system. These methods may perform better in case solving the corresponding differential equations is faster than making a forward pass through the neural representation.

Comparison with a baseline method.
We have demonstrated the effectiveness of our method on a number of case studies in compressing finite transition systems and controllers which are stored in the form of look-up tables. In the introduction and related work sections of our paper, we have discussed why other methods cannot be used to solve our problem. In below, we have listed our main arguments.

* While transition systems and controllers can be encoded using BDDs instead of look-up tables, the memory blow-up problem still exists for systems of higher dimensions. However, using our technique, we empirically show that the size of the computed representations is not necessarily affected by size of the original mapping. See for example Fig. <ref> (Left), wherein the memory required by the trained compressed representation stays at 488 kB, despite the fact that the required memory by the original transition system has increased by a factor of 5000.

* Also, our synthesis setting is different from the one considered in references <cit.>, wherein memory-efficient synthesis methods are proposed based on a (compact) analytical description of the nominal dynamics of the system and its growth bound. We consider the case wherein the input is a huge finite transition system which can also be learned from simulations.

* Finally, while the control determinization and compression schemes proposed in <cit.> are based on the BDD and ADD encodings of the controller, the only methodologically that is in a similar spirit as our deployment approach is the symbolic regression of <cit.>. As mentioned by the authors of <cit.>, their regression-based method is not able to represent the original controller with an acceptable accuracy. Our superior performance is mainly because of our classification-based formulation, as opposed to a regression-based formulation.

Utilizing invertible neural networks. Our method requires training two different neural networks associated with the forward and backward dynamics. A possible future research direction would be to use invertible neural networks instead of training two separate neural networks.
However, given the specific application and inherent differences between our approach and the successful experiences with invertible neural networks, it is currently not obvious to us that the same performance would be accessible.

Choice of hyper-rectangular reachable sets.
Hyper-rectangular sets are the most popular choice for representing reachable sets in abstraction-based controller synthesis (see e.g., <cit.>). Although other templates could also be used to represent reachable sets, the conservativeness of the over-approximation reduces as the size of the discretization decreases. Our approach can in principle be applied to any parametrization of the reachable sets.

Robustness of the deployable controller:
The controllers synthesized by abstraction-based methods are discontinuous in general but certify satisfaction of the specification under the modelled disturbances. Therefore, robustness of the closed-loop system to the set of disturbances is already encoded in the computation of the controller. Our compression approach takes the discontinuous controller as a lookup table and tries to assign neighboring states to control inputs with similar values such that the continuity index is improved. In particular, applying Eq. (17) does not result in a worse continuity index despite the different rules applied for the two categories of states.

Robustness against adversarial examples.
In general, it is true that neural networks are not robust to adversarial examples, meaning that a small change in their input could give large enough changes in their output resulting in errors. We emphasize that going from a look-up table representation of the controller to a neural network representation does not influence the robustness against adversarial attacks unless the attacker gains access to middle layers of the neural network. Any adversarial attack on the inputs of the neural network can be studied using similar techniques and concepts from the robustness analysis of abstraction-based methods and is independent of the controller representation.

Comparison with BDD.	While transition systems and controllers can be encoded using BDDs instead of look-up tables, the memory blow-up problem still exists for systems of higher dimensions. We empirically show that the size of our computed representations do not necessarily grow by dimension of the state space.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonRajeev Alur.
booktitlePrinciples of cyber-physical systems.
publisherMIT press.

[Baier and KatoenBaier and Katoen2008]
authorpersonC. Baier and personJ.-P.
Katoen. year2008.
booktitlePrinciples of model checking.
publisherMIT press.

[Belta, Yordanov, and GolBelta
et al2017]
authorpersonCalin Belta, personBoyan
Yordanov, and personEbru Aydin Gol.
booktitleFormal methods for discrete-time dynamical
systems. Vol. volume15.

authorpersonD.P. Bertsekas.
booktitleNonlinear Programming.
publisherAthena Scientific.

[Boyan and MooreBoyan and Moore1994]
authorpersonJustin Boyan and personAndrew
Moore. year1994.
Generalization in Reinforcement Learning: Safely
Approximating the Value Function. In booktitleAdvances in
Neural Information Processing Systems, Vol. volume7.
publisherMIT Press.

authorpersonBryant. year1986.
Graph-Based Algorithms for Boolean Function
journalIEEE Trans. Comput. volumeC-35,
number8 (year1986), pages677–691.

[Devonport, Saoud, and ArcakDevonport
et al2021]
authorpersonAlex Devonport, personAdnane
Saoud, and personMurat Arcak.
Symbolic Abstractions From Data: A PAC Learning
journalarXiv preprint arXiv:2104.13901

[Dutta, Chen, and SankaranarayananDutta
et al2019]
authorpersonSouradeep Dutta, personXin
Chen, and personSriram Sankaranarayanan.
Reachability analysis for neural feedback systems
using regressive polynomial rule inference. In
booktitleProceedings of the 22nd ACM International
Conference on Hybrid Systems: Computation and Control.

authorpersonAntoine Girard.
Low-Complexity Switching Controllers for Safety
using Symbolic Models.
journalIFAC Proceedings Volumes
volume45, number9 (year2012),

4th IFAC Conference on Analysis and Design of Hybrid Systems.

[Hertneck, Köhler, Trimpe, and
AllgöwerHertneck et al2018]
authorpersonMichael Hertneck, personJohannes
Köhler, personSebastian Trimpe, and
personFrank Allgöwer. year2018.
Learning an Approximate Model Predictive Controller
With Guarantees.
journalIEEE Control. Syst. Lett.
volume2, number3 (year2018),

[Hsu, Majumdar, Mallik, and SchmuckHsu
et al2018]
authorpersonKyle Hsu, personRupak Majumdar,
personKaushik Mallik, and personAnne-Kathrin
Schmuck. year2018.
Multi-Layered Abstraction-Based Controller
Synthesis for Continuous-Time Systems. In
booktitleProceedings of the 21st International Conference on
Hybrid Systems: Computation and Control (part of CPS Week).

[Huang, Fan, Chen, Li, and ZhuHuang
et al2022]
authorpersonChao Huang, personJiameng Fan,
personXin Chen, personWenchao Li, and
personQi Zhu. year2022.
POLAR: A Polynomial Arithmetic Framework
for Verifying Neural-Network Controlled Systems.
In booktitleAutomated Technology for Verification
and Analysis. publisherSpringer International Publishing,

[Huang, Fan, Li, Chen, and ZhuHuang
et al2019]
authorpersonChao Huang, personJiameng Fan,
personWenchao Li, personXin Chen, and
personQi Zhu. year2019.
journalACM Transactions on Embedded Computing
Systems volume18, number5s (dateOct.
year2019), pages1–22.

[Ivanov, Weimer, Alur, Pappas, and LeeIvanov
et al2019]
authorpersonRadoslav Ivanov, personJames
Weimer, personRajeev Alur, personGeorge J. Pappas,
and personInsup Lee. year2019.
Verisig. In booktitleProceedings
of the 22nd ACM International Conference on Hybrid Systems: Computation and
Control. publisherACM.

[Ivanova, Saoud, and GirardIvanova
et al2022]
authorpersonElena Ivanova, personAdnane
Saoud, and personAntoine Girard.
Lazy controller synthesis for monotone transition
systems and directed safety specifications.
journalAutom.  volume135
(year2022), pages109993.

[Julian, Kochenderfer, and OwenJulian
et al2019]
authorpersonKyle D. Julian, personMykel J.
Kochenderfer, and personMichael P. Owen.
Deep Neural Network Compression for Aircraft
Collision Avoidance Systems.
journalJournal of Guidance, Control, and Dynamics
volume42, number3 (dateMarch
year2019), pages598–608.

[Julian, Lopez, Brush, Owen, and
KochenderferJulian et al2016]
authorpersonKyle D. Julian, personJessica
Lopez, personJeffrey S. Brush, personMichael P.
Owen, and personMykel J. Kochenderfer.
Policy compression for aircraft collision avoidance
systems. In booktitle2016 IEEE/AIAA 35th Digital Avionics
Systems Conference (DASC). pages1–10.

[Kazemi, Majumdar, Salamati, Soudjani, and
WoodingKazemi et al2022]
authorpersonMilad Kazemi, personRupak
Majumdar, personMahmoud Salamati, personSadegh
Soudjani, and personBen Wooding.
titleData-Driven Abstraction-Based Control Synthesis.

[Khaled, Kim, Arcak, and ZamaniKhaled
et al2019]
authorpersonMahmoud Khaled, personEric S.
Kim, personMurat Arcak, and personMajid Zamani.
Synthesis of Symbolic Controllers: A Parallelized
and Sparsity-Aware Approach. In booktitleTools and
Algorithms for the Construction and Analysis of Systems - 25th International
Conference, TACAS 2019, Held as Part of the European Joint Conferences on
Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April
6-11, 2019, Proceedings, Part II (seriesLecture Notes in
Computer Science), editorpersonTomás Vojnar
and personLijun Zhang (Eds.), Vol. volume11428.
publisherSpringer, pages265–281.

[Khaled and ZamaniKhaled and Zamani2019]
authorpersonMahmoud Khaled and personMajid
Zamani. year2019.
pFaces: an acceleration ecosystem for symbolic
control. In booktitleProceedings of the 22nd ACM
International Conference on Hybrid Systems: Computation and Control, HSCC
2019, Montreal, QC, Canada, April 16-18, 2019. publisherACM,

[Kochenderfer and MonathKochenderfer and
authorpersonMykel J. Kochenderfer and
personNicholas Monath. year2013.
Compression of Optimal Value Functions for Markov
Decision Processes. In booktitle2013 Data Compression
Conference. pages501–501.

[Kwiatkowska, Norman, and ParkerKwiatkowska
et al2005]
authorpersonMarta Kwiatkowska, personGethin
Norman, and personDavid Parker.
Probabilistic model checking in practice: Case
studies with PRISM.
journalACM SIGMETRICS Performance Evaluation
Review volume32, number4 (year2005),

[Lavaei, Khaled, Soudjani, and ZamaniLavaei
et al2020]
authorpersonAbolfazl Lavaei, personMahmoud
Khaled, personSadegh Soudjani, and personMajid
Zamani. year2020.
AMYTISS: Parallelized automated controller
synthesis for large-scale stochastic systems. In
booktitleComputer Aided Verification: 32nd International
Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings,
Part II 32. Springer, pages461–474.

[Lee and SeshiaLee and Seshia2016]
authorpersonEdward Ashford Lee and
personSanjit Arunkumar Seshia. year2016.
booktitleIntroduction to embedded systems: A
cyber-physical systems approach.
publisherMIT Press.

[Macoveiciuc and ReissigMacoveiciuc and
authorpersonE. Macoveiciuc and personG.
Reissig. year2022.
On-the-fly symbolic synthesis with memory reduction
journalIEEE Trans. Automat. Control
(year2022), pages1–8.

[Majumdar, Ozay, and SchmuckMajumdar
et al2020]
authorpersonRupak Majumdar, personNecmiye
Ozay, and personAnne-Kathrin Schmuck.
On abstraction-based controller design with output
feedback. In booktitleHSCC '20: 23rd ACM International
Conference on Hybrid Systems: Computation and Control, Sydney, New South
Wales, Australia, April 21-24, 2020,
editorpersonAaron D. Ames, personSanjit A.
Seshia, and personJyotirmoy Deshmukh (Eds.).
publisherACM, pages15:1–15:11.

[Makdesi, Girard, and FribourgMakdesi
et al2021]
authorpersonAnas Makdesi, personAntoine
Girard, and personLaurent Fribourg.
Efficient Data-Driven Abstraction of Monotone
Systems with Disturbances.
journalIFAC-PapersOnLine volume54,
number5 (year2021), pages49–54.
7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS

[Reissig, Weber, and RunggerReissig
et al2016]
authorpersonG. Reissig, personA. Weber,
and personM. Rungger. year2016.
Feedback refinement relations for the synthesis of
symbolic controllers.
journalIEEE TAC volume62,
number4 (year2016), pages1781–1796.

[Roy, Tabuada, and MajumdarRoy
et al2011]
authorpersonPritam Roy, personPaulo
Tabuada, and personRupak Majumdar.
Pessoa 2.0. In
booktitleProceedings of the 14th international conference on
Hybrid systems: computation and control. publisherACM.

authorpersonSebastian Ruder.
An overview of gradient descent optimization
journalArXiv  volumeabs/1609.04747

[Rungger and StursbergRungger and
authorpersonMatthias Rungger and
personOlaf Stursberg. year2012.
On-the-fly model abstraction for controller
synthesis. In booktitle2012 American Control Conference
(ACC). pages2645–2650.

[Rungger and ZamaniRungger and
authorpersonM. Rungger and personM.
Zamani. year2016.
SCOTS: A Tool for the Synthesis of Symbolic
Controllers. In booktitleHSCC.

[Salamati, Salvia, Darulova, Soudjani, and
MajumdarSalamati et al2019]
authorpersonMahmoud Salamati, personRocco
Salvia, personEva Darulova, personSadegh Soudjani,
and personRupak Majumdar. year2019.
Memory-Efficient Mixed-Precision Implementations
for Robust Explicit Model Predictive Control.
journalACM Trans. Embed. Comput. Syst.
volume18, number5s (year2019),

[Samuel, Mallik, Schmuck, and NeiderSamuel
et al2020]
authorpersonStanly Samuel, personKaushik
Mallik, personAnne-Kathrin Schmuck, and
personDaniel Neider. year2020.
Resilient abstraction-based controller design. In
booktitleHSCC '20: 23rd ACM International Conference on
Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia,
April 21-24, 2020. publisherACM, pages33:1–33:2.

[Sutton and BartoSutton and Barto2018]
authorpersonRichard S. Sutton and
personAndrew G. Barto. year2018.
booktitleReinforcement Learning: An Introduction
(editionsecond ed.).

authorpersonPaulo Tabuada.
booktitleVerification and Control of Hybrid Systems:
A Symbolic Approach (edition1st ed.).
publisherSpringer Publishing Company, Incorporated.

[Tran, Cai, Diego, Musau, Johnson, and
KoutsoukosTran et al2019]
authorpersonHoang-Dung Tran, personFeiyang
Cai, personManzanas Lopez Diego, personPatrick
Musau, personTaylor T. Johnson, and personXenofon
Koutsoukos. year2019.
Safety Verification of Cyber-Physical Systems with
Reinforcement Learning Control.
journalACM Transactions on Embedded Computing
Systems volume18, number5s (dateOct.
year2019), pages1–22.

[Tran, Yang, Manzanas Lopez, Musau, Nguyen,
Xiang, Bak, and JohnsonTran et al2020]
authorpersonHoang-Dung Tran, personXiaodong
Yang, personDiego Manzanas Lopez, personPatrick
Musau, personLuan Viet Nguyen, personWeiming Xiang,
personStanley Bak, and personTaylor T. Johnson.
NNV: The Neural Network Verification Tool for Deep
Neural Networks and Learning-Enabled Cyber-Physical Systems. In
booktitleComputer Aided Verification,
editorpersonShuvendu K. Lahiri and
personChao Wang (Eds.). publisherSpringer
International Publishing, addressCham, pages3–17.

[Tsitsiklis and Van RoyTsitsiklis and
Van Roy1997]
authorpersonJ.N. Tsitsiklis and personB.
Van Roy. year1997.
An analysis of temporal-difference learning with
function approximation.
journalIEEE Trans. Automat. Control
volume42, number5 (year1997),

[Zapreev, Verdier, and MazoZapreev
et al2018]
authorpersonIvan S. Zapreev, personCees
Verdier, and personManuel Mazo.
Optimal Symbolic Controllers Determinization for
BDD storage.
journalIFAC-PapersOnLine volume51,
number16 (year2018), pages1–6.

6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS

§ DESCRIPTION OF CASE STUDIES

Description of the case studies used in this paper can be found in Tab. <ref>.

Catalog of models used to generate the finite abstractions in Sec. <ref>.

2*Case study   2*Dynamics of the model    4cConfiguration (1)   4|cConfiguration (2)
$X$   $U$   $\eta_x$   $\eta_u$   $X$   $U$   $\eta_x$   $\eta_u$

1*2D car    2*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\end{bmatrix}\in\begin{bmatrix}\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2$   $[-1,1]^2$   2*$\begin{bmatrix}0.05\\0.05\end{bmatrix}$   2*$\begin{bmatrix}0.23\\0.23\end{bmatrix}$   $[0,10]^2$   $[-2,2]^2$   2*$\begin{bmatrix}0.025\\0.025\end{bmatrix}$   2*$\begin{bmatrix}0.23\\0.23\end{bmatrix}$
$(\xb(1),\xb(2))$- position
$(\ub(1),\ub(2))$- speed   $\tau=0.4$, $W=[-0.025,0.025]^2$

1*3D car    3*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\end{bmatrix}\in\begin{bmatrix}\ub(1)\cos(\xb(3))\\\ub(1)\sin(\xb(3))\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   3*$\begin{bmatrix}0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-1.5,1.5]\times$   3*$\begin{bmatrix}0.1\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$
$(\xb(1),\xb(2))$- position      $[-1.6, 1.6]$            $[-\pi, \pi]$   $[-1, 1]$

$\xb(3)$- angle

$\ub(1)$- speed

$\ub(2)$- turn rate   $\tau=0.3$, $W=\set{\textbf 0}$

1*4D car    4*$\begin{bmatrix}\dot\xb(1)\\\dot\xb(2)\\\dot \xb(3)\\\dot \xb(4)\end{bmatrix}\in\begin{bmatrix}\xb(4)\cos(\xb(3))\\\xb(4)\sin(\xb(3))\\\ub(1)\\\ub(2)\end{bmatrix}+W$   $[0,5]^2\times$   $[-1,1]^2$   4*$\begin{bmatrix}0.2\\0.2\\0.2\\0.2\end{bmatrix}$   2*$\begin{bmatrix}0.3\\0.3\end{bmatrix}$   $[0,10]^2\times$   $[-2,2]^2$   4*$\begin{bmatrix}0.05\\0.05\\0.1\\0.1\end{bmatrix}$   2*$\begin{bmatrix}0.2\\0.2\end{bmatrix}$