Physically-Feasible Repair of Reactive, Linear Temporal Logic-based, High-Level Tasks

TL;DR

This paper introduces a method that combines symbolic repair and physical feasibility checks to automatically modify robot skills encoded in Linear Temporal Logic, enabling robots to accomplish complex tasks that were previously infeasible.

Contribution

It presents a novel approach integrating symbolic repair with physical feasibility checks for LTL-based robot skills, considering full skill execution and enabling automatic modifications.

Findings

Successfully applied to Baxter and Jackal robots.

Automatically modifies skills to achieve previously infeasible tasks.

Ensures physical feasibility of repaired skills.

Abstract

A typical approach to creating complex robot behaviors is to compose atomic controllers, or skills, such that the resulting behavior satisfies a high-level task; however, when a task cannot be accomplished with a given set of skills, it is difficult to know how to modify the skills to make the task possible. We present a method for combining symbolic repair with physical feasibility-checking and implementation to automatically modify existing skills such that the robot can execute a previously infeasible task. We encode robot skills in Linear Temporal Logic (LTL) formulas that capture both safety constraints and goals for reactive tasks. Furthermore, our encoding captures the full skill execution, as opposed to prior work where only the state of the world before and after the skill is executed are considered. Our repair algorithm suggests symbolic modifications, then attempts to physically implement the suggestions by modifying the original skills subject to LTL constraints derived from the symbolic repair. If skills are not physically possible, we automatically provide additional constraints for the symbolic repair. We demonstrate our approach with a Baxter and a Clearpath Jackal.