Path Planning for Unmanned Campus Sightseeing Vehicle with Linear Temporal Logic
In order to solve the global path planning problem of unmanned campus sightseeing vehicles, this paper proposes a path optimization method based on linear temporal logic (LTL). First, the plan avoids the cumbersome and huge modeling for the actual road environment, and all the stops are modeled as a weighted finite-state transition system. Second, use LTL language to describe the tasks that the unmanned sightseeing vehicle needs to perform in actual operations. Next, construct a Product automaton that contains the environment model and task requirements. Finally, use a path search method based on Dijkstra algorithm to search for the optimal route on the Product automaton, and the optimal route is mapped back to the stops transition system in the actual environment, so that the route which the vehicle needs to perform during actual operation is obtained. Simulation results show that this method can completely solve the problem of patrolling between multiple stops, and can guarantee the optimality of the operating route.
KeywordsUnmanned campus sightseeing vehicle Linear temporal logic Path planning Multi-point patrol
This work is supported by Natural Science Fund of Henan Provice, China (182300410112).
- 4.H. Lin, W. Zhang, Model checking: theories, techniques and application. Acta Electron. Sinica S1, 1907–1912 (2002). (in Chinese)Google Scholar
- 5.X. Ding, M. Lazar, C. Belta, Receding horizon temporal logic control for finite deterministic systems. Automatica, 2012, 50(2), 399–408Google Scholar
- 9.S.L. Smith, C. Belta, D. Rus, Optimal path planning under temporal logic contstraints, in International Conference on Intelligent Robots and Systems. IEEE, 3288–3293 (2010)Google Scholar
- 10.J. Guo, M. Bian, J. Han, Translation from LTL formula into Büchi automata. Comput. Sci. 35(7), 241–243 (2008). (in Chinese)Google Scholar