论文标题
自动验证通用计划的声音抽象
Automatic Verification of Sound Abstractions for Generalized Planning
论文作者
论文摘要
广义计划研究针对一系列计划问题的一般解决方案的计算。长期以来，具有正确性保证的一般解决方案一直是广义计划中的关键问题。抽象被广泛用于解决广义计划问题。声音抽象的解决方案是对于广义计划问题提供正确性保证的方法。最近，Cui等。提出了一个统一的抽象框架，用于广义计划。他们给出了声音的模型理论定义和通用计划问题的完整抽象。在本文中，基于Cui等人的作品，我们探讨了自动验证通用计划的声音抽象。我们首先介绍了声音抽象的证明理论表征。然后，基于表征，我们为一阶可验证的声音抽象提供了足够的条件。为了实现它，我们利用回归扩展，并开发方法来处理计数和及时关闭。最后，我们实施了声音抽象验证系统，并在几个领域报告实验结果。
Generalized planning studies the computation of general solutions for a set of planning problems. Computing general solutions with correctness guarantee has long been a key issue in generalized planning. Abstractions are widely used to solve generalized planning problems. Solutions of sound abstractions are those with correctness guarantees for generalized planning problems. Recently, Cui et al. proposed a uniform abstraction framework for generalized planning. They gave the model-theoretic definitions of sound and complete abstractions for generalized planning problems. In this paper, based on Cui et al.'s work, we explore automatic verification of sound abstractions for generalized planning. We firstly present the proof-theoretic characterization for sound abstraction. Then, based on the characterization, we give a sufficient condition for sound abstractions which is first-order verifiable. To implement it, we exploit regression extensions, and develop methods to handle counting and transitive closure. Finally, we implement a sound abstraction verification system and report experimental results on several domains.
