Automatic Verification of Sound Abstractions for Generalized Planning

TL;DR

This paper develops a method to automatically verify sound abstractions in generalized planning, ensuring correctness guarantees through a proof-theoretic approach and implementing a verification system tested on multiple domains.

Contribution

It introduces a proof-theoretic characterization for sound abstractions, providing a first-order verifiable sufficient condition and a practical verification system.

Findings

Successfully verified sound abstractions in several planning domains.

Developed methods to handle counting and transitive closure in verification.

Experimental results demonstrate effectiveness of the verification system.

Abstract

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.