Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control

TL;DR

This paper introduces a framework for automatically revising formal specifications in robot control to account for system dynamics and environmental changes, ensuring safety and goal achievement.

Contribution

It presents a novel algorithm for synthesizing controllers with discrete robot dynamics and a method for automatically modifying specifications based on system-environment interactions.

Findings

Successfully applied to a unicycle robot model

Demonstrates automatic specification revision in dynamic environments

Provides user-friendly explanations of modifications

Abstract

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.