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.

翻译：我们提出了一种用于自主系统在线安全验证的新技术，通过采用神经屏障证书，高效实现了有界和无界时域下的可达性分析。该方法使用参数化神经网络给出的屏障证书，这些证书依赖于给定的初始集、不安全集和时间范围。此类网络利用从状态空间区域采样的系统仿真进行离线高效训练。随后，我们采用元神经网络将屏障证书推广至训练集之外的状态空间区域。这些证书在线生成并验证为可达状态的有效超近似，从而在确保系统安全的同时，在不安全场景中触发适当的替代行动。我们通过从线性模型到非线性控制依赖模型的案例研究（涵盖在线自动驾驶场景）展示了该技术的有效性。