A Uniform Abstraction Framework for Generalized Planning

1 Introduction

Generalized planning, where a single plan works for possibly infinitely many similar planning problems, has received continual attention in the AI community [Srivastava et al., 2008; Hu and De Giacomo, 2011; Srivastava et al., 2011; Segovia-Aguas et al., 2016; Bonet and Geffner, 2018; Illanes and McIlraith, 2019]. For example, the generalized plan "while the block A is not clear, pick the top block above A and place it on the table" meets the goal clear(A) no matter how many blocks the tower has.

Abstractions are widely used to solve generalized planning problems. The idea is to develop an abstract model of the problem that suppresses less important details, find a solution in the abstract model, and use this solution to guide the search for a solution in the concrete model. For example, Srivastava et al. [2011] introduced qualitative numerical planning (QNP) problems, which represents a set of quantitative numerical planning problems. They showed that a QNP problem P can be easily abstracted into a FOND (fully observable non-deterministic planning) problem whose strong cyclic solutions that terminate in P are solutions to P. To explain why the termination condition is needed and how it can be removed, Bonet et al. [2017] showed that a planning problem can be extended with a trajectory constraint and the solutions to the problem are programs whose executions satisfying the constraint terminate. Bonet and Geffner [2018] considered solving generalized classical planning problems. They showed that if such a problem P

∗Corresponding Author

a QNP problem P ′ and if the abstraction is sound, then the solution of P ′ is a solution of P. Illanes andMcIlraith [2019] considered solving a class of generalized classical planning problems by automatically deriving a sound QNP abstraction from an instance of the problem, by introducing a counter for each set of indistinguishable objects.

The existing abstraction works for generalized planning are closely related to each other. However, the similarities and differences of them remain vague. Thus, to facilitate a deep understanding and further exploration of abstraction approaches for generalized planning, it is important to develop a uniform theoretical framework for them.

Recently, Banihashemi et al. [2017] proposed an agent abstraction framework based on the situation calculus [Reiter, 2001] and the Golog [Levesque et al., 1997] agent programming language. They relate a high-level action theory to a low-level action theory by the notion of a refinement mapping, which specifies how each high-level action is implemented by a low-level Golog program and how each high-level fluent can be translated into a low-level formula. They define the concepts of sound/complete abstractions of a low-level action theory and prove properties that relate the behavior of a low-level action theory to the behavior of its sound/complete abstractions. However, expressiveness of such an abstraction framework is limited, and cannot serve as a uniform abstraction framework for generalized planning.

In this paper, by extending the abstraction framework of Banihashemi et al., we propose a uniform abstraction framework for generalized planning. We first extend the situation calculus with counting and use non-deterministic Golog programs to represent actions with non-deterministic effects, and 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/complete abstractions of a generalized planning problem. We show that solutions to a generalized planning problem are nicely related to those of its sound/complete abstractions. Finally, we review some important abstraction works for generalized planning and show that they can be formalized in our framework.

2 Preliminaries

In this section, we introduce the situation calculus extended with infinite histories and Golog.

The situation calculus [Reiter, 2001] is a many-sorted firstorder language with some second-order ingredients suitable for describing dynamic worlds. There are three disjoint sorts: action for actions, situation for situations, and object for everything else. The language also has the following components: a situation constant S0 denoting the initial situation; a binary function do(a, s) denoting the successor situation to s resulting from performing action a; a binary relation Poss(a, s) indicating that action a is possible in situation s; a binary relation s ⊑ s′ , meaning situation s is a sub-history of s′ ; a set of relational (functional) fluents, i.e., predicates (functions) taking a situation term as their last argument. A formula is uniform in s if it does not mention any situation term other than s. We call a formula with all situation arguments eliminated a situation-suppressed formula. For a situation-suppressed formula φ, we use φ[s] to denote the formula obtained from φ by restoring s as the situation arguments to all fluents.

In the situation calculus, a particular domain of application can be specified by a basic action theory (BAT) of the form

1. Σ is the set of the foundational axioms for situations;
2. Dap is a set of action precondition axioms, one for each action function A of the form Poss(A(⃗x), s) ≡ ΠA(⃗x, s), where ΠA(⃗x, s) is uniform in s;
3. Dss is a set of successor state axioms, one for each relation fluent symbol P of the form P(⃗x, do(a, s)) ≡ ΦP (⃗x, a, s), and one for each functional fluent symbol f of the form f(⃗x, do(a, s)) = y ≡ φf (⃗x, y, a, s), where ΦP (⃗x, a, s) and φf (⃗x, y, a, s) are uniform in s;
4. Duna is the set of unique name axioms for actions;
5. DS0 is the initial knowledge base stating facts about S0.

