Learning Approximate Forward Reachable Sets
Using Separating Kernels

Reachability analysis is important in many dynamical systems for its ability to provide assurances of desired behavior, such as reaching a desired target set or anticipating potential intersection with a set known to be unsafe. Such analysis has shown utility in a variety of safety-critical applications, including autonomous cars, UAVs, and spacecraft. The forward stochastic reachable set describes the set of states that the system will reach with a non-zero likelihood. While most approaches for stochastic reachability are model-based, data-driven approaches are important when mathematical models may not exist or may be too complex for existing numerical approaches. In particular, the growing presence of learning-enabled components in dynamical systems warrants the development of new tools for stochastic reachability that can accommodate neural networks, look-up tables, and other model-resistant elements. In this paper, we propose a technique for data-driven stochastic reachability analysis that provides a convergent approximation to the true stochastic reachable set.

Significant advances have been made in verification of dynamical systems with neural network components. Recent work in Seidman et al. (2020); Weinan (2017) has shown that neural networks can be modeled as a nonlinear dynamical system, making them amenable in some cases to model-based reachability analysis. Typically, these approaches presume that the neural network exhibits a particular structure, such as having a particular activation function, as in Sidrane and Kochenderfer (2019); Tran et al. (2020), and exploit existing tools for forward reachability, such as Althoff (2015); Chen et al. (2013). Other approaches employ a mixed integer linear programming approach, as in Dutta et al. (2017, 2019); Lomuscio and Maganti (2017). These techniques exploit Lipschitz constants or perform set propagation, however, the latter approach becomes intractable for large-scale systems due to vertex facet enumeration. Further, in practice, knowledge of the network structure or dynamics may not be available, or may be too complex to use with standard reachability methods. Thus, additional tools are needed to efficiently compute stochastic reachable sets.

Data-driven reachability methods provide convergent approximations of reachable sets with high confidence, but are typically unable to provide assured over-approximations. Methods have been developed that use convex hulls in Lew and Pavone (2020) and scenario optimization in Devonport and Arcak (2020). However, these approaches rely upon convexity assumptions which can be limiting in certain cases. Other data-driven approaches leverage a class of machine learning techniques known as kernel methods, including Gaussian processes in Devonport and Arcak (2020) and support vector machines in Allen et al. (2014); Rasmussen et al. (2017). However, the approach in Rasmussen et al. (2017) can suffer from stability issues and does not provide probabilistic guarantees of convergence, and the approach in Allen et al. (2014) requires that we repeatedly solve a nonlinear program offline to generate data for the SVM classifier. The approach in Devonport and Arcak (2020) requires use of a Gaussian process prior. In contrast to these approaches, we propose a method that can accommodate nonlinear dynamical systems with arbitrary stochastic disturbances.

Our approach employs a class of kernel methods known as separating kernels to form a reachable set classifier. By learning a set classifier in Hilbert space, we convert the problem of learning a set boundary into the problem of learning a classifier in a high-dimensional space of functions. Our approach extends the work in De Vito et al. (2014) to the problem of learning reachable sets for stochastic systems that overcomes the stability and convergence issues faced by existing kernel based approaches and allows for arbitrary stochastic disturbances. Our main contribution is an application of the techniques presented in De Vito et al. (2014) to the problem of learning approximate forward reachable sets and neural network verification. Similar to other data-driven approaches, the approximation proposed here does not provide guarantees in the form of assured over- or under-approximations of the forward reachable set. However, although empirically derived, the approximation can be shown to converge in probability almost surely.

The paper is structured as follows: Section 2 formulates the problem. We describe the application of kernel methods to compute approximate forward reachable sets in Section 3, and discuss their convergence properties and finite sample bounds. In Section 4, we demonstrate our approach on a realistic satellite rendezvous and docking problem, as well as two neural network verification benchmarks from Dutta et al. (2019). Concluding remarks are presented in Section 5.

We use the following notation throughout: Let $E$ be an arbitrary nonempty space, and denote the $\sigma$-algebra on $E$ by $\mathcal{E}$. Let $\wp(E)$ denote the set of all subsets (the power set) of $E$. If $E$ is a topological space (Çinlar, 2011), the $\sigma$-algebra generated by the set of all open subsets of $E$ is called the Borel $\sigma$-algebra, denoted by $\mathscr{B}(E)$. If $E$ is countable, with $\sigma$-algebra $\wp(E)$, then it is called discrete. Let $(\Omega,\mathcal{F},\mathbb{P})$ denote a probability space, where $\mathcal{F}$ is the $\sigma$-algebra on $\Omega$ and $\mathbb{P}:\mathcal{F}\rightarrow[0,1]$ is a probability measure on the measurable space $(\Omega,\mathcal{F})$. A measurable function $X:\Omega\rightarrow E$ is called a random variable taking values in $(E,\mathcal{E})$. The image of $\mathbb{P}$ under $X$, $\mathbb{P}(X^{-1}A)$, $A\in\mathcal{E}$ is called the distribution of $X$. Let $T$ be an arbitrary set, and for each $t\in T$, let $X_{t}$ be a random variable. The collection of random variables $\{X_{t}:t\in T\}$ on $(\Omega,\mathcal{F})$ is a stochastic process.

