Abstraction is an important and useful concept in the field of artificial intelligence. To the best of our knowledge, there is no syntactic method to compute a sound and complete abstraction from a given low-level basic action theory and a refinement mapping. This paper aims to address this issue. To this end, we first present a variant of situation calculus, namely linear integer situation calculus, which serves as the formalization of high-level basic action theory. We then migrate Banihashemi, De Giacomo, and Lesperance’s abstraction framework to one from linear integer situation calculus to extended situation calculus. Furthermore, we identify a class of Golog programs, namely guarded actions, so as to restrict low-level Golog programs, and impose some restrictions on refinement mappings. Finally, we design a syntactic approach to computing a sound and complete abstraction from a low-level basic action theory and a restricted refinement mapping.

Generalized planning (GP) 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 GP. Abstractions are widely used to solve GP problems. For example, a popular abstraction model for GP is qualitative numeric planning (QNP), which extends classical planning with non-negative real variables that can be increased or decreased by some arbitrary amount. The refinement of correct solutions of sound abstractions are solutions with correctness guarantees for GP problems. More recent literature proposed a uniform abstraction framework for GP and gave model-theoretic definitions of sound and complete abstractions for GP problems. In this paper, based on the previous work, we explore automatic verification of sound abstractions for GP. Firstly, we present a proof-theoretic characterization for sound abstractions. Secondly, based on the characterization, we give a sufficient condition for sound abstractions with deterministic actions. Then we study how to verify the sufficient condition when the abstraction models are bounded QNPs where integer variables can be incremented or decremented by one. To this end, we develop methods to handle counting and transitive closure, which are often used to define numerical variables. Finally, we implement a sound bounded QNP abstraction verification system and report experimental results on several domains.

Generalized planning aims at finding a general solution for a set of similar planning problems. Abstractions are widely used to solve such problems. However, the connections among these abstraction works remain vague. Thus, to facilitate a deep understanding and further exploration of abstraction approaches for generalized planning, it is important to develop a uniform abstraction framework for generalized planning. Recently, Banihashemi et al. proposed an agent abstraction framework based on the situation calculus. However, expressiveness of such an abstraction framework is limited. In this paper, by extending their abstraction framework, we propose a uniform abstraction framework for generalized planning. We formalize a generalized planning problem as a triple of a basic action theory, a trajectory constraint, and a goal. Then we define the concepts of sound abstractions of a generalized planning problem. We show that solutions to a generalized planning problem are nicely related to those of its sound abstractions. We also define and analyze the dual notion of complete abstractions. Finally, we review some important abstraction works for generalized planning and show that they can be formalized in our framework.