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

• URL: http://arxiv.org/abs/2511.14755v1
• Date: Tue, 18 Nov 2025 18:55:20 GMT
• Title: Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis
• Authors: Albert Lin, Alessandro Pinto, Somil Bansal,
• Abstract summary: Hamilton-Jacobi (J) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable under worst-case uncertainties.<n>This work is the first HJ-based reachability-based system verification framework for the Robust Verification Controllers via HJ rover.<n>Within Ro-CoRe, we propose novel methods for safety verification and controller design.
• Score: 49.31947916567367
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Verification of Visual Controllers via Compositional Geometric Transformations [49.81690518952909]
  We introduce a novel verification framework for perception-based controllers that can generate outer-approximations of reachable sets.<n>We provide theoretical guarantees on the soundness of our method and demonstrate its effectiveness across benchmark control environments.
  arXiv  Detail & Related papers  (2025-07-06T20:22:58Z)
• Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
  Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. Lyapunov stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain. We demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations.
  arXiv  Detail & Related papers  (2024-04-11T17:49:15Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Discovering Closed-Loop Failures of Vision-Based Controllers via Reachability Analysis [7.679478106628509]
  Machine learning driven image-based controllers allow robotic systems to take intelligent actions based on the visual feedback from their environment. Existing methods leverage simulation-based testing (or falsification) to find the failures of vision-based controllers. In this work, we cast the problem of finding closed-loop vision failures as a Hamilton-Jacobi (HJ) reachability problem.
  arXiv  Detail & Related papers  (2022-11-04T20:22:58Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Learning Hybrid Control Barrier Functions from Data [66.37785052099423]
  Motivated by the lack of systematic tools to obtain safe control laws for hybrid systems, we propose an optimization-based framework for learning certifiably safe control laws from data. In particular, we assume a setting in which the system dynamics are known and in which data exhibiting safe system behavior is available.
  arXiv  Detail & Related papers  (2020-11-08T23:55:02Z)
• Safety Verification of Model Based Reinforcement Learning Controllers [7.407039316561176]
  We present a novel safety verification framework for model-based RL controllers using reachable set analysis. The proposed frame-work can efficiently handle models and controllers which are represented using neural networks.
  arXiv  Detail & Related papers  (2020-10-21T03:35:28Z)
• Runtime Safety Assurance Using Reinforcement Learning [37.61747231296097]
  This paper aims to design a meta-controller capable of identifying unsafe situations with high accuracy. We frame the design of RTSA with the Markov decision process (MDP) and use reinforcement learning (RL) to solve it.
  arXiv  Detail & Related papers  (2020-10-20T20:54:46Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.