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.