Formalizing and Guaranteeing* Human-Robot Interaction

Hadas Kress-Gazit*, Kerstin I Eder, Guy Hoffman, Henny Admoni, Henna D Argall, Ruediger Ehlers, Christoffer Heckman, Nils Jansen, Ross Knepper, Jan Křetínský, Shelly Levy-Tzedek, Jamy Li, Todd D Murphey, Laurel Riek, Dorsa Sadigh

*Corresponding author for this work

Research output: Contribution to journalArticle (Academic Journal)peer-review

20 Citations (Scopus)
127 Downloads (Pure)


Robot capabilities are maturing across domains, from self-driving cars, to bipeds and drones. As a result, robots will soon no longer be confined to safety-controlled industrial settings; instead, they will directly interact with the general public. The growing field of Human-Robot Interaction (HRI) studies various aspects of this scenario - from social norms to joint action to human-robot teams and more. Researchers in HRI have made great strides in developing models, methods, and algorithms for robots acting with and around humans, but these "computational HRI" models and algorithms generally do not come with formal guarantees and constraints on their operation. To enable human-interactive robots to move from the lab to real-world deployments, we must address this gap.
This article provides an overview of verification, validation and synthesis techniques used to create demonstrably trustworthy systems, describes several HRI domains that could benefit from such techniques, and provides a roadmap for the challenges and the research needed to create formalized and guaranteed human-robot interaction.
Original languageEnglish
Pages (from-to)78-84
Number of pages7
JournalCommunications of the ACM
Issue number9
Publication statusPublished - 24 Aug 2021


  • Human-robot interaction
  • Verification and Validation
  • Trustworthiness
  • Formal Verification
  • Simulation


Dive into the research topics of 'Formalizing and Guaranteeing* Human-Robot Interaction'. Together they form a unique fingerprint.

Cite this