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.
| Original language | English |
|---|---|
| Title of host publication | 10th International Conference on Interactive Theorem Proving (ITP 2019) |
| Editors | John Harrison, John O'Leary and Andrew Tolmach |
| Place of Publication | USA |
| Publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| Pages | 1-19 |
| ISBN (Print) | 978-3-95977-122-1 |
| DOIs | |
| Publication status | Published - 2019 |
| Event | Interactive Theorem Proving (ITP 2019) - Portland, Oregon Duration: 1 Jan 2019 → … |
Conference
| Conference | Interactive Theorem Proving (ITP 2019) |
|---|---|
| Period | 1/01/19 → … |
| Other | 8-13 September |