As perception-based controllers for autonomous systems become increasingly popular in the real world, it is important that we can formally verify their safety and performance despite perceptual uncertainty. Unfortunately, the verification of such systems remains challenging, largely due to the complexity of the controllers, which are often nonlinear, nonconvex, learning-based, and/or black-box. Prior works propose verification algorithms that are based on approximate reachability methods, but they often restrict the class of controllers and systems that can be handled or result in overly conservative analyses. Hamilton-Jacobi (HJ) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable sets under worst-case system uncertainties; however, its application to perception-based systems is currently underexplored. In this work, we propose RoVer-CoRe, a framework for the Robust Verification of Controllers via HJ Reachability. To the best of our knowledge, RoVer-CoRe is the first HJ reachability-based framework for the verification of perception-based systems under perceptual uncertainty. Our key insight is to concatenate the system controller, observation function, and the state estimation modules to obtain an equivalent closed-loop system that is readily compatible with existing reachability frameworks. Within RoVer-CoRe, we propose novel methods for formal safety verification and robust controller design. We demonstrate the efficacy of the framework in case studies involving aircraft taxiing and NN-based rover navigation. Code is available at the link in the footnote.

翻译：随着基于感知的自主系统控制器在现实世界中日益普及，在存在感知不确定性的情况下，对这些控制器的安全性和性能进行形式化验证变得至关重要。然而，此类系统的验证仍面临挑战，主要源于控制器本身的复杂性——它们通常是非线性、非凸、基于学习的和/或黑盒的。先前的研究提出了基于近似可达性方法的验证算法，但这些方法往往限制了可处理的控制器和系统类别，或导致过于保守的分析结果。Hamilton-Jacobi（HJ）可达性分析是一种广泛应用于一般非线性系统的形式化验证工具，能够计算最坏情况系统不确定性下的最优可达集；然而，其在基于感知系统中的应用目前尚未得到充分探索。在本研究中，我们提出了RoVer-CoRe框架，用于通过HJ可达性实现控制器的鲁棒验证。据我们所知，RoVer-CoRe是首个基于HJ可达性、针对感知不确定性下基于感知系统的验证框架。我们的核心思路是将系统控制器、观测函数和状态估计模块串联，构建一个等效的闭环系统，使其能够直接兼容现有的可达性分析框架。在RoVer-CoRe框架内，我们提出了用于形式化安全验证和鲁棒控制器设计的新方法。我们通过飞机滑行和基于神经网络的漫游车导航案例研究，验证了该框架的有效性。代码可通过脚注中的链接获取。