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.
翻译：通用规划研究对一套规划问题的一般解决办法的计算; 具有正确性保证的计算机一般解决办法长期以来一直是普遍规划中的一个关键问题; 抽象学被广泛用于解决普遍规划问题; 健全的抽象学的解决方案是普遍规划问题具有正确性保障的解决方案; 最近, Cui et al. 提议了一个统一的全面规划抽象学框架; 给出了普遍规划问题健全和完整的抽象学的模型理论定义; 在本文件中,根据Cui et al. 的工作,我们探索了对合理抽象学的自动核查,以便进行普遍规划。 我们首先提出了对合理抽象学的校对特征的描述。 然后,根据特征,我们为合理的抽象学提供了充分的条件,这是可以首先核查的。 为了实施这一特征,我们利用回归延伸,并制订方法来处理普遍规划问题的计算和过渡性结束。 最后,我们实施了一个健全的抽象核查系统,并报告若干领域的实验结果。
相关内容
微信扫码咨询专知VIP会员