Synthesis, Analysis, And Revision Of Correct-By-Construction Controllers For Robots With Sensing And Actuation Errors

Recently developed techniques in automatic synthesis of correct-by-construction robot controllers from a set of high-level task specifications offer a number of advantages over other, more traditional, methods of programming robots. Such synthesis techniques allow for quick, intuitive creation of controllers for complex tasks, such that the resulting controller is guaranteed to satisfy its underlying task specification. This guarantee, however, is predicated on the assumption that the robot operates without error in its sensing and actuation. My Ph.D. dissertation provides methods for probabilistically modeling errors in the robot's sensors and actuators, and using those models to compute the probability that the robot (running such a synthesized controller) will exhibit the desired behavior. Furthermore, I provide methods for leveraging that analysis of the controller to automatically provide the user with suggestions for revisions to the task specification, in order to improve the robot's probabilistic behavior. Finally, I discuss the incorporation of the sensor/actuator error models into the actual synthesis step. By considering the error models, we can synthesize the controller that is most likely to satisfy the given specification, when operating with the modeled errors. This work provides an important tool for reliably applying controller synthesis techniques to real-world problems, where the robot's sensors and actuators are imperfect