Abstract

Hamilton-Jacobi (HJ) reachability analysis is an important formal verification method for safety properties of dynamical systems; it has been applied to many small-scale systems in the past decade. It can treat properties of nonlinear continuous and hybrid systems with bounded disturbances, with well-developed numerical tools. The main challenge is addressing its exponential computational complexity with respect to the number of state variables. In this talk, we present an overview of HJ reachability theory and present the most recent numerical tools, including an efficient GPU-parallelized implementation of a Level Set Toolbox for computing reachable sets. In addition, we present current research in high-dimensional HJ reachability to show how the dimensionality challenge can be alleviated via various general theoretical and application-specific insights.

Biography

Claire Tomlin is the Charles A. Desoer Professor of Engineering in EECS at Berkeley.  She was an Assistant, Associate, and Full Professor in Aeronautics and Astronautics at Stanford from 1998 to 2007, and in 2005 joined Berkeley.  Claire works in the area of control theory and hybrid systems, with applications to air traffic management, UAV systems, energy, robotics, and systems biology.  She is a MacArthur Foundation Fellow (2006), an IEEE Fellow (2010), and in 2017 was awarded the IEEE Transportation Technologies Award.