The situation calculus cannot be used to express and reason about infinite sequences of actions. Schulte and Delgrande [2004] extended the situation calculus with infinite histories. They introduce: a sort infhist for infinite sequences of actions, with variables h, h′ ; the extended binary relation ⊑, where s ⊑ h means s is a subhistory of h; predicates possible(s) and possible(h) stating that no impossible action occurs in s and h respectively. The set Σ∞ of axioms that characterize infinite histories are as follows:

• S0 ❁ h; possible(S0);
• s ❁ h → ∃s′ .s ❁ s′ ∧ s′ ❁ h;
• (s′ ❁ s ∧ s ❁ h) → s′ ❁ h;
• possible(h) ≡ ∀s ❁ h.possible(s);
• possible(do(a, s)) ≡ possible(s) ∧Poss(a, s).

Levesque et al. [1997] introduced a high-level programming language Golog with the following syntax:

where α is an action term; ϕ is a situation-suppressed formula and ϕ? tests whether ϕ holds; program δ1; δ2 represents the sequential execution of δ1 and δ2; program δ1|δ2 denotes the non-deterministic choice between δ1 and δ2; program πx.δ denotes the non-deterministic choice of a value for parameter x in δ; program δ∗ means executing program δ for a nondeterministic number of times.

Golog has two kinds of semantics: transition semantics and evaluation semantics. In transition semantics, a configuration of a Golog program is a pair (δ, s) of a situation s and a program δ remaining to be executed. The predicate Trans(δ, s, δ′ , s′ ) means that there is a transition from configuration (δ, s) to (δ′ , s′ ) in one elementary step. The predicate Final(δ, s) means that the configuration (δ, s) is a final one, which holds if program δ may legally terminate in situation s. Please refer to [De Giacomo et al., 2000] for details of the definitions of Trans and Final. We use C to denote the axioms for defining Trans and Final. In evaluation semantics, the predicate Do(δ, s, s′ ) means that executing the program δ in situation s will terminate in a situation s′ . Do can be defined with T rans and F inal as follows:

Trans∗ denotes the reflexive transitive closure of Trans.

3 Extension of the Situation Calculus

To represent the property of termination, we use the situation calculus with infinite histories. To represent planning with non-deterministic actions, following [Bacchus et al., 1995], we treat a non-deterministic action as a non-deterministic program. To represent numerical planning based on counting, we extend the situation calculus with counting.

The counting ability of first-order logic is very limited. Kuske and Schweikardt [2017] extended FOL by counting, getting a new logic FOCN. The key construct of FOCN are counting terms of the form #¯ y.ϕ, meaning the number of tuples ¯ y satisfying formula ϕ. Formulas of FOCN are interpreted over finite structures.

To extend the situation calculus with counting, as in [Li and Liu, 2020], we make the assumption that there are finitely many non-number objects. We introduce a sort nat for natural numbers with the + and · operations, and a function symbol µ of sort object → nat. The intended interpretation of µ is a coding of objects into natural numbers. We use n, m for variables of nat, and x, y for variables of non-number objects. If ϕ(¯ y) is a formula, then #¯ y.ϕ is a nat term, with the same meaning as in FOCN.

Transitive closure is often used to define counting terms. Following transitive closure logic [Immerman and Vardi,

1997], we introduce the notation [TC¯x,¯ yϕ](¯u, ¯ v), where ϕ(¯x, ¯ y) is a formula with 2k free variables, ¯u and ¯ v are two k-tuples of terms, which says that the pair (¯u, ¯ v) is contained in the reflexive transitive closure of the binary relation on k-tuples that is defined by ϕ. It is defined as an abbreviation in the situation calculus using a formula in second-order logic. We omit the definition here. In case P(x, y) is a binary predicate, we simply write P ∗ (x, y) to mean [TCx,yP(x, y)](x, y), and write P +(x, y) to mean P ∗ (x, y) ∧ x ̸= y.