Let $\mathscr{H}$ denote the Hilbert space of real-valued functions $f:\mathcal{X}\rightarrow\mathbb{R}$ on $\mathcal{X}$ equipped with the inner product $\langle\cdot,\cdot\rangle_{\mathscr{H}}$ and the induced norm $\lVert\cdot\rVert_{\mathscr{H}}$.

Alternatively, by the Moore-Aronszajn theorem (Aronszajn, 1950), for any positive definite kernel function $K$, there exists a unique RKHS $\mathscr{H}$ with $K$ as its reproducing kernel, where $\mathscr{H}$ is the closure of the linear span of functions $\{K(x,\cdot)\}$. In other words, the Moore-Aronszajn theorem allows us to define a kernel function and obtain a corresponding RKHS.

Let $K:\mathcal{X}\times\mathcal{X}\rightarrow\mathbb{R}$ be the reproducing kernel function for the RKHS $\mathscr{H}$ on $\mathcal{X}$. We stipulate that the kernel also satisfies the conditions for being a completely separating kernel. This property ensures that the kernel function can be used to learn the support of any probability measure on $\mathcal{X}$. We induce a metric $d_{K}$ on $\mathcal{X}$ via the kernel function $K$,

which is known as the kernel-induced metric on $\mathcal{X}$, and is equivalent to the Euclidean metric if $K$ is completely separating and continuous. Following De Vito et al. (2014), we define the notion of $\mathscr{H}$ separating a subset $C\subset\mathcal{X}$.

According to Theorem 3.2, we need to determine the existence of a function in $\mathscr{H}$ that acts as a classifier for a subset $C\subset\mathcal{X}$. Since the functions $f\in\mathscr{H}$ have the form $f=\sum_{i}\alpha_{i}K(x_{i},\cdot)$, this amounts to choosing a kernel function which exhibits the separating property. Note that not all kernel functions can separate every subset $C\subset\mathcal{X}$. In order to ensure that this is possible, the notion of completely separating kernels is defined.

For example, with $\mathcal{X}=\mathbb{R}^{n}$, the Abel kernel $K(x,x^{\prime})=\exp(-\lVert x-x^{\prime}\rVert_{2}/\sigma)$, where $\sigma>0$, is a completely separating kernel function (De Vito et al., 2014, Proposition 5). Thus, by properly selecting the kernel function $K$, we ensure that we can classify any subset $C\subset\mathcal{X}$.

We now turn to a discussion of the classifier $F$ in (3). The following theorems are reproduced with modifications for simplicity from De Vito et al. (2014), and ensure we can define $\mathscr{F}(x_{0})$ as the support of $x_{N}$, and that (3) holds.

For any subset $C\subset\mathcal{X}$, let $\mathscr{H}_{C}$ denote the closure of the linear span of functions $\{K(x,\cdot)\,|\,x\in C\}$, and define $P_{C}:\mathscr{H}\rightarrow\mathscr{H}$ as the orthogonal projection onto the closed subspace $\mathscr{H}_{C}$. Define the function $F_{C}:\mathcal{X}\rightarrow\mathbb{R}$ such that $F_{C}(x):=\langle P_{C}K(x,\cdot),K(x,\cdot)\rangle_{\mathscr{H}}$. Using this definition, we can now define the support $\mathscr{F}(x_{0})$ in terms of a function $F$.

Thus, we aim to learn the forward reachable set (3) by identifying a function $F\in\mathscr{H}$ that separates the support in $\mathcal{X}$.

For all examples, we choose an Abel kernel $K(x,x^{\prime})=\exp(-\lVert x-x^{\prime}\rVert_{2}/\sigma)$, $\sigma>0$. We chose the parameters to be $\sigma=0.1$, $\tau$ according to (11), and $\lambda=1/M$, where $M$ is the sample size used to construct the classifier. As noted in De Vito et al. (2014), $\sigma$ can be chosen via cross-validation and we require that $\lambda$ be chosen such that $\lim_{M\rightarrow\infty}\lambda=0$. Numerical experiments were performed in Matlab on an AWS cloud computing instance, and computation times were obtained using Matlab’s Performance Testing Framework. Code to reproduce the analysis and all figures is available at: \urlhttps://github.com/unm-hscl/ajthor-ortiz-L4DC2021

We presented a method for computing forward reachable sets using reproducing kernel Hilbert spaces with separating kernel functions. We demonstrated the effectiveness of the technique at performing neural network verification, and validated its accuracy on a satellite rendezvous and docking problem with Clohessy-Wiltshire-Hill dynamics. This technique is scalable, computationally efficient, and model-free, making it well-suited for systems with learning-enabled components. We plan to investigate extension of this to other reachability problems, such as safety problems that require calculation of the backward reachable set.

This material is based upon work supported by the National Science Foundation under NSF Grant Number CNS-1836900. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. This research was supported in part by the Laboratory Directed Research and Development program at Sandia National Laboratories, a multimission laboratory managed and operated by National Technology and Engineering Solutions of Sandia, LLC., a wholly owned subsidiary of Honeywell International, Inc., for the U.S. Department of Energy’s National Nuclear Security Administration under contract DE-NA-0003525. The views expressed in this article do not necessarily represent the views of the U.S. Department of Energy or the United States Government.