Matt Strong

Matt Strong

CS PhD at Stanford University

← Paper Digest

Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances

Somil Bansal, Mo Chen, Sylvia Herbert, Claire J. Tomlin

Seminal September 2017

TL;DR A tutorial on Hamilton-Jacobi reachability. It shows how the set of states that can be driven into a target is computed by solving an HJ Isaacs PDE on a grid, introduces the MATLAB and GPU tools that do this, and reviews ways around the exponential cost in state dimension, such as decomposing a 10D quadrotor into small subsystems.

What they do

A tutorial on Hamilton-Jacobi (HJ) reachability, a verification method that finds the states from which a nonlinear system with bounded disturbances can be driven into a target set, or kept out of an unsafe one. It covers the theory, the numerical tools and recent work on the method’s main weakness: grid-based computation that scales exponentially with state dimension.

How it works

  • A two-player game. Control and disturbance are opponents. The disturbance gets an instantaneous informational advantage, so the result is a worst-case guarantee.
  • Level set method. The target is the zero sublevel set of a function such as a signed distance. The backward reachable set is the zero sublevel set of a value function solving an HJ Isaacs PDE, and its gradient gives the optimal safety controller.
  • Variants. Forward or backward, sets or tubes (reaching the target at the final time or at any time), and state constraints.
  • Tools. MATLAB toolboxLS with helperOC, and BEACLS, a C++ port that runs on GPUs; an appendix walks through a 3D Dubins car.

Results

No new experiments; the paper summarizes prior work:

  • Decomposing nonlinear dynamics into coupled subsystems computes reachable sets orders of magnitude faster, exactly or slightly conservatively, including for 6D and 10D quadrotors.
  • FaSTrack bounds the tracking error so a 10D quadrotor model can safely follow a 3D RRT path.
  • A reachability safety layer let a quadrotor run policy-gradient RL without crashing and retreat from a strong disturbance.
  • Pairwise HJ solutions combined in a mixed-integer program proved three-vehicle collision avoidance, previously intractable for HJ reachability.

Limitations

Direct HJ reachability stays intractable in high dimensions. The workarounds rely on structure (decomposable or linear dynamics) or give conservative approximations, and the neural-network approximations are preliminary, shown only on 2D and 3D systems. In helperOC the optimal control and disturbance are derived by hand for each system.

Figures

From Figure 1: Target set and backward reachable set. Trajectories start at the same time from different states; inpu...
From Figure 1: Target set and backward reachable set. Trajectories start at the same time from different states; input a drives the trajectory away from the target set, input b drives it toward the target.
From Figure 2: Reachable set and tube for a 10D quadrotor reaching a target, computed by decomposing the nonlinear dy...
From Figure 2: Reachable set and tube for a 10D quadrotor reaching a target, computed by decomposing the nonlinear dynamics.
From Figure 5: Real-time safe planning with FaSTrack, where a 10D quadrotor model tracks a 3D path from an RRT planner.
From Figure 5: Real-time safe planning with FaSTrack, where a 10D quadrotor model tracks a 3D path from an RRT planner.
From Figure 6: A Hummingbird UAV rejects a disturbance with online guarantee validation (left) and fails to without i...
From Figure 6: A Hummingbird UAV rejects a disturbance with online guarantee validation (left) and fails to without it (right).
Abstract

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.

Summaries are written automatically from each paper's text. Figures and videos come from the paper and its project page; all credit goes to the authors.