Sampling-based motion planning with deterministic μ-calculus specifications

In this paper, we propose algorithms for the on-line computation of control programs for dynamical systems that provably satisfy a class of temporal logic specifications. Such specifications have recently been proposed in the literature as a powerful tool to synthesize provably correct control programs, for example for embedded systems and robotic applications. The proposed algorithms, generalizing state-of-the-art algorithms for point-to-point motion planning, incrementally build finite transition systems representing a discrete subset of dynamically feasible trajectories. At each iteration, local μ-calculus model-checking methods are used to establish whether the current transition system satisfies the specifications. Efficient sampling strategies are presented, ensuring the probabilistic completeness of the algorithms. We demonstrate the effectiveness of the proposed approach on simulation examples.