Reactive Planner Synthesis Under Temporal Logic Specifications

Abstract

This paper proposes a novel, reactive control scheme for autonomous vehicles that fulfills mission specifications as defined by Linear Temporal Logic (LTL) formulas. Our method designs a point-to-point local planner utilizing control Lyapunov functions, which searches for a trajectory that satisfies given mission specifications, providing a path for the vehicle’s low-level controller to follow. Two key characteristics of this local planner are: 1) its ability to generate a trajectory responsive to the current state; and 2) its reflection of the reference path procured from offline planning. Our method exhibits adaptability to disturbances and efficiently guides the vehicle to meet mission requirements. We furnish simulation experiments which manifest the robust performance of our algorithm in diverse scenarios, including evading obstacles and maintaining control amid external disturbances. The proposed approach consistently delivers high mission completion rates and robustness in facing external perturbations.

Keywords

• Formal methods
• reactive control
• robot mission planning