Formal Verification of Line-following Robot Control Using Linear Temporal Logic

This paper addresses the challenge of ensuring formally verified behaviors in autonomous line-following robots by integrating Linear Temporal Logic (LTL) with sensor-based control. A control synthesis methodology is proposed that transforms temporal logic specifications into executable control strategies for differential drive robots. The approach utilizes an observation map that converts continuous sensor readings into discrete propositions, allowing real-time evaluation of LTL formulas. The implementation features a dual-mode simulation environment, supporting both physics-based dynamic simulation and simplified kinematic analysis. Key contributions include: a formal problem formulation for temporal logic-based line following, a control framework that guaranties satisfaction of complex temporal specifications, and validation demonstrating robust performance under the given track configurations. The results show that the proposed method maintains the accuracy of the tracking while providing formal guaranties for recovery behaviors that meet specifications such as coverage and sequencing requirements. In this work, the integration of formal methods with robot control allows a foundation for developing autonomous systems with verifiable safety and performance characteristics.

Paper Link: https://ieeexplore.ieee.org/document/11502046
Citation/Reference: M. K. M. Rabby, M. F. Jubayer, A. I. Bhuiyan and Z. Mahmud, "Formal Verification of Line-Following Robot Control Using Linear Temporal Logic," 2025 IEEE 4th International Conference on Robotics, Automation, Artificial-Intelligence and Internet-of-Things (RAAICON), Dhaka, Bangladesh, 2025, pp. 621-624, doi: 10.1109/RAAICON69033.2025.11502046.

Видео Formal Verification of Line-following Robot Control Using Linear Temporal Logic канала Md Khurram Monir Rabby