CAREER: Formal Methods for Robotics and Automation

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

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.