Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances
For researchers and practitioners in formal verification and control, this tutorial provides accessible guidance on HJ reachability tools and recent advances to address scalability issues.
This tutorial reviews Hamilton-Jacobi reachability analysis for formal verification of dynamical systems, highlighting its advantages and the key challenge of exponential computational complexity in state variables. It presents numerical tools including a GPU-parallelized Level Set Toolbox and reviews methods to alleviate the dimensionality challenge.
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.