License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.4
URN: urn:nbn:de:0030-drops-110596
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11059/
Go to the corresponding LIPIcs Volume Portal

Abdulaziz, Mohammad ; Gretton, Charles ; Norrish, Michael

A Verified Compositional Algorithm for AI Planning

pdf-format:
LIPIcs-ITP-2019-4.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{abdulaziz_et_al:LIPIcs:2019:11059,
  author =	{Mohammad Abdulaziz and Charles Gretton and Michael Norrish},
  title =	{{A Verified Compositional Algorithm for AI Planning}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11059},
  URN =		{urn:nbn:de:0030-drops-110596},
  doi =		{10.4230/LIPIcs.ITP.2019.4},
  annote =	{Keywords: AI Planning, Compositional Algorithms, Algorithm Verification, Transition Systems}
}

Keywords: AI Planning, Compositional Algorithms, Algorithm Verification, Transition Systems
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: All of our HOL4 scripts are available online at https://doi.org/10.5281/zenodo.3298914.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI