Sampling-Based Optimal Control Synthesis for Multi-Robot Systems under Global Temporal Tasks

This paper proposes a sampling-based algorithm for optimal multi-robot control synthesis under global Linear Temporal Logic formulas. Existing planning approaches under global temporal goals rely on graph search techniques applied to a product automaton constructed among the robots. In this paper, we propose a new sampling-based algorithm that builds incrementally trees that approximate the state-space and transitions of the synchronous product automaton. By approximating the product automaton by a tree rather than representing it explicitly, we require much fewer resources to store it and motion plans can be found by tracing sequences of parent nodes without the need for sophisticated graph search techniques. This significantly increases scalability of our algorithm compared to existing optimal control synthesis methods. We also show that the proposed algorithm is probabilistically complete and asymptotically optimal. Finally, we present numerical experiments that show that our sampling-based approach can synthesize optimal plans from product automata with billions of states, which is not possible using standard optimal control synthesis algorithms or off-the-shelf model checkers.