Verification and Control of Hybrid Systems using Reachability Analysis with Machine Learning

This talk will present reachability analysis as a tool for model checking and controller synthesis for dynamic systems. We will consider the problem of guaranteeing reachability to a given desired subset of the state space while satisfying a safety property defined in terms of state constraints. We allow for nonlinear and hybrid dynamics, and possibly non-convex state constraints. We use these results to synthesize controllers that ensure safety and reachability properties under bounded model disturbances that vary continuously. The resulting control policy is a set-valued feedback map involving both a selection of continuous inputs and discrete switching commands as a function of system state. We show that new control policies based on machine learning are included in this map, resulting in high performance with guarantees of safety. We discuss real-time implementations of this, and present several examples from multiple aerial vehicle control, human-robot interaction, and multiple player games.