Temporal Logic Optimal Control for Large-Scale Multi-Robot Systems: 10⁴⁰⁰ States and Beyond

Abstract

This paper proposes a new optimal control synthesis algorithm for multi-robot systems with Linear Temporal Logic (LTL) specifications. Existing planning approaches with LTL specifications rely on graph search techniques applied to a product automaton constructed among the robots. In our previous work, we have proposed a more tractable sampling-based algorithm that builds incrementally trees that approximate the state-space and transitions of the synchronous product automaton and does not require sophisticated graph search techniques. Here, we extend our previous work by introducing bias in the sampling process which is guided by transitions in the Büchi automaton that belong to the shortest path to the accepting states. This allows us to synthesize optimal motion plans from product automata with hundreds of orders more states than those that state-of-the-art methods can manipulate. We also show that the proposed algorithm is probabilistically complete and asymptotically optimal.