Automated Robot Recovery from Assumption Violations of High-Level Specifications

TL;DR

The paper addresses recovering from runtime assumption violations in high-level temporal logic task specifications for robots. It combines online violation monitoring, assumption relaxation to admit observed environment behavior, and synthesis-based repair to acquire new robot skills, enabling continued task completion under updated models. The approach is instantiated with a GR(1) framework, a formal monitor built from environment safety assumptions, and a repair mechanism that suggests new skills via Modify-Preconditions and Modify-Postconditions, integrated with a motion planner when needed. Demonstrations on a Hello Robot Stretch in factory-like settings show automatic recovery from multiple unexpected obstacle behaviors and user-input changes, illustrating practical robustness. The work advances autonomous, correct-by-construction robotics by closing the loop from execution to adaptation without user intervention, while noting limitations when hard postconditions are violated or low-level controllers fail, and outlining future work in local repair and multi-agent scenarios.

Abstract

This paper presents a framework that enables robots to automatically recover from assumption violations of high-level specifications during task execution. In contrast to previous methods relying on user intervention to impose additional assumptions for failure recovery, our approach leverages synthesis-based repair to suggest new robot skills that, when implemented, repair the task. Our approach detects violations of environment safety assumptions during the task execution, relaxes the assumptions to admit observed environment behaviors, and acquires new robot skills for task completion. We demonstrate our approach with a Hello Robot Stretch in a factory-like scenario.

Figures (5)

• Figure 1: Workspace of Example \ref{['example:1']}.
• Figure 2: Our framework for automatic recovery from assumption violations during task execution. Blue arrows represent regular execution; red arrows represent our recovery process.
• Figure 3: Abstract Syntax Tree for $\pi_{{obs}}^{{wlkwy}} \to \bigcirc \pi_{{obs}}^{{wlkwy}}$.
• Figure 4: Workflow of the assumption relaxation procedure.
• Figure 5: Stretch moving $\tt{cup}$ between tables. The task is $\square\lozenge (\pi_{{empty}}^{{}}\to\pi_{{cup}}^{{t_2}}) \land \square\lozenge (\neg\pi_{{empty}}^{{}}\to\pi_{{cup}}^{{t_4}})$. (A) Physical workspace. (B) Initial positions of the objects. (C) Original behavior of the synthesized strategy. Arrows represent the motion of the objects, orange: $\tt{block}$, grey: $\tt{cup}$, green: $\tt{base}$. The numbers represent the order of their movements. (D) Recovery from Violation 1 where $\tt{stone}$ moves from $t_0$ to $t_3$. (E) Recovery from Violation 2 where $\tt{cup}$ becomes empty in $x_2$. (F) Recovery from Violation 3 where $\tt{cone}$ moves from $x_3$ to $x_2$. In (D)-(F), red dashed arrows represent the violations and blue solid arrows represent the new skills.