Robust reach-avoid controller synthesis for switched nonlinear systems

In this paper, we describe a method to automatically synthesize controllers that provide hard guarantees of safety and target reachability for sampled-data switched systems under bounded continuous disturbances. Techniques from hybrid system verification are used to perform continuous time differential game calculations on each sampling interval. Iterative procedures are given for computing the set of states for which there exists an admissible control policy so that the closed-loop system satisfies the properties of safety and reachability over a finite time horizon. From this computation, we show how to obtain an explicit state feedback policy in the form of multiple reachable sets, and an algorithm is given for using this feedback law in closed-loop control of the switched system. A simulation example of automated aerial refueling is used to illustrate the application of our approach.