Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances

TL;DR

This paper provides an overview of Hamilton-Jacobi reachability analysis, highlighting recent computational advances and methods to address high-dimensional challenges in verifying safety and performance of nonlinear dynamical systems.

Contribution

It offers a comprehensive overview of HJ reachability theory, recent numerical tools including GPU implementations, and insights into high-dimensional problem solutions.

Findings

GPU-parallelized Level Set Toolbox improves computation speed

Recent methods mitigate exponential complexity in high dimensions

HJ reachability effectively verifies safety in nonlinear systems

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.