Abstract

We present a formal methods based approach to human-robot handovers. Specifically, we use the automatic synthesis of a robot controller from specifications in Signal Temporal Logic (STL). This allows users to specify and dynamically change the robot’s behaviors using high-level abstractions of goals and constraints rather than by tuning controller parameters. Also, in contrast to existing controllers, this controller can provide guarantees on the timing of each of the handover phases. We replicate the behavior of existing handover strategies from the literature to illustrate the proposed approach. We are currently implementing this approach on a collaborative robot arm and we will evaluate it’s usability through human-participant experiments.