Guaranteeing reactive high-level behaviors for robots with complex dynamics

Applying correct-by-construction planning techniques to robots with complex nonlinear dynamics requires new formal analysis methods which guarantee that the requested behaviors can be achieved in the continuous space. In this paper, we construct low-level controllers that ensure the execution of a high-level mission plan. Controllers are generated using trajectory-based verification to produce a set of robust reach tubes which strictly guarantee that the required motions achieve the desired task specification. Reach tubes, computed here by solving a series of sum-of-squares optimization problems, are composed in such a way that all trajectories ensure correct highlevel behaviors. We illustrate the new method using an input-limited unicycle robot satisfying task specifications expressed in linear temporal logic.