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.