To formalize planning problems where actions may have non-deterministic effects, following [Bacchus et al., 1995], we represent a non-deterministic action A(⃗x) as follows: we introduce associated deterministic actions Ad(⃗x, ⃗y), and define A(⃗x) as a non-deterministic program of Ad(⃗x, ⃗y) actions. For example, suppose we have a functional fluent f(x, s) and an action dec(x) which decreases the value of f(x, s) by an arbitrary positive amount. To represent dec(x), we introduce a deterministic action decd(x, y) which is possible when y > 0 and has the effect of decreasing the value of f(x, s) by y. Then we have the definition dec(x) .= πy.decd(x, y).

A particular domain of application where there are finitely many non-number objects is specified by a finite model basic action theory of the following form:

1. Du = Σ∪Dap∪Dss∪Duna∪DS0 as before, where Dap and Dss specify the action precondition and successor state axioms for the deterministic actions, respectively.
2. Σ∞ is the set of axioms for infinite histories.
3. P: the second-order axiomatization of Peano arithmetic.
4. C is the set of axioms for defining Trans and Final.
5. F is the set of the following axioms:
6. ∀x, y.µ(x) = µ(y) → x = y;
7. ∃n∀x.µ(x) ≤ n.

The above axioms state that the codings of different objects are different and there is a largest coding.

1. Ddef is a set of definition axioms where for each nondeterminstic action A(⃗x), there are two axioms of the form Trans(A(⃗x), s, δ, s′ ) ≡ Trans(δA(⃗x), s, δ, s′ ) and Final(A(⃗x), s) ≡ Final(δA(⃗x), s), where δA(⃗x) is the definition for A(⃗x).

Note that we treat non-deterministic actions as abbreviations for non-deterministic programs, thus we do not define their preconditions and successor state axioms.

Example 1. An agent needs to clear all the blocks above a block. Her behavior is constrained by the battery level. She needs to charge her battery when its level is < 10 (we assume that the battery level is an integer between 0 and 100). Action execution may consume electricity. There are 4 relational fluents: on(x, y, s), holding(x, s), clear(x, s), handempty(s), and a functional fluent battery-level(s). We also have 3 actions: unstack(x, y), drop(x) and charge. The effect of unstack(x, y) is unstacking x from y, nondeterministically decreasing the battery level by 1 or 2, depending on the weight of x. To represent unstack(x, y), we introduce a deterministic action unstack(x, y, η), where η is the amount of electricity consumption. Below are example axioms from the BAT for this domain.

Precondition Axioms:

Successor State Axioms:

clear(x, do(a, s)) ≡ (∃y, η)a = unstack(y, x, η)∨

clear(x, s) ∧ ∀z, η.a ̸= unstack(x, z, η)

battery-level(do(a, s)) = r ≡ r = 100 ∧ a = charge∨

Non-deterministic Action Definitions:

unstack(x, y) .= πη. unstack(x, y, η)

Initial Situation Axiom:

handempty(S0) ∧ battery-level(S0) ≥ 10

4 Our Abstraction Framework

In this section, based on the agent abstraction framework in [Banihashemi et al., 2017], we propose a uniform abstraction framework for generalized planning.

4.1 Generalized Planning Problems and Solutions

A generalized planning (g-planning) problem can be defined as a pair of an action theory and a goal. However, in the presence of non-deterministic actions, solutions to planning problems are programs whose execution under certain trajectory constraints are guaranteed to terminate and achieve the goal. For example, strong cyclic solutions to FOND problems are policies that terminate and achieve the goal under the fairness assumption, which states that if an action occurs infinitely often, then any of its possible effects occurs infinitely often. Thus when defining g-planning problems, we include an extra component of a trajectory constraint, which is a situation calculus formula with a free variable h of infinite histories.

Definition 1. A generalized planning problem is a tuple G = 〈D,C,G〉, where D is a BAT, C is a trajectory constraint, i.e., a situation calculus formula with a free variable of infinite histories, and G, a situation-suppressed formula, is a goal condition.

For example, the fairness assumption can be expressed as follows. We use ND to denote the set of non-deterministic actions. For each A ∈ ND, we assume that its definition is A(⃗x) .= π⃗y.Ad(⃗x, ⃗y). Then the fairness assumption is expressed as ∧A∈ND ∀⃗x.ψ1 ⊃ ψ2, where

Example 1 cont'd. Let Dl denote the BAT specified earlier. The low-level g-planning problem is Gl = 〈Dl,Cl,Gl〉, where Cl is ⊤, and Gl is clear(A).

