2021/02/24 by Tanmoy Kundu, Kundu, Tanmoy, Indranil Saha +1
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Robotic Path Planning Algorithms #Robotics (cs.RO) #Vehicle Routing Optimization Methods
paper · pdf · doi:10.48550/arxiv.2102.12296
openalex publication_date 2021/02/24 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
In many multi-robot applications, mobile worker robots are often engaged in performing some tasks repetitively by following pre-computed trajectories. As these robots are battery-powered, they need to get recharged at regular intervals. We envision that in the future, a few mobile recharger robots will be employed to supply charge to the energy-deficient worker robots recurrently, to keep the overall efficiency of the system optimized.In this setup, we need to find the time instants and locations for the meeting of the worker robots and recharger robots optimally. We present a Satisfiability Modulo Theory (SMT)-based approach that captures the activities of the robots in the form of constraints in a sufficiently long finite-length time window (hypercycle) whose repetitions provide their perpetual behavior. Our SMT encoding ensures that for a chosen length of the hypercycle, the total waiting time of the worker robots due to charge constraints is minimized under certain condition, and close to optimal when the condition does not hold. Moreover, the recharger robots follow the most energy-efficient trajectories. We show the efficacy of our approach by comparing it with another variant of the SMT-based method which is not scalable but provides an optimal solution globally, and with a greedy algorithm.