Toscano-Moreno Manuel, Mandow Anthony, Martínez María Alcázar, García-Cerezo Alfonso José
Institute for Mechatronics Engineering and Cyber-Physical Systems, Robotics and Mechatronics Group, Universidad de Málaga, 29071 Málaga, Spain.
Sensors (Basel). 2024 Aug 10;24(16):5166. doi: 10.3390/s24165166.
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.
线性时态逻辑（LTL）形式化方法能够通过简洁、可读且可验证的任务规范来确保移动机器人规划的正确性。对于不平坦地形，规划必须考虑与不对称斜坡可穿越性和机动性相关的运动约束。然而，尽管诸如开源的简单Promela解释器（SPIN）之类的模型检查工具包含搜索优化技术来解决状态爆炸问题，但在数字高程模型（DEM）上定义一个既包含任务规范又包含运动约束的全局LTL属性可能会导致模型复杂且计算时间长。在本文中，我们提出了一个包含一组无人地面车辆（UGV）运动约束的系统模型，使得这些约束在LTL模型检查中可以被省略。该模型用于路径规划的LTL合成器中，其中LTL属性仅描述任务规范。此外，我们给出了一种使用SPIN进行路径规划合成的特定参数化方法。我们还针对具有代表性的UGV任务分别提供了两个对SPIN高效的通用LTL公式，用于按指定或未指定顺序到达DEM分区集。在合成和真实世界的DEM上进行的验证实验证明了该框架对于DEM上复杂任务规范的可行性，与包含全局LTL属性的基线方法相比，即使在两个路径规划器上都应用了适当的搜索优化技术，计算成本也显著降低。
