CAREER: Formal Methods for Robotics and Automation

职业：机器人和自动化的形式化方法

• 批准号: 0953365
• 负责人: Hadas Kress Gazit
• 金额: $ 51.18万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-04-15 至 2016-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0953365&HistoricalAwards=false
• 关键词: CAREER; Formal; Methods; Robotics; Automation

Robots today can assist surgeons and explore space; however, they cannot be trusted to drive autonomously in a real city. Robots either perform simple or hard-coded tasks fully autonomously or they operate with close human supervision. While most of the sensing and actuation technology exists, what is lacking is the ability to provide guarantees for safety and correctness of a robot's high-level, autonomous behavior.The objective of this project is to develop mathematical formalisms and algorithms that will provide guarantees for the success of a high-level task, specified by a human using temporal logic and performed by a robot operating in an uncertain world. These techniques will pave the way towards creating truly correct autonomous robots thus making a significant impact in our community. Specifically, the PI is developing mathematical theory, algorithms and open-source tools to address the following challenges: (i) When a robot task is infeasible determine and communicate why it cannot be achieved;(ii) Given known bounds on sensor and action uncertainties, provide offline guarantees for task success; (iii) Provide online guarantees and task progress as new information regarding the workspace is gathered.Broader impacts of the project include: (i) building a community of researchers interested in formal methods for robotics and automation, and (ii) increasing the number of women pursuing an engineering career. For the former, undergraduate and graduate students are mentored, two courses taught by the PI are enhances and workshops are organized. For the latter, the PI is designing and supervising a robotics-based project for female high school students during a summer program, and is working to recruit women through recruiting weekends and a series of talks at other institutions.

如今的机器人可以协助外科医生并探索太空；然而，不能相信它们能够在真实的城市中自动驾驶。机器人要么完全自主地执行简单或硬编码的任务，要么在人类的密切监督下运行。虽然大多数传感和驱动技术都存在，但缺乏的是为机器人高级自主行为的安全性和正确性提供保证的能力。该项目的目标是开发数学形式和算法，为高级任务的成功提供保证，该高级任务由人类使用时间逻辑指定并由在不确定世界中运行的机器人执行。 这些技术将为创建真正正确的自主机器人铺平道路，从而对我们的社区产生重大影响。 具体来说，PI 正在开发数学理论、算法和开源工具，以应对以下挑战：(i) 当机器人任务不可行时，确定并传达无法实现的原因；(ii) 给定传感器和动作不确定性的已知界限，为任务成功提供离线保证； (iii) 随着收集到有关工作空间的新信息，提供在线保证和任务进展。该项目的更广泛影响包括：(i) 建立一个对机器人和自动化正式方法感兴趣的研究人员社区，以及 (ii) 增加从事工程职业的女性数量。 对于前者，本科生和研究生得到指导，PI教授的两门课程得到加强，并组织研讨会。 对于后者，PI 正在暑期项目期间为女高中生设计和监督一个基于机器人的项目，并致力于通过周末招募和在其他机构举行的一系列讲座来招募女性。