Synthesis of nonlinear continuous controllers for verifiably correct high-level, reactive behaviors

Planning robotic missions in environments shared by humans involves designing controllers that are reactive to the environment yet able to fulfill a complex high-level task. This paper introduces a new method for designing low-level controllers for nonlinear robotic platforms based on a discrete-state high-level controller encoding the behaviors of a reactive task specification. We build our method upon a new type of trajectory constraint which we introduce in this paper, reactive composition, to provide the guarantee that any high-level reactive behavior may be fulfilled at any moment during the continuous execution. We generate pre-computed motion controllers in a piecewise manner by adopting a sample-based synthesis method that associates a certificate of invariance with each controller in the sample set. As a demonstration of our approach, we simulate different robotic platforms executing complex tasks in a variety of environments.