Sequential composition of robust controller specifications

We present a general notion of robust controller specification and a mechanism for sequentially composing them. These specifications form tubular abstractions of the trajectories of a system in different control modes, and are motivated by the techniques available for certifying the performance of low-level controllers. The notion of controller specification provides a rigorous interface for connecting a planner and lower-level controllers that are designed independently. With this approach, the planning layer does not integrate the closed-loop system dynamics and does not require the knowledge of how the controllers operate, but relies only on the specifications of the output tracking performance achieved by these controllers. The control layer aims at satisfying specifications that account quantitatively for robustness to unmodeled dynamics and various sources of disturbance and sensor noise, so that this robustness does not need to be revalidated at the planning level. As an illustrative example, we describe a randomized planner that composes different controller specifications from a given database to guarantee that any corresponding sequence of control modes steers a robot to a given region while avoiding obstacles.