NRI: FND: Robotic Collaboration through Scalable Reactive Synthesis

随着人机协作扩展到越来越复杂的任务，对人类和机器人代理组成的系统进行形式化建模的需求日益增加。这样的建模支持对系统的可靠性、安全性、正确性和可伸缩性进行推理。然而，建模是一项艰巨的任务。本研究的目标是对机器人和人类可以扮演不同角色的场景进行正式建模。其目的是开发可扩展的方法，使机器人能够适应人类的行为和偏好，而无需改变其底层软件或硬件。装配场景将用于模拟制造环境，其中机器人和人类可以一起工作，机器人的动作可以提高人类工作的质量和安全性。该项目是使机器人与人类合作并对人类做出反应的关键一步，同时允许人类控制。本研究将开发一个人机协作的框架，该框架将正式方法中的反应性合成与机器人规划方法相结合。通过将合成方法的开发与机器人技术紧密结合，它将追求一个直观和可扩展的框架的开发。重点是任务级协作，而不是与人的物理交互。该框架以一种新的形式语言定义的任务规范作为输入，这种语言在有限的轨迹上解释：一种适合机器人问题的语言。它为机器人代理生成一个策略，以帮助人类代理，而不管人类代理为该子任务选择了哪个子任务或执行顺序。该策略既包括机器人代理的高级动作，也包括相应的可由实际机器人直接执行的低级动作。该方法的一个关键新颖组成部分是自动构建机器人操作的抽象，可用于综合方法。所提出的工作的可扩展性将沿着不同的维度进行调查：符号推理可以应用的程度，新合成算法的发展，以及抽象的正确使用，包括它们的自动细化和要素抽象的构建。将调查使用部分政策和重新规划相结合的权衡，以及如何解释由于观察不完整而导致的不完整信息。理论贡献将在真实的机器人硬件上实现，并在类似于现实世界组装任务的实验中进行演示。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

As human-robot collaboration is scaled up to more and more complex tasks, there is an increased need for formally modeling the system formed by human and robotic agents. Such modeling enables reasoning about reliability, safety, correctness, and scalability of the system. The modeling, however, presents a daunting task. This research aspires to formally model scenarios where the robot and the human can have varying roles. The intent is to develop scalable methodologies that will endow the robot with the ability to adapt to human actions and preferences without changes to its underlying software or hardware. An assembly scenario will be used to mimic manufacturing settings where a robot and a human may work together and where the actions of the robot can improve the quality and safety of the work of the human. The project is a critical step towards making robots collaborative with and responsive to humans while allowing the human to be in control. This research will develop a framework for human-robot collaboration that integrates reactive synthesis from formal methods with robotic planning methods. By tightly combining the development of synthesis methods with robotics, it will pursue the development of a framework that is intuitive and scalable. The focus is on task-level collaboration as opposed to physical interaction with a human. The framework takes as input a task specification defined in a novel formal language interpreted over finite traces: a language suitable for robotics problems. It produces a policy for a robotic agent to assist a human agent regardless of which subtask or execution order for this subtask that the human agent chooses. The policy includes both high-level actions for the robotic agent as well as corresponding low-level motions that can be directly executed by the actual robot. One key novel component of the approach is the automated construction of abstractions for robotic manipulation that can be used by synthesis methods. The scalability of the proposed work will be investigated along different dimensions: the extent to which symbolic reasoning can be applied, the development of new synthesis algorithms, and the proper use of abstractions including their automatic refinement and the construction of factored abstractions. The trade-offs in using a combination of partial policies and replanning will be investigated as well as how to account for incomplete information due to incomplete observations. The theoretical contributions will be implemented on real robot hardware and demonstrated in experiments that are analogous to real-world assembly tasks.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.