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 nonconvex state constraints. We use these results to synthesize controllers that ensure safety and reachability properties under bounded model disturbances that vary continuously.

In this paper, we present details of the real time implementation onboard a quadrotor helicopter of learning-based model predictive control (LBMPC). LBMPC rigorously combines statistical learning with control engineering, while providing levels of guarantees about safety, robustness, and convergence. Experimental results show that LBMPC can learn physically based updates to an initial model, and how as a result LBMPC improves transient response performance. We demonstrate robustness to mis-learning. Finally, we show the use of LBMPC in an integrated robotic task demonstration-The quadrotor is used to catch a ball thrown with an a priori unknown trajectory.