Seminar 2017-05-03

Date: 2017-05-03

Time: 11:00-12:00

Speaker: Jana Tumova, Assistant Professor, KTH Royal Institute of Technology
 

Title: Formal methods-based robot task and motion planning

Abstract
Today's state-of-the-art autonomous robots can do amazing things. They can walk, fly, swim, they can grasp an egg without breaking it, or flip a pancake. And they can accomplish even more complex missions. Driverless cars can navigate through a city, autonomous drones can inspect buildings, and two handed-robots can prepare a pancake from scratch. How do these robots make the right decisions? One of the recently emerged approaches to decision making, planning, and control in robotics uses results from theoretical computer science, in particular from formal verification. This formal verification-based approach combines two strengths: it creates the possibility to capture complex robotic missions in rigorous, yet user-friendly manner, and at the same time offers provable guarantees on the correctness of the behavior resulting from the robot’s decisions.

In this talk, we discuss the opportunities that formal verification brings to robotics and show several of our recent results and applications. In particular, we focus on situations, when a fully correct-by-design behavior cannot be synthesized, e.g., due to logical conflicts in the mission specifications or the constraints imposed by the robot's environment. We introduce the concept of maximally-satisfying planning, where we aim to synthesize as good plan/control strategy as possible instead of reporting the failure to meet the mission specification. Three specific use cases are discussed: reactive control of a NAO robot, whose attempt to execute an action primitive may succeed as well as fail, sampling-based motion planning for an autonomous golf cart that cannot achieve its goal destination without a partial violation of the prescribed road rules, and vehicle routing in a mobility-on-demand system, where all customers’ demands cannot be serviced in time.

Bio
Jana Tumova is an assistant professor at the Department of Robotics, Perception, and Learning at KTH Royal Institute of Technology in Stockholm, Sweden. Prior to that, she was a postdoctoral researcher at the Automatic Control Department at KTH. She received the PhD degree in computer science from Masaryk University in Brno, Czech Republic in 2013 and she was also a visiting researcher at Boston University and MIT. Her research interests include formal verification, control synthesis, and temporal logics in general, as well as formal methods applied in robot motion planning, control and analysis of dynamical and hybrid systems and multi-agent control.