EAGER: Representations and Methods for Verifiable Human-Robot Interactions

机器人技术有望改变人们的工作、学习、交流和参与其他日常生活活动的方式。要做到这一点，机器人必须按照人们期望的惯例和规范与用户交互，这样人们就可以很容易地将它们应用到他们的环境中。然而，这些约定和规范非常复杂和细微差别，要求设计人员在设计过程中考虑大量不切实际的场景、约束和要求。该项目将建立新的计算方法来促进这一过程，使未来机器人系统的设计者能够更容易地探索人与机器人交互的设计空间，并验证他们的解决方案是否满足设计目标。这些方法将通过提高机器人的安全性、有效性和可靠性来帮助实现机器人的承诺。用于人类交互的机器人技术的设计提出了一个复杂的、多方面的设计问题，要求得到的设计满足几个约束。系统地探索满足用户期望的动作和行为的解决方案空间，遵循人类交互规范，并确保附近人类的安全，需要一个适当的计算框架来评估和主动探索可能的人-机器人交互空间。这个项目将设计一个新的框架，用于以计算方式表示人与机器人的交互，并探索满足定义的正确性属性的机器人行为和动作的解空间。具体地说，该项目将开发一套典型的交互场景和正确性属性；使用各种时序逻辑指定交互状态和属性的形式表示；应用和扩展现有的验证方法以验证正确性；设计将验证输出转换为设计反馈的方法；以及验证和演示所开发框架的适用性。

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.