STyLuS*: A Temporal Logic Optimal Control Synthesis Algorithm for\n Large-Scale Multi-Robot Systems

Abstract

This paper proposes a new highly scalable and asymptotically optimal control\nsynthesis algorithm from linear temporal logic specifications, called\n$\\text{STyLuS}^{*}$ for large-Scale optimal Temporal Logic Synthesis, that is\ndesigned to solve complex temporal planning problems in large-scale multi-robot\nsystems. Existing planning approaches with temporal logic specifications rely\non graph search techniques applied to a product automaton constructed among the\nrobots. In our previous work, we have proposed a more tractable sampling-based\nalgorithm that builds incrementally trees that approximate the state-space and\ntransitions of the synchronous product automaton and does not require\nsophisticated graph search techniques. Here, we extend our previous work by\nintroducing bias in the sampling process which is guided by transitions in the\nB$\\ddot{\\text{u}}$chi automaton that belong to the shortest path to the\naccepting states. This allows us to synthesize optimal motion plans from\nproduct automata with hundreds of orders of magnitude more states than those\nthat existing optimal control synthesis methods or off-the-shelf model checkers\ncan manipulate. We show that $\\text{STyLuS}^{*}$ is probabilistically complete\nand asymptotically optimal and has exponential convergence rate. This is the\nfirst time that convergence rate results are provided for sampling-based\noptimal control synthesis methods. We provide simulation results that show that\n$\\text{STyLuS}^{*}$ can synthesize optimal motion plans for very large\nmulti-robot systems which is impossible using state-of-the-art methods.\n