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

Area of Science:

• Robotics
• Artificial Intelligence
• Computer Science

Background:

• Linear Temporal Logic (LTL) ensures mobile robot planning correctness.
• Planning on uneven terrain requires considering slope traversability and maneuverability constraints.
• Global LTL properties for complex missions on Digital Elevation Models (DEMs) lead to high computation times.

Purpose of the Study:

• To propose a system model that separates Uncrewed Ground Vehicle (UGV) motion constraints from LTL model checking.
• To enable LTL properties to solely define mission specifications for path planning.
• To reduce computational cost in LTL-based path planning for UGVs on DEMs.

Main Methods:

• Developed a system model incorporating UGV motion constraints, allowing their omission from LTL model checking.
• Utilized an LTL synthesizer for path planning with mission specifications only.
• Parameterized path planning synthesis using the Simple Promela Interpreter (SPIN).
• Formulated two SPIN-efficient general LTL formulas for UGV missions on DEM partitions.

Main Results:

• Demonstrated feasibility for complex mission specifications on DEMs through validation experiments.
• Achieved significant reduction in computation cost compared to a baseline global LTL property approach.
• Showcased effectiveness on both synthetic and real-world DEM data.

Conclusions:

• The proposed framework effectively handles complex UGV missions on DEMs.
• Separating motion constraints from LTL model checking drastically reduces computational overhead.
• This method enhances the efficiency of LTL-based path planning for mobile robots in challenging terrains.