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 等人的研究，探索了用于广义规划的 sound abstraction 的自动验证，并提出了基于模型理论的 sound 和 complete abstraction 的定义。本文还提出了可验证 sound abstraction 的充分条件，并开发了处理计数和传递闭包的方法来实现其验证。最后，本文实现了一个 sound abstraction 验证系统，并在几个领域进行了实验。