# Automatic Verification of Sound Abstractions for Generalized Planning

arXiv: https://arxiv.org/abs/2205.11898 · HTML: https://mlsanity.com/paper/2205.11898/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 31 references that are in the map.
- First posted on arXiv 24 May 2022.

## Builds on (most cited first, 5 of 5)

- [Learning Features and Abstract Actions for Computing Generalized Plans](https://mlsanity.com/paper/1811.07231/) (2018)
- [Features, Projections, and Representation Change for Generalized Planning](https://mlsanity.com/paper/1801.10055/) (2018)
- [Qualitative Numeric Planning: Reductions and Complexity](https://mlsanity.com/paper/1912.04816/) (2019)
- [First-Order Logic with Counting: At Least, Weak Hanf Normal Forms Always Exist and Can Be Computed!](https://mlsanity.com/paper/1703.01122/) (2017)
- [Guarantees for Sound Abstractions for Generalized Planning (Extended Paper)](https://mlsanity.com/paper/1905.12071/) (2019)

## Built on by (most cited first, 1 of 1)

- [Abstracting Situation Calculus Action Theories](https://mlsanity.com/paper/2410.14712/) (2024)

## Abstract (arXiv)

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.