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 Linear Temporal Logic (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.

We propose a novel planning technique for satisfying tasks specified in temporal logic in partially revealed environments. We define high-level actions derived from the environment and the given task itself, and estimate how each action contributes to progress towards completing the task. As the map is revealed, we estimate the cost and probability of success of each action from images and an encoding of that action using a trained neural network. These estimates guide search for the minimum-expected-cost plan within our model. Our learned model is structured to generalize across environments and task specifications without requiring retraining. We demonstrate an improvement in total cost in both simulated and real-world experiments compared to a heuristic-driven baseline.

Recently, Linear Temporal Logic (LTL) has been used as a formalism for defining high-level robot tasks, and LTL synthesis has been used to automatically create correct-by-construction robot control. The underlying premise of this approach is that the robot has a set of actions, or skills, that can be composed to achieve the high- level task. In this paper we consider LTL specifications that cannot be synthesized into robot control due to lack of appropriate skills; we present algorithms for automatically suggesting new or modified skills for the robot that will guarantee the task will be achieved. We demonstrate our approach with a physical Baxter robot and a simulated KUKA IIWA arm.

This paper combines techniques from Formal Methods and Human-Robot Interaction (HRI) to address the challenge of a robot walking with a human while maintaining a socially acceptable distance and avoiding collisions. We formulate a set of constraints on the robot motion using Satisfiability Modulo Theories (SMT) formulas, and synthesize robot control that is guaranteed to be safe and correct. Due to its use of high-level formal specifications, the controller is able to provide feedback to the user in situations where human behavior causes the robot to fail. This feedback allows the human to adjust their behavior and recover joint navigation. We demonstrate the behavior of the robot in a variety of simulated scenarios and compare it to utility-based side-by-side navigation control.