RT Journal Article
T1 SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models
A1 Toscano-Moreno, Manuel
A1 Mandow, Anthony
A1 Martínez-Sánchez, María Alcázar
A1 García-Cerezo, Alfonso José
K1 Lógica
AB 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.
PB MDPI
YR 2024
FD 2024
LK https://hdl.handle.net/10630/37354
UL https://hdl.handle.net/10630/37354
LA eng
NO Toscano-Moreno, Manuel, Anthony Mandow, María Alcázar Martínez, y Alfonso José García-Cerezo. «SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models». Sensors 24, n.º 16 (2024). https://doi.org/10.3390/S24165166.
NO This research was partially funded by the Spanish Ministerio de Ciencia e Innovación, Gobierno de España, project PID2021-122944OB-I00, and co-financed by the Agencia Estatal de Investigación and the European Regional Development Fund. The first author would like to acknowledge the Spanish predoctoral grant number BES-2016-077022 from the “Subprograma Estatal de Formación del MICINN” co-financed by the European Social Fund and Universidad de Málaga.
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 19 ene 2026