Document Open Access Logo

A Verified Compositional Algorithm for AI Planning

Authors Mohammad Abdulaziz , Charles Gretton , Michael Norrish

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.4.pdf
  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Mohammad Abdulaziz
  • Technical University of Munich, Germany
Charles Gretton
  • Australian National University, Canberra, Australia
Michael Norrish
  • Data61, CSIRO, Canberra, Australia
  • Australian National University, Canberra, Australia

Funding

  • Abdulaziz, Mohammad: This author is supported by the DFG Koselleck Grant NI 491/16-1.

Cite As Get BibTex

Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. A Verified Compositional Algorithm for AI Planning. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.4

Abstract

We report on our HOL4 verification of an AI planning algorithm. The algorithm is compositional in the following sense: a planning problem is divided into multiple smaller abstractions, then each of the abstractions is solved, and finally the abstractions' solutions are composed into a solution for the given problem. Formalising the algorithm, which was already quite well understood, revealed nuances in its operation which could lead to computing buggy plans. The formalisation also revealed that the algorithm can be presented more generally, and can be applied to systems with infinite states and actions, instead of only finite ones.
Our formalisation extends an earlier model for slightly simpler transition systems, and demonstrates another step towards formal treatments of more and more of the algorithms and reasoning used in AI planning, as well as model checking.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Artificial intelligence
  • Computing methodologies → Planning for deterministic actions
  • Computing methodologies → Planning with abstraction and generalization
  • Software and its engineering → Software verification
