pith. sign in

arxiv: 2511.14755 · v2 · submitted 2025-11-18 · 💻 cs.RO · cs.LG· cs.SY· eess.SY

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

Albert Lin , Alessandro Pinto , Somil Bansal This is my paper

Pith reviewed 2026-05-17 20:32 UTC · model grok-4.3

classification 💻 cs.RO cs.LGcs.SYeess.SY
keywords Hamilton-Jacobi reachabilityperceptual uncertaintyperception-based controllersrobust verificationclosed-loop systemssafety verificationautonomous systemscontroller design
0
0 comments X

The pith

Concatenating controller, observation, and estimation modules enables Hamilton-Jacobi reachability verification of perception-based systems under uncertainty

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces RoVer-CoRe, a framework that applies Hamilton-Jacobi reachability analysis to verify safety of perception-based controllers despite uncertainties in how the system senses its environment. It achieves this by combining the controller with the observation function and state estimation module into one equivalent closed-loop dynamical system that standard reachability tools can process directly under worst-case perceptual errors. This approach matters because perception-based controllers in autonomous systems are often nonlinear, learning-based, or black-box and resist verification by existing approximate methods. A sympathetic reader would value the promise of formal safety guarantees and robust design for real systems like aircraft taxiing or rover navigation where perceptual mistakes can cause failures.

Core claim

By concatenating the system controller, observation function, and state estimation modules, the authors obtain an equivalent closed-loop system that is compatible with existing Hamilton-Jacobi reachability frameworks, allowing computation of reachable sets under worst-case perceptual uncertainty for both formal safety verification and robust controller design.

What carries the argument

Concatenation of the controller, observation function, and state estimation modules into an equivalent closed-loop dynamical system

If this is right

  • Formal safety verification becomes feasible for nonlinear, nonconvex, learning-based, or black-box controllers under perceptual uncertainty.
  • Robust controller design is supported directly inside the reachability framework.
  • The approach applies to concrete systems such as aircraft taxiing and neural-network-based rover navigation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same concatenation step could be tested on systems whose uncertainty arises from sources other than perception to check whether the reduction to standard dynamics remains valid.
  • This reduction might connect reachability-based verification to other formal methods that already operate on closed-loop dynamical systems.
  • Extensions could include handling time-varying or sensor-specific uncertainty models while preserving the equivalence property.

Load-bearing premise

Concatenating the controller with the observation function and state estimation modules produces an equivalent closed-loop dynamical system whose reachable sets under worst-case perceptual uncertainty can be computed accurately by standard Hamilton-Jacobi methods without unmodeled dynamics or approximation errors.

What would settle it

A concrete experiment in which the reachable sets computed from the concatenated system fail to contain or bound the actual states visited by the original perception-based controller in a high-fidelity simulation with explicit perceptual uncertainty would falsify the claim.

Figures

Figures reproduced from arXiv: 2511.14755 by Albert Lin, Alessandro Pinto, Somil Bansal.

Figure 1
Figure 1. Figure 1: (Black) A perception-based system under perceptual uncertainty e, which result in noisy state estimates xˆ. (Red) The closed-loop system abstraction used for safety analysis. Since many perception-based controllers are implemented with neural networks (NN) due to their ability to process general inputs, a substantial body of prior works focuses on verifying such systems by combining NN verification tools w… view at source ↗
Figure 2
Figure 2. Figure 2: , we plot the error distribution over a test dataset of runway images generated in the X￾Plane simulator (Laminar Research, 2016). Using the error distribution, we compute element-wise norm bounds e¯pˆx , e¯θˆ that correspond to different coverages 0 ≤ c ≤ 1 of the observed errors [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Evolution of the BRTs for the taxiing controller as the error coverage increases. Safety is guaranteed in the blue region. (Black) The BRT boundary. (Dot) The initial state. Finally, we demonstrate how RoVer-CoRe can guide robust controller design [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: (a) Value function at the initial state under an error coverage of 0.997 across the controller space. (b) Actual (solid) and perceived (dashed) trajectories under worst-case uncertainty. 6.2. NN-Based Rover Navigation Our second case study considers a rover navigating around obstacles under perceptual uncertainty, inspired by NASA’s Endurance concept for long-range lunar night exploration (Baker et al., 20… view at source ↗
Figure 5
Figure 5. Figure 5: From left to right: the lower bounds, nominal outputs, and upper bounds of the NN at (θ = 0 rad, t = 1.5 s). Rightmost: Rollouts by the NN-based controller successfully reach a goal (green star) while avoiding obstacles (red circles) under perfect state estimation. of the α, β-CROWN bounds. This yields a conservative but sound guarantee; starting from any state outside these BRTs is guaranteed to be safe u… view at source ↗
Figure 6
Figure 6. Figure 6: Left: BRT boundaries computed by RoVer-CoRe when the lights are off for the origi￾nal MPC (dashed) and the NN-based controller (solid) as the time horizon T increases (color). Right: The initial-time value function for T = 5s for the original MPC as com￾puted by RoVer-CoRe (color) compared with the Monte Carlo baseline (purple). True (solid) and perceived (dotted) worst-case rollouts that lead to collision… view at source ↗
Figure 7
Figure 7. Figure 7: True (solid) and perceived (dotted) worst-case rollouts starting from the same initial states as in [PITH_FULL_IMAGE:figures/full_fig_p011_7.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript proposes RoVer-CoRe, a framework for the robust verification of perception-based controllers under perceptual uncertainty using Hamilton-Jacobi reachability analysis. The central contribution is the insight that concatenating the controller, observation function, and state estimation modules produces an equivalent closed-loop dynamical system that is compatible with existing HJ reachability tools. The framework includes novel methods for formal safety verification and robust controller design, demonstrated via case studies on aircraft taxiing and neural-network-based rover navigation. Code is made available.

Significance. If the concatenation step can be shown to preserve formal guarantees without unmodeled state-dependent dynamics or approximation errors, the work would constitute a meaningful extension of HJ reachability to perception-based systems, addressing a gap left by prior approximate methods that restrict controller classes or produce excessive conservatism. The provision of reproducible code strengthens the contribution by enabling direct verification of the implementation.

major comments (2)
  1. [Abstract / §3] Abstract and §3 (concatenation step): the claim that the concatenated system is 'readily compatible with existing reachability frameworks' rests on modeling perceptual uncertainty as an exogenous disturbance d drawn from a compact set independent of state. Standard HJ solvers solve the HJI PDE for dynamics ẋ = f(x, u, d) with D compact and state-independent. When perceptual error (true state minus ê(h(x))) varies with x—as occurs with distance-dependent sensor noise, occlusion, or lighting—the effective disturbance set becomes D(x). The manuscript must either (a) prove that the chosen perception models admit a state-independent over-approximation whose reachable sets remain valid certificates, or (b) quantify the conservatism or invalidity introduced by treating D as fixed. Without this, the safety claims for the aircraft and rover examples are not formally supported.
  2. [Case Studies] Case studies (aircraft taxiing and NN rover navigation): the abstract reports successful verification and design but provides no quantitative results, error bounds, or comparison against ground-truth reachable sets. The central efficacy claim therefore cannot be evaluated without explicit metrics (e.g., volume of verified safe set, computation time, or violation rate under sampled perceptual noise). These numbers are load-bearing for the assertion that RoVer-CoRe outperforms prior approximate methods.
minor comments (2)
  1. [§3] Notation for the concatenated dynamics should be introduced explicitly (e.g., define the augmented state and the effective f̃(x, u, d)) rather than left implicit in the concatenation description.
  2. [Introduction] The manuscript should include a brief related-work paragraph contrasting RoVer-CoRe with existing HJ extensions to uncertain observations (e.g., works on sensor attacks or set-valued observers) to clarify novelty.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their detailed and constructive feedback on our manuscript. We have carefully considered each comment and will make revisions to address the concerns raised, particularly regarding the formal guarantees of the concatenation approach and the presentation of quantitative results in the case studies. Below, we provide point-by-point responses.

read point-by-point responses

  1. Referee: [Abstract / §3] Abstract and §3 (concatenation step): the claim that the concatenated system is 'readily compatible with existing reachability frameworks' rests on modeling perceptual uncertainty as an exogenous disturbance d drawn from a compact set independent of state. Standard HJ solvers solve the HJI PDE for dynamics ẋ = f(x, u, d) with D compact and state-independent. When perceptual error (true state minus ê(h(x))) varies with x—as occurs with distance-dependent sensor noise, occlusion, or lighting—the effective disturbance set becomes D(x). The manuscript must either (a) prove that the chosen perception models admit a state-independent over-approximation whose reachable sets remain valid certificates, or (b) quantify the conservatism or invalidity introduced by treating D as fixed. Without this, the safety claims for the aircraft and rover examples are not formally supported.

    Authors: We thank the referee for highlighting this critical aspect of modeling perceptual uncertainty. In RoVer-CoRe, the concatenation of the controller, observation, and estimation modules is designed such that the perceptual error is captured as a bounded exogenous disturbance d ∈ D, where D is a compact set derived from the maximum possible estimation error over the state space. For the perception models considered in our work, including the range-based sensors in the aircraft taxiing example and the neural network estimator in the rover navigation, we employ conservative state-independent bounds that over-approximate any potential state-dependent variations. We will revise §3 to include a formal proposition proving that the reachable sets computed under this over-approximation are valid safety certificates for the original system (i.e., safety in the over-approximated system implies safety in the true system). This approach ensures compatibility with existing HJ tools while maintaining formal guarantees, albeit with some conservatism that we will quantify in the revised manuscript through additional analysis. revision: yes

  2. Referee: [Case Studies] Case studies (aircraft taxiing and NN rover navigation): the abstract reports successful verification and design but provides no quantitative results, error bounds, or comparison against ground-truth reachable sets. The central efficacy claim therefore cannot be evaluated without explicit metrics (e.g., volume of verified safe set, computation time, or violation rate under sampled perceptual noise). These numbers are load-bearing for the assertion that RoVer-CoRe outperforms prior approximate methods.

    Authors: We agree that providing quantitative metrics is crucial for demonstrating the efficacy of RoVer-CoRe. The current manuscript includes qualitative descriptions and some timing information in the case study sections, but we acknowledge the need for more explicit quantitative comparisons and error bounds. We will update the abstract to summarize key results, such as the size of the verified safe sets and computation times for both case studies. In the revised version, we will add a new table in the case studies section that reports: (1) volume of the verified safe set, (2) computation time, (3) violation rates under Monte Carlo sampling of perceptual noise, and (4) comparisons to ground-truth reachable sets obtained from high-resolution simulations and to prior approximate verification methods. This will allow readers to better assess the performance and any conservatism introduced. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper proposes RoVer-CoRe by treating the concatenation of the controller, observation function, and state estimator as an independent modeling choice that yields a closed-loop system compatible with standard Hamilton-Jacobi reachability. This step is presented as a distinct insight rather than a reduction to fitted parameters, self-referential definitions, or load-bearing self-citations. The subsequent safety verification and controller design rely on established HJ methods whose value functions and reachable-set computations are not redefined or forced by the paper's own inputs. No equations or claims in the provided text reduce the new framework to quantities obtained by construction from prior results of the same authors.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on standard properties of Hamilton-Jacobi reachability for nonlinear systems and the modeling assumption that perceptual uncertainty can be treated as worst-case disturbances in the closed-loop dynamics. No new free parameters or invented entities are introduced in the abstract description.

axioms (2)
  • domain assumption Hamilton-Jacobi reachability computes optimal reachable sets under worst-case uncertainties for general nonlinear systems
    Invoked as the core verification engine after the concatenation step.
  • domain assumption Concatenation of controller, observation function, and state estimator yields an equivalent closed-loop system compatible with existing reachability tools
    Central modeling step stated in the abstract; treated as preserving dynamics and uncertainty structure.

pith-pipeline@v0.9.0 · 5568 in / 1481 out tokens · 37270 ms · 2026-05-17T20:32:13.566569+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Robust Direct Data-Driven Hamiltonian for Safe Set Computation under Measurement Noise and Disturbances

    eess.SY 2026-06 unverdicted novelty 6.0

    Derives Robust Data-Driven Hamiltonian (R-DDH) from noisy data that provides a certified lower bound on the exact Hamiltonian, yielding an inner approximation of the safe set.

Reference graph

Works this paper leans on

3 extracted references · 3 canonical work pages · cited by 1 Pith paper

  1. [1]

    ISBN 978-3-031-65112-0

    Springer Nature Switzerland. ISBN 978-3-031-65112-0. John D Baker, John O Elliott, James T Keane, Nadia R Khan, Richard P Kornfeld, Hari D Nayar, and Issa A Nesnas. The endurance lunar rover sample return mission. In2024 IEEE Aerospace Conference, pages 1–13. IEEE, 2024. Somil Bansal, Mo Chen, Sylvia Herbert, and Claire J Tomlin. Hamilton-Jacobi Reachabil...

    work page 2024

  2. [2]

    Kaustav Chakraborty and Somil Bansal

    doi: 10.1109/TRO.2024.3454470. Kaustav Chakraborty and Somil Bansal. Discovering closed-loop failures of vision-based con- trollers via reachability analysis.IEEE Robotics and Automation Letters, 8(5):2692–2699, 2023. doi: 10.1109/LRA.2023.3258719. Jason J Choi, Christopher A Strong, Koushil Sreenath, Namhoon Cho, and Claire J Tomlin. Data-driven hamilton...

    work page doi:10.1109/tro.2024.3454470 2024

  3. [3]

    ISBN 9781450391962

    Association for Computing Machinery. ISBN 9781450391962. doi: 10.1145/3501710. 3519511. URLhttps://doi.org/10.1145/3501710.3519511. 14

    work page doi:10.1145/3501710