Formal Assurances for Autonomous Systems from Fast Reachability

Abstract

Reachability analysis, which considers computing or approximating the set of future states attainable by a dynamical system over a time horizon, is receiving increased attention motivated by new challenges in, e.g., learning-enabled systems, assured and safe autonomy, and formal methods in control systems. Such challenges require new approaches that scale well with system size, accommodate uncertainties, and can be computed efficiently for in-the-loop or frequent computation. In this talk, we present and demonstrate a suite of tools for efficiently over-approximating reachable sets of nonlinear systems based on the theory of mixed monotone dynamical systems. A system is mixed monotone if its vector field or update map is decomposable into an increasing component and a decreasing component. This decomposition allows for constructing an embedding system with twice the states such that a single trajectory of the embedding system provides hyperrectangular over-approximations of reachable sets for the original dynamics. This efficiency can be harnessed, for example, to compute finite abstractions for tractable formal control verification and synthesis or to embed reachable set computations in the control loop for runtime safety assurance. We demonstrate these ideas on several examples, including an application to safe quadrotor flight that combines runtime reachable set computations with control barrier functions implemented on embedded hardware.

Description

Biography

Dr. Sam Coogan is an assistant professor at Georgia Tech with a joint appointment in the School of Electrical and Computer Engineering and the School of Civil and Environmental Engineering. Prior to joining Georgia Tech in 2017, he was an assistant professor in the Electrical Engineering Department at UCLA from 2015-2017. He received the B.S. degree in Electrical Engineering from Georgia Tech and the M.S. and Ph.D. degrees in Electrical Engineering from the University of California, Berkeley. His research is in the area of dynamical systems and control and focuses on developing scalable tools for verification and control of networked, cyber-physical systems with an emphasis on transportation systems. He received the Outstanding Paper Award for the IEEE Transactions on Control of Network Systems in 2017, a CAREER award from the National Science Foundation in 2018, a Young Investigator Award from the Air Force Office of Scientific Research in 2018, and the Donald P Eckman Award from the American Automatic Control Council in 2020.