There is a growing trend in robotics moving from industrial robots that work physically separated from people to robots that collaborate and interact with people in the workplace and the home. The field of human-robot interaction (HRI) studies such interactions from the computational, design and social points of view. At the same time, there is growing interest in research regarding the safety, verification and automated synthesis of behaviors for robots and autonomous systems. The fields of formal methods and testing, which focus on verification and synthesis of systems, aim to model systems and define and prove specifications over these systems; in the context of robotics, these techniques take into account the robot dynamics and its interaction with its changing and uncertain environment.

However, a human collaborating with a robot is not just part of the robot's environment, but an autonomous agent with intentions, beliefs, and actions that mesh with those of the robotic agent. This raises new research questions related to verification and synthesis including what appropriate models and specifications for human-robot interaction would be; whether and how algorithms for HRI can enable verification; how to take the human into account in automatic synthesis of robotic systems; and what (if any) guarantees can be provided with a human in the loop.

To date, very little work has explored questions of verification, safety guarantees and automated synthesis in the context of Human-Robot Interaction. HRI has modeled humans computationally but not from a verification point of view and without providing guarantees. Furthermore, there are rarely any formal specifications in the computational HRI literature; validated objective metrics for evaluation are also scarce. The verification and synthesis community has mostly focused on the robot's autonomous behavior and its environment, and not paid much attention to the integral presence of the human or the interaction, including the psychological, social, and intentional aspects of human activity.

In this Dagstuhl Seminar we bring together experts in computational HRI, verification and synthesis of autonomous systems, formal methods, and cognitive and social psychology to exchange ideas, define research directions, and foster collaborations toward a new theory and practice of verifiable HRI.

Creative Commons BY 3.0 DE

Rachid Alami, Kerstin I. Eder, Guy Hoffman, and Hadas Kress-Gazit

• Erika Abraham (RWTH Aachen, DE) [dblp]
• Henny Admoni (Carnegie Mellon University - Pittsburgh, US) [dblp]
• Rachid Alami (LAAS - Toulouse, FR) [dblp]
• Dejanira Araiza-Illan (ARTC - Singapore, SG) [dblp]
• Brenna D. Argall (Northwestern University - Evanston, US) [dblp]
• Frank Broz (Heriot-Watt University - Edinburgh, GB) [dblp]
• Maya Cakmak (University of Washington - Seattle, US) [dblp]
• Alessandro Cimatti (Bruno Kessler Foundation - Povo, IT) [dblp]
• Aurelie Clodic (LAAS - Toulouse, FR) [dblp]
• Kerstin I. Eder (University of Bristol, GB) [dblp]
• Rüdiger Ehlers (Bremen, DE) [dblp]
• Victor Fernandez Castro (ENS - Paris, FR) [dblp]
• Ivan Gavran (MPI-SWS - Kaiserslautern, DE) [dblp]
• Michael Gienger (Honda Research Europe - Offenbach, DE) [dblp]
• Marc Hanheide (University of Lincoln, GB) [dblp]
• Christoffer R, Heckman (University of Colorado - Boulder, US) [dblp]
• Guy Hoffman (Cornell University - Ithaca, US) [dblp]
• Shanee Honig (Ben Gurion University - Beer Sheva, IL) [dblp]
• Felix Ingrand (LAAS - Toulouse, FR) [dblp]
• Nils Jansen (Radboud University Nijmegen, NL) [dblp]
• Ross A. Knepper (Cornell University, US) [dblp]
• Hadas Kress-Gazit (Cornell University - Ithaca, US) [dblp]
• Jan Kretinsky (TU München, DE) [dblp]
• Morteza Lahijanian (University of Colorado - Boulder, US) [dblp]
• Ute Leonards (University of Bristol, GB) [dblp]
• Shelly Levy-Tzedek (Ben Gurion University - Beer Sheva, IL) [dblp]
• Jamy Jue Li (University of Twente, NL) [dblp]
• Daniele Magazzeni (King's College London, GB) [dblp]
• Björn Matthias (ABB AG Forschungszentrum - Ladenburg, DE) [dblp]
• Todd Murphey (Northwestern University - Evanston, US) [dblp]
• Laurel Riek (University of California - San Diego, US) [dblp]
• Kristin Yvonne Rozier (Iowa State University, US) [dblp]
• Dorsa Sadigh (Stanford University, US) [dblp]
• Maha Salem (Google UK - London, GB) [dblp]
• Satoru Satake (ATR - Kyoto, JP) [dblp]
• Jana Tumova (KTH Royal Institute of Technology - Stockholm, SE) [dblp]