Keywords
  • AI Planning
  • Compositional Algorithms
  • Algorithm Verification
  • Transition Systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. Mechanising Theoretical Upper Bounds in Planning. In Workshop on Knowledge Engineering for Planning and Scheduling, 2014. Google Scholar
  2. Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. In Interactive Theorem Proving, pages 1-16. Springer, 2015. Google Scholar
  3. Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. A State Space Acyclicity Property for Exponentially Tighter Plan Length Bounds. In International Conference on Automated Planning and Scheduling (ICAPS). AAAI, 2017. Google Scholar
  4. Mohammad Abdulaziz and Peter Lammich. A Formally Verified Validator for Classical Planning Problems and Solutions. In 2018 IEEE 30th International Conference on Tools with Artificial Intelligence (ICTAI), pages 474-479. IEEE, 2018. Google Scholar
  5. Mohammad Abdulaziz, Michael Norrish, and Charles Gretton. Exploiting symmetries by planning for a descriptive quotient. In Proc. of the 24th International Joint Conference on Artificial Intelligence, IJCAI, pages 25-31, 2015. Google Scholar
  6. Mohammad Abdulaziz, Michael Norrish, and Charles Gretton. Formally Verified Algorithms for Upper Bounding State Space Diameters. In To appear in the Journal of Automated Reasoning, 2017. Google Scholar
  7. Eyal Amir and Barbara Engelhardt. Factored planning. In IJCAI, volume 3, pages 929-935. Citeseer, 2003. Google Scholar
  8. Masataro Asai and Alex Fukunaga. Classical Planning in Deep Latent Space: Bridging the Subsymbolic-Symbolic Boundary. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 6094-6101, 2018. Google Scholar
  9. Saddek Bensalem, Klaus Havelund, and Andrea Orlandini. Verification and validation meet planning and scheduling, 2014. Google Scholar
  10. Craig Boutilier, Richard Dearden, and Moisés Goldszmidt. Stochastic dynamic programming with factored representations. Artificial Intelligence, 121(1):49-107, 2000. Google Scholar
  11. Ronen I Brafman and Carmel Domshlak. Factored planning: How, when, and when not. In AAAI, volume 6, pages 809-814, 2006. Google Scholar
  12. Julian Brunner and Peter Lammich. Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. In NASA Formal Methods Symposium, pages 307-321. Springer, 2016. Google Scholar
  13. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv symbolic model checker. In International Conference on Computer Aided Verification, pages 334-342. Springer, 2014. Google Scholar
  14. Robert L Constable, Paul B Jackson, Pavel Naumov, and Juan C Uribe. Constructively formalizing automata theory. In Proof, language, and interaction, pages 213-238, 2000. Google Scholar
  15. Christian Doczkal, Jan-Oliver Kaiser, and Gert Smolka. A Constructive Theory of Regular Languages in Coq. In International Conference on Certified Programs and Proofs, pages 82-97. Springer, 2013. Google Scholar
  16. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In International Conference on Computer Aided Verification, pages 463-478. Springer, 2013. Google Scholar
  17. Richard E Fikes and Nils J Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial intelligence, 2(3-4):189-208, 1971. Google Scholar
  18. Maria Fox, Richard Howey, and Derek Long. Exploration of the robustness of plans. In AAAI, pages 834-839, 2006. Google Scholar
  19. Robert P Goldman, Ugur Kuter, and Tony Schneider. Using classical planners for plan verification and counterexample generation. In Workshops at the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012. Google Scholar
  20. Marc Hanheide, Moritz Göbelbecker, Graham S. Horn, Andrzej Pronobis, Kristoffer Sjöö, Alper Aydemir, Patric Jensfelt, Charles Gretton, Richard Dearden, Miroslav Janícek, Hendrik Zender, Geert-Jan M. Kruijff, Nick Hawes, and Jeremy L. Wyatt. Robot task planning and explanation in open and uncertain worlds. Artif. Intell., 247:119-150, 2017. Google Scholar
  21. Klaus Havelund, Alex Groce, Gerard Holzmann, Rajeev Joshi, and Margaret Smith. Automated testing of planning models. In International Workshop on Model Checking and Artificial Intelligence, pages 90-105. Springer, 2008. Google Scholar
  22. C Norris Ip and David L Dill. Verifying systems with replicated components in Murϕ. In International Conference on Computer Aided Verification, pages 147-158. Springer, 1996. Google Scholar
  23. C Norris Ip and David L Dill. Verifying systems with replicated components in Murϕ. Formal Methods in System Design, 14(3):273-310, 1999. Google Scholar
  24. Elena Kelareva, Olivier Buffet, Jinbo Huang, and Sylvie Thiébaux. Factored Planning Using Decomposition Trees. In IJCAI, pages 1942-1947, 2007. Google Scholar
  25. C. A. Knoblock. Automatically Generating Abstractions for Planning. Artificial Intelligence, 68(2):243-302, 1994. URL: https://doi.org/10.1016/0004-3702(94)90069-8.
  26. Derek Long. The AIPS-98 Planning Competition. AI MAgazine, 21(2):13-32, 2000. Google Scholar
  27. Kenneth L McMillan. Symbolic model checking. In Symbolic Model Checking, pages 25-60. Springer, 1993. Google Scholar
  28. Lawrence C Paulson. A formalisation of finite automata using hereditarily finite sets. In International Conference on Automated Deduction, pages 231-245. Springer, 2015. Google Scholar
  29. John Penix, Charles Pecheur, and Klaus Havelund. Using model checking to validate AI planner domain models. In Proceedings of the 23rd Annual Software Engineering Workshop, NASA Goddard, 1998. Google Scholar
  30. Nir Pochter, Aviv Zohar, and Jeffrey S. Rosenschein. Exploiting Problem Symmetries in State-Based Planners. In Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2011, San Francisco, California, USA, August 7-11, 2011, 2011. Google Scholar
  31. Buser Say and Scott Sanner. Planning in Factored State and Action Spaces with Learned Binarized Neural Network Transition Models. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., pages 4815-4821, 2018. Google Scholar
  32. Alexander Schimpf, Stephan Merz, and Jan-Georg Smaus. Construction of Büchi automata for LTL model checking verified in Isabelle/HOL. In International Conference on Theorem Proving in Higher Order Logics, pages 424-439. Springer, 2009. Google Scholar
  33. Konrad Slind and Michael Norrish. A Brief Overview of HOL4. In Theorem Proving in Higher Order Logics, volume 5170 of LNCS, pages 28-32. Springer, 2008. Google Scholar
  34. Benjamin Smith, William Millar, Julia Dunphy, Yu-Wen Tung, Pandu Nayak, Ed Gamble, and Micah Clark. Validation and verification of the remote agent for spacecraft autonomy. In 1999 IEEE Aerospace Conference. Proceedings (Cat. No. 99TH8403), volume 1, pages 449-468. IEEE, 1999. Google Scholar
  35. Benjamin D Smith, Martin S Feather, and Nicola Muscettola. Challenges and Methods in Testing the Remote Agent Planner. In AIPS, pages 254-263, 2000. Google Scholar
  36. Margaret H Smith, Gerard J Holzmann, Gordon C Cucullu, and BD Smith. Model Checking Autonomous Planners: Even the Best Laid Plans Must be Verified. In 2005 IEEE Aerospace Conference, pages 1-11. IEEE, 2005. Google Scholar
  37. Christoph Sprenger. A verified model checker for the modal μ-calculus in Coq. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 167-183. Springer, 1998. Google Scholar
  38. Sam Toyer, Felipe W. Trevizan, Sylvie Thiébaux, and Lexing Xie. Action Schema Networks: Generalised Policies With Deep Learning. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 6294-6301, 2018. Google Scholar
  39. Brian C. Williams and P. Pandurang Nayak. A Reactive Planner for a Model-based Executive. In International Joint Conference on Artificial Intelligence, pages 1178-1185. Morgan Kaufmann Publishers, 1997. Google Scholar
  40. Chunhan Wu, Xingyuan Zhang, and Christian Urban. A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). In International Conference on Interactive Theorem Proving, pages 341-356. Springer, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact