Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis

1. Problem Statement

The paper addresses the critical challenge of formally verifying the safety of autonomous systems that rely on perception-based controllers (e.g., those using Neural Networks or state estimators) in the presence of perceptual uncertainty.

• Context: As autonomous systems (rovers, aircraft) increasingly use sensors and learning-based modules, their state estimates ($\hat{x}$) are noisy due to sensor noise, learning errors, or environmental factors (e.g., GPS blockage).
• The Gap: Existing verification methods often struggle with this complexity.
  • Approximate Reachability Methods: Tools like NNV use set propagation (zonotopes, polytopes) but often result in overly conservative analyses that fail to certify safety, or they are restricted to specific system classes.
  • Certificate-Based Methods: Control Barrier Functions (CBFs) face challenges with global feasibility and constructing barriers for general nonlinear systems under uncertainty.
  • Hamilton-Jacobi (HJ) Limitations: Traditional HJ reachability assumes the controller has access to the true state. It cannot be directly applied when the controller acts on a noisy estimate $\hat{x}$.

Goal: To compute formal safety guarantees (Backward Reachable Tubes) for systems where the controller $u = \pi(\hat{x})$ operates under worst-case perceptual errors $e$ and external disturbances $d$.

2. Methodology: RoVer-CoRe Framework

The authors propose RoVer-CoRe (Robust Verification of Controllers via Reachability), a framework that adapts HJ reachability to handle perception-based systems.

A. Closed-Loop System Abstraction

The core insight is to treat the controller, observation map, and state estimator as a single, concatenated closed-loop system.

• System Dynamics: $\dot{x} = f(x, u, d)$
• Observation: $o = p(x)$
• Estimation: $\hat{x} = q(o, e)$ (where $e$ is perceptual error)
• Control: $u = \pi(\hat{x})$
• Abstraction: The authors define an equivalent dynamics function $h(x, d, e) = f(x, \pi(q(p(x), e)), d)$.
• Key Shift: In this abstraction, the only external inputs are the disturbance $d$ and the perceptual error $e$. This allows the system to be treated as a standard HJ reachability problem where $d$ and $e$ are adversarial inputs.

B. The Hamiltonian Challenge

The main technical hurdle is computing the Closed-Loop Hamiltonian:
$$H(x, t, \nabla V) = \min_{d \in D, e \in E} \nabla V(x, t) \cdot h(x, d, e)$$
Because the controller $\pi$ and estimator $q$ are often non-convex (e.g., Neural Networks), solving this optimization exactly is difficult. The paper proposes two approaches:

1. Exact Computation: If the controller is simple (e.g., linear feedback or grid-based), the Hamiltonian can be solved exactly. This yields non-conservative results and provides concrete worst-case counterexamples.
2. Lower Bounding (Conservative but Sound): For complex controllers (e.g., NNs), the authors propose bounding the controller output.
   • Assume the state estimate error is bounded: $\hat{x} = x + e$, where $e \in \mathcal{E}$.
   • Compute bounds on the control output $u$: $\underline{U}(x) \leq \pi(\hat{x}) \leq \bar{U}(x)$.
   • For NNs, these bounds are computed using verification tools like $\alpha,\beta$-CROWN.
   • The Hamiltonian is then lower-bounded by minimizing over the set of possible controls $\mathcal{U}(x)$ rather than the specific function. This results in a conservative (safer) but sound verification.

C. Robust Controller Design

Beyond verification, the framework supports safety-guided hyperparameter optimization. By evaluating the robust value function $V_\alpha$ across a family of controllers parameterized by $\alpha$, one can select parameters that maximize safety margins or the volume of the safe set.

3. Key Contributions

1. RoVer-CoRe Framework: The first HJ reachability-based framework specifically designed to verify perception-based systems under perceptual uncertainty.
2. Novel Hamiltonian Handling: Methods to exactly compute or conservatively bound the closed-loop Hamiltonian, bridging the gap between HJ theory and black-box/perception-based controllers.
3. Formal Guarantees & Design: A unified approach for both verifying safety and designing robust controllers (e.g., optimizing gains or activation policies).
4. Open Source: Release of code and case study implementations.

4. Results and Case Studies

The authors validate RoVer-CoRe on two distinct case studies:

Case Study 1: Aircraft Taxiing

• Scenario: An aircraft follows a runway centerline using a DNN to estimate cross-track and heading errors from camera images.
• Verification: The controller is simple enough for exact Hamiltonian computation.
• Outcome: The system was formally verified as safe up to a perceptual error coverage of 99.68%.
• Design: The framework identified unsafe controller gains (e.g., high cross-track gain causing over-correction) and guided the selection of robust gains that maintain safety under worst-case perception errors.

Case Study 2: NN-Based Rover Navigation

• Scenario: A lunar rover navigates obstacles using visual odometry. Uncertainty grows over time when headlights are off (low-light conditions).
• Verification: Compared two controllers:
  1. Grid-based MPC: Verified via exact enumeration.
  2. Imitation NN: Verified using $\alpha,\beta$-CROWN to bound the NN output.
• Outcome:
  • RoVer-CoRe produced tighter safety guarantees than the popular set-based tool NNV 2.0.
  • It successfully identified unsafe states that Monte Carlo simulations missed (demonstrating completeness).
  • The NN-based controller had larger Backward Reachable Tubes (BRTs) due to imitation error and verification looseness, correctly reflecting its lower robustness.
• Application: The framework was used to derive a light-activation policy. It calculates the maximum time the rover can operate with lights off before the growing uncertainty drives it into the failure set, ensuring safety while minimizing energy consumption.

5. Significance

• Bridging Theory and Practice: It extends the rigorous, worst-case guarantees of HJ reachability to the modern reality of perception-based, learning-enabled control systems.
• Reducing Conservatism: By moving away from approximate set propagation (which often fails to certify safety due to over-approximation) toward optimal control formulations, RoVer-CoRe provides significantly tighter and more useful safety certificates.
• Actionable Insights: Unlike "black-box" verification that simply says "safe/unsafe," RoVer-CoRe provides worst-case trajectories (counterexamples) and diagnostic insights into why a system fails (e.g., specific error modes), enabling principled controller refinement.
• Scalability: While HJ reachability suffers from the "curse of dimensionality," the paper demonstrates efficacy in 3D state spaces (position, heading, time) and offers a pathway for future learning-based scalability.

In summary, RoVer-CoRe provides a mathematically rigorous, computationally feasible, and practically applicable method to ensure that autonomous systems remain safe even when their "eyes" (sensors) and "brain" (estimators) are imperfect.