Automatic Verification of Sound Abstractions for Generalized Planning
This work addresses the challenge of ensuring correctness in generalized planning for AI researchers, but it is incremental as it builds directly on prior work by Cui et al.
The paper tackles the problem of automatically verifying sound abstractions in generalized planning, which ensures correctness guarantees for general solutions, by presenting a proof-theoretic characterization and implementing a verification system with experimental results.
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.