Abstract

The application of formal verification methods to automatic control of 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 temporal logic goals are not feasible, e.g. due to logical conflicts in the goal specifications or environmental constraints. We introduce the concept of 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 metrics to measure the level of satisfiability, 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.