Verification and control of hybrid systems using reachability analysis

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. We also consider the effects of sampling and quantization. The resulting control policy is an explicit feedback law involving both a selection of continuous inputs and discrete switching commands at each time instant, based upon measurement of system state. We discuss real time implementations of this, and present several examples from multiple aerial vehicle control, human-robot interaction, and multi-stage games. Finally, we show how reachability techniques can be used to guarantee safety in robotics systems that use machine learning to generate dynamic models on-the-fly.