Energy-Aware Temporal Logic Motion Planning for Mobile Robots

Abstract

This paper presents a methodology for synthesizing a motion plan for a mobile robot to ensure that the robot never gets depleted with battery charge while carrying out its mission successfully. The specification of the robot is provided in the form of an LTL (Linear Temporal Logic) formula. A trajectory satisfying an LTL formula may contain a loop whose repetitive execution causes the depletion of battery charge in the robot. The motion plan generated by our methodology ensures that the robot visits the charging station periodically in such a way that it never gets depleted with battery charge while carrying out its mission optimally. Given a set of potential charging station locations and an LTL specification, our algorithm also finds the best location for the charging station along with the optimal trajectory for the robot. We encode the motion planning problem as an SMT (Satisfiability Modulo Theory) solving problem and use the off-the-shelf SMT solver Z3 to solve the constraints to find the location of the charging station and generate an optimal trajectory for the robot. We apply our methodology to synthesize energy-aware trajectories for robots with different dynamics in various workspaces and for various LTL specifications.