Solutions to g-planning problems take the form of Golog programs. To define solutions, we introduce three abbreviations. Achieve(δ,G) means starting in S0, there is an execution of δ that makes δ hold:

Ensure(δ, G) means starting in S0, whenever program δ terminates, G is satisfied:

Term(δ, s, C) means starting in situation s, program δ terminates under constraint C, i.e., there is no infinite execution of δ starting in s and satisfying C:

Note that when ∃s.Do(δ, S0, s) is false, Ensure(δ,G) holds trivially. The execution of a Golog program may abort when a test falsifies or the precondition of a primitive action does not hold. For example, the execution of φ?; α may abort when φ falsifies or the precondition of α does not hold.

Definition 2. Let G = 〈D,C,G〉 be a g-planning problem, and δ a Golog program.

1. We say δ is a weak solution to G if D |= Achieve(δ, G).
2. We say δ is a strong solution to G if

So a weak solution is a program that may achieve the goal, but is not guaranteed to do so. A strong solution is a weak solution that, under the trajectory constraint, is guaranteed to achieve the goal unless the program execution aborts.

Example 2. There is a block on the table and the goal is to have the block at hand. We have an action pickup, which may succeed or fail. A weak solution is to pickup the block. Under the fairness assumption, a strong solution is to pickup the block until it is at hand. The only infinite executions of the program are unfair ones.

4.2 Simulations and Back-simulations

The concept of refinement mappings is the same as that in [Banihashemi et al., 2017] except that a refinement mapping can also map a high-level function to a low-level term.

Definition 3. A function m is a refinement mapping from Gh= 〈Dh, Ch, Gh〉 to Gl= 〈Dl, Cl, Gl〉 if for each high-level deterministic or non-deterministic action type A, m(A(⃗x)) = δA(⃗x), where δA(⃗x) is a low-level program; for each highlevel relational fluent P , m(P (⃗x)) = φP (⃗x), where φP (⃗x) is a low-level situation-suppressed formula; for each high-level functional fluent f , m(f(⃗x)) = τf (⃗x), where τf (⃗x) is a lowlevel term, possibly a counting term.

In the following, we will relate models of Dh and Dl. When we relate a model Mh of Dh and a model Ml of Dl, we do not require that the two models have the same object domain, which is the case in [Banihashemi et al., 2017]. By m(A(⃗x)) = δA(⃗x), we mean that the arguments of δA are included in ⃗x, but some xi's may not appear as arguments of δA. If some xi is an argument of δA, it represents an object belonging to both the high-level and low-level models.

Let δ be a high-level program, and φ a high-level formula. We use m(δ) to denote the program resulting from replacing each high-level symbol in δ with its low-level definitions. m(φ) is similarly defined.

Example 1 cont'd. We have two high-level actions: clearablock(x) and charge, where clearablock(x) means removing the top block of the tower of x. We have two high-level functional fluents: n(x, s) and battery-level(s), where n(x, s) counts the number of blocks above x. The initial KB is battery-level(S0) ≥ 10. We omit axioms from the high-level action theory Dh. The high-level g-planning problem is Gh = 〈Dh,Ch,Gh〉, where Ch is also ⊤, and Gh is n(A) = 0. Below is the refinement mapping from Dh to Dl:

where on∗ (z, x) and on+(y, x) are transitive closure formulas which we introduce in Section 3.

To relate high-level and low-level models, we first define the m-isomorphism relations between high-level and lowlevel situations. The main difference from the definition in [Banihashemi et al., 2017] is that we do not require that Mh and Ml have the same object domain, as stated earlier.

We use the following notation. For a variable assignment v, v[s/sh] denotes the assignment which maps variable s to situation sh and is the same as v elsewhere. For a model M of the situation calculus, let ∆MS stand for the domain of situations inM, and SM 0 for the denotation of S0 inM.

Definition 4. Given a refinement mapping m, a situation sh of a high-level model Mh is m-isomorphic to a situation sl in a low-level model Ml, written sh ∼Mh,Ml m sl, if: for any high-level relational fluent P, variable assignment v, we have Mh, v[s/sh] |= P(⃗x, s) iff Ml, v[s/sl] |= m(P)(⃗x, s); for any high-level functional fluent f, variable assignment v, we have Mh, v[s/sh] |= f(⃗x, s) = y iff Ml, v[s/sl] |= m(f )(⃗x, s) = y.

