SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models

Abstract

Linear temporal logic (LTL) formalism can ensure the correctness of mobile robot planning through concise, readable, and verifiable mission specifications. For uneven terrain, planning must consider motion constraints related to asymmetric slope traversability and maneuverability. However, even though model checker tools like the open-source Simple Promela Interpreter (SPIN) include search optimization techniques to address the state explosion problem, defining a global LTL property that encompasses both mission specifications and motion constraints on digital elevation models (DEMs) can lead to complex models and high computation times. In this article, we propose a system model that incorporates a set of uncrewed ground vehicle (UGV) motion constraints, allowing these constraints to be omitted from LTL model checking. This model is used in the LTL synthesizer for path planning, where an LTL property describes only the mission specification. Furthermore, we present a specific parameterization for path planning synthesis using a SPIN. We also offer two SPIN-efficient general LTL formulas for representative UGV missions to reach a DEM partition set, with a specified or unspecified order, respectively. Validation experiments performed on synthetic and real-world DEMs demonstrate the feasibility of the framework for complex mission specifications on DEMs, achieving a significant reduction in computation cost compared to a baseline approach that includes a global LTL property, even when applying appropriate search optimization techniques on both path planners.