Robotics promises to transform how people work, learn, communicate, and engage in other activities of daily living. To do so, robots must interact with users following conventions and norms that people expect, so that people readily adopt them into their environments. These conventions and norms, however, are highly complex and nuanced, requiring that designers consider an impractical number of scenarios, constraints, and requirements in the design process. This project will build new computational methods to facilitate this process, enabling designers of future robot systems to more easily explore the design space for human-robot interactions and to verify that their solutions satisfy design goals. These methods will help achieve the promise of robotics by improving their safety, effectiveness, and reliability.
The design of robotic technologies for human interaction poses a complex, multifaceted design problem that requires that resulting designs satisfy several constraints. Systematically exploring the solution space for actions and behaviors that meet user expectations, follow norms of human interaction, and ensure safety of nearby humans requires an appropriate computational framework for the evaluation and proactive exploration of the space of possible human-robot interactions. This project will devise a novel framework for computationally representing human-robot interactions and exploring the solution space for robot behaviors and actions that satisfy defined correctness properties. Specifically, the project will develop a set of prototypical interaction scenarios and correctness properties; specify formal representations for interaction states and properties, using a variety of temporal logics; apply and extend existing verification methods to verify correctness; devise methods to translate verification output to design feedback; and validate and demonstrate the applicability of the developed framework.