Note that as before, by writing m(P)(⃗x, s), we mean that the object arguments of m(P) are included in ⃗x, but some xi's may not appear as arguments of m(P). If some xi is an argument of m(P), it represents an object belonging to both Mh and Ml.

Example 1 cont'd. Let Ml be a model of Dl where there are 3 blocks A, B, C, and let Mh be a model of Dh with only one block A. Then a low-level situation where C is on B, B is on A, and battery-level = 10 is m-isomorphic to a high-level situation where n(A) = 2 and battery-level = 10.

Proposition 1. Suppose sh ∼Mh,Ml m sl. Let φ be a high-level situation-suppressed formula. Then Mh, v[s/sh] |= φ[s] iff Ml, v[s/sl] |=m(φ)[s].

In [Banihashemi et al., 2017], high-level and low-level models are related by an m-bisimulation relation. To define sound/complete abstractions, we do not require the strong condition of bisimulation, so we break the bisimulation relation into the simulation and back-simulation relations. Intuitively, simulation means: whenever a refinement of a high-level action can occur, so can the high-level action, and back-simulation means the other direction. Two extra conditions distinguish our definitions from that of [Banihashemi et al., 2017]: for each high level action A(⃗o), programm(A(⃗o))

terminates; we relate the infinite histories of the high-level and low-level models satisfying the trajectory constraints.

Definition 5. (m-simulation) A relation B ⊆ ∆Mh S × ∆Ml S is an m-simulation relation between Mh and Ml, if 〈SMh 0 , SMl 0 〉 ∈ B and the following hold:

1. 〈sh, sl〉 ∈ B implies that: sh ∼Mh,Ml m sl; for any highlevel action A, and variable assignment v, Ml, v[s/sl] |= Term(m(A(⃗x)), s,Cl), and if there is a situation s′l s.t. Ml, v[s/sl, s′ /s′l ] |= Do(m(A(⃗x)), s, s′ ), then there is a situation s′h s.t. Mh, v[s/sh, s′ /s′h ] |= Do(A(⃗x), s, s′ ) and 〈s′h , s′l 〉 ∈ B.
2. For any infinite high-level action sequence σ, if there is an infinite history in Ml generated by m(σ) and satisfying Cl, then there is an infinite history in Mh generated by σ and satisfying Ch.

By an infinite history generated by a program, we mean an infinite execution of the program.

Definition 6. (m-back-simulation) A relation B ⊆ ∆Mh S × ∆Ml S is an m-back-simulation relation between Mh and Ml, if 〈SMh 0 , SMl 0 〉 ∈ B, and the following hold:

1. 〈sh, sl〉 ∈ B implies that: sh ∼Mh,Ml m sl; for any high-level action A, and variable assignment v, Ml, v[s/sl] |= Term(m(A(⃗x)), s,Cl), and if there is a situation s′h s.t. Mh, v[s/sh, s′ /s′h ] |= Do(A(⃗x), s, s′ ), then there is a situation s′l s.t. Ml, v[s/sl, s′ /s′l ] |= Do(m(A(⃗x)), s, s′ ) and 〈s′h , s′l 〉 ∈ B;
2. For any infinite high-level action sequence σ, if there is an infinite history in Mh generated by σ and satisfying Ch, then there is an infinite history in Ml generated by m(σ) and satisfying Cl.

4.3 Sound/Complete Abstractions onModel Level

We first define sound/complete abstractions on model level, then we define sound/complete abstractions on theory level. For both model and theory levels, sound abstractions mean that high-level behavior entails low-level behavior, and complete abstractions mean the other direction.

Definition 7. We say that Mh is a sound m-abstraction of Ml, written Mh ∼→m Ml, if there is an m-back-simulation relation B between Mh and Ml.

The following proposition generalizes the back-simulation from actions to programs.

Proposition 2. Suppose that Mh is a sound m-abstraction of Ml via the m-back-simulation relation B. Let δ be a highlevel Golog program, and 〈sh, sl〉 ∈ B. Then

1. if there is a situation s′h inMh s.t. Mh, v[s/sh, s′ /s′h ] |= Do(δ, s, s′ ), then there is a situation s′l in Ml s.t. Ml, v[s/sl, s′ /s′l ] |= Do(m(δ), s, s′ ) and 〈s′h , s′l 〉 ∈ B;
2. if there is an infinite history in Mh generated by δ and satisfying Ch, then there is an infinite history in Ml generated by m(δ) and satisfying Cl.

