LIPIcs.ITP.2019.4.pdf
- Filesize: 0.54 MB
- 19 pages
Document
A Verified Compositional Algorithm for AI Planning
Authors
Mohammad Abdulaziz 
,
Charles Gretton ,
Michael Norrish
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Author Details
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)
https://doi.org/10.4230/LIPIcs.ITP.2019.4
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)
0PDF Downloads