Path planning with probabilistic roadmaps and co-safe linear temporal logic

Linear Temporal Logic makes it possible to express tasks in terms of propositions, logical connectives, and temporal connectives. This paper shows how to incorporate a subclass of LTL, namely co-safe LTL, into Probabilistic RoadMap (PRM) path planners. PRMs provide an important class of approaches which have been shown to work well for high-dimensional configuration spaces. The proposed Temporal-PRM approach combines the roadmap with a finite automaton representing the co-safe LTL formula φ and conducts the search over the combined graph. As a result, roadmap connections are reused when needed to find paths that satisfy φ. Experimental validation is provided in simulation by using different scenes, co-safe LTL specifications, a snake-like robot model with numerous degrees-of-freedom, and different sampling strategies.