A temporal logic programming approach to planning. (English) Zbl 1419.68101
Summary: 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.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 68N17 | Logic programming |
| 68T30 | Knowledge representation |
Software:
SHOP2References:
| [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-153 |
| [2] | Bacchus F, Kabanza F (2000) Using temporal logics to express search control knowledge for planning. Artif Intell 116(1):123-191 · Zbl 0939.68827 · doi:10.1016/S0004-3702(99)00071-5 |
| [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-42 · Zbl 1379.68287 |
| [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-548 |
| [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-142 |
| [6] | Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle upon Tyne |
| [7] | Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Ottawa |
| [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-186 |
| [9] | Duan Z, Tian C (2014) A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci 554:169-190 · Zbl 1358.68188 · doi:10.1016/j.tcs.2014.02.011 |
| [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-344 |
| [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-199 |
| [12] | Fox M, Long D (2003) PDDL2. 1: an extension to pddl for expressing temporal planning domains. J Artif Intell Res 20:61-124 · Zbl 1036.68093 · doi:10.1613/jair.1129 |
| [13] | Gabrel V (2006) Strengthened 0-1 linear formulation for the daily satellite mission planning. J Comb Optim 11(3):341-346 · Zbl 1255.90138 · doi:10.1007/s10878-006-7912-4 |
| [14] | Ghallab M, Nau D, Traverso P (2004) Automated planning: theory & practice. Elsevier, Amsterdam · Zbl 1074.68613 |
| [15] | Giunchiglia F, Traverso P (1999) Planning as model checking. In: European conference on planning. Springer, pp 1-20 |
| [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-35 |
| [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-123 |
| [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-517 |
| [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-139 |
| [20] | Kvarnström J, Doherty P (2000) Talplanner: a temporal logic based forward chaining planner. Ann Math Artif Intell 30(1-4):119-169 · Zbl 1002.68158 · doi:10.1023/A:1016619613658 |
| [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-202 · Zbl 1291.68263 · doi:10.1007/s10703-013-0197-1 |
| [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-89 · Zbl 1159.68562 · doi:10.1007/s10849-006-9022-1 |
| [23] | Mishra G, Mazumdar S, Pal A (2018) Improved algorithms for the evacuation route planning problem. J Comb Optim 36(1):280-306 · Zbl 1402.90154 · doi:10.1007/s10878-016-0082-0 |
| [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-404 · Zbl 1058.68106 · doi:10.1613/jair.1141 |
| [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-82 |
| [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-778 · Zbl 1390.90552 · doi:10.1007/s10878-016-0003-2 |
| [27] | Shangin RE, Pardalos P (2016) Heuristics for the network design problem with connectivity requirements. J Comb Optim 31(4):1461-1478 · Zbl 1347.90084 · doi:10.1007/s10878-015-9834-5 |
| [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-791 |
| [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-228 |
| [30] | Yang K, Duan Z, Tian C, Zhang N (2018) A compiler for msvl and its applications. Theor Comput Sci 749:2-16 · Zbl 1407.68096 · doi:10.1016/j.tcs.2017.07.032 |
| [31] | Yoon S, Fern A, Givan R (2008) Learning control knowledge for forward search planning. J Mach Learn Res 9:683-718 · Zbl 1225.68246 |
| [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-458 |
| [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-603 · Zbl 1333.90055 · doi:10.1007/s10878-014-9776-3 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
