Spatio-temporal planning at run time
From self-driving vehicles to household vacuum cleaners, mobile autonomous systems have permeated a wide range of application areas. They have a potential to revolutionize today’s transportation and improve quality of life. However, if not realized properly, they may become ineffective, inefficient, or even unsafe, and damage our society’s trust in them. It is thus essential to establish the reliability of autonomous behavior by engaging formal verification and formal methods-based planning and control synthesis methodologies next to testing and simulation.
During the past several years, research in formal methods for mobile autonomous systems has largely focused on considering complex behavioral specifications of such systems, given typically in a rich, rigorous, yet relatively user-friendly language, such as linear temporal logic. As the name suggests, temporal logics allow us to reason about the temporal evolution of internal system states.
However, mobile autonomous systems operate in time and space and it is essential to reason about the physical location of a system or a system component in the environment over time. In state-of-the-art temporal logic-based motion planning, this is typically handled by partitioning of the environment and manual labeling of the obtained regions with atomic propositions, while integrated environment mapping and planning has only been considered in a limited number of very recent works. On the other hand, a major subfield of mobile robotics, localization and mapping, focuses on building spatial representations of the environment, while largely neglecting the temporal aspects.
In this research project, we propose to systematically bridge the two viewpoints. Our main objective is to learn spatio-temporal representations of the environment, and utilize them in motion planning and control under complex spatio-temporal tasks. In addressing this objective, we devote special attention to two particular aspects that are in fact inherent and critical already in traditional motion planning for many mobile autonomous systems: their operation in uncertain environments and their deployment in a team.