A temporal logic programming approach to planning

  • Kai Yang
  • Cong TianEmail author
  • Nan ZhangEmail author
  • Zhenhua DuanEmail author
  • Hongwei Du


This paper presents an approach to performing artificial intelligence planning through temporal logic programming with Search Control Knowledge (SCK). First, the planning problem described with Planning Domain Description Language is modeled as a program m in Modeling, Simulation and Verification Language (MSVL). Second, the SCK is also specified with an MSVL program \(m'\). Third, using the basic operation “and” in MSVL, a new MSVL program “\(m~and~m'\)” is obtained. Forth, with the compiler MC of MSVL, an executable binary code of program “\(m~and~m'\)” is obtained. Finally, planning result can be obtained via executing the executable code. Experimental results on selected benchmark planning domains from the International Planning Competition 2014 show that our approach is more effective in practice. Furthermore, the obtained plans are verified with the toolkit MSV so that a plan can be confirmed whether it is a reliable one.


Planning Temporal logic MSVL PDDL Search control knowledge 



  1. Bacchus F, Kabanza F (1995) Using temporal logic to control search in a forward chaining planner. In: Proceedings of the 3rd European workshop on planning. IOS Press, pp 141–153Google Scholar
  2. Bacchus F, Kabanza F (2000) Using temporal logics to express search control knowledge for planning. Artif Intell 116(1):123–191MathSciNetCrossRefzbMATHGoogle Scholar
  3. Barták R, Dovier A, Zhou NF (2015) On modeling planning problems in tabled logic programming. In: Proceedings of the 17th international symposium on principles and practice of declarative programming. ACM, pp 31–42Google Scholar
  4. Chrpa L, Barták R (2016) Guiding planning engines by transition-based domain control knowledge. In: Proceedings of the 15th international conference on the principles of knowledge representation and reasoning. AAAI, pp 545–548Google Scholar
  5. Cimatti A, Giunchiglia E, Giunchiglia F, Traverso P (1997) Planning via model checking: a decision procedure for AR. In: European conference on planning. Springer, pp 130–142Google Scholar
  6. Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle upon TyneGoogle Scholar
  7. Duan Z (2005) Temporal logic and temporal logic programming. Science Press, OttawaGoogle Scholar
  8. Duan Z, Tian C (2008) A unified model checking approach with projection temporal logic. In: Proceedings of the 10th international conference on formal engineering methods. Springer, pp 167–186Google Scholar
  9. Duan Z, Tian C (2014) A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci 554:169–190MathSciNetCrossRefzbMATHGoogle Scholar
  10. Duan Z, Koutny M, Holt C (1994) Projection in temporal logic programming. In: Pfenning F (ed) Proceedings of the 5th international conference on logic programming and automated reasoning. Springer, Berlin, LNCS, vol 822, pp 333–344Google Scholar
  11. Fern A, Yoon SW, Givan R (2004) Learning domain-specific control knowledge from random walks. In: Proceedings of the 14th international conference on automated planning and scheduling. AAAI, pp 191–199Google Scholar
  12. Fox M, Long D (2003) PDDL2. 1: an extension to pddl for expressing temporal planning domains. J Artif Intell Res 20:61–124CrossRefzbMATHGoogle Scholar
  13. Gabrel V (2006) Strengthened 0–1 linear formulation for the daily satellite mission planning. J Comb Optim 11(3):341–346MathSciNetCrossRefzbMATHGoogle Scholar
  14. Ghallab M, Nau D, Traverso P (2004) Automated planning: theory & practice. Elsevier, AmsterdamzbMATHGoogle Scholar
  15. Giunchiglia F, Traverso P (1999) Planning as model checking. In: European conference on planning. Springer, pp 1–20Google Scholar
  16. Helmert M, Röger G, Karpas E (2011) Fast downward stone soup: a baseline for building planner portfolios. In: 3rd Workshop on planning and learning (PAL 2011), pp 28–35Google Scholar
  17. Hörne T, van der Poll JA (2008) Planning as model checking: the performance of ProB vs NuSMV. In: Proceedings of the 2008 annual research conference of the South African Institute of Computer Scientists and Information Technologists on IT research in developing countries: riding the wave of technology. ACM, pp 114–123Google Scholar
  18. Huang YC, Selman B, Kautz H, et al. (1999) Control knowledge in planning: benefits and tradeoffs. In: Proceedings of The 16th national conference on artificial intelligence. AAAI, pp 511–517Google Scholar
  19. Kabanza F, Thiébaux S, et al (2005) Search control in planning for temporally extended goals. In: Proceedings of the 15th international conference on automated planning and scheduling. AAAI, pp 130–139Google Scholar
  20. Kvarnström J, Doherty P (2000) Talplanner: a temporal logic based forward chaining planner. Ann Math Artif Intell 30(1–4):119–169CrossRefzbMATHGoogle Scholar
  21. Li Y, Dong JS, Sun J, Liu Y, Sun J (2014) Model checking approach to automated planning. Formal Methods Syst Des 44(2):176–202CrossRefzbMATHGoogle Scholar
  22. Mayer MC, Limongelli C, Orlandini A, Poggioni V (2007) Linear temporal logic as an executable semantics for planning languages. J Log Lang Inf 16(1):63–89MathSciNetCrossRefzbMATHGoogle Scholar
  23. Mishra G, Mazumdar S, Pal A (2018) Improved algorithms for the evacuation route planning problem. J Comb Optim 36(1):280–306MathSciNetCrossRefzbMATHGoogle Scholar
  24. Nau DS, Au TC, Ilghami O, Kuter U, Murdock JW, Wu D, Yaman F (2003) Shop2: an HTN planning system. J Artif Intell Res (JAIR) 20:379–404CrossRefzbMATHGoogle Scholar
  25. Pasula H, Zettlemoyer LS, Kaelbling LP (2004) Learning probabilistic relational planning rules. In: Proceedings of the 14th international conference on automated planning and scheduling. AAAI, pp 73–82Google Scholar
  26. Santos RF, Andrioni A, Drummond AC, Xavier EC (2017) Multicolour paths in graphs: NP-hardness, algorithms, and applications on routing in wdm networks. J Comb Optim 33(2):742–778MathSciNetCrossRefzbMATHGoogle Scholar
  27. Shangin RE, Pardalos P (2016) Heuristics for the network design problem with connectivity requirements. J Comb Optim 31(4):1461–1478MathSciNetCrossRefzbMATHGoogle Scholar
  28. Valenzano RA, Nakhost H, Müller M, Schaeffer J, Sturtevant NR (2012) Arvandherd: Parallel planning with a portfolio. In: Proceedings of the 20th European conference on artificial intelligence. IOS Press, pp 786–791Google Scholar
  29. Wang M, Tian C, Duan Z (2017) Full regular temporal property verification as dynamic program execution. In: Proceedings of the 39th International Conference on Software Engineering. IEEE, pp 226–228Google Scholar
  30. Yang K, Duan Z, Tian C, Zhang N (2018) A compiler for msvl and its applications. Theor Comput Sci 749:2–16MathSciNetCrossRefzbMATHGoogle Scholar
  31. Yoon S, Fern A, Givan R (2008) Learning control knowledge for forward search planning. J Mach Learn Res 9:683–718Google Scholar
  32. Zhang N, Duan Z, Tian C (2014) Extending msvl with function calls. In: Proceedings of the 16th international conference on formal engineering methods. Springer, pp 446–458Google Scholar
  33. Zhang N, Yang M, Gu B, Duan Z, Tian C (2016) Verifying safety critical task scheduling systems in pptl axiom system. J Comb Optim 31(2):577–603MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Institute of Computing Theory and Technology, and ISN Laboratory, Xidian UniversityXi’anChina
  2. 2.Harbin Institute of Technology Shenzhen Graduate SchoolShenzhenChina

Personalised recommendations