Document Open Access Logo

A Verified Compositional Algorithm for AI Planning

Authors Mohammad Abdulaziz , Charles Gretton , Michael Norrish

Thumbnail 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

Cite AsGet 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)


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
  • AI Planning
  • Compositional Algorithms
  • Algorithm Verification
  • Transition Systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail