{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:21:17Z","timestamp":1760145677475,"version":"build-2065373602"},"reference-count":30,"publisher":"MDPI AG","issue":"16","license":[{"start":{"date-parts":[[2024,8,10]],"date-time":"2024-08-10T00:00:00Z","timestamp":1723248000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004837","name":"Spanish Ministerio de Ciencia e Innovaci\u00f3n, Gobierno de Espa\u00f1a","doi-asserted-by":"publisher","award":["PID2021-122944OB-I00","BES-2016-077022"],"award-info":[{"award-number":["PID2021-122944OB-I00","BES-2016-077022"]}],"id":[{"id":"10.13039\/501100004837","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Agencia Estatal de Investigaci\u00f3n and the European Regional Development Fund","award":["PID2021-122944OB-I00","BES-2016-077022"],"award-info":[{"award-number":["PID2021-122944OB-I00","BES-2016-077022"]}]},{"name":"Subprograma Estatal de Formaci\u00f3n del MICINN","award":["PID2021-122944OB-I00","BES-2016-077022"],"award-info":[{"award-number":["PID2021-122944OB-I00","BES-2016-077022"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.3390\/s24165166","type":"journal-article","created":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T11:23:46Z","timestamp":1723461826000},"page":"5166","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models"],"prefix":"10.3390","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2012-7853","authenticated-orcid":false,"given":"Manuel","family":"Toscano-Moreno","sequence":"first","affiliation":[{"name":"Institute for Mechatronics Engineering and Cyber-Physical Systems, Robotics and Mechatronics Group, Universidad de M\u00e1laga, 29071 M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9994-6239","authenticated-orcid":false,"given":"Anthony","family":"Mandow","sequence":"additional","affiliation":[{"name":"Institute for Mechatronics Engineering and Cyber-Physical Systems, Robotics and Mechatronics Group, Universidad de M\u00e1laga, 29071 M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8249-9201","authenticated-orcid":false,"given":"Mar\u00eda Alc\u00e1zar","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"Institute for Mechatronics Engineering and Cyber-Physical Systems, Robotics and Mechatronics Group, Universidad de M\u00e1laga, 29071 M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3432-3230","authenticated-orcid":false,"given":"Alfonso Jos\u00e9","family":"Garc\u00eda-Cerezo","sequence":"additional","affiliation":[{"name":"Institute for Mechatronics Engineering and Cyber-Physical Systems, Robotics and Mechatronics Group, Universidad de M\u00e1laga, 29071 M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2024,8,10]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1109\/TRO.2020.3031254","article-title":"Control of Mobile Robots Using Barrier Functions under Temporal Logic Specifications","volume":"37","author":"Srinivasan","year":"2021","journal-title":"IEEE Trans. Robot."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Filippidis, I., Dathathri, S., Livingston, S.C., Ozay, N., and Murray, R.M. (2016, January 19\u201322). Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox. Proceedings of the IEEE Conference on Control Applications, Buenos Aires, Argentina.","DOI":"10.1109\/CCA.2016.7587949"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Belta, C., Yordanov, B., and Gol, E.A. (2017). Formal Methods for Discrete-Time Dynamical Systems, Springer.","DOI":"10.1007\/978-3-319-50763-7"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","article-title":"Linear Temporal Logic Symbolic Model Checking","volume":"5","author":"Rozier","year":"2011","journal-title":"Comput. Sci. Rev."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"112086","DOI":"10.1016\/j.knosys.2024.112086","article-title":"VALIO: Visual attention-based linear temporal logic method for explainable out-of-the-loop identification","volume":"299","author":"Lyu","year":"2024","journal-title":"Knowl. Based Syst."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1109\/TAC.2007.914952","article-title":"A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications","volume":"53","author":"Kloetzer","year":"2008","journal-title":"IEEE Trans. Autom. Control."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","article-title":"Temporal-logic-based reactive mission and motion planning","volume":"25","author":"Fainekos","year":"2009","journal-title":"IEEE Trans. Robot."},{"key":"ref_8","first-page":"588","article-title":"Simulation of collaborative multi-robots","volume":"310 CCIS","author":"Kim","year":"2012","journal-title":"Commun. Comput. Inf. Sci."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"1956","DOI":"10.1017\/S0263574719000377","article-title":"Optimal Path Planning Satisfying Complex Task Requirement in Uncertain Environment","volume":"37","author":"Yu","year":"2019","journal-title":"Robotica"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Amram, G., Maoz, S., Segall, I., and Yossef, M. (2022, January 25\u201327). Dynamic Update for Synthesized GR(1) Controllers. Proceedings of the International Conference on Software Engineering, Pittsburgh, PA, USA.","DOI":"10.1145\/3510003.3510054"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"1082","DOI":"10.1109\/TRO.2018.2830370","article-title":"Multirobot Data Gathering under Buffer Constraints and Intermittent Communication","volume":"34","author":"Guo","year":"2018","journal-title":"IEEE Trans. Robot."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"4991","DOI":"10.1109\/LRA.2023.3290531","article-title":"Fast Task Allocation of Heterogeneous Robots with Temporal Logic and Inter-Task Constraints","volume":"8","author":"Li","year":"2023","journal-title":"IEEE Robot. Autom. Lett."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Kikuchi, Y., Adachi, S., Inoue, H., and Hashimoto, K. (2020, January 6\u201310). Path planning for lunar polar exploration mission using linear temporal logic. Proceedings of the AIAA Scitech 2020 Forum, Orlando, FL, USA. PartF.","DOI":"10.2514\/6.2020-2199"},{"key":"ref_14","unstructured":"Khalidi, D., Gujarathi, D., and Saha, I. (August, January 31). T*: A Heuristic Search Based Path Planning Algorithm for Temporal Logic Specifications. Proceedings of the IEEE International Conference on Robotics and Automation, Paris, France."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Baek, C., and Cho, K. (2024). Deep Learning-Enhanced Sampling-Based Path Planning for \u201cLTL\u201d Mission Specifications. Sensors, 24.","DOI":"10.3390\/s24102998"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"4913","DOI":"10.1109\/TRO.2023.3299524","article-title":"Integrated Task and Motion Planning for Safe Legged Navigation in Partially Observable Environments","volume":"39","author":"Shamsah","year":"2023","journal-title":"IEEE Trans. Robot."},{"key":"ref_17","unstructured":"Holzmann, G.J. (2003). The SPIN Model Checker\u2014Primer and Reference Manual, Addison-Wesley."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., and Murray, R.M. (2011, January 12\u201314). TuLiP: A software toolbox for receding horizon temporal logic planning. Proceedings of the Hybrid Systems: Computation and Control, Chicago, IL, USA.","DOI":"10.1145\/1967701.1967747"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"3602","DOI":"10.1109\/TRO.2022.3181948","article-title":"Temporal Logic Task Allocation in Heterogeneous Multirobot Systems","volume":"38","author":"Luo","year":"2022","journal-title":"IEEE Trans. Robot."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"1472","DOI":"10.1109\/TRO.2018.2861901","article-title":"Control of Magnetic Microrobot Teams for Temporal Micromanipulation Tasks","volume":"34","author":"Kantaros","year":"2018","journal-title":"IEEE Trans. Robot."},{"key":"ref_21","unstructured":"Bernardo, M., and Corradini, F. (2004). A Tutorial on Uppaal. Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Bertinora, Italy, 13\u201318 September 2004; Revised Lectures, Springer."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3342355","article-title":"Formal Specification and Verification of Autonomous Robotic Systems: A Survey","volume":"52","author":"Luckcuck","year":"2019","journal-title":"ACM Comput. Surv."},{"key":"ref_23","first-page":"445","article-title":"Formal Synthesis of Safe Stop Tactical Planners for an Automated Vehicle","volume":"53","author":"Krook","year":"2020","journal-title":"IFAC Workshop Discret. Event Syst. IFAC-PapersOnLine"},{"key":"ref_24","unstructured":"Ben-Ari, M. (2008). Principles of the Spin Model Checker, Springer Science & Business Media."},{"key":"ref_25","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, The Massachusetts Institute of Technology."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"105976","DOI":"10.1016\/j.engappai.2023.105976","article-title":"DEM-AIA: Asymmetric inclination-aware trajectory planner for off-road vehicles with digital elevation models","volume":"121","author":"Mandow","year":"2023","journal-title":"Eng. Appl. Artif. Intell."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"5181","DOI":"10.1109\/LRA.2020.3005123","article-title":"Terrain-Aware Path Planning and Map Update for Mars Sample Return Mission","volume":"5","author":"Hedrick","year":"2020","journal-title":"IEEE Robot. Autom. Lett."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez-Iba\u00f1ez, J.R., P\u00e9rez-del Pulgar, C.J., and Garc\u00eda-Cerezo, A. (2021). Path Planning for Autonomous Mobile Robots: A Review. Sensors, 21.","DOI":"10.3390\/s21237898"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Toscano-Moreno, M., Bravo-Arrabal, J., S\u00e1nchez-Montero, M., Ser\u00f3n Barba, J., V\u00e1zquez-Mart\u00edn, R., Fernandez-Lozano, J.J., Mandow, A., and Garcia-Cerezo, A. (2022, January 8\u201310). Integrating ROS and Android for Rescuers in a Cloud Robotics Architecture: Application to a Casualty Evacuation Exercise. Proceedings of the IEEE International Symposium on Safety, Security, and Rescue Robotics, Sevilla, Spain.","DOI":"10.1109\/SSRR56537.2022.10018629"},{"key":"ref_30","unstructured":"UMA (2024, June 01). LAENTIEC: Laboratory and Experimentation Area in New Technologies for Emergency Intervention. Available online: https:\/\/www.uma.es\/laentiec."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/24\/16\/5166\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T15:34:31Z","timestamp":1760110471000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/24\/16\/5166"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,10]]},"references-count":30,"journal-issue":{"issue":"16","published-online":{"date-parts":[[2024,8]]}},"alternative-id":["s24165166"],"URL":"https:\/\/doi.org\/10.3390\/s24165166","relation":{},"ISSN":["1424-8220"],"issn-type":[{"type":"electronic","value":"1424-8220"}],"subject":[],"published":{"date-parts":[[2024,8,10]]}}}