A Verified Compositional Algorithm for AI Planning
A Verified Compositional Algorithm for AI Planning
复制标题
一种经过验证的人工智能规划组合算法
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Michael Norrish
中科院分区：
文献类型：
--
作者：
Mohammad Abdulaziz;Charles Gretton;Michael Norrish
我们报告了我们对AI规划算法的HOL 4验证。该算法在以下意义上是组合的：规划问题被划分为多个较小的抽象，然后解决每个抽象，最后将抽象的解决方案组合成给定问题的解决方案。对算法进行形式化，这已经很好地理解了，揭示了其操作中的细微差别，这可能导致计算错误的计划。形式化还表明，该算法可以更一般地提出，并可以应用于系统的无限状态和行动，而不是只有有限的。我们的形式化扩展了稍简单的过渡系统的早期模型，并展示了对人工智能规划中使用的越来越多的算法和推理以及模型检查的正式处理的另一个步骤。2012年ACM主题分类计算方法学→人工智能;计算方法学→确定性行为规划;计算方法学→抽象和概括规划;软件及其工程→软件验证
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. 2012 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