# Safe Reach Set Computation
via Neural Barrier Certificates

Alessandro Abate  Sergiy Bogomolov  Alec Edwards  Kostiantyn Potomkin  Sadegh
Soudjani  Paolo Zuliani  University of Oxford, Oxford, UK  Newcastle
University, Newcastle, UK  Max Planck Institute for Software Systems, Germany
Università di Roma “La Sapienza”, Rome, Italy

###### Abstract

We present a novel technique for online safety verification of autonomous
systems, which performs reachability analysis efficiently for both bounded and
unbounded horizons by employing neural barrier certificates. Our approach uses
barrier certificates given by parameterized neural networks that depend on a
given initial set, unsafe sets, and time horizon. Such networks are trained
efficiently offline using system simulations sampled from regions of the state
space. We then employ a meta-neural network to generalize the barrier
certificates to state-space regions that are outside the training set. These
certificates are generated and validated online as sound over-approximations
of the reachable states, thus either ensuring system safety or activating
appropriate alternative actions in unsafe scenarios. We demonstrate our
technique on case studies from linear models to nonlinear control-dependent
models for online autonomous driving scenarios.

###### keywords:

reachability, safety, soundness, barrier certificates, neural networks,
verification, control, online autonomous systems

††thanks: Sergiy Bogomolov, contributing author, deceased in 2023.

##  1 Introduction

Reachability analysis, _i.e.,_ determining the regions of the state space the
temporal dynamics of a system eventually enters, is crucial for establishing
safety of a system. Unfortunately, this problem is in general undecidable
except for a restricted class of linear dynamical models (Alur et al., 1993;
Henzinger et al., 1998). Furthermore, algorithmic solutions for sound
relaxations of the problem (Fränzle et al., 2019) typically suffer from either
the “curse of dimensionality” (exceeding time/space complexity with respect to
system size) or limited practical utility (very coarse over-approximations
returning too many “false alarms”). One reason is because many reachability
techniques require the explicit computation of the system dynamics, which most
often entails integrating ordinary differential equations (ODEs). Symbolic
integration is restricted to limited cases of ODEs, and in general numerical
integration is hard – solving Lipschitz continuous ODEs over compact domains
is a PSPACE-complete problem (Kawamura, 2009).

Inductive methods for reachability offer an alternative approach in which one
looks for a barrier certificate (Tiwari, 2003; Prajna and Jadbabaie, 2004), a
function of the system state whose zero-level set separates the “unsafe”
region from the system trajectories that start from a given initial set. The
existence of a barrier certificate entails that the system is safe. Three
advantages of barrier certificates are that they can establish safety: 1) over
infinite time horizons, 2) for systems with nonlinear dynamics, and 3)
uncertain inputs or parameters. Reachability methods that offer some or all of
these advantages do exist, but are usually computationally expensive. In
contrast, checking that a candidate function is indeed a barrier certificate
can be done in many cases efficiently and automatically. However, finding
barrier certificates is much harder, and this is a disadvantage of the
approach.

In this work, we provide a novel approach to synthesize, via barrier
certificates, sound over-approximations of reach sets for dynamical systems,
whether linear or non-linear, possibly under control inputs. We go beyond
establishing safety by computing valid over-approximations without explicitly
solving the system dynamics. We devise a two-level technique which utilizes
neural networks as efficient emulators of both the system dynamics and barrier
certificates. Since barrier certificate candidates are efficiently generated
via neural networks, our approach enables online computation of reach sets
after appropriate offline training. Key to our approach is a meta-neural
network MetaNN that generalizes barrier certificates over varying initial and
unsafe sets. We use FOSSIL (Abate et al., 2021) as the underlying generator of
example barrier certificates with correctness guarantees. We note that FOSSIL
does not scale to online use due to the intrinsic complexity of the algorithms
implemented – this motivates the introduction of our MetaNN. The overall
soundness of our approach is guaranteed by utilizing Satisfiability Modulo
Theories (SMT) solvers for checking candidate barrier certificates.

We show that our approach successfully generates sound over-approximations of
reach sets of linear and non-linear systems. The efficiency of reach-sets
generation is demonstrated in an online autonomous driving scenario. Our
approach not only extends the capabilities of barrier certificate verification
to the synthesis of parameterized controllers, but also increases the success
rate of online barrier certificate generation from $78\%$ to $99\%$ compared
to direct application of FOSSIL (at a cost of 10 hours of offline training on
a standard laptop).

To summarize, the contributions of this paper are:

  * •

We show that level sets of barrier certificates can be used to over-
approximate reach sets.

  * •

We consider barrier certificates as functions of initial and unsafe sets and
use them for reach set computations.

  * •

We provide a computational framework that fixes parameterized templates for
initial and unsafe sets and computes a MetaNN as generator of barrier
certificates.

  * •

We employ offline training and fast online validation and execution that
increase the success rate of generating barrier certificates for safe online
autonomous driving.

Related Work. Verifying safe behavior of autonomous systems is an important,
timely topic which is receiving much attention from the research community
(Fisher et al., 2021). In particular, one area of interest include the
synthesis of provably safe controllers for autonomous systems (_e.g.,_(Fan et
al., 2020; Johnson et al., 2016)) possibly featuring machine learning
components, such as controllers based on neural networks (Ivanov et al.,
2020a, b), reinforcement learning (Tran et al., 2019; Kazemi and Soudjani,
2020), data-driven model predictive control (Rosolia and Borrelli, 2018), or
subject to perceptual uncertainty (Jha et al., 2018).

Barrier certificates, first introduced by Prajna (2006), can be used to
certify safety of dynamical systems. The computations rely on convex
optimization and hence can result in solutions which are numerically sensitive
and unsound. A recent approach aims at synthesizing weaker barrier
certificates using bilinear matrix inequalities (Wang et al., 2021), while the
work by Ames et al. (2017) seeks to include performance requirements in
barrier certificates. Usage of counter-examples within a counter-example
guided inductive synthesis (CEGIS) framework is a powerful and common approach
for synthesizing barrier certificates (Ahmed et al., 2021; Abate et al., 2021;
Heersink et al., 2021; Ratschan, 2017; Samari et al., 2024). Learning barrier
certificates using data is also studied in (Nejati et al., 2023) for
deterministic systems and in (Schön et al., 2024) for stochastic systems.
Neural networks are utilized to synthesize barrier certificates, _e.g.,_ in
the works by Jin et al. (2020) and Zhao et al. (2020, 2021a, 2021b). However,
these approaches are either unsound (Jin et al., 2020), or limited to the
usage of ReLU-based activation functions. The paper by Srinivasan et al.
(2020) is close in spirit to our approach, although it uses support vector
machines and is limited to a specific class of systems (affine control robotic
systems), while we do not pose such restrictions. Our proposed framework may
leverage any tool that generates certified barrier certificates. We employ
FOSSIL (Abate et al., 2021) due to its ability to provide training data
(_i.e.,_ example barrier certificates) with correctness guarantees.

##  2 Preliminaries

Feed-Forward Neural Networks. Consider a network $\mathcal{N}$ with $h_{0}$
input neurons, $k$ hidden layers each with $h_{1},\ldots,h_{k}$ neurons and an
output layer of $h_{k+1}$ neurons. We consider each layer to be fully
connected and denote the corresponding weight matrix for the $i$-th layer as
$W_{i}$ and bias vector as $b_{i}$ for $i=0,\ldots,k+1$, where $i=0$ denotes
the input layer and $i=k+1$ the output layer. Each hidden layer $i$ has a
corresponding activation function $\sigma_{i}:\mathbb{R}\to\mathbb{R}$ such
that the output of the $i$-th layer is given by
$z_{i}=\sigma_{i}(W_{i}z_{i-1}+b_{i})$.

Barrier Certificates. We are interested in the safety verification of
autonomous systems. Consider a dynamical system modelled by

$\frac{d}{dt}x(t)=f(x(t)),\quad t\in\mathbb{R}_{\geq 0},$ (1)

with system state $x\in\mathcal{X}\subseteq\mathbb{R}^{n}$ and vector field
$f:\mathcal{X}\rightarrow\mathbb{R}^{n}$. The differential equation (1) has a
unique, continuous solution from any initial state $x(0)=x_{0}\in\mathcal{X}$
under standard Lipschitz continuity of the vector field $f(\cdot)$.

###### Definition 1

Given an initial set $\mathcal{X}_{0}\subseteq\mathcal{X}$ and an unsafe set
$\mathcal{X}_{u}\subseteq\mathcal{X}$, the system (1) is called safe if all
trajectories starting from any initial state $x_{0}\in\mathcal{X}_{0}$ do not
enter the unsafe set $\mathcal{X}_{u}$.

###### Definition 2

Given an initial set $\mathcal{X}_{0}$ and unsafe set $\mathcal{X}_{u}$, a
function $B:\mathcal{X}\rightarrow\mathbb{R}$ is called a barrier certificate
for the system (1) if it satisfies

$\displaystyle B(x)\leq 0\ \forall x\in\mathcal{X}_{0}\text{ and }B(x)>0\
\forall x\in\mathcal{X}_{u},$ (2) $\displaystyle\frac{\partial B(x)}{\partial
x}f(x)<0,\ \forall x\in\mathcal{X}\ s.t.\ B(x)=0.$

###### Theorem 2.1

(Prajna and Jadbabaie, 2004; Prajna et al., 2007) Given the initial set
$\mathcal{X}_{0}$ and unsafe set $\mathcal{X}_{u}$, the system (1) is safe if
there exists a barrier certificate $B(\cdot)$ satisfying the conditions (2).

The characterization of a barrier certificate $B$ relies on its Lie
derivative, which appears in the last requirement of (2). The Lie derivative
of a continuously differentiable scalar function $B$ with respect to a vector
field $f$ is

$\dot{B}(x)=\nabla B(x)\cdot f(x)=\sum_{i=1}^{n}\frac{\partial B}{\partial
x_{i}}f_{i}(x),$ (3)

where $x_{i}$ is the $i^{\text{th}}$ element of the state:
$x=(x_{1},x_{2},\ldots,x_{n})$. The Lie derivative describes how the value of
the barrier certificate varies along the flow of $f$, namely along
trajectories of the model. Indeed, if we consider a trajectory $x(t)$, with
$x(0)\in\mathcal{X}_{0}$, and the value of $B(x)$ along this trajectory, the
first condition ensures $B(x(0))\leq 0$. The condition on the Lie derivative
then guarantees that the evolution of $x(t)$ cannot make $B(x)$ become
positive, and hence $x(t)$ cannot enter $\mathcal{X}_{U}$ (where $B(x)$ is
positive).

Sound Synthesis of Barrier Certificates. Our proposed framework is applicable
to any technique that generates sound barrier certificates. We employ the
FOSSIL tool (Abate et al., 2021), which uses a CEGIS loop that consists of two
complementary components: the learner and the verifier. The learner is a
neural network, of which the structure and characteristics (_i.e.,_ layers and
activation functions) can be selected freely within the tool. This flexibility
allows for the construction of reach sets of varying structural complexity.
The verifier is an SMT-solver that can check the satisfiability of formulae
over the real numbers. It provides correctness guarantees of the candidate
barrier certificates proposed by the learner, or alternatively returns
counter-examples to the learner: these are points within the region of
interest where the candidate barrier certificate is invalid. This is achieved
by checking the satisfiability of the negation of the conditions in (2).
FOSSIL leverages two choices of SMT-solvers: Z3 (de Moura and Bjørner, 2008),
which is limited to reasoning over polynomial functions, and dReal (Gao et
al., 2013), which can handle general nonlinear functions.

##  3 Barrier Certificates for Reach Sets

Barrier certificates demonstrate the existence of an invariant set in the
vector field $f$, via the final condition of (2). Meanwhile the first two
conditions ensure that our initial set lies within this invariant set and that
our unsafe set does not. Notably, any invariant set containing our initial set
must be a true overapproximation of the reachable set from the initial set.
This is our first contribution and is stated formally next as a corollary of
Theorem 2.1.

Simulation engine MetaNN Verifier (SMT solver)
$BC$$\mathcal{X}_{u}$$\mathcal{X}_{b}$FOSSILTraining
data$\begin{array}[]{l}BC\\\ \text{cand.}\end{array}$$\mathcal{X}_{0}$
Simulation engine $\mathcal{X}_{b}$ Generate training samples
$\displaystyle\mathcal{X}_{0}$
TrainingDeployment$\mathcal{X}_{u}$$\displaystyle\mathcal{X}_{0}$ Figure 1:
The proposed framework has two phases: (i) a training phase (top) where the
training data is prepared and the MetaNN is trained; and (ii) a deployment
phase (bottom) where sound reach sets are generated via neural barrier
certificates. $\mathcal{X}_{0}=$ initial set; $\mathcal{X}_{u}=$ unsafe set;
$\mathcal{X}_{b}=$ working region; $BC$= barrier certificate.

###### Corollary 3.1

Define $\mathcal{R}$ to be the set of states reachable from the initial set
$\mathcal{X}_{0}$ under the dynamics (1). Assume $B(x)$ is a barrier
certificate satisfying the conditions of Definition 2. Then, the set
$\mathcal{R}_{o}=\\{x\in\mathcal{X}\,|\,B(x)\leq 0\\}$ gives an over-
approximation of $\mathcal{R}$, _i.e.,_ $\mathcal{R}\subseteq\mathcal{R}_{o}$.

Barrier certificates can also be used to study the safety of dynamical systems
when their trajectories are restricted to a subset of the state space called a
_working region_. This is formally stated next and will be relevant in our
case study on safe autonomy.

###### Theorem 3.1

Consider a working region $\mathcal{X}_{b}\subseteq\mathcal{X}$, the initial
set $\mathcal{X}_{0}\subseteq\mathcal{X}_{b}$, and unsafe set
$\mathcal{X}_{u}\subseteq\mathcal{X}$. If a function
$B:\mathcal{X}\rightarrow\mathbb{R}$ satisfies the following conditions:

$\displaystyle B(x)\leq 0\ \forall x\in\mathcal{X}_{0},\,\,B(x)>0\ \forall
x\in\mathcal{X}_{u}\cap\mathcal{X}_{b},$ $\displaystyle\frac{\partial
B(x)}{\partial x}f(x)<0,\ \forall x\in\mathcal{X}_{b}\ s.t.\ B(x)=0,$ (4)

then the trajectories of (1) evolve inside
$\mathcal{R}_{b}:=\\{x\in\mathcal{X}_{b}\,|\,B(x)\leq 0\\}$ before leaving the
working region $\mathcal{X}_{b}$.

Theorem 3.1 entails that we can use $\mathcal{R}_{b}$ as an over-approximation
of the reach set when trajectories are restricted to $\mathcal{X}_{b}$.

##  4 Computation of Safe Reach Sets

We utilize machine learning techniques and barrier certificate properties to
efficiently compute sound reachable sets for the system modeled by (1). Given
an initial region $\mathcal{X}_{0}$ as an input we seek a barrier certificate
as an output. By parameterizing the initial set (_e.g.,_ as vertices of a box)
and the barrier certificate (_e.g.,_ as coefficients of a polynomial), we can
train a neural network to provide barrier certificates for any general initial
set.

We present schematically our algorithm in Fig. 1, which consists of two
phases. The first stage is _training_ , and consists of training the MetaNN to
generalize the computation of barrier certificates from initial sets. The
generation of training data for this phase will be discussed shortly.

The second phase of our approach is _deployment_. Here we tap onto the MetaNN
to generate reachable sets for a given initial set, by providing a candidate
barrier certificate. This candidate is checked for validity using an SMT-
solver. If the candidate barrier certificate is valid, then we have
successfully computed a safe reachable set. Otherwise, we can use the counter-
example generated by the SMT solver to _refine_ the training of the MetaNN.

###### Remark 1

The framework presented in Fig. 1 is underpinned on the continuity properties
of the system trajectories with respect to its initial state. The problem of
barrier certificate synthesis may be seen as a (continuous) function of this
initial set $\mathcal{X}_{0}$, with similar certificates existing for similar
initial sets. The MetaNN generalizes by learning over a dataset of barrier
certificates.

Simulation engine MetaNN Verifier (SMT solver) Base Controller
$\left[\text{control inputs}\right]$$\begin{array}[]{l}BC\\\
\text{cand.}\end{array}$$\mathcal{X}_{u}$$\mathcal{X}_{b}$$\mathcal{X}_{0},\
{\color[rgb]{0.82,0.01,0.11}\definecolor[named]{pgfstrokecolor}{rgb}{0.82,0.01,0.11}\mathcal{X}_{u}}$
Safe controller isSafefalsetruetimeout$\left[\text{control inputs}\right]$
STOP $\mathcal{R}_{b}$ Figure 2: Structure of online safe planning scheme. The
base controller (yellow) operates in normal conditions, while the safe
controller (purple) is activated to avoid unsafe regions in case of potential
hazard. The MetaNN is already trained. The Verifier checks the barrier
certificate (BC) candidate and calls the safe controller in case the result is
unsafe. Then the process of generating a BC candidate and running the
simulation engine repeats and the new candidate is checked. If the system is
unsafe or the MetaNN fails to generate a valid BC within the time bound the
system stops.

We now discuss each part of our framework in more detail.

###  4.1 Simulation Engine

If the model dynamics are unstable the set of reachable states $\mathcal{R}$
is unbounded, which a barrier certificate cannot represent. To alleviate this,
we construct a compact working region $\mathcal{X}_{b}$, as in Thm. 3.1. Given
an initial set $\mathcal{X}_{0}$ (a hyperbox), the simulation engine generates
a working region for it. We simulate trajectories from the vertices of the
initial set and a random sample of points inside of it. Then we take the
convex hull of the generated trajectories, and take an octagonal over-
approximation of the generated convex hull. This provides a working region
$\mathcal{X}_{b}$ that corresponds to $\mathcal{X}_{0}$.

The working region generated by the simulation engine is key to both the
_training phase_ and the _deployment phase_.

Training Phase. The working region is used to calculate the unsafe set as
$\mathcal{X}_{u}=\mathcal{X}\setminus\mathcal{X}_{b}$. This unsafe set is
necessary to generate barrier certificate training data using FOSSIL.

Deployment Phase. The working region is intersected with the sub-zero level
set of the candidate barrier certificate to obtain the candidate reach set.
Note that this means safety guarantees only hold while trajectories stay in
the bounding box.

###  4.2 Training of the MetaNN

Let $\mathcal{X}_{0}$ denote initial sets represented as parameterized boxes
and $a\in\mathbb{R}^{d}$ the coefficients of a barrier certificate, $B(a,x)$,
for a given template with $d$ terms. For example, if the template is a
polynomial then $a$ represents the coefficients of the polynomial. For each
initial set, we compute a corresponding unsafe set $\mathcal{X}_{u}$ as
described previously, which represents the non-reachable region of the state
space. We seek to learn a mapping from $\mathcal{X}_{0}$ to $a$, _i.e.,_
MetaNN should be able to generate barrier certificates that represent the
reach sets of the system.

Computing safe reach sets. We compute (the over-approximation of) the safe
reachable region $\mathcal{R}_{b}$ in four steps, as illustrated in Fig. 3.
First, we run multiple simulations from the initial set $\mathcal{X}_{0}$.
Second, we construct from simulation traces the working region
$\mathcal{X}_{b}$ and octagon approximation. Next, we bloat the octagon region
by a factor $\varepsilon$, and pass its complement $\mathcal{X}_{u}$ to
FOSSIL, along with $\mathcal{X}_{0}$. Once we obtain a valid barrier
certificate from FOSSIL, we intersect it with the working region $X_{b}$.
Whenever FOSSIL cannot produce a valid barrier certificate for the provided
$X_{b}$, we further bloat the working region and call FOSSIL again. We repeat
this until a certificate is found or until a specified maximal bloating level
is reached, in which case the system is deemed to be locally unsafe.

Figure 3: Four-step construction of a safe reach set $R_{b}$. From the left-
hand side: Step 1. Running simulations from the initial set $X_{0}$. Step 2.
Computation of the octagonal over-approximation of the simulations. Step 3.
Bloating of the octagonal over-approximation. Step 4. Computation of reachable
set $R_{b}$.

Training Data Generation. We start by generating with FOSSIL a barrier
certificate $B(a,\cdot)$ for each pair $(\mathcal{X}_{0},\mathcal{X}_{u})$,
and by storing the coefficients $a$ of the barrier certificate, which will be
our training data. Once trained, the MetaNN should map an initial set to a set
of coefficients for which the barrier certificate results in a set
$\mathcal{R}_{b}$ such that $\mathcal{R}\subseteq\mathcal{R}_{b}$, _i.e.,_ an
over-approximation of the true reach set.

The barrier certificate generation in FOSSIL uses neural network templates.
FOSSIL initializes weights and biases of the neural network template randomly,
which are then guided to a solution using gradient descent. Since the training
can be done by sequentially moving the initial set gradually and iteratively
through the state space, we can utilize this to find more useful training
data. Specifically, we ‘seed’ the parameters of the next initialization using
the parameters of the most recent solution. In other words, we begin searching
for the next barrier certificate from the previous one. The advantage of this
seeding is twofold. First, it reduces the amount of computation required to
generate the training data by improving the performance of FOSSIL since we
start closer to a valid certificate. Second, it allows us to take advantage of
potential continuity results when generalizing over a function space. Many
barrier certificates may exist for a given initial set and template. While the
resulting functions may be structurally similar, the corresponding
coefficients may not be, making generalization more difficult. This seeding
approach encourages congruous barrier certificates representations, which in
turn enhances the ability of MetaNN to generalize over the function space. If
at any point we fail to find a barrier certificate for a given initial set, we
simply use the most recent solution to ‘seed’ the next attempt.

For a given data point consisting of an initial set $\mathcal{X}_{0}$ and a
barrier certificate representation $a$, it is reasonable to assume that other
valid barrier certificate representations exist near (in the Euclidean sense)
to $a$. Thus, we can generate additional data points for a fixed initial set
by perturbing the representation $a$ with multiplicative noise as
$\tilde{a}=a\cdot c$, where $c\sim N(1,\sigma^{2})$ and $N$ is a normal
distribution with unit mean and variance $\sigma^{2}$. Then, we can verify
whether the new barrier certificate constructed from $\tilde{a}$ is also a
valid barrier certificate for the given initial set and corresponding unsafe
(unreachable) region. If so, the generated barrier certificate can be added to
the training dataset. If $\sigma$ is sufficiently large this will provide
meaningful additional data to the training procedure.

Loss function and Network Structure. MetaNN is a ReLU network trained using
gradient descent with an L1 loss function, can be expressed as

$\mathcal{L}=\frac{1}{n_{d}}\sum_{i=i}^{n_{d}}|a_{i}-\mathcal{N}(\mathcal{X}_{0_{i}})|,$
(5)

where $|\cdot|$ denotes the absolute value, $n_{d}$ is the number of data
points, $\mathcal{X}_{0}$ are input sets and $a$ is the output of the network
representing the barrier certificate coefficients.

Online safe planning. Our approach can be implemented online, safe planning
over bounded time horizons, as depicted in Fig. 2. The online phase of our
approach is embedded in a loop that provides control inputs and iteratively
checks for system safety. The loop uses two controllers: a ‘base’ controller
for normal use and a ‘safe’ controller which takes over in emergency
situations. The base controller provides inputs to control the system over a
short time horizon; such inputs and the current system state are used to
compute a candidate reach set. This is passed to the SMT solver, which decides
whether the system is safe (for the current time horizon), _i.e.,_ whether the
computed reach set and the unsafe set do not intersect. If the SMT solver
cannot guarantee an empty intersection, then the safe controller is activated
and will provide input controls for the current time horizon. However, if the
verifier cannot guarantee the system is safe even for the input from the safe
controller, then the system stops. Otherwise, the inputs provided by the base
controller are applied to the actual system, and the loop repeats for the next
time horizon. In the current implementation, to generate an initial set for
the next time horizon we use a center trajectory as the dynamics of the
system. Any trajectory can be used instead and it does not affect the
soundness of the algorithm. In addition, we bloat around the last state of the
trajectory to account for sensing errors of real-world models.

##  5 Simulation Results

In this section, we apply our framework for the computation of safe reach sets
on a number of linear and nonlinear autonomous models. Then, we present the
application in an autonomous driving setup. We have implemented our algorithms
in Julia, using the LazySets package of JuliaReach (Bogomolov et al., 2019)
for set operations and the DifferentialEquations.jl package to perform
simulations, the PyCall.jl111https://github.com/JuliaPy/PyCall.jl package to
call FOSSIL and dReal. We utilize PyTorch with CUDAt to train the MetaNN.

For all case studies, we use a second-order polynomial as a template for the
barrier certificate.

Validation for linear systems. We performed the data generation and MetaNN
training steps described in the previous section for two linear systems.

Next, we validated the reliability of our approach at generating safe reach
sets for a separate test dataset. The test dataset is composed of input-output
pairs $(\mathcal{X}_{0},a)$, where $\mathcal{X}_{0}$ are input sets and $a$
are the coefficients of a barrier certificate for a candidate reach set. The
validation consists in certifying whether the set
$\mathcal{R}_{b}=\\{x\in\mathcal{X}_{b}|B(x)\leq 0\\}$ constructed using the
candidate certificate computed by MetaNN is in fact a correct over-
approximation of the true reach set. This is equivalent to checking whether
the candidate barrier certificate is valid within the working region, for the
given initial set and an empty unsafe set. This can be achieved by asking an
SMT-solver to seek a counterexample for the barrier certificate’s validity. If
no counterexample is found, this is a successful output of the MetaNN. Our
validation consists of finding the percentage of successful outputs obtained
over the test inputs.

####  5.0.1 Linear system with real eigenvalues

We first consider a simple linear system with real eigenvalues:

$\begin{cases}\frac{d}{dt}x(t)=-x,&x(0)=x_{0}\\\ \frac{d}{dt}y(t)=-2\cdot
y,&y(0)=y_{0}.\\\ \end{cases}$ (6)

An example barrier certificate generated for this model is shown in Fig. 4. We
train and test the MetaNN on different initial sets of different size, but
within the same specified domain. The test data consist of 1000 randomly
sampled initial sets of random size. The proportion of successful outputs over
the test dataset is 99.3%.

####  5.0.2 Linear system with complex eigenvalues.

Next, we consider a linear system with complex eigenvalues:

$\begin{cases}\frac{d}{dt}x(t)=y,&x(0)=x_{0}\\\ \frac{d}{dt}y(t)=-0.2\cdot
x-0.2\cdot y,&y(0)=y_{0}.\\\ \end{cases}$ (7)

A sample barrier certificate generated for this model is shown in Fig. 4.
Similarly to the previous model, we have trained a MetaNN, and the correctness
of the obtained neural barrier certificates is 99.2% over 1000 randomly
sampled initial sets of random size.

(a) Linear system with real eigenvalues.

(b) Linear system with complex eigenvalues.

Figure 4: Safe reach sets for the linear systems with real (6) and complex (7)
eigenvalues. The red traces are simulation trajectories. The inner and outer
octagons are, respectively, the convex hull of the generated trajectories, and
its over-approximation. The yellow rectangle is a bounding box. The black
ellipsoid is the zero level-set of the validated barrier certificate.

Online safe path planning for nonlinear vehicle dynamics. Consider

$\begin{cases}\frac{d}{dt}x(t)=v\cos\theta(t),&x(0)=x_{0}\\\
\frac{d}{dt}y(t)=v\sin\theta(t),&y(0)=y_{0}\\\
\frac{d}{dt}\theta(t)=\omega,&\theta(0)=\theta_{0},\\\ \end{cases}$ (8)

where $(x,y)$ indicate the location in two-dimensional space and $\theta$ is
an angle describing the orientation of the car. We assume that the velocity
$v$ and the rotational speed $\omega$ are inputs that are selected by a
feedback controller.

We seek to design $v$ and $\omega$ such that the car, starting from an initial
region, will reach a target region $\mathcal{X}_{r}$, while avoiding obstacles
that are present over the $(x,y)$ domain. Here, we consider obstacles as
static boxes, however the online implementation of our approach can in
principle also handle dynamically-changing obstacles. We emphasize that the
control inputs ought to be executed in a provably safe manner, with sound
certificates.

The literature in path planning is mature but it generally neglects the
dynamics of the vehicle, and most often does not come with formal safety
guarantees. We show that we can first neglect the obstacles and design a
baseline controller for steering the dynamics from the initial set to the
target region $\mathcal{X}_{r}$. We then show how the scheme presented in Sec.
4 can be used to provide sound safety guarantees on the executed control
inputs.

We have designed the following baseline controller for reaching the target:

$\begin{cases}v(t)=\alpha_{1}\left(1-\exp(-\alpha_{2}\|(x(t)-x_{r},y(t)-y_{r})\|_{2})\right)\\\
\omega(t)=\alpha_{3}(\theta_{r}(t)-\theta(t))\\\
\theta_{r}(t):=\arctan\left(\frac{y(t)-y_{r}}{x(t)-x_{r}}\right),\end{cases}$

where $(x_{r},y_{r})\in\mathcal{X}_{r}$ is a reference point within the target
region and $\theta_{r}(t)$ is the relative angle between current and target
location. The angular speed $\omega(t)$ is designed to steer the car from the
current orientation towards the reference angle. The speed is also
proportional to the distance from the reference point passed through an
exponentially decaying function, thus slowing down the vehicle when
approaching the reference point. Note that this simple controller can be
replaced with any path planning algorithm that can be synthesized over (8).

The above baseline controller does not consider obstacles and does not come
with any safety guarantees. These desirable features can be attained with our
safe reach set approach. First, let us note that the dynamics in (8) admit two
structural properties that are useful in the computation of barrier
certificates. While these properties are not specifically required by our
approach, they can be leveraged to reduce the computational burden.

Property 1. The dynamics are shift invariant with respect to location $(x,y)$
for fixed control inputs $(v,\omega)$: if $(x(t),y(t),\theta(t))$ is a
solution from an initial condition $(x_{0},y_{0},\theta_{0})$, then
$(x(t)-x^{\prime},y(t)-y^{\prime},\theta(t))$ is a solution from the initial
condition $(x_{0}-x^{\prime},y_{0}-y^{\prime},\theta_{0})$. This means the
computation of barrier certificate can always be done for initial sets that
are centered at the origin $(0,0)$.

Property 2. The dynamics are symmetric with respect to the $x$-axis. If
$(x(t),y(t),\theta(t))$ is a solution from an initial condition
$(x_{0},y_{0},\theta_{0})$ with fixed control inputs $(v,\omega)$, then
$(x(t),-y(t),-\theta(t))$ is a solution from the initial condition
$(x_{0},-y_{0},-\theta_{0})$ with fixed control inputs $(v,-\omega)$. This
means we can restrict the computations to $\omega\geq 0$.

(a) Reachable sets for a total time horizon $T=20$ along with unsafe
occurrences at step 2 and step 7; the car starts in the top-right corner.

(b) Original unsafe control (top) along with the safe control (bottom) for
step 2.

Figure 5: Plot of the trajectory of the autonomous driving case study for
$T=20$. Each block corresponds to $T_{r}=2$. Red traces correspond to
trajectories which lead to unsafe region. Green trajectories are safe. Red
sets represent unsafe regions. Black curves are zero-level set of barrier
certificates.

We choose the values $\alpha_{1}\\!=\\!0.2$, $\alpha_{2}\\!=\\!3.54$, and
$\alpha_{3}\\!=\\!0.06$ for the baseline controller, and train MetaNN over the
domain $v\in[1.5;10],\ \omega\in[0;0.125]$ and $\theta\in[0;6.5]$ by
generating 5414 valid barrier certificates. The trained MetaNN gives a 99.5%
correctness over 1000 randomly sampled initial sets of random size. It takes
20 minutes to train the model with CUDA (NVIDIA GeForce RTX 3060 Laptop GPU)
for 750000 epochs. Fig. 5 shows the trajectories of the car over a time
horizon $T=20$ in which safe reachability is computed every $T_{r}=2$, thus
corresponding to ten iterations of the procedure in Fig. 2.

Online Certification of Safe Reach Sets. We now study online correctness
guarantees for the safe reach sets constructed by the procedure. We wish to
provide a guarantee that for a chosen control action, the vehicle does not
collide with an obstacle over some fixed horizon. Note that, as per Theorem
3.1, any such guarantee is conditional on the vehicle remaining within the
working region $\mathcal{X}_{b}$: if the vehicle leaves this region within the
time horizon our approach can no longer guarantee safety.

This certification check involves asserting that the function constructed from
the output of MetaNN, which we denote as $B(x)$, is a valid barrier
certificate. Define the unsafe set $\mathcal{X}_{u}$ as the union of all box-
shaped obstacles. The initial set $\mathcal{X}_{0}$ is a box containing the
vehicle’s true location. The size of this initial set accounts for the
uncertainty in the location of obstacles, and to take care of the change in
location of the vehicle that occurs during the computation time allocated to
the generation of the safe reach sets: this vouches for the online
implementation of our scheme. Finally, the working region $\mathcal{X}_{b}$ is
computed as in Sec. 3. Due to the trigonometric terms present in the system
dynamics (8), dReal is a suitable choice of SMT solver.

We report in Figs. 5 an example of the control action that would result in
unsafe behavior, and its resolution. For cases when the dynamics leads to the
unsafe region we use the same controller to avoid obstacles. We exploit the
unsafe state as the target region and take a complement of the output angular
speed to steer away. We note that each iteration of the algorithm (see Fig. 2)
takes about $0.03$ seconds to execute on a standard laptop for $T_{r}=2$.

If dReal is unable to find a counter-example, the reach set is certified as
being a safe over-approximation of the true reach set, and can safely proceed
with the control action over the time horizon. Meanwhile, the existence of a
counter-example does not imply that our control action is inherently
dangerous, but rather that we cannot assert that it is safe. Our immediate
response, as depicted in Fig. 5, is to select a different control input to
attempt to steer the car safely.

Comparison with Direct Online Certification of Safe Reach Sets. As
demonstrated with the car model case study, our proposed MetaNN enables us to
perform controller synthesis together with online certification. In order to
compare the performance of the MetaNN vs. FOSSIL, we take the same controller
synthesized by the MetaNN and give it directly to FOSSIL for online
certification. Figure 6 demonstrates the cumulative distribution of the
computational time taken to synthesize 100 barrier certificates directly by
FOSSIL. Note, that for the car model under consideration we utilize $T_{r}=2$,
which means if the barrier certificate is not computed within 2 seconds,
online certification is not possible and an auxiliary controller should be
employed. We report that only $78\%$ of instances are verified by FOSSIL on
time. In addition, three cases reach time-out (200 seconds), which means that
FOSSIL cannot generate certified barrier certificates with the provided
specifications of the model. In Table 1 we report the statistics of the
computational time for the certification process directly from FOSSIL. We can
observe that FOSSIL demonstrates divergence in computational time for
different instances of the model, _e.g.,_ maximum computation time for one
instance is 160s, while the minimum is 0.11s and the average is 7.11s.

Figure 6: Cumulative distribution of time taken to generate barrier
certificates via FOSSIL instead of MetaNN. The red vertical line is the
acceptable time bound for the car model (2 seconds). FOSSIL synthesizes only
$78\%$ valid barrier certificates by FOSSIL in this time.

| All (s) | Valid (s)
---|---|---
Total | 1290.43 | 690.43
Avg | 12.90 | 7.11
min | 0.11 | 0.11
max | 200 | 160.63

Table 1: Statistics of the computational time to synthesize valid barrier
certificates for 100 instances on the car model. FOSSIL was not able to find a
barrier certificate in 3 instances within the fixed time bound (200s). These
exceptions are excluded in the Valid column.

The computational time for our MetaNN remains instead constant for each
instance. It takes less than 0.7s to extract a barrier certificate from the
neural network and verify it with dReal. In addition, we were able to obtain
valid barrier certificates for the instances where FOSSIL timed out.
Therefore, by using the MetaNN and offline training, we not only extend the
capabilities of barrier certificate verification to synthesis of parameterized
controllers, but also increases the success rate of online barrier certificate
generation within two seconds from 78% to 99%. This is at the cost of offline
training that takes 10 hours in our case study.

##  6 Discussion and Conclusions

In this paper, we developed a novel approach for sound computation of reach
sets of dynamical systems using level sets of barrier certificates. We
developed a meta-neural network that is trained offline on samples of barrier
certificates and is used online, integrated with an SMT solver, for ensuring
safety. Our framework can take any technique for computing barrier
certificates and use it for generating training data. As a result, the offline
training step of our approach highly depends on the scalability and precision
of such a computational technique. In the future, we plan to explore
alternative computational techniques as the core of our framework and compare
against newly developed online reach set computational tools.

The research of S. Soudjani was supported by the following grants: EPSRC
EP/V$043676$/$1$, EIC $101070802$, and ERC $101089047$.

## References

  * Abate et al. (2021) Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., and Peruffo, A. (2021).  FOSSIL: A software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks.  In _HSCC 2021_. ACM.
  * Ahmed et al. (2021) Ahmed, D., Peruffo, A., and Abate, A. (2021).  Automated formal synthesis of neural barrier certificates for dynamical models.  In _TACAS_ , volume 12651, 370–388.
  * Alur et al. (1993) Alur, R., Courcoubetis, C., Henzinger, T.A., and Ho, P.H. (1993).  Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems.  In _Hybrid Systems_ , 209–229. Springer.
  * Ames et al. (2017) Ames, A.D., Xu, X., Grizzle, J.W., and Tabuada, P. (2017).  Control barrier function based quadratic programs for safety critical systems.  _IEEE Trans. Autom. Control._ , 62(8), 3861–3876.
  * Bogomolov et al. (2019) Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., and Schilling, C. (2019).  JuliaReach: a toolbox for set-based reachability.  In _HSCC_ , 39–44.
  * de Moura and Bjørner (2008) de Moura, L. and Bjørner, N. (2008).  Z3: An Efficient SMT Solver.  In _TACAS’08_ , volume 4963, 337–340. Springer.
  * Fan et al. (2020) Fan, C., Miller, K., and Mitra, S. (2020).  Fast and guaranteed safe controller synthesis for nonlinear vehicle models.  In _CAV_ , 629–652.
  * Fisher et al. (2021) Fisher, M., Mascardi, V., Rozier, K.Y., Schlingloff, B., Winikoff, M., and Yorke-Smith, N. (2021).  Towards a framework for certification of reliable autonomous systems.  _Auton. Agents Multi Agent Syst._ , 35(1), 8.
  * Fränzle et al. (2019) Fränzle, M., Chen, M., and Kröger, P. (2019).  In memory of Oded Maler: Automatic reachability analysis of hybrid-state automata.  _ACM SIGLOG News_.
  * Gao et al. (2013) Gao, S., Kong, S., and Clarke, E.M. (2013).  dReal: An SMT Solver for Nonlinear Theories over the Reals.  In _CADE-24_ , volume 7898, 208–214. Springer.
  * Heersink et al. (2021) Heersink, B., Sylla, P., and Warren, M.A. (2021).  Formal verification of octorotor flight envelope using barrier functions and SMT solving.  _arXiv:2107.00612_.
  * Henzinger et al. (1998) Henzinger, T.A., Kopke, P.W., Puri, A., and Varaiya, P. (1998).  What’s decidable about hybrid automata?  _Journal of Computer and System Sciences_.
  * Ivanov et al. (2020a) Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., and Lee, I. (2020a).  Case study: verifying the safety of an autonomous racing car with a neural network controller.  In _HSCC 2020_. ACM.
  * Ivanov et al. (2020b) Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., and Lee, I. (2020b).  Verifying the safety of autonomous systems with neural network controllers.  _ACM Trans. Embed. Comput. Syst._ , 20(1).
  * Jha et al. (2018) Jha, S., Raman, V., Sadigh, D., and Seshia, S.A. (2018).  Safe autonomy under perception uncertainty using chance-constrained temporal logic.  _J. Autom. Reason._ , 60(1), 43–62.
  * Jin et al. (2020) Jin, W., Wang, Z., Yang, Z., and Mou, S. (2020).  Neural certificates for safe control policies.  _arXiv preprint arXiv:2006.08465_.
  * Johnson et al. (2016) Johnson, T.T., Bak, S., Caccamo, M., and Sha, L. (2016).  Real-time reachability for verified simplex design.  _ACM Trans. Embed. Comput. Syst._ , 15(2).
  * Kawamura (2009) Kawamura, A. (2009).  Lipschitz continuous ordinary differential equations are polynomial-space complete.  In _CCC 2009_ , 149–160. IEEE.
  * Kazemi and Soudjani (2020) Kazemi, M. and Soudjani, S. (2020).  Formal policy synthesis for continuous-state systems via reinforcement learning.  In _International Conference on Integrated Formal Methods_ , 3–21. Springer.
  * Nejati et al. (2023) Nejati, A., Lavaei, A., Jagtap, P., Soudjani, S., and Zamani, M. (2023).  Formal verification of unknown discrete-and continuous-time systems: A data-driven approach.  _IEEE Transactions on Automatic Control_.
  * Prajna (2006) Prajna, S. (2006).  Barrier certificates for nonlinear model validation.  _Automatica_ , 42(1), 117–126.
  * Prajna and Jadbabaie (2004) Prajna, S. and Jadbabaie, A. (2004).  Safety verification of hybrid systems using barrier certificates.  In _HSCC 2004_ , volume 2993 of _LNCS_ , 477–492. Springer.
  * Prajna et al. (2007) Prajna, S., Jadbabaie, A., and Pappas, G.J. (2007).  A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates.  _IEEE Trans. on Auto. Contr._ , 52(8), 1415–1428.
  * Ratschan (2017) Ratschan, S. (2017).  Simulation based computation of certificates for safety of dynamical systems.  In _FORMATS_ , volume 10419 of _LNCS_ , 303–317.
  * Rosolia and Borrelli (2018) Rosolia, U. and Borrelli, F. (2018).  Learning model predictive control for iterative tasks. a data-driven control framework.  _IEEE Trans. on Autom. Cont._ , 63(7), 1883–1896.
  * Samari et al. (2024) Samari, B., Della Rossa, M., Lavaei, A., Soudjani, S., and Jungers, R.M. (2024).  Multiplicative barrier certificates for probabilistic safety of Markov jump systems.  _8th IFAC Conference on Analysis and Design of Hybrid Systems_.
  * Schön et al. (2024) Schön, O., Zhong, Z., and Soudjani, S. (2024).  Data-driven distributionally robust safety verification using barrier certificates and conditional mean embeddings.  _ACC’24, arXiv:2403.10497_.
  * Srinivasan et al. (2020) Srinivasan, M., Dabholkar, A., Coogan, S., and Vela, P.A. (2020).  Synthesis of control barrier functions using a supervised machine learning approach.  In _IROS’20_ , 7139–7145. IEEE.
  * Tiwari (2003) Tiwari, A. (2003).  Approximate reachability for linear systems.  In _HSCC 2003_ , volume 2623 of _LNCS_ , 514–525.
  * Tran et al. (2019) Tran, H.D., Cai, F., Diego, M.L., Musau, P., Johnson, T.T., and Koutsoukos, X. (2019).  Safety verification of cyber-physical systems with reinforcement learning control.  _ACM Trans. Embed. Comput. Syst._ , 18(5s).
  * Wang et al. (2021) Wang, Q., Chen, M., Xue, B., Zhan, N., and Katoen, J.P. (2021).  Synthesizing invariant barrier certificates via difference-of-convex programming.  In _CAV_ , 443–466.
  * Zhao et al. (2020) Zhao, H., Zeng, X., Chen, T., and Liu, Z. (2020).  Synthesizing barrier certificates using neural networks.  In _HSCC_ , 1–11.
  * Zhao et al. (2021a) Zhao, H., Zeng, X., Chen, T., Liu, Z., and Woodcock, J. (2021a).  Learning safe neural network controllers with barrier certificates.  _Formal Aspects of Computing_ , 33(3), 437–455.
  * Zhao et al. (2021b) Zhao, Q., Chen, X., Zhang, Y., Sha, M., Yang, Z., Lin, W., Tang, E., Chen, Q., and Li, X. (2021b).  Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems.  In _HSCC 2021_ , 1–11. ACM.


# Velocity Driven Vision: Asynchronous Sensor Fusion Birds Eye View Models for
Autonomous Vehicles

Seamie Hayes  University of Limerick, Ireland  Sushil Sharma  University of
Limerick, Ireland  Ciarán Eising  University of Limerick, Ireland

###### Abstract

Fusing different sensor modalities can be a difficult task, particularly if
they are asynchronous. Asynchronisation may arise due to long processing times
or improper synchronisation during calibration, and there must exist a way to
still utilise this previous information for the purpose of safe driving, and
object detection in ego vehicle/ multi-agent trajectory prediction.
Difficulties arise in the fact that the sensor modalities have captured
information at different times and also at different positions in space.
Therefore, they are not spatially nor temporally aligned. This paper will
investigate the challenge of radar and LiDAR sensors being asynchronous
relative to the camera sensors, for various time latencies. The spatial
alignment will be resolved before lifting into BEV space via the
transformation of the radar/LiDAR point clouds into the new ego frame
coordinate system. Only after this can we concatenate the radar/LiDAR point
cloud and lifted camera features. Temporal alignment will be remedied for
radar data only, we will implement a novel method of inferring the future
radar point positions using the velocity information. Our approach to
resolving the issue of sensor asynchrony yields promising results. We
demonstrate velocity information can drastically improve IoU for asynchronous
datasets, as for a time latency of 360 milliseconds (ms), IoU improves from
49.54 to 53.63. Additionally, for a time latency of 550ms, the camera+radar
(C+R) model outperforms the camera+LiDAR (C+L) model by 0.18 IoU. This is an
advancement in utilising the often-neglected radar sensor modality, which is
less favoured than LiDAR for autonomous driving purposes.

Keywords: Autonomous Driving, Asynchronous Sensors, Sensor Fusion, Radar, BEV.

##  1 Introduction

The area of 3D perception is a growing area of research and is imperative in
the applications of autonomous driving and computer vision. The dangers of
driving are not something that can be disregarded, and there has been huge
work devoted to making roads safer, such as the drink-driving ban in Ireland
in 1969, along with the wearing of seatbelts becoming mandatory in 1979. With
the recent digital revolution of the past decades, particularly the huge
breakthroughs in machine learning, extensive work has been put into applying
these to areas of driving to aid the driver in difficult scenarios or even
fully autonomous driving where there is no driver present. One of the major
hurdles of autonomous driving is the idea of 3D perception. How is it possible
to provide the vehicle information so that it can efficiently process it and
make quicker decisions than a human?

The mainstream method to acquire data to feed to a network for 3D perception
is via three sensors: camera, radar, and LiDAR. These sensors can be used
alone or together, a method known as multi-modal fusion. Camera sensors
provide a flat 2D representation of the surroundings but have the advantage of
supplying us with colour information, which allows us to discern road markings
and stop signs. Radar and LiDAR provide us with a 3D representation of the
world in a point cloud where these sensors emit signals that will hit objects
and reflect back to the sensor, indicating the presence of an object. One
major advantage LiDAR provides is the density of its point cloud [Sless et
al., 2019]. In the widely known nuScenes dataset, LiDAR data is approximately
40 times denser than radar data [Caesar et al., 2020]. This density lends
itself to greater model performance, which is a huge reason why there has been
much more research in the area of C+L fusion.

However, radar has a distinct capability that we will utilise in this
research, that being the velocity information. The nuScenes vehicle, known as
the ego vehicle, is equipped with five Continental ARS 408-21 radar sensors,
which are capable of capturing velocity information in one measurement cycle.
However, the LiDAR sensor used, Velodyne HDL 32 E, is incapable of such. This
velocity information can be utilised in a novel way to predict the future
position of these radar points, which as we will see in the results section,
gives a notable boost in performance in asynchronous C+R models. This boost in
the performance of asynchronous C+R models places them ever closer to the
performance of asynchronous C+L models. Previous research has struggled to
find use cases where C+R models can outperform C+L models.

Figure 1: Millisecond timestamp capture of all sensors for two consecutive
keyframes. Time is standardised such that CAM_FRONT_LEFT’s timestamp is zero

One aspect of the nuScenes dataset that must be noted is the radar sensors are
not synchronised with the cameras, whereas the LiDAR sensors are synchronised
with the cameras. This is evident in Figure 1 where we can see that for two
consecutive frames, LiDAR and camera timestamps are consistent, whereas radar
is sporadic. This is a limitation of radar sensors in the nuScenes dataset and
will introduce problems with spatial and temporal alignment in perception
algorithms. This paper aims to examine the limit of asynchrony via manual
manipulation of the nuScenes dataset, which may occur due to incorrect
calibration of sensors. We will analyse this problem in the context of Birds
Eye View (BEV) Transformers [Harley et al., 2023]. The BEV space, put very
simply, is the 3D space with the $z-axis$ flattened to give a 2D plane, which
is a more simple representation of the world. Due to this, it has been widely
used, and well researched [Shi et al., 2024].

In short, this paper aims to improve the safety of autonomous vehicles via a
comprehensive exploration of asynchronous radar and LiDAR sensors. The main
contributions are as follows:

  1. 1.

An investigation into the effect asynchrony has on radar and LiDAR sensors via
the construction of a novel asynchronous and corresponding synchronous dataset
made from the nuScenes dataset.

  2. 2.

A novel implementation of radar velocity information to infer future radar
points for asynchronous radar sensors. For a time latency of 360ms, we examine
IoU improvement from 49.54 to 53.63

##  2 Background

###  2.1 State of the Art

Following vehicle segmentation, trajectory prediction of both our ego vehicle
and other vehicles is a crucial and extensively studied task [Hu et al., 2021,
Sharma et al., 2024]. Accurately detecting vehicle position and orientation is
crucial for precise movement prediction. Our approach to resolving asynchrony
demonstrates promising results in addressing this challenge.

The task of lifting camera images into 3D or BEV space can be achieved in
numerous ways. 2D features can be ‘pushed’ from the image into 3D [Philion and
Fidler, 2020, Schramm et al., 2024], whereas some methods opt to pull features
from the image to each 3D voxel [Harley et al., 2023] which is the method we
will utilise for our experiments.

Modality | IoU
---|---
Camera | 47.4
Camera + radar | 55.7
Camera + LiDAR | 60.8
Table 1: Multi-Modal Fusion Analysis [Harley et al., 2023]

Multi-modal fusion is an area of research with a large emphasis placed on it,
namely due to the complementary nature both radar, and LiDAR have on cameras
due to depth perception. C+L fusion provides huge improvements over camera-
only [Li et al., 2022b] and LiDAR-only models [Liu et al., 2023, Li et al.,
2022a]. However, LiDAR sensors can be unattractive as they are quite costly.
C+R fusion has been seen to give great improvement over single modality models
using cameras only [Schramm et al., 2024, Harley et al., 2023]. Table 1
displays the benefits of multi-modal fusion. In the field of multi-modal
fusion, the issue of asynchrony has been largely neglected. Particularly in
the context of C+R fusion, one would expect this to be a focal point of
discussion, especially given the inherent asynchrony present in the nuScenes
dataset. Here, we aim to address and resolve the challenge of
asynchronisation.

###  2.2 nuScenes Dataset

Figure 2: Top-down view of a rendition of the nuScenes ego vehicle with its
sensor modalities annotated

For the purpose of these experiments, we utilise the widely known nuScenes
dataset [Caesar et al., 2020], namely due to its numerous modality sensors and
extensive amount of data available for training.

The vehicle used to capture the nuScenes dataset is equipped with six cameras,
five radar sensors, and one LiDAR sensor as seen in Figure 2. LiDAR operates
at 20Hz, performing a 360-degree sweep from the front left camera to the back
left camera. Cameras are synchronized to LiDAR, as each camera is triggered
once the LiDAR sweep covers its field of view. Consequently, the front left
camera is triggered first, and the timing and order of captures remain
constant for all keyframes (Figure 1). In contrast, radar is captured at a
rate of 13Hz [Caesar et al., 2020], with a non-constant ordering of capture
across keyframes making it inherently asynchronous, although only slightly. To
further explore the boundaries of asynchrony, we will examine greater time
latencies, specifically considering latencies exceeding 500 milliseconds.

###  2.3 Simple-BEV

Figure 3: Architecture flow diagram for Simple-BEV

The machine learning model used for these experiments is based on Simple-BEV
[Harley et al., 2023]. Firstly, two 3D voxel grids centred on the chosen
reference camera of size $200\times 200\times 8$ are initialized for both
camera and radar [Harley et al., 2023]. A 2D ResNet-101 backbone is applied to
each camera image to extract features such as pedestrians, vehicles, etc.
Following this, bilinear sampling is performed to lift these features into the
3D voxel which was initialized previously, and this is then flattened to yield
camera BEV features as illustrated in Figure 3. The radar point cloud occupies
the remaining voxel grid. The voxel grids are concatenated to achieve a
unified voxel grid, which is then flattened on the $z$ axis to achieve a BEV
grid. The unified voxel grid is input to the BEV decoder, producing our BEV
vehicle segmentation output.

We evaluate our C+R datasets using the pre-trained C+R model provided. We must
train our C+L model independently as it is not provided, and we employ the
same hyperparameters as those used for the C+R model.

##  3 Methodology

###  3.1 Construction of the Asynchronous and Synchronous Datasets

Figure 4: Asynchronous Dataset: Construction and translation between
coordinate frames

Each driving scene in the nuScenes dataset is comprised of keyframes which are
annotated with ground truth data for the purpose of supervised training. In
between these keyframes are additional data captures that are not annotated.
We will utilize this additional data to make our dataset asynchronous.
Manipulation of the data will yield two new datasets which we will refer to as
the synchronous, and asynchronous datasets. The synchronous dataset will serve
as our baseline for comparing the asynchronous dataset to analyze the
degradation. For the synchronous dataset, we remove the first two keyframes of
data to ensure the consistency of previous radar/LiDAR sweeps between both
datasets.

For the asynchronous dataset, we again remove the first two keyframes. We then
take the radar/LiDAR data from time $t-1$ as seen in Figure 4. Given a time
latency of approximately 140 ms for radar, this involves using the radar data
two captures prior. One challenge in this process is that the radar/LiDAR data
is still stored in reference to its old ego-vehicle frame. We must translate
it into the current ego frame, and this is done via a straightforward
transformation between coordinate systems:

$\displaystyle\mathsf{EgoFrame}_{\mathsf{\
t-1}}\rightarrow\mathsf{Global}\rightarrow\mathsf{EgoFrame}_{\mathsf{\ t}}$

One important note is that we assume we do not have the ego frame for radar
for current time $t$. Instead, we will translate the radar/LiDAR data to the
ego frame of CAM_FRONT as illustrated in Figure 4. The reasoning for choosing
CAM_FRONT is this is the reference camera during validation.

Thus two datasets are constructed. As mentioned previously, radar and camera
are not synchronous, the term synchronous dataset is not to be taken literally
and is used for distinction purposes. We will train the model displayed in
Figure 3 using the above-constructed datasets. Time latencies greater than
360ms yield similar results and are therefore excluded for the sake of
brevity. C+L datasets are constructed in a manner that approximates the same
time latency as an equivalent C+R closely as possible for fair comparison

Figure 5: Visualization of inferring future radar points: The red arrow
indicates the movement of the original radar point to its inferred future
position

###  3.2 Enhancing Radar Data with Velocity Information

As mentioned previously, the radar sensors equipped on the ego vehicle are
capable of capturing velocity information, with an accuracy of ±0.1 km/h
[Caesar et al., 2020]. Therefore, for our outdated radar data at time $t-1$,
we can update the point positions, $P_{t-1}$, by inferring what their current
position should be, $P_{t}$, with the $xy$ velocity information, $P_{vel}$.
Note, that there is no vertical ($z$) velocity. As noted previously, we
represent our data relative to the ego frame of CAM_FRONT, and so the duration
of time which has passed is the timestamp of CAM_FRONT $t_{cam}$, minus the
timestamp our of radar sensor, $t_{radar}$. We use the following formula to
predict future position:

$\displaystyle P_{t}\ =\ P_{t-1}\ +\ P_{vel}\times[t_{cam}-t_{radar}]$

##  4 Results

###  4.1 Quantitative Analysis: Intersection over Union

The first step of evaluating the performance of our models is qualitative
analysis which we will do using the IoU metric. IoU refers to Intersection
over Union and is a widely used metric for evaluating object detection models.
It is computed by taking the predicted bounding boxes $\text{B}_{\text{pred}}$
from the BEV decoder seen in Figure 3 and comparing them to the ground truth
bounding boxes $\text{B}_{\text{gt}}$. This is calculated using the well-known
IoU formula:

$\displaystyle\text{IoU}=\frac{|\text{B}_{\text{gt}}\cap\text{B}_{\text{pred}}|}{|\text{B}_{\text{gt}}\cup\text{B}_{\text{pred}}|}$

One important note is that IoU penalizes the model in the case of predicting a
vehicle in a position where there is none, which is crucial for ensuring
safety in autonomous driving systems.

Configuration | Metrics
---|---
Sync/Async | Modality | Latency | Infer Position | IOU $\uparrow$ | Velocity Improvement
Sync | C+R | 0ms | ✓ | 55.60 | +0.03
Sync | C+R | 0ms | ✗ | 55.57 |
Async | C+R | 70ms | ✓ | 55.33 (-0.27) | +0.69
Async | C+R | 70ms | ✗ | 54.64 (-0.93) |
Async | C+R | 140ms | ✓ | 54.91 (-0.69) | +1.59
Async | C+R | 140ms | ✗ | 53.32 (-2.25) |
Async | C+R | 220ms | ✓ | 54.49 (-1.11) | +2.55
Async | C+R | 220ms | ✗ | 51.94 (-3.63) |
Async | C+R | 290ms | ✓ | 54.01 (-1.59 | +3.32
Async | C+R | 290ms | ✗ | 50.69 (-4.88) |
Async | C+R | 360ms | ✓ | 53.63 (-1.97) | +4.09
Async | C+R | 360ms | ✗ | 49.54 (-6.03) |
Async | C+R | 570ms | ✓ | 52.30 (-3.30) | +5.12
Async | C+R | 570ms | ✗ | 47.18 (-8.39) |
Table 2: IoU Comparirson for various asynchronous C+R models: Note the degradation asynchrony introduces (seen in red) and the improvement inferring position using velocity has on performance (seen in blue). Asynchrony degradation is relative to its synchronous equivalent (inferring position). Configuration | Metrics
---|---
Sync/Async | Modality | Latency | IOU $\uparrow$ | Asychrony Degradation
Sync | C+L | 0ms | 62.66 |
Async | C+L | 50ms | 62.07 | -0.57
Async | C+L | 150ms | 60.01 | -2.65
Async | C+L | 200ms | 58.86 | -3.80
Async | C+L | 300ms | 56.57 | -6.09
Async | C+L | 350ms | 55.52 | -7.14
Async | C+L | 550ms | 52.12 | -10.54
Table 3: IoU Comparirson for various asynchronous C+L models: Asynchrony
introduces a great amount of degradation (seen in red).

First, we will analyze the impact of asynchrony on the performance of both C+R
and C+L models’ performance as shown in Table 2 and 3. Analysis of the C+R
asynchronous models reveals a minor performance decline when the radar data
latency is 70ms, with an IoU drop of 0.93. This trend continues, where for
greater time latencies we note a greater reduction in performance. For radar
data latency 360ms we examine a massive 6.03 drop in IoU. Similar results can
be observed for the C+L models where for a near equivalent 350ms latency, we
see a 7.14 drop in IoU. It appears that as the data is becoming progressively
outdated, the performance is tending towards a camera-only model. The more
pronounced drop in IoU for C+L compared to C+R can be attributed to the
significant performance boost LiDAR data provides initially.

The impact of inferring future point positions using velocity information in
C+R models cannot be understated. For the 70ms model, we observe a 0.69
increase in IoU, placing it only 0.27 IoU points below the equivalent
synchronous model. Moreover, the gains in IoU for the inferring points model
continue to increase as the radar data latency grows. At a latency of 360 ms,
the difference between the asynchronous inferring model and the corresponding
synchronous model’s IoU is 1.97 points. However, as expected, the performance
gap between the asynchronous and synchronous models widens with increasing
time latency.

Comparing the C+R models to the C+L models, it is evident the C+L model
outperforms C+R by a significant margin. For the base synchronous model, the
difference is 7.09 IoU. However, this gap narrows for the asynchronous models
as radar velocity information is utilized to appreciable effect at greater
time latencies. At a latency of 560ms, the C+R model surpasses the C+L model.
Although this occurs at quite a large latency, it is a rare instance where a
C+R model can outperform a C+L model.

###  4.2 Qualitative Analysis: BEV Vehicle Segmentation Comparison

For the qualitative analysis, we will visually inspect the output of the BEV
encoder from select models against the ground truth for a selected key frame
of a scene. The specific frame is chosen due to the abundance of moving
vehicles in traffic.

The impact of asynchrony is particularly evident in both the C+R and C+L
models, especially with time latencies exceeding 500 milliseconds. In the 70ms
latency dataset, we examine minor misalignments of vehicles, namely for the
vehicles highlighted in red and pink. Notably, the vehicle highlighted in
orange is not segmented in any of the 500ms models.

Inferring future radar point cloud positions significantly improves BEV
vehicle segmentation, especially for the great latency of 560ms. Inferring
future data does not necessarily allow the model to detect more vehicles,
however, it positions them more accurately due to the correct alignment of
radar points. This is most prominent for the vehicles highlighted by the red
and pink boxes. This change is not prominent for the synchronous models, as
reflected by a minimal IoU difference of only 0.03 seen in the previous
analysis.

Comparing the C+R and C+L models, it is evident that C+L excels in vehicle
segmentation. Note that the vehicle highlighted in cyan is not segmented in
any C+R model. In the previous analysis, we found that C+R with inferred
positions outperforms the C+L model at a time latency of approximately 500ms.
Although C+L can detect more vehicles in this case, such as the cyan vehicle,
C+R provides better-aligned vehicle segmentation when inferring future data.
This alignment is crucial for ego vehicle and multi-agent trajectory
prediction models.

Figure 6: BEV image comparison for select experiments: C+R tick involves
inferring future radar point cloud positions.C+R cross indicates not inferring
future positions. Time latency is labelled on each image. Some vehicles are
surrounded by coloured boxes for analysis.

##  5 Conclusion

To conclude, it is apparent that the asynchrony of radar and LiDAR severely
degrades the performance of multi-modal models. For radar data, inferring
future positions using velocity information provides a major boost in
performance and approaches the synchronous model which is very impressive.
Although a great time latency, we see at a latency of 550ms that the C+R model
outperforms the C+L model when utilizing velocity information. This is one of
the only instances in which we have examined C+R outperforming C+L. This is a
noteworthy advancement in the research of novel ways to improve radar data,
notably for the asynchronous case.

Future work includes investigating the effect of training the model from
scratch, and not using pretained model. Also, the development of a novel
machine learning model to further improve inferring future radar point cloud
data will be inquired, perhaps specially tailored for the non-manipulated
synchronous datasets.

## Acknowledgements

This publication has emanated from research conducted with the financial
support of Science Foundation Ireland under Grant number 18/CRT/6049. For the
purpose of Open Access, the author has applied a CC BY public copyright
licence to any Author Accepted Manuscript version arising from this
submission.

## References

  * [Caesar et al., 2020] Caesar, H., Bankiti, V., Lang, A. H., Vora, S., Liong, V. E., Xu, Q., Krishnan, A., Pan, Y., Baldan, G., and Beijbom, O. (2020).  nuscenes: A multimodal dataset for autonomous driving.  In 2020 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pages 11618–11628.
  * [Harley et al., 2023] Harley, A. W., Fang, Z., Li, J., Ambrus, R., and Fragkiadaki, K. (2023).  Simple-bev: What really matters for multi-sensor bev perception?  In 2023 IEEE International Conference on Robotics and Automation (ICRA), pages 2759–2765.
  * [Hu et al., 2021] Hu, A., Murez, Z., Mohan, N., Dudas, S., Hawke, J., Badrinarayanan, V., Cipolla, R., and Kendall, A. (2021).  Fiery: Future instance prediction in bird’s-eye view from surround monocular cameras.  In 2021 IEEE/CVF International Conference on Computer Vision (ICCV), pages 15253–15262.
  * [Li et al., 2022a] Li, Y., Yu, A. W., Meng, T., Caine, B., Ngiam, J., Peng, D., Shen, J., Lu, Y., Zhou, D., Le, Q. V., Yuille, A., and Tan, M. (2022a).  Deepfusion: Lidar-camera deep fusion for multi-modal 3d object detection.  In 2022 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pages 17161–17170.
  * [Li et al., 2022b] Li, Z., Wang, W., Li, H., Xie, E., Sima, C., Lu, T., Yu, Q., and Dai, J. (2022b).  Bevformer: Learning bird’s-eye-view representation from multi-camera images via spatiotemporal transformers.  In In European Conference on Computer Vision (ECCV), pages 1–18. Springer, 2022.
  * [Liu et al., 2023] Liu, Z., Tang, H., Amini, A., Yang, X., Mao, H., Rus, D. L., and Han, S. (2023).  Bevfusion: Multi-task multi-sensor fusion with unified bird’s-eye view representation.  In 2023 IEEE International Conference on Robotics and Automation (ICRA), pages 2774–2781.
  * [Philion and Fidler, 2020] Philion, J. and Fidler, S. (2020).  Lift, splat, shoot: Encoding images from arbitrary camera rigs by implicitly unprojecting to 3d.  In Computer Vision – ECCV 2020: 16th European Conference, Glasgow, UK, August 23–28, 2020, Proceedings, Part XIV, page 194–210, Berlin, Heidelberg. Springer-Verlag.
  * [Schramm et al., 2024] Schramm, J., Vödisch, N., Petek, K., Kiran, R. B., Yogamani, S., Burgard, W., and Valada, A. (2024).  Bevcar: Camera-radar fusion for bev map and object segmentation.  arXiv preprint arXiv:2403.11761.
  * [Sharma et al., 2024] Sharma, S., Das, A., Sistu, G., Halton, M., and Eising, C. (2024).  Bevseg2tp: Surround view camera bird’s-eye-view based joint vehicle segmentation and ego vehicle trajectory prediction.  In Proceedings of the 19th International Conference on Computer Vision Theory and Applications (VISAPP), Rome, Italy.
  * [Shi et al., 2024] Shi, Y., Jiang, K., Li, J., Qian, Z., Wen, J., Yang, M., Wang, K., and Yang, D. (2024).  Grid-centric traffic scenario perception for autonomous driving: A comprehensive review.
  * [Sless et al., 2019] Sless, L., Shlomo, B. E., Cohen, G., and Oron, S. (2019).  Road scene understanding by occupancy grid learning from sparse radar clusters using semantic segmentation.  In 2019 IEEE/CVF International Conference on Computer Vision Workshop (ICCVW), pages 867–875.