Dynamics-Driven Adaptive Abstraction for Reactive High-Level Mission and Motion Planning

We present a new framework for reactive synthesis that considers the dynamics of the robot when synthesizing correct-by-construction controllers for nonlinear systems. Many high-level synthesis approaches employ discrete abstractions to reason about the dynamics of the continuous system in a simplified manner. Often, these abstractions are expensive to compute. We circumvent the need to have detailed abstractions for nonlinear systems by proposing a framework for adapting abstractions based on partial solutions to the low-level controller synthesis problem. The contribution of this paper is a reactive synthesis algorithm that makes use of our adaptation procedure to update the high-level strategy each time the non-deterministic discrete abstraction is modified. We combine this with a verified low-level controller synthesis scheme capable of automatically synthesizing controllers for a wide class of nonlinear systems. This novel synthesis framework is demonstrated on a dynamical robot executing an autonomous inspection task.