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.