Proof. To prove 1, use structural induction on δ. For the case of tests, use Prop. 1. To prove 2, use the condition that for each high level action A(⃗o), m(A(⃗o)) terminates.

Definition 8. We say that Mh is a complete m-abstraction of Ml, written Mh ∼←m Ml, if there is a m-simulation relation B between Mh and Ml.

Proposition 3. Suppose that Mh is a complete m-abstraction of Ml via the m-simulation relation B. Let δ be a high-level Golog program, and 〈sh, sl〉 ∈ B. Then

1. if there is a situation s′l in Ml s.t. Ml, v[s/sl, s′ /s′l ] |= Do(m(δ), s, s′ ), then there is a situation s′h in Mh s.t. Mh, v[s/sh, s′ /s′h ] |= Do(δ, s, s′ ) and 〈s′h , s′l 〉 ∈ B;
2. if there is an infinite history in Ml generated by m(δ) and satisfying Cl, then there is an infinite history in Mh generated by δ and satisfying Ch.

4.4 Sound/Complete Abstractions on Theory Level

For both sound and complete abstractions, we first define their weak versions.

Definition 9. Gh is a weak sound m-abstraction of Gl, if for any model Ml of Dl, there is a model Mh of Dh s.t.

1. Mh is a sound m-abstraction of Ml via B;
2. for any situations sh inMh and sl inMl, if 〈sh, sl〉 ∈ B andMh, v[sh/s] |= Gh[s], thenMl, v[sl/s] |= Gl[s].

In case that Gl ≡ m(Gh), by Prop. 1, the above Condition 2 holds, and thus it can be removed from the definition.

Sound abstractions of theories require that each low-level model should have both sound and complete abstractions.

Definition 10. Gh is a sound m-abstraction of Gl, if it is a weak sound m-abstraction of Gl, and for any model Ml of Dl, there is a model Mh of Dh s.t.

1. Mh is a complete m-abstraction of Ml via B;
2. for any situations sh inMh and sl inMl, if 〈sh, sl〉 ∈ B andMh, v[sh/s] |= Gh[s], thenMl, v[sl/s] |= Gl[s].

Theorem 1. Let Gh be a weak sound m-abstraction of Gl. If δ is a weak solution to Gh, so is m(δ) to Gl.

Proof. Let Ml be a model of Dl. Then there is a model Mh of Dh s.t. Mh is a sound abstraction of Ml via B. We show that Ml |= Achieve(m(δ),Gl). Since Mh |= Achieve(δ,Gh), there is a situation sh in Mh s.t. Mh, v[s/sh] |= Do(δ, S0, s) ∧ Gh[s]. By Prop. 2, there is a situation sl in Ml s.t. Ml, v[s/sl] |= Do(m(δ), S0, s) and 〈sh, sl〉 ∈ B. By Condition 2 of Definition 9, Ml, v[s/sl] |= Gl[s].

Theorem 2. Let Gh be a sound m-abstraction of Gl. If δ is a strong solution to Gh, so is m(δ) to Gl.

Proof. By Theorem 1, m(δ) is weak solution to Gl. We now prove it is also a strong solution. Let Ml be a model of Dl. Then there is a model Mh of Dh s.t. Mh is a complete abstraction of Ml via B. We first show that Ml |= Ensure(m(δ),Gl). Let sl be a situation in Ml s.t. Ml, v[s/sl] |= Do(δ, S0, s). By Prop. 3, there is a situation sh in Mh s.t. Mh, v[s/sh] |= Do(δ, S0, s) and 〈sh, sl〉 ∈ B. Since Mh |= Ensure(δ,Gh), Mh, v[s/sh] |= Gh[s]. By Condition 2 of Definition 10, Ml, v[s/sl] |= Gl[s]. We now show that Ml |= Term(m(δ), S0,Cl). Assume that hl is an infinite history in Ml generated by m(δ) and satisfying Cl. By Prop.

3, there is an infinite history in Mh generated by δ and satisfying Ch, contradicting withMh |= Term(δ, S0,Ch).

Example 1 cont'd. It is easy to prove that Gh is a sound abstraction of Gl. The following is a strong solution to Gh:

Then, by Theorem 2, we get a strong solution of Gl as follows:

Definition 11. Gh is a weak complete m-abstraction of Gl, if for any model Mh of Dh, there is a model Ml of Dl s.t.

1. Mh is a complete m-abstraction of Ml via B;
2. for any situations sh in Mh, sl in Ml, if 〈sh, sl〉 ∈ B andMl, v[sl/s] |= Gl[s], thenMh, v[sh/s] |= Gh[s].

Complete abstractions of theories require that every highlevel model is both a sound abstraction of a low-level model and a complete abstraction of a low-level model.

Definition 12. Gh is a complete m-abstraction of Gl, if it is a weak complete m-abstraction of Gl, and for any model Mh of Dh, there is a model Ml of Dl s.t.

1. Mh is a sound m-abstraction of Ml via B;
2. for any situations sh in Mh, sl in Ml, if 〈sh, sl〉 ∈ B andMl, v[sl/s] |= Gl[s], thenMh, v[sh/s] |= Gh[s].

Theorem 3. Let Gh be a weak complete m-abstraction of Gl. If m(δ) is a weak solution to Gl, so is δ to Gh.

Theorem 4. Let Gh be a complete m-abstraction of Gl. If m(δ) is a strong solution to Gl, so is δ to Gh.

Corollary 1. Let Gh be a sound and complete m-abstraction of Gl. Then δ is a strong solution to Gh iff m(δ) is a strong solution to Gl.

5 Formalizing Existing AbstractionWorks

In this section, we show that three main abstraction works in generalized planning can be formalized in our framework.

5.1 Srivastava et al.'s Work

QNP problems are classical planning problems extended with a set of non-negative numerical variables whose values are real numbers and can be decreased or increased randomly.

Definition 13. Let X be a set of non-negative numeric variables. LX denotes the class of all consistent sets of literals of the form x = 0 and x ̸= 0, for x ∈ X. A QNP problem Q = 〈X, I,G,O〉 consists of X; I ∈ LX, a set of initially true literals; G ∈ LX, a set of goal literals; and O, a set of action operators. Every o ∈ O has a set of preconditions pre(o) ∈ LX, and a set eff(o) of effects of the form inc(x) or dec(x) for x ∈ X. An instance of Q is a quantitative planning problem whose initial state, which specifies a nonnegative real number for each x ∈ X, satisfies I.

Definition 14. Let Q = 〈X, I,G,O〉 be a QNP problem. A policy for Q is a mapping from qualitative states to actions. For ϵ > 0, a trajectory of states is ϵ-bounded, if for any action o performed, if o decreases a variable x, then either the old value is < ϵ and the new value equals 0 or the amount of decrease is ≥ ϵ. A policy π solves an instance of Q if for any ϵ > 0, every ϵ-bounded trajectory induced by π is goal reaching. A policy π solves Q if it solves every instance of it.

FOND problems are like classical planning problems except that an action o may have non-deterministic effects expressed as eff1(o)| . . . |effn(o).

Definition 15. A QNP problem Q = 〈X, I , G, O〉 is abstracted into a FOND problem Q′ as follows: the literal x ̸= 0 is replaced by an atom px; effect inc(x) is replaced by deterministic effect px; and effect dec(x) is replaced by nondeterministic effect px|¬px.

Theorem 3 in [Srivastava et al., 2011]. π is a policy that solves Q iff it is a strong cyclic policy for Q′ that terminates.

Srivastava et al. proposed the Sieve algorithm to determine if a policy terminates. They made the key observation: In any ϵ-bounded trajectory, no variable can be decreased infinitely often without an intermediate increase. Based on this observation, Bonet and Geffner [2018] formalized the concept of conditional fairness. A strong cyclic policy for Q′ that terminates can be equivalently defined as: a policy π s.t. every conditional fair trajectory induced by π is goal reaching.

Definition 16. A trajectory of states of Q′ is conditionally fair if: from any time point on, for any x ∈ X, if no action with effect px ever occurs and actions with effect px|¬px occur infinitely often, then eventually px falsifies.

We now formalize the above work in our framework:

The low-level language is as follows: for each x ∈ X, we have a functional fluent fx(s); for each o ∈ O, we have an action Ao and a primitive action ao(⃗ηo), where ⃗ηo contains a parameter ηx for each x ∈ X s.t. inc(x) or dec(x) is in eff(o). The following is the specification of the g-planning problem Gq. We omit the initial KB and the goal condition.

Precondition axioms: for each action o ∈ O,

Successor state axioms: for each x ∈ X,

Non-deterministic action definitions: for each o ∈ O,

Trajectory constraint (ϵ-boundedness):

where S = {(x, o) | x ∈ X, o ∈ O, dec(x) ∈ eff(o)}.

The high-level language is as follows: for each x ∈ X, we have a relational fluent px(s), meaning x > 0; for each o ∈ O, we have an action Bo and a primitive action bo(⃗ηo), where each ηx takes values from {0, 1}, where 0 means px becomes false and 1 means true.

We omit the specification of the high-level g-planning problem Gf except the trajectory constraint for conditional fairness. We let dec(x, s) abbreviate for the following formula, which means s results from an action which decreases x (inc(x, s) can be similarly defined.):

Then conditional fairness is formalized as follows:

Below is the refinement mapping: for each x ∈ X, m(px) = fx > 0; for each o ∈ O, m(Bo) = Ao.

Theorem 5. Gf is a sound & complete m-abstraction of Gq.

Proof. Note that we have Gq = m(Gf). To prove that a conditional fair high-level infinite history corresponds to a ϵbounded low-level infinite history, we use the technique in the proof of Theorem 5 (Completeness of the Sieve algorithm) in [Srivastava et al., 2011].

5.2 Bonet and Geffner's Work

Bonet and Geffner [2018] proposed solving generalized classical planning problems by abstracting them into QNP problems. For example, for the problem of achieving clear(A), it can be abstracted into a QNP problem with one numeric feature depth(A), meaning the number of blocks above A, an action that decrements depth(A), and the goal depth(A) = 0. They showed that if the abstraction is sound, then a solution to the QNP problem is also a solution to the original problem. However, their abstract actions are restricted in the sense that the execution of an abstract action results in the execution of a single concrete action.

Using our framework, we can give a more general formalization of their work where the execution of an abstract action may correspond to that of a sequence of concrete actions. The language of a generalized classical planning problem Gc consists of a set of relational fluents and a set of deterministic actions. The trajectory constraint of Gc is simply ⊤. Such a problem is abstracted into a generalized numerical planning problem Gbq extended with a set of relational fluents p(s). The refinement mapping maps a relational fluent to a low-level formula, a functional fluent to a low-level nat term, possibly a counting term, and maps an action A to a low-level program δ executable when the precondition of A holds and achieving the effect of A. Gbq is a sound abstraction of Gc, if for every instance Mc of Gc, which is a classical planning problem, there is an instance of Gbq, which is a quantitative numerical planning problem, s.t. Mbq is a sound abstraction of Mc. Then we have the following result:

Corollary 2. If Gbq is a sound abstraction of Gc and δ is a strong solution to Gbq, then m(δ) is a strong solution to Gc.

5.3 Illanes andMcIlraith's Work

Illanes and McIlraith[2019] considered solving a class of generalized classical planning problems by automatically deriving a sound QNP abstraction from an instance of the problem. The automatic abstraction process is based on introducing a counter for each set of indistinguishable objects using the idea from [Fuentetaja and de la Rosa, 2016]. For example, suppose we have an instance where a number of packages must be delivered from a source location to either of two other locations A or B. Then we can automatically extract two counters, one for packages to be relocated to A, and one for packages to be relocated to B. Then the QNP problem is solved by converting it into a FOND problem, which they call a quantified planning problem. What distinguishes this work from that of [Bonet and Geffner, 2018] is that the latter didn't address the issue of automatical derivation of sound QNP abstractions.

Similarly to [Bonet and Geffner, 2018], Illanes and McIlraith's abstraction from generalized classical planning to QNP can be formalized in our framework as G ′c and G ′bq , and the refinement mapping maps each functional fluent to a counting term. Then we have the following result:

Corollary 3. G ′bq is a sound abstraction of G ′c . Thus if δ is a strong solution to G ′bq , then m(δ) is a strong solution to G ′c .

6 Conclusions

In this paper, we proposed a uniform abstraction framework for generalized planning based on the situation calculus and Golog. We formalized the concept of generalized planning problems and solutions, covering generalized classical planning, QNP, and FOND. We defined the concepts of sound/complete abstractions of generalized planning problems and show that solutions to a generalized planning problem are nicely related to those of its sound/complete abstractions. In this paper, we only give model-theoretic definitions of sound/complete abstractions. In the future, we are interested in their proof-theoretic characterizations. Further, we would like to explore automatic discovery of sound/complete abstractions.

Acknowledgments

We thank Yves Lesp´erance for helpful discussions on the paper. We acknowledge support from the Natural Science Foundation of China under Grant No. 62076261.