Partial Satisfaction of Signal Temporal Logic Specifications for Coordination of Multi-Robot Systems

This paper introduces a partial satisfaction (PS) notion for Signal Temporal Logic (STL), finding solutions for specifications that might contain unfeasible or conflicting subformulae. We formulate the planning problem for teams of agents with robust PS of STL missions as a bi-level optimization problem. The goal is to maximize the number of subformulae satisfied with preference to larger ones that have lower depth in the syntax tree of the overall specification. The second objective is to maximize the smallest STL robustness of the feasible subformulae. First, we propose three Mixed Integer Linear Programming (MILP) methods to solve the inner level of the optimization problem, two exact and a relaxation. Then, the MILP solutions are used to find approximate solutions to the outer level optimization using a linear program. Finally, we show the performance of our methods in two multi-robot case studies: motion planning in continuous spaces, and routing for heterogeneous teams over finite graph abstractions.