2014/10/23 by Jonathan DeCastro, DeCastro, Jonathan A., Matthias Rungger +8
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Petri Nets in System Modeling #Robotics (cs.RO)
paper · pdf · doi:10.48550/arxiv.1410.6375
openalex publication_date 2014/10/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.