Working Seminar on Formal Models, Discrete Structures, and Algorithms

Maximally-satisfying LTL strategy synthesis for robot motion planning

Jana Tůmová (KTH)

When: November 10, 2:00pm

Where: room C417


The application of formal verification methods to automatic control of dependable robotic systems brings two main benefits. First, very complex goals and requirements on the robots' behaviors can be considered thanks to temporal logics. Second, correct-by-design plans/controllers can be automatically generated, guaranteeing that the desired behaviors are achieved. In this talk we discuss situations when the given Linear Temporal Logic (LTL) goals are not feasible, e.g. due to logical conflicts in the goal specifications or environmental constraints. We introduce the concept of LTL maximally-satisfying planning, where we aim to synthesize as good plan/controller as possible instead of reporting the failure to meet the specification. We propose quantitative semantics of LTL, and techniques to automatically generate a maximally-satisfying motion plan. Finally, we show a demonstration of the proposed framework in a NAO robot testbed and an integration with RRT motion planning algorithms implemented in an autonomous golf cart.