Sampling-based algorithms for optimal motion planning using process algebra specifications

This paper investigates motion-planning using formal language specifications for dynamical systems with differential constraints. In particular, we focus on process algebra as a language to specify complex task specifications motivated by autonomous electric vehicles operating in a mobility-on-demand scenario. We use ideas from sampling-based motion-planning algorithms to incrementally construct a finite abstraction of the dynamical system as a Kripke structure. Given a task specification expressed as a process graph, we use model checking techniques to construct a weighted product graph of the specification with the Kripke structure. We then devise an algorithm that provably converges to the optimal trajectory of the dynamical system that satisfies the task specification as the number of the states in the Kripke structure goes to infinity. The algorithm is demonstrated in simulation experiments, viz., charging the electric car at a busy charging station and scheduling pick-ups and drop-offs of passengers.