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.

在线安全验证自主系统的一项新技术，通过使用神经屏障证书有效地进行有界和无界时域的可达性分析，我们的方法使用由参数化神经网络给出的屏障证书，这些证书依赖于给定的初始集合，不安全集合和时间范围。

通过神经障碍证明实现安全可达集的计算

Safe Reach Set Computation via Neural Barrier Certificates

The rapid advance of deep reinforcement learning techniques enables the
oversight of safety-critical systems through the utilization of Deep Neural
Networks (DNNs). This underscores the pressing need to promptly establish
certified safety guarantees for such DNN-controlled systems. Most of the
existing verification approaches rely on qualitative approaches, predominantly
employing reachability analysis. However, qualitative verification proves
inadequate for DNN-controlled systems as their behaviors exhibit stochastic
tendencies when operating in open and adversarial environments. In this paper,
we propose a novel framework for unifying both qualitative and quantitative
safety verification problems of DNN-controlled systems. This is achieved by
formulating the verification tasks as the synthesis of valid neural barrier
certificates (NBCs). Initially, the framework seeks to establish almost-sure
safety guarantees through qualitative verification. In cases where qualitative
verification fails, our quantitative verification method is invoked, yielding
precise lower and upper bounds on probabilistic safety across both infinite and
finite time horizons. To facilitate the synthesis of NBCs, we introduce their
$k$-inductive variants. We also devise a simulation-guided approach for
training NBCs, aiming to achieve tightness in computing precise certified lower
and upper bounds. We prototype our approach into a tool called $\textsf{UniQQ}$
and showcase its efficacy on four classic DNN-controlled systems.

通过定性和定量安全性验证问题的综合合成有效的神经屏障证书，本文提出了一种用于 DNN 控制系统的新型框架，并通过 $	extsf {UniQQ}$ 工具在四个经典 DNN 控制系统上展示了其有效性。