Abstract
Planning systems use a variety of heuristic search or control knowledge in order to enhance the performance. Control knowledge is often described in a specific formalism, e.g. temporal logic, automata, or HTN (Hierarchical Task Network) etc. Heuristic search exploits heuristic functions to evaluate potential feasible moves. Control knowledge constraints the search space by pruning the states which violate the knowledge. In this paper, we propose a general heuristic algorithm that combines control knowledge specified by a spatio-temporal logic named PPTL\(^{\text{ SL }}\). Both heuristic search and control knowledge are handled in a forward chaining manner. Our approach involves the evaluation of PPTL\(^{\text{ SL }}\) formulas using a variant of the traditional progression technique during heuristic search. Consequently, we are enabled to take advantage of the two methods together to further reduce the search space.
This research is supported by the National Natural Science Foundation of China Grant Nos. 61806158, China Postdoctoral Science Foundation Nos. 2019T120881 and 2018M643585.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1–2), 123–191 (2000). https://doi.org/10.1016/S0004-3702(99)00071-5
Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals using heuristic search. In: Proceedings of the Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16–20, 2006, Boston, Massachusetts, USA, pp. 788–795 (2006). http://www.aaai.org/Library/AAAI/2006/aaai06-125.php
Cui, J., Duan, Z., Tian, C., Du, H.: A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans. Reliab. 67(2), 481–493 (2018). https://doi.org/10.1109/TR.2018.2806349
Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169–190 (2014). https://doi.org/10.1016/j.tcs.2014.02.011
Duan, Z., Tian, C., Zhang, N.: A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor. Comput. Sci. 609, 544–560 (2016). https://doi.org/10.1016/j.tcs.2015.08.039
Erol, K., Hendler, J.A., Nau, D.S.: HTN planning: complexity and expressivity. In: Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31–August 4, 1994, vol. 2, pp. 1123–1128 (1994). http://www.aaai.org/Library/AAAI/1994/aaai94-173.php
Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for the heuristic determination of minimum cost paths. IEEE Trans. Syst. Sci. Cybern. 4(2), 100–107 (1968). https://doi.org/10.1109/TSSC.1968.300136
Helmert, M.: Complexity results for standard benchmark domains in planning. Artif. Intell. 143(2), 219–262 (2003). https://doi.org/10.1016/S0004-3702(02)00364-8
Helmert, M.: The fast downward planning system. J. Artif. Intell. Res. 26, 191–246 (2006). https://doi.org/10.1613/jair.1705
Hoffmann, J., Nebel, B.: The FF planning system: fast plan generation through heuristic search. J. Artif. Intell. Res. 14, 253–302 (2001). https://doi.org/10.1613/jair.855
Kvarnström, J., Magnusson, M.: Talplanner in IPC-2002: extensions and control rules. CoRR. http://arxiv.org/abs/1106.5266 (2011)
Lu, X., Tian, C., Duan, Z.: Temporalising separation logic for planning with search control knowledge. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19–25, 2017, pp. 1167–1173 (2017). https://doi.org/10.24963/ijcai.2017/162
Lu, X., Tian, C., Duan, Z., Du, H.: Planning with spatio-temporal search control knowledge. IEEE Trans. Knowl. Data Eng. 30(10), 1915–1928 (2018). https://doi.org/10.1109/TKDE.2018.2810144
Nau, D.S., et al.: SHOP2: an HTN planning system. J. Artif. Intell. Res. (JAIR) 20, 379–404 (2003). https://doi.org/10.1613/jair.1141
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th IEEE Symposium on Logic in Computer Science (LICS 2002), July 22–25, 2002, Copenhagen, Denmark, pp. 55–74 (2002). https://doi.org/10.1109/LICS.2002.1029817
Tian, C., Duan, Z., Duan, Z., Ong, C.L.: More effective interpolations in software model checking. In: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30–November 03, 2017, pp. 183–193 (2017). https://doi.org/10.1109/ASE.2017.8115631
Tian, C., Duan, Z.: Complexity of propositional projection temporal logic with star. Math. Struct. Comput. Sci. 19(1), 73–100 (2009). https://doi.org/10.1017/S096012950800738X
Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729–1744 (2011). https://doi.org/10.1016/j.tcs.2010.12.047
Tian, C., Duan, Z., Duan, Z.: Making CEGAR more efficient in software model checking. IEEE Trans. Softw. Eng. 40(12), 1206–1223 (2014). https://doi.org/10.1109/TSE.2014.2357442
Wang, L., Baier, J., McIlraith, S.: Viewing landmarks as temporally extended goals. In: ICAPS 2009 Workshop on Heuristics for Domain-Independent Planning, pp. 49–56 (2009)
Yang, K., Duan, Z., Tian, C., Zhang, N.: A compiler for MSVL and its applications. Theor. Comput. Sci. 749, 2–16 (2018). https://doi.org/10.1016/j.tcs.2017.07.032
Yu, B., Duan, Z., Tian, C., Zhang, N.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118(Part), 89–99 (2018). https://doi.org/10.1016/j.jpdc.2017.09.003
Zhang, N., Duan, Z., Tian, C.: A complete axiom system for propositional projection temporal logic with cylinder computation model. Theor. Comput. Sci. 609, 639–657 (2016). https://doi.org/10.1016/j.tcs.2015.05.007
Zhang, N., Duan, Z., Tian, C.: Model checking concurrent systems with MSVL. Sci. China Inf. Sci. 59(11), 118101 (2016). https://doi.org/10.1007/s11432-015-0882-6
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Lu, X. et al. (2020). A Forward Chaining Heuristic Search with Spatio-Temporal Control Knowledge. In: Miao, H., Tian, C., Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2019. Lecture Notes in Computer Science(), vol 12028. Springer, Cham. https://doi.org/10.1007/978-3-030-41418-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-41418-4_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41417-7
Online ISBN: 978-3-030-41418-4
eBook Packages: Computer ScienceComputer Science (R0)