Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control
This addresses issues in high-level robot control for robotics applications, but appears incremental as it builds on existing synthesis methods with dynamics integration.
The paper tackles the problem of formal specifications failing due to robot dynamics and changing environments, resulting in a framework that automatically synthesizes and explains revisions to these specifications, demonstrated with a unicycle model.
The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system subjected to a changing environment. Such failures occur whenever the dynamics of the system restrict the robot in such a way that the environment may prevent the robot from progressing safely to its goals. We provide a framework that automatically synthesizes revisions to such specifications that restrict the assumed behaviors of the environment and the behaviors of the system. We provide a means for explaining such modifications to the user in a concise, easy-to-understand manner. Integral to the framework is a new algorithm for synthesizing controllers for reactive specifications that include a discrete representation of the robot's dynamics. The new approach is demonstrated with a complex task implemented using a unicycle model.