Sampling-based algorithms for optimal motion planning with deterministic μ-calculus specifications

Automatic generation of control programs that satisfy complex task specifications given in high-level specification languages such as temporal logics has been studied extensively. However, optimality of such control programs, for instance with respect to a cost function, has received relatively little attention. In this paper, we study the problem of optimal trajectory synthesis for a large class of specifications, given in the form of deterministic mu-calculus. We propose a sampling-based algorithm, based on the Rapidly-exploring Random Graphs (RRGs), that solves this problem with probabilistic completeness and asymptotic optimality guarantees. We evaluate our algorithm in a simulation studies involving a curvature constrained car. Our simulation results show that in this scenario the algorithm quickly discovers a trajectory that satisfies the specification, and improves this trajectory towards an optimal one if allowed more computation time. We also point out connections to (optimal) memoryless winning strategies in infinite parity games, which may be of independent interest.