Formal methods based motion planning and control

Autonomous systems like household service robots, self-driving cars and drones are emerging as important parts of our daily lives in the near future. It is desirable to specify robotic tasks in a rich and natural high-level language, and have the robot(s) automatically convert the specifications into a set of low-level primitives, such as feedback controllers and communication protocols to accomplish the task. In this dissertation, we employ formal methods to describe complex motion planning tasks, rather than the well-studied point-to-point navigation in traditional control problems. We bring ideas from formal verification and hybrid control to build a framework in which probably correct motion control laws can be generated to fulfill complex missions in uncertain and dynamic environments.