CAREER: Formal Methods for Robotics and 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.