Informatics, TU Vienna

Optimal Robot Path Planning with LTL Specifications

We focus on automatic optimal control strategy synthesis specifically tailored for mobile robotic systems.

Abstract

We focus on automatic optimal control strategy synthesis specifically tailored for mobile robotic systems. In particular, we consider high-level planning, when a robot's motion capabilities are modeled as a discrete transition system and its desired task is specified as a linear temporal logic formula. We address cases when multiple plans meet the specification and we introduce an algorithm to find an optimal plan with respect to a carefully chosen cost function. In contrast, we also aim at instances when there is no control strategy ensuring the satisfaction of the desired task as a whole. For such cases, we propose methods to find a least-violating plan. We address separately tasks in the form of long-term missions to be accomplished and safety rules to be obeyed.

Biography

Jana Tumova received the B.S. and M.Sc. degrees in Computer Science from Masaryk University in Brno, Czech Republic in 2006 and 2009, respectively.

Currently, she is a Ph.D. candidate in the Department of Computer Science at Masaryk University. She has spent several months working as a visiting researcher with the Department of Mechanical Engineering at Boston University, the Laboratory for Information and Decision Systems at Massachusetts Institute of Technology (MIT), and the Future Urban Mobility project at Singapore-MIT Alliance for Research and Technology. Her research interests include formal methods and their applications, temporal logics, verification and control strategy synthesis as well as formal methods in robotics, and in robot motion planning in particular.

Note

This talk is organized by the Cyber-Physical Systems Group at the Institute of Computer Engineering.