Path Planning for Unmanned Campus Sightseeing Vehicle with Linear Temporal Logic

  • Mengtian Jiao
  • Yunzhong SongEmail author
Conference paper
Part of the Lecture Notes in Electrical Engineering book series (LNEE, volume 528)


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.


Unmanned campus sightseeing vehicle Linear temporal logic Path planning Multi-point patrol 



This work is supported by Natural Science Fund of Henan Provice, China (182300410112).


  1. 1.
    F. Duchoň, A. Babinec, M. Kajan et al., Path planning with modified a star algorithm for a mobile robot. Proc. Eng. 96(96), 59–69 (2014)CrossRefGoogle Scholar
  2. 2.
    E. Onieva, J.E. Naranjo, V. Milanés et al., Automatic lateral control for unmanned vehicles via genetic algorithms. Appl. Soft Comput. 11(1), 1303–1309 (2011)CrossRefGoogle Scholar
  3. 3.
    K. Ghoseiri, B. Nadjari, An ant colony optimization algorithm for the bi-objective shortest path problem. Appl. Soft Comput. 10(4), 1237–1246 (2010)CrossRefGoogle Scholar
  4. 4.
    H. Lin, W. Zhang, Model checking: theories, techniques and application. Acta Electron. Sinica S1, 1907–1912 (2002). (in Chinese)Google Scholar
  5. 5.
    X. Ding, M. Lazar, C. Belta, Receding horizon temporal logic control for finite deterministic systems. Automatica, 2012, 50(2), 399–408Google Scholar
  6. 6.
    A. Ulusoy, C. Belta, Receding horizon temporal logic control in dynamic environments. Int. J. Robot. Res. 33(12), 1593–1607 (2014)CrossRefGoogle Scholar
  7. 7.
    T. Wongpiromsarn, U. Topcu, R.M. Murray, Receding horizon temporal logic planning. IEEE Trans. Autom. Control 57(11), 2817–2830 (2012)MathSciNetCrossRefGoogle Scholar
  8. 8.
    S.L. Smith, J. Tůmová, C. Belta et al., Optimal path planning for surveillance with temporal-logic constraints. Int. J. Robot. Res. 30(14), 1695–1708 (2011)CrossRefGoogle Scholar
  9. 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. 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
  11. 11.
    Y. Jia, Robust control with decoupling performance for steering and traction of 4WS vehicles under velocity-varying motion. IEEE Trans. Control Syst. Technol. 8(3), 554–569 (2000)CrossRefGoogle Scholar
  12. 12.
    Y. Jia, Alternative proofs for improved LMI representations for the analysis and the design of continuous-time systems with polytopic type uncertainty: a predictive approach. IEEE Trans. Autom. Control 48(8), 1413–1416 (2003)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Singapore Pte Ltd. 2019

Authors and Affiliations

  1. 1.School of Electrical Engineering and AutomationHenan Polytechnic UniversityJiaozuoChina

Personalised recommendations