Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis
Albert Lin, Alessandro Pinto, Somil Bansal
TL;DR
RoVer-CoRe advances formal safety verification for perception-based controllers by embedding the perception, estimation, and control stack into a single closed-loop abstraction compatible with Hamilton-Jacobi reachability. It develops exact and conservative methods to compute or bound the closed-loop Hamiltonian, enabling safe analysis under bounded perceptual uncertainty and guiding robustness via safety-guided hyperparameter optimization. The approach is validated through aircraft taxiing and NN-based rover navigation case studies, demonstrating guaranteed safety margins, failure diagnostics, and practical design insights such as adaptive lighting policies to manage uncertainty. This framework broadens the applicability of HJ reachability to real-world perception pipelines, offering rigorous guarantees where approximate methods may be overly conservative. $$V(x,t)$$-based safety guarantees and the closed-loop Hamiltonian bounding form the core technical contributions, with open-source code to enable reuse and extension in perception-rich control systems.
Abstract
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.