Source-linked AI summary
Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances
Somil Bansal, Mo Chen, Sylvia Herbert, Claire J. Tomlin
TL;DR
HJ reachability addresses formal verification for nonlinear dynamical systems with bounded disturbances, while its exponential state-dimensionality cost limits direct application. This tutorial develops the theory, presents computational tools and dimensionality-mitigation techniques, and reviews applications that use these ideas to ensure safety.
Problem
HJ reachability supports safety and goal guarantees under bounded disturbances, but direct application is generally intractable because computational complexity scales exponentially with continuous state dimension.
Method
The tutorial presents HJ reachability theory, computational tools, and theoretical, decomposition-based, and application-specific approaches for alleviating dimensionality challenges.
Results
The tutorial reviews applications of high-dimensional HJ reachability, including decomposition-based reachable-set computations and safety frameworks for tracking, learning-based control, and vehicle traffic management.
Takeaways & Limitations
HJ reachability provides safe sets and controllers for bounded-disturbance scenarios, while recent structural approaches extend its use beyond direct low-dimensional computation.
Abstract
from arXiv · showhide
Hamilton-Jacobi (HJ) reachability analysis is an important formal verification method for guaranteeing performance and safety properties of dynamical systems; it has been applied to many small-scale systems in the past decade. Its advantages include compatibility with general nonlinear system dynamics, formal treatment of bounded disturbances, and the availability of well-developed numerical tools. The main challenge is addressing its exponential computational complexity with respect to the number of state variables. In this tutorial, we present an overview of basic HJ reachability theory and provide instructions for using the most recent numerical tools, including an efficient GPU-parallelized implementation of a Level Set Toolbox for computing reachable sets. In addition, we review some of the current work in high-dimensional HJ reachability to show how the dimensionality challenge can be alleviated via various general theoretical and application-specific insights.
I. INTRODUCTION
HJ reachability provides formal verification for nonlinear, disturbed, continuous-time systems, but its grid-based computations face exponential scaling with state dimension. This tutorial introduces reachability theory and tools, then reviews theoretical and application-specific approaches to reducing that computational burden.
- Motivation: Formal verification must account for all system behaviors, disturbances, and complex nonlinear dynamics, making simulation-based approaches insufficient.The challenge is amplified by continuous-time evolution and high-dimensional state spaces.
- HJ reachability: HJ reachability computes states that can reach a target while satisfying time-varying constraints, supporting guarantees of system performance and safety.Its numerical tools have been applied to differential games, path planning, and optimal control.
- Computational challenge: Grid-based reachable-set computation has exponential complexity in the number of state variables, creating the curse of dimensionality.Recent approaches decompose computations into smaller subsystems, while Hopf-Lax convex optimization enables real-time solutions for linear dynamics.
- Tutorial scope: The tutorial introduces reachability theory, available computation tools, dimensionality-reduction developments, and safety-critical applications.These are presented as four goals of the tutorial.
- Backward reachable sets: Backward reachable sets identify states that can reach a target over a finite horizon, including states that may lead to unsafe configurations despite control actions.The target may represent unsafe states, which the computed set should therefore be avoided.
- Differential games: Level set methods transform reachability games of kind into analytically sound and computationally tractable games of degree.The BRS computation is formulated as a differential game involving opposing inputs.
III. TWO-PERSON ZERO-SUM DIFFERENTIAL GAMES
Two-person zero-sum differential games model trajectory optimization as opposing control objectives under shared system dynamics. Dynamic programming converts the resulting value function into a Hamilton-Jacobi-Isaacs PDE whose Hamiltonian captures the players’ control choices.
- Game formulation: Differential games optimize a terminal-state cost together with running costs or rewards accumulated over a finite time horizon.The cost depends on the controls selected by both players and the resulting system trajectory.
- Hamilton-Jacobi-Isaacs PDE: Dynamic programming shows that the value function is the viscosity solution of a Hamilton-Jacobi-Isaacs PDE with terminal condition G(0, x) = q(x).The PDE is written as D_tG(t, x) + H(t, x, ∇G(t, x)) = 0.
- Hamiltonian: The Hamiltonian combines running cost with the costate’s inner product with system dynamics, optimizing over the players’ inputs.The costate is defined as λ = ∇G(t, x).
- Optimal controls: The costate λ is the gradient of the value function and is used to obtain Player 1’s optimal control.Player 2’s optimal control can be obtained similarly.
IV. THE LEVEL SET APPROACH: FROM GAMES OF KIND TO GAMES OF DEGREE
The level set approach converts a Boolean reachability game into a quantitative value-function problem, whose solution is obtained from an HJI PDE. The resulting reachable set identifies states that can be driven to the target despite opposing controls, while its complement comes with a safety-preserving controller.
- The level set approach encodes the Boolean outcome of reaching a target through a quantitative value function compared with a threshold.Using terminal distance as a cost makes target attainment equivalent to a value-function inequality.
- A Lipschitz function can represent the target set as its zero sublevel set, enabling a signed-distance-based cost construction.The target set G0 is represented by g(x) ≤ 0.
- The Hamiltonian and optimal control use max-min optimization to represent the opposing roles of the players in the differential game.The lower game value suffices for the scenarios considered, and the control is selected through the associated optimization.
- The value function G satisfies the HJI PDE DtG(t, x) + H(t, x, λ) = 0 with initial condition G(0, x) = g(x).
- States in G(t) can be driven to the target by Player 2 regardless of Player 1, while states in G(t)C admit a Player 1 strategy that avoids the target despite Player 2.For unsafe targets, the complement is the effective safe set and the optimal control keeps the system safe from it.
V. DIFFERENT FLAVORS OF REACHABILITY
Reachability analysis includes multiple reachable-set formulations beyond backward reachable sets, allowing the computed set to match the verification problem.
- Different kinds of reachable sets can be computed depending on the verification problem at hand.
A. Forward vs. Backward Reachable Set
Forward reachable sets describe states reachable from an initial set after a positive time duration, complementing backward reachable-set analyses. They can be computed similarly, but require an initial-value HJ PDE formulation.
- A forward reachable set contains all states a system can reach from a given initial set after a duration |t|.The initial set is denoted G0.
- The forward reachable set accounts for Player 1 keeping the system in G0 while Player 2 drives it out of G0.
- Forward reachable sets are computed similarly to backward reachable sets, except that an initial-value HJ PDE is solved.A change of variables can convert the initial-value PDE into an equivalent final-value PDE.
B. Reachable Sets vs. Tubes
Reachable tubes extend reachable sets from an exact terminal time to an entire time horizon, which is useful when safety depends on whether an unsafe state is reached at any time.
- A reachable tube contains states from which the system can reach a target within a duration |t|, rather than exactly at time 0.
- Reachable tubes support safety analysis by checking whether disturbances can drive the system into unsafe states at any time within a horizon.
- Backward reachable tubes are defined in the tutorial, while forward reachable tubes can be defined analogously.
- The backward reachable tube can be computed by solving a final-value PDE similar to the backward reachable-set formulation.
- The max-min ordering depends on whether the formulation seeks the existence of a control or characterizes behavior for all controls.Existential controls use minimization in the corresponding Hamiltonian, whereas universal-control characterizations use maximization.
D. Presence of State Constraints
HJ reachability supports time-dependent state constraints and multiple reachability variants, while recent decomposition methods reduce the computational burden of high-dimensional analyses. Available MATLAB and GPU-parallelized tools support practical reachable-set computation.
- Time-dependent state constraints can be handled within the HJ reachability framework, alongside other reachability variants.
- The Level Set Toolbox solves final-value HJ PDEs and supports computation of multiple reachable-set definitions.
- BEACLS accelerates Level Set Toolbox computations by implementing its functions in C++ and parallelizing computations on GPUs.
- A. System Decomposition Techniques for Nonlinear Systems: Decomposition methods address exponential computational scaling by splitting certain nonlinear dynamics into coupled subsystems without linearization or polytope approximations.
- A. System Decomposition Techniques for Nonlinear Systems: BRSs and BRTs for systems including 6D and 10D quadrotors were computed using decomposition, with exact solutions available for many high-dimensional nonlinear systems.
- A. System Decomposition Techniques for Nonlinear Systems: Approximate decomposition treats key states as disturbances and preserves conservatism through reachable-set overapproximations or underapproximations.
C. Fast and Safe Tracking for Motion Planning
FaSTrack combines fast planning with HJ-based safety control by bounding tracking errors under dynamic infeasibility and disturbances. HJ-based learning safety frameworks similarly preserve constraint satisfaction while allowing online learning and disturbance rejection.
- C. Fast and Safe Tracking for Motion Planning: FaSTrack combines a simplified, fast planner with a safety controller and guaranteed tracking-error bound for the vehicle.
- C. Fast and Safe Tracking for Motion Planning: The tracking-error bound is computed in error coordinates through a differential game and captures deviations caused by dynamic infeasibility and external disturbances.
- D. HJ Reachability for Safe Learning-Based Control: Learning-based control remains difficult to guarantee during training, particularly for safety-critical robotic systems.
- D. HJ Reachability for Safe Learning-Based Control: An HJ-based framework works with arbitrary learning algorithms, using approximate dynamics to guarantee constraint satisfaction while minimally interfering with learning.
- D. HJ Reachability for Safe Learning-Based Control: A Bayesian mechanism updates safety analysis with new evidence, reducing conservativeness when appropriate and strengthening guarantees through real-time validation.
- D. HJ Reachability for Safe Learning-Based Control: The framework was demonstrated on a quadrotor that ran policy-gradient reinforcement learning without crashing and retracted safely from a strong external disturbance.
E. HJ Reachability Analysis using Neural Networks
Recent HJ methods use neural networks and optimization-based formulas to approximate or compute value functions and PDE solutions more efficiently. These approaches target the dimensionality limits of grid-based reachability while extending applications to linear systems and autonomous-airspace coordination.
- E. HJ Reachability Analysis using Neural Networks: Neural networks have been used to approximate HJ PDE solutions and value functions representing reachable sets.
- F. Generalized Hopf Formula for Linear Systems: The generalized Hopf formula transforms HJ PDE solution into a minimization problem for linear, potentially time-varying systems.
- F. Generalized Hopf Formula for Linear Systems: Coordinate descent with multiple initializations, numerical quadrature, and alternatives such as ADMM can solve the optimization problem.
- F. Generalized Hopf Formula for Linear Systems: The optimization reformulation produces HJ PDE solutions at desired state-space and time points, alleviating the exponential scaling of finite-difference methods.
- Applications: HJ reachability supports UTM applications by ensuring safe hybrid mode transitions for UAVs on designated air highways.
- Applications: A Crazyflies 2.0 quadrotor lab implemented the proposed platooning concept using reachable-set-based vehicle coordination.
B. Sequential Robust Space-Time Reservations
The tutorial describes scalable HJ-based strategies for robust multi-vehicle planning and coordination under disturbances, collisions, and adversarial intruders. These approaches replace intractable joint analyses with sequential reservations or higher-level logic built from pairwise solutions.
- Sequential Robust Space-Time Reservations: Sequential path planning robustly synthesizes controllers for many vehicles reaching destinations while avoiding collisions under disturbances and a single intruder vehicle.Vehicles receive a strict priority ordering, and lower-priority vehicles treat higher-priority vehicles as moving obstacles.
- Sequential Robust Space-Time Reservations: The method creates dynamically feasible space-time reservations that support disturbance rejection and collision avoidance against an adversarial intruder.These reservations provide a last-mile route from air highways to final postal addresses.
- Multi-Vehicle Coordination Using HJ Reachability and High-Level Logic: A mixed integer program uses pair-wise HJ solutions to provide higher-level control logic and overcome scalability limitations.This approach proves safety guarantees for three-vehicle collision avoidance without significant additional computation cost and scales beyond three vehicles.
- Multi-Vehicle Coordination Using HJ Reachability and High-Level Logic: The higher-level collision-avoidance protocol performs significantly better across several metrics than extending pairwise collision avoidance directly to multiple vehicles.An 8-vehicle collision-avoidance simulation is shown in Figure 11a.
- Multi-Vehicle Coordination Using HJ Reachability and High-Level Logic: For multiplayer reach-avoid games, maximum matching assigns defenders attackers they are guaranteed to defeat, enabling coordinated defense against attackers targeting restricted airspace.The joint solution is intractable, motivating the maximum-matching approximation.
X. APPENDIX: QUICK-START GUIDE
The quick-start guide introduces the object-oriented helperOC structure for defining dynamical systems and demonstrates how optimal controls and disturbances are computed for a 3D Dubins car. It then connects these definitions to the reachability-analysis example workflow.
- Quick-Start Guide: helperOC represents dynamical systems through a base DynSys class and subclasses such as DubinsCar, with files for construction, dynamics, optimal control, and optimal disturbance.DubinsCar.m defines system properties and constructs the object, while dynamics.m specifies the system equations.
- Quick-Start Guide: The Hamiltonian is computed from the spatial gradient of the value function and system dynamics to select optimal control and disturbance at each grid point and time step.The control and disturbance functions must currently be defined by hand.
- Quick-Start Guide: For the Dubins car, the optimal control is obtained by minimizing the Hamiltonian term Gθ * a.The displayed dynamics include velocity, angular control, and disturbance components.
B. Reachability Analysis Setup
The reachability-analysis setup defines the grid, target and obstacle sets, system parameters, and numerical accuracy before solving for the value function. The workflow uses helperOC and toolboxLS to compute and visualize reachable sets or tubes.
- Reachability Analysis Setup: The tutorial_test.m script contains modifiable blocks for trajectory computation, grid construction, target definition, parameter packing, obstacles, and value-function computation.These blocks organize the numerical setup for the 3D Dubins car reachability analysis.
- Reachability Analysis Setup: The level set toolbox discretizes the state space into a grid and solves for the value function over that grid.Grid bounds must enclose the target and reachable set or tube, and finer discretization improves accuracy.
- Reachability Analysis Setup: The backward reachable-set computation’s curse of dimensionality is caused by discretizing the state space on a grid.This setup dependence makes grid resolution and state dimension central computational constraints.
- Reachability Analysis Setup: The grid is specified by minimum and maximum states, grid-point counts, and periodic dimensions, while the target is a reachable or unsafe set of interest.Obstacles are defined in the same format as target sets and passed as additional reachability inputs.
- Reachability Analysis Setup: Higher numerical accuracy improves the value-function gradient calculation but increases computation time.The accuracy level is packed with the system, grid, and control or disturbance modes before solving.
- Reachability Analysis Setup: HJIPDE Solve.m interfaces helperOC with toolboxLS, taking initial grid values, a time vector, problem parameters, set-or-tube mode, and additional arguments to produce value functions.Additional arguments can enable obstacles, visualization, stopping conditions, and periodic data saving.