When humans and robots perform complex tasks together, the robot must have a strategy to choose its actions based on observed human behavior. One well-studied approach for finding such strategies is reactive synthesis. Existing approaches for finite-horizon tasks have used an explicit state approach, which incurs high runtime. In this work, we present a compositional approach to perform synthesis for finite-horizon tasks based on binary decision diagrams. We show that for pick-and-place tasks, the compositional approach achieves orders-of-magnitude speed-ups compared to previous approaches. We demonstrate the synthesized strategy on a UR5 robot.

There are many applications where robots have to operate in environments that other agents can change. In such cases, it is desirable for the robot to achieve a given high-level task despite interference. Ideally, the robot must decide its next action as it observes the changes in the world, i.e. act reactively. In this paper, we consider a reactive planning problem for finite robotic tasks with resource constraints. The task is represented using a temporal logic for finite behaviors and the robot must achieve the task using limited resources under all possible finite sequences of moves of other agents. We present a formulation for this problem and an approach based on quantitative games. The efficacy of the approach is demonstrated through a manipulation case study.

Manipulation planning from high-level task specifications, even though highly desirable, is a challenging problem. The large dimensionality of manipulators and complexity of task specifications make the problem computationally intractable. This work introduces a manipulation planning framework with linear temporal logic (LTL) specifications. The use of LTL as the specification language allows the expression of rich and complex manipulation tasks. The framework deals with the state-explosion problem through a novel abstraction technique. Given a robotic system, a workspace consisting of obstacles, manipulable objects, and locations of interest, and a co-safe LTL specification over the objects and locations, the framework computes a motion plan to achieve the task through a synergistic multi-layered planning architecture. The power of the framework is demonstrated through case studies, in which the planner efficiently computes plans for complex tasks. The case studies also illustrate the ability of the framework in intelligently moving away objects that block desired executions without requiring backtracking.