Synthesis and Robotics
Robots today can mop the floor, assist surgeons and explore space; however, there is no robot that could 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 required for high-level operation exists, what is lacking is the ability to plan at a high-level while providing guarantees for safety and correctness of a robot’s autonomous behavior.
In this talk I will present a formal approach for automatically creating provably correct robot controllers from high-level specifications given in structured English and temporal logic. I will discuss recent work done in my group; specifically, I will describe algorithms and results for (i) analysis of the feasibility of the specifications themselves, (ii) reasoning about the correctness of the robot behavior when it receives wrong sensor information and (iii) guaranteeing high-level behaviors for robots with actions of different time durations. I will also present a python-based toolbox we have designed that controls physical and simulated robots according to specifications written in structured English.