Title: Least-violating Robot Path Planning with LTL Specifications

Abstract: The talk aims at the problem of automatic generation of a 
control strategy for a robotic vehicle given a complex mission 
specification. In particular, we focus on cases when the robot cannot 
accomplish the desired goal as a whole due to the unrealizability of the 
specification and/or the environmental constraints. Our target is to 
find the least-violating control strategy while taking into 
consideration different priorities of different parts of the 
specification. We consider the robot modeled as a deterministic 
transition system and the mission expressed as a set of linear temporal 
logic formulas. We suggest a quantitative metric determining "how close" 
each violating trace of the robot is to a trace satisfying the 
specification and we propose a method that builds on the automata-based 
approach to model-checking to automatically find a provably optimal 
robotic trace with respect to this metric.