Guarantees for Sound Abstractions for Generalized Planning

1 Introduction

Generalized planning is about finding plans that solve a whole collection of instances of planning problems rather than finding a plan for a single instance as in classical planning [Srivastava et al., 2008; Hu and De Giacomo, 2011; Srivastava et al., 2011b; Belle and Levesque, 2016; Segovia et al., 2016]. In its simplest form, the instances in the collection share a common pool of actions and observable features [Hu and De Giacomo, 2011; Bonet et al., 2017], yet other formulations consider relational domains where the actions and features in the instances result of grounding a collection of actions and atom schemas with different sets of objects [Boutilier et al., 2001; Wang et al., 2008; Srivastava et al., 2011a; van Otterlo, 2012].

∗On sabbatical leave from Universidad Sim´on Bol´ıvar.

A recent proposal for handling relational domains casts the problem of generalized planning as the problem of solving a single abstraction, or reformulation, that captures all the instances in the collection [Bonet and Geffner, 2018]. This abstraction however involves qualitative numerical features, in addition to the standard boolean features, that are defined in terms of the objects in the states and their relationships. The actions in the abstraction tell how the features change their values when actions are applied. Qualitative rather than exact numerical features are used to avoid undecidability issues [Helmert, 2002]. The change for such features is only qualitative as they only specify whether the numerical feature increases, decreases, or remain unchanged. Under such effects, the problem of solving the abstraction, and hence the generalized planning problem, can be reduced to the problem of solving a single fully observable non-deterministic (FOND) problem [Geffner and Bonet, 2013].

This formulation of generalized planning is appealing as it leverages the existing FOND planners to solve, in one shot, a complete (often infinite) class of problems, but it requires the right set of features and the right abstraction. Bonet et al. [2019a] learn the abstraction inductively from a small sample of transitions from instances in the collection. The abstraction is guaranteed to generalize when the sample is sufficiently general and diverse, but, as far as we know, there have been no attempts to automatically check whether the learned abstraction is sound for the collection.

In this work we bridge this gap by providing a general framework for the synthesis of guarantees for generalization. The guarantees are in the form of first-order formulas that provide sufficient conditions for generalization: every instance whose reachable states satisfy the formulas is guaranteed to be handled correctly by the abstraction. We only address the synthesis of such formulas and defer to future work the problem of verifying whether the formulas are satisfied on the reachable states of a given instance. Nonetheless, the automatically synthesized formulas have a rich and complex structure, and they often express novel and interesting invariants on well-known benchmarks. For example, in Blocksworld, the classical problem of moving blocks with a gripper, one such formula says that every tower must end in a clear block, a formula that thus forbids the existence of "circular towers"; we are not aware of any other approach for invariant synthesis that is able to produce such a formula.

Our contributions are the following: 1) a crisp theoretical foundation for the synthesis of formulas only using as input the relational planning domain and the abstraction, 2) the obtained formulas define subcollections of instances that are guaranteed to be handled correctly by the abstraction, 3) under additional assumptions, necessary conditions for generalization are obtained, and 4) the synthesis also provides candidates for invariants that would then need to be verified.

The paper is organized as follows. The next section provides background on the feature-based account for generalized planning. First-order structures and abstractions are discussed in Sect. 3. The framework for generalization and the synthesis algorithm are given in Sect. 4 and 5. Sect. 6, discusses necessary conditions and the synthesis of invariants. The paper concludes with examples and a discussion.

2 Background

2.1 Collections of Instances

We consider collections Q of grounded STRIPS instances P = (F,A, I,G) where F is a set of atoms (propositions), A is a set of actions, and I ⊆ F and G ⊆ F describe the initial and goal states of P. It is assumed that all instances in Q result from grounding a common domain D with a set of objects, particular to each instance, and descriptions of the initial and goal situations. As it is standard, D specifies the constant and predicate symbols that define the propositions via the grounding process, and it also contains lifted action schemas that generate the set A of grounded actions. Q(D) denotes the class of all grounded instances for domain D. Hence, Q ⊆ Q(D) as all instances in Q come from D.

2.2 Abstractions

The boolean and numerical features are used to build uniform abstractions for the instances in Q. Such instances, although sharing a common relational domain, may differ substantially in the number of actions, objects, and observables.

A boolean feature φ for Q is a function that maps each instance P ∈ Q and state s for P (reachable from the initial state of P ) into a truth value φ(P, s) ∈ {⊤, ⊥}. A numerical feature is a function φ that maps P and s into a non-negative integer φ(P, s). When P or s are clear from context we may simplify notation. The set of features for Q is denoted by F. For boolean features f, an F-literal is either f or ¬f, while for numerical features n, an F -literal is n > 0 or n = 0.

An abstraction for Q is a tuple ¯Q = (F,AF , IF ,GF ) where F is a set of features, AF is a set of abstract actions, and IF and GF describe the abstract initial and goal states in terms of the features. An abstract action ¯a is a pair 〈Pre; Eff〉 where Pre is a collection of F-literals, and Eff is a collection of effects for F. Effects for boolean features are denoted by F-literals, while effects for numerical features n correspond to increments or decrements denoted by n↑ or n↓ respectively. The items IF and GF denote consistent sets of F-literals. It is assumed that the effects of actions and GF are consistent sets of literals, and that IF is maximal consistent. 1

The pair (IF ,GF ) of initial and goal states in the abstraction ¯Q = (F, AF , IF , GF ) complies with Q when (IF , GF ) complies with each instance P in Q. The pair (IF ,GF ) complies with the instance P when the initial state of P is consistent with IF , and if s is a state in P that is consistent with GF , then s is a goal state for P. A state s in P is consistent with IF (resp. GF ) iff ¯ s ∪ IF (resp. ¯ s ∪ GF ) is consistent, where ¯ s denotes the boolean valuation of F on s; i.e., ¯ s = {f : f(s)=⊤} ∪ {¬f : f(s)=⊥} ∪ {n=0 : n(s)=0} ∪ {n>0 : n(s)>0}. If the pair (IF ,GF ) for the abstraction ¯Q complies with P, we write ¯Q ∼ P.

Following Bonet and Geffner [2018], an abstraction ¯Q is sound for Q if it complies with Q and each action ¯a in AF is sound (for Q). An abstract action ¯a = 〈Pre; Eff〉 is sound iff for each instance P in Q and reachable state s in P where Pre holds in ¯ s, ¯a represents at least one action a from P in s. The abstract action ¯a represents the action a in the state s iff 1) the preconditions of a and ¯a both hold in s and ¯ s respectively, and 2) the effects of a and ¯a over F are similar; namely,

1. for any boolean feature f in F, if f changes from true to false (resp. false to true) in the transition s ⇝ res(a, s) (where res(a, s) is the state that results of applying a in s), then ¬f ∈ Eff (resp. f ∈ Eff),
2. for any boolean feature f in F, if f (resp. ¬f) is in Eff, then f is true (resp. false) in res(a, s), and
3. for each numerical feature n in F, n ↓ (resp. n ↑) appears in Eff if and only if n(P, res(a, s)) < n(P, s) (resp. n(P, s) < n(P, res(a, s))).

We write ¯a ∼P,s a to denote that the abstract action ¯a represents the action a in the (reachable) state s of P. In such a case, we also say that a instantiates ¯a in s. When there is no confusion about P , we simplify notation to ¯a ∼s a.

Soundness links plans for ¯Qwith generalized plans: if ¯π is a plan that solves an abstraction ¯Q that is sound for Q and P is an instance in Q, then any execution (a0, a1, . . .) spawned by ¯π on P reaches a goal state for P . The execution (a0, a1, . . .) is spawned by ¯π on P iff 1) ai instantiates ¯π(¯ si) in si, for i ≥ 0, 2) ¯ si is the boolean valuation of si, for i ≥ 0, 3) si+1 = res(ai, si), for i ≥ 0, and 4) s0 is the initial state of P.

Example. Consider the collection Qclear with all Blocksworld instances with goal clear(A) where A is a fixed block. The domain Dclear has no explicit gripper, contains a single constant A, and has two action schemas: Newtower(x, y) to move block x from block y to the table, and Move(x, y, z) to move block x from block y onto block z. An abstraction for Qclear is ¯Qclear = (F,AF , IF ,GF ) where F = {n} and n is the feature that counts the number of blocks above A, AF = {¯a} where ¯a = 〈n>0; n↓〉, IF = {n>0}, and GF = {n=0}. It is easy to check that ¯Qclear is sound and solved by the plan ¯πclear that executes ¯a whenever n>0. An action Newtower(x, y) or Move(x, y, z) that "removes"

1 A set S of F -literals is consistent if for any boolean feature f , S excludes either f or ¬f , and for any numerical feature n, S excludes either n > 0 or n = 0. S is maximal consistent if it is consistent, and S ∪ {L} is not consistent for any F -literal L /∈ S.

a block from above A in state s is an action that instantiates ¯a in s. Notice that Qclear ̸= Q(Dclear) since, for example, Q(Dclear) contains instances that have "circular towers".

2.3 Inductive Learning and Concepts

Bonet et al. [2019a] show how an abstraction can be learned from a sample of transitions and a collection F of candidate features. In their approach, each feature in F is associated with a concept C that is obtained from a set of atomic concepts, and a concept grammar [Baader et al., 2003]. 2

In general, a concept for Q may be thought of as a function C that maps instances P in Q and states s in P into sets C(P, s) of tuples of objects. Concepts define features: boolean features fC that denote whether C(P, s) is nonempty, and numerical features nC that denote the cardinality of C(P, s). The concepts by Bonet et al. are limited to denotations that are subsets of objects rather than object tuples.

3 First-Order Abstractions

We deal with formulas in first-order logic that are built from a signature σ = σ(D) given by the relational domain D. The constants defined in D appear as constant symbols in σ, and the predicates defined in D appear as relational symbols of corresponding arity in D. The signature also contains binary relations p+ and p∗ for the binary predicates p in D. As usual, L(σ) denotes the class of well-formed formulas over σ.

First-order formulas are interpreted over first-order structures, also called interpretations. We are only interested in structures that are associated with states. A state s provides the universe Us of objects and the interpretations for the constant and relational symbols in D. The interpretations for p+ and p∗ , for the binary predicates p, are provided by the transitive and reflexive-transitive closure of the interpretation of p provided by s. We write ϕ(¯x) to denote a formula whose free variables are among those in ¯x. If ϕ(¯x) is a formula, s is a state in P, and ¯u is a tuple of objects in Us of dimension |¯x|, s ⊨ ϕ(¯u) denotes that the interpretation provided by s satisfies ϕ when the variables in ¯x are interpreted by the corresponding objects in ¯u.

For a concept C characterized by ΨC(¯x), the extension of C for s in P is C s = C(P, s) = {¯u : s ⊨ ΨC(¯u)}. We assume that all features correspond to concepts whose characteristic functions are first-order definable:

Definition 1 (First-Order Abstraction). Let D be a planning domain and let σ = σ(D) be the signature for D. A concept C is (first-order) D-definable if ΨC(¯x) belongs to L(σ). A feature f is D-definable if f is given by a concept C that is D-definable. An abstraction ¯Q = (F, AF , IF , GF ) is a firstorder abstraction for D if each feature f in F is D-definable.

When D is clear from the context, we just say that ¯Q is a first-order abstraction without mentioning D. The applicability of an abstract action ¯a in a first-order abstraction ¯Q on a state s can be decided with a first-order formula Pre(¯a).

Example. The abstraction ¯Qclear is a first-order abstraction because F = {n} and n is the cardinality of the concept C

2 We do not consider the distance features [Bonet et al., 2019a] as it is not clear how to express them in first-order logic.

given by ΨC(x) = ∃y(on(x, y) ∧ on∗ (y, A)). However, C is also given by Ψ′C (x) = on+(x, A). As usual, both representations may yield different results although being logically equivalent; more about this below.

4 Conditions for Generalization

Let ¯Q = (F, AF , IF , QF ) be a first-order abstraction for D. We look for conditions to establish the soundness of ¯Q for a generalized problem Q ⊆ Q(D). In particular, we aim for conditions of the form G = {Φ¯a : ¯a ∈ AF} where Φ¯a = ∃¯ z(∨i Ψai ¯a (¯ z)) is associated with the abstract action ¯a and satisfies the following:

• ai is an action schema in D,
• ¯ z is a tuple of variables that represent the parameters of the action schemas in D (these are existentially quantified on the objects of the given state s in problem P), and
• if ¯ o is a tuple of objects of dimension |¯ z| such that s ⊨ Pre(¯a) ∧ Ψai ¯a (¯ o), where s is a reachable state in problem P ∈ Q(D), then the ground action ai(¯ o) instantiates the abstract action ¯a in the state s (i.e., ¯a ∼s ai(¯ o)).

The idea is that Ψai ¯a (¯ o) suffices to establish ¯a ∼s ai(¯ o) directly from Pre(¯a) and the (lifted) domain D without using any other information about the reachability of state s (e.g., invariant information for reachable states). On the other hand, such formulas would be "accompanied" by assumed conditions Pre(¯a) ⇒ ∃¯ z(∨i Ψai ¯a (¯ z)) on the reachable states that together with the above properties provide the guarantee:

Definition 2 (Guarantee). Let D be a planning domain and let ¯Q = (F,AF , IF ,GF ) be a first-order abstraction. A guarantee for ¯Q is a set G = {Φ¯a = ∃¯ z(∨i Ψai ¯a (¯ z)) : ¯a ∈ AF} of formulas for each abstract action ¯a in ¯Q. The guarantee is valid in instance P ∈ Q(D) iff for each state s ∈ P (reachable or not) and tuple ¯ o of objects in P , if s ⊨ Pre(¯a)∧Ψai ¯a (¯ o) then ¯a ∼s ai(¯ o). The guarantee G is valid for D iff it is valid for each problem P in Q(D).

Theorem 3 (Soundness). Let D be a planning domain, let ¯Q = (F, AF , IF , IF , GF ) be a first-order abstraction, and let G = {Φ¯a = ∃¯ z(∨i Ψai ¯a (¯ z)) : ¯a ∈ AF } be a guarantee for D. If G is valid, then ¯Q is a sound abstraction for the generalized problemQ = {P ∈ Q(D) : ¯Q ∼ P and Pre(¯a) ⇒Φ¯a holds in the reachable states in P}.

Proof. Let P be a problem in Q, let s be a reachable state in P , and let ¯a be an abstract action that is applicable in ¯ s. Since ¯Q ∼ P , we only need to show ¯a ∼s a for some action a. By definition of Q, s ⊨ Φ¯a where Φ¯a = ∃¯ z(∨i Ψai ¯a (¯ z)). Hence, there is a tuple ¯ o of objects such that s ⊨ Pre(¯a) ∧ Ψai ¯a (¯ o) for some schema ai in D. Then, by Definition 2, ¯a ∼s ai(¯ o).

5 Synthesis

For a feature f defined by concept C we need to track its value along transitions s ⇝ res(a(¯ o), s). Let ΨaC (¯ z, ¯x) be a formula that defines at state s the extension of C in the state res(a(¯ o), s) that results of applying a(¯ o) in s; i.e.,

where ¯u is a tuple of objects. For example, a boolean feature f defined by C goes from true to false in s ⇝ res(a(¯ o), s) iff C s ̸= ∅ and C res(a(¯ o),s) = ∅ iff s ⊨ ∃¯x(ΨC(¯x)) and s′ ⊨ ¬∃¯x(ΨC(¯x)) iff s ⊨ ∃¯x(ΨC(¯x)) ∧ ∀¯x(¬ΨaC (¯ o, ¯x)).

Since the concept C may be defined in terms of relations p∗ or p+ that denote the transitive closure of p, and that transitive closure is not first-order definable [Vardi, 1982], it is not always possible to track in first-order logic the change of denotation for p∗ or p+ after an action changes the denotation of p. Hence, we settle for a "logical approximation" of ΨaC (¯ z, ¯x) in terms of necessary and sufficient conditions:

A base for synthesis provides approximations for all the atoms in the language L(σ):

Definition 4 (Base for Synthesis). A base for synthesis for domain D is a set T that contains formulas TX(a, p)(¯ z, ¯x) for X∈{N, S}, action schemas a(¯ z) ∈ D, and predicates p ∈ D of arity |¯x|. It also contains formulas TX(a, pc )(¯ z, x, y) for X∈{N, S}, action schemas a(¯ z) ∈ D, binary predicates p ∈ D, and at least one of c = ∗ or c = +. These formulas should provide necessary and sufficient conditions as follows. For any problem P in Q(D), state s in P, tuple ¯ o such that a(¯ o) is applicable at s, tuple ¯u, objects u and v, and c ∈ {∗, +}:

where C s p ={¯u : s ⊨ p(¯u)} and C s pc ={(u, v) : s ⊨ pc (u, v)} are the concepts associated with p and pc respectively.

The approximation for the atoms in L(σ) that is provided by the base T is lifted over all first-order formulas. Indeed, the following structural induction gives necessary and sufficient conditions N a ϕ (¯ z, ¯x) and Saϕ(¯ z, ¯x) for any concept C defined in terms of formula ϕ. For X∈{N, S}:

• Xa p (¯ z, ¯x)=TX(a, p)(¯ z, ¯x) where p is a predicate of arity |¯x|, or p = qc for some binary predicate q, and c ∈ {∗, +},
• Xaϕ◦ψ (¯ z, ¯x) = Xaϕ(¯ z, ¯x) ◦ Xaψ (¯ z, ¯x) where ◦ ∈ {∧, ∨},

The base provides approximations for either p∗ or p+, or both. In the former case, this is enough since one of the closures can be expressed in terms of the other; e.g., on+(x, y) ≡ ∃z(on(x, z) ∧ on∗ (z, y))).

Below we propose a general base for synthesis of formulas. With this base, the formulas N a ϕ and Saϕ are identical except when ϕ contains a transitive closure. Hence, except for such ϕ, both formulas are necessary and sufficient.

Theorem 5 (Lift). Let T be a base for synthesis for domain D, let a = a(¯ z) be an schema in D, and let ϕ(¯ z, ¯x) be a first-order formula in L(σ(D)). Then, for any instance P in Q(D), state s for P, and tuples ¯ o and ¯u of objects in P:

As noted earlier, tracking the change of boolean features f defined by concepts C is easy since f is true or false at s iff C s is non-empty or empty respectively. Tracking the qualitative numerical changes is more challenging, however. For example, f increases in the transition s ⇝ s′ iff |C s | < |C s′ |. This condition is difficult to capture because the extension of C may increase size by the result of a small change, as simple as one new element entering the set, or by a large change involving many elements. The case of local, small, changes is common and easy to define:

Definition 6 (Monotonicity). Let D be a domain and let P be an instance in Q(D). A concept C for Q(D) is monotone in P if for every reachable state s in P, and action a(¯ o) that is applicable in s, either C(P, s) ⊆ C(P, s′ ), C(P, s) ⊇ C(P, s′ ), or C(P, s) = C(P, s′ ) for s′=res(a(¯ o), s). A firstorder abstraction ¯Q is monotone for P if each feature f in ¯Q is defined by a concept C that is D-definable and monotone.

Necessary and sufficient conditions for the change of value of monotone features f along transitions s ⇝ res(a(¯ z), s), for action schema a(¯ z), are provided by the formulas:

where C is the concept that defines f, X∈{N, S} denotes a necessary or sufficient condition, Ψ and XaΨ denote ΨC(¯x) and XaΨC (¯ z, ¯x) respectively, and ̂ N aΨ = SaΨ and ̂ SaΨ = N aΨ.

For example, Sdec C (¯ z) = ∃¯x(Ψ ∧ ¬N aΨ). If s ⊨ Sdec C (¯ o), there is object tuple ¯u such that s ⊨ Ψ(¯u) ∧ ¬N aΨ(¯ o, ¯u); i.e., ¯u ∈ C s and ¯u /∈ C res(a(¯ o),s) . For monotone features, the only possibility is C res(a(¯ o),s) ⊊ C s which means that the feature decreases in the transition s ⇝ res(a(¯ o), s).

For obtaining sufficient conditions for general features, the first two formulas from above are strengthen as

where the added conjunct enforces that the feature defined by the concept C is indeed monotone. For the remaining cases, the formulas for sufficiency correspond to those above.

Lemma 7. Let C be a concept characterized by formula ΨC(¯x), and let s be a state in P ∈ Q(D) on which the action a(¯ o) is applicable. Then,

where s′ = res(a(¯ o), s) is the result of applying a(o) in s.

We have expressed how the value of individual features changes in transitions. Before providing the complete synthesis, we need to express the value of preconditions of abstract actions, and how the actions affect the different features.

Preconditions of abstract actions ¯a on features f = fC are expressed by Pre(¯a)C = ⊤ if there is no precondition on f, Pre(¯a)C = ∃¯x(ΨC(¯x)) if f is boolean (resp. numeric) and Pre(¯a) contains f (resp. f > 0), and Pre(¯a)C = ∀¯x(¬ΨC(¯x)) if f is boolean (resp. numeric) and Pre(¯a) contains ¬f (resp. f = 0).

On the other hand, ¯a partitions the set of features according to their type and the effects of ¯a on them:

∆inc ¯a = {n ∈ F : n is numeric and n↑∈ Eff(¯a)} ,

∆dec ¯a = {n ∈ F : n is numeric and n↓∈ Eff(¯a)} ,

∆eq ¯a = {f ∈ F : f is not affected by ¯a} ,

∆true ¯a = {f ∈ F : f is boolean and f ∈ Eff(¯a)} ,

∆f alse ¯a = {f ∈ F : f is boolean and ¬f ∈ Eff(¯a)} .

Definition 8 (Synthesis). Let T be a base for synthesis for domain D, and let ¯Q = (F, AF , IF , GF ) be a first-order abstraction for D. For abstract action ¯a in AF and schema a(¯ z) in D, we define the formula Ψa¯a (¯ z) as

where Chg={inc, dec, eq, true, false}. The guarantee for ¯Q is G(T , ¯Q) = {Φ¯a = ∃¯ z(∨a∈D Ψa¯a (¯ z)) : ¯a ∈ AF}.

Theorem 9 (Main). Let T be a base for synthesis for domain D, and let ¯Q = (F, AF , IF , GF ) be a first-order abstraction. Then, G(T , ¯Q) is a valid guarantee for D (cf. Definition 2).

We cannot yet provide a complete example because the synthesis requires the conditions for the atoms in the language that are given by the base for synthesis. We now provide one such base, and apply it to the running example.

5.1 AGeneral Base for Synthesis

The synthesis framework is parametrized by the base. Trivial, non-informative, bases are easy to obtain: it is enough to define sufficient and necessary conditions as ⊥ and ⊤ respectively for each atom in the language. We provide a simple, general, and non-trivial base that can be used with any domain D. The conditions provided by two different bases, or by the same base for different but logically equivalent formulas, do not need to be logically equivalent.

Table 1 shows a template for obtaining bases B(D) for any domain D. No formula in the template involves the predicate p+; i.e., all such predicates have been replaced by equivalent formulas involving p∗ . (Alternatively, we may define a base that only resolves p+ and assumes that no formula contains p∗ .) Two versions for the necessary condition for p∗ are provided: one when the action a adds at most one atom p(u, v), and the other when a adds two or more such atoms.

The formulas in Table 1 involve "bracket expressions" that instantiate to first-order formulas. For schema a(¯ z) and tuple ¯x, a bracket expression reduces to either to a logical constant ⊤ or ⊥, or to an expression involving equality over the variables in ¯ z and ¯x, and the constant symbols in D. For example, [[¬on(x, y) /∈ Post]] reduces to xy ̸= z1z2 for the action Newtower(z1, z2) since this action removes only on(z1, z2).

Theorem 10 (General Base). Let D be a planning domain. The set B(D) is a base for synthesis for domain D.

Corollary 11. Let D be a domain and let ¯Q = (F,AF , IF , GF ) be a first-order abstraction for D. The guarantee G(B(D), ¯Q) is valid for D and, hence, ¯Q is a sound abstraction for the generalized problem Q = {P ∈ Q(D) : ¯Q ∼ P and Pre(¯a) ⇒ Φ¯a holds in the reachable states in P}.

Example. The abstraction ¯Qclear = (F,AF , IF ,GF ) has a single feature n=nC for ΨC(x)=∃y(on(x, y) ∧ on∗ (y, A)). Dclear has two schemas a1 = Newtower(z1, z2) and a2 = Move(z3, z4, z5). The condition Sdec C (z1, z2) for a1 is equivalent (after simplification) to

The formula Ψa1 ¯a (z1, z2) is this formula conjoined with clear(z1). For action a2, Sdec C (z3, z4, z5) is

The formula Ψa2 ¯a (z1, z2) is this formula conjoined with clear(z3), on(z3, z4), and clear(z5). The guarantee for ¯a is Φ¯a = ∃¯ z(Ψa1 ¯a (z1, z2) ∨Ψa2 ¯a (z3, z4, z5)).

By Corollary 11, Qclear is sound for instances with goal clear(A) and reachable states that satisfy ∃x(on+(x, A)) ⇒ Φ¯a. Namely, if there is a block above A, then either there are blocks z1 and z2 such that z1 is clear and on z2, z2 is A or above it, and z2 mediates any "path of blocks" from z1 to A, or there are blocks z3, z4 and z5 such that z3 is clear, on z4, and above A, z5 is clear and not equal to A or above it, and z4

mediates any path from z3 to A. This formula indeed holds in all "real instances" of Blocksworld. ¯Qclear is then sound for all of them, and the policy ¯πclear that solves the abstraction is a generalized plan for Qclear. A full derivation appears in the extended version of this paper [Bonet et al., 2019b].

6 Necessary Conditions and Invariants

The conditions provided by G are only sufficient; i.e., no conclusion about an abstraction ¯Q for instance P can be drawn if some reachable state s in P satisfies Pre(¯a) but not Φ¯a. For reasoning in such cases, one needs necessary rather than sufficient conditions for soundness.

For obtaining necessary conditions, we need to assume that the features in the abstraction are indeed monotone; i.e., their value changes in a local manner along the transitions in any instance P in Q(D). For example, under monotonicity, f decreases in s ⇝ res(a(¯ o), s) iff C res(a(¯ o),s) ⊊ C s iff

(where C is the concept that defines f) only if

We obtain necessary conditions similarly as before:

Theorem 12 (Necessary Conditions). Let D be a domain, let ¯Q be a first-order abstraction for D, and let P be an instance in Q(D) such that ¯Q is sound and monotone for P. If s is a reachable state in P, then

where Γai ¯a (¯ z) is the formula

Necessary conditions are useful for showing that ¯Q is not sound for instance P: it is enough to find a reachable state where the condition does not hold. On the other hand, we cannot infer that Q is sound for P only if the necessary condition does hold in P .

If the abstraction ¯Q is sound for Q, every instance P in Q for which ¯Q is monotone must satisfy the necessary conditions. Such conditions, that by definition hold in all reachable states, are state invariants in P . Therefore, sufficient and necessary conditions for the soundness of an abstraction ¯Q can be regarded as candidates for invariants, which may then be verified by a theorem prover in order to avoid an explicit enumeration of reachable states [Slind and Norrish, 2008].

7 Other Examples

In this section we present two additional examples. One for a gripper problem with an arbitrary number of balls and grippers, and the other about connectivity in directed graphs.

7.1 Gripper

We consider a domain D for Gripper with constants A (destination) and B (origin) for the rooms, objects l and r for the grippers, and objects bi for the different balls. The predicates are at(r) and in(b, r) for the position of the robot and balls in rooms, ca(b, g) to indicate when ball b is held by gripper g, and fr(g) to indicate that gripper g is not holding any ball. The action schemas are a1 =Move(r1, r2) for moving the robot, and a2 =Pick(b, g, r) and a3 =Drop(b, g, r) for picking and dropping balls in rooms using specific grippers.

Bonet et al. [2019a] learn an abstraction that is made of a boolean feature X, and numerical features B, C, and G:

• X = {r : at(r) ∧ r=A} tells whether the robot is in A,
• B = {b : ∃r(in(b, r) ∧ r̸=A)} counts the balls in B,
• C = {b : ∃g(ca(b, g))} counts the balls being held, and
• G = {g : fr(g)} counts the free grippers.

The abstract actions in abstraction ¯Qgripper are:

Both, go1 and go2, move the robot from A to B. Go1 moves the robot that still has room to pick more balls only when there are no more balls to be picked at B; go2 moves the robot when it cannot hold any more balls. The formulas Ψai ¯a (¯ z) are ⊥ except for (conditions in Pre(ai) removed to fit space):

For example, Ψa1 pick = Ψa3 pick = ⊥ means that the abstract pick action cannot be instantiated by any ground instance of Move(r1, r2) or Drop(b, g, r): the first changes the feature X that is not affected by pick, and the second increases G in contradiction with the effect G↓.

On the other hand, Ψa2 pick = ∀x[¬ca(b, x)] ∧ r ̸= A means that the ground action Pick(b, g, r) instantiates the pick action when r ̸= A, otherwise the effect B↓ is not achieved, and when the ball b is not being held by any gripper x, otherwise C↑ is not met. Ψa2 pick is logically implied at reachable states by the preconditions of Pick(b, g, B) and the mutex information that is polynomially computable. Indeed, the preconditions are at(B), in(b, B) and fr(g), while the mutex invariants include ¬in(b, r) ∨ ¬ca(b, g) for any b, r, and g. Actually, we can show that the mutex information is enough to show Pre(¯a) ⇒ ∃¯ z(∧i Ψai ¯a ) for all the actions ¯a in the abstraction. Hence, the abstraction is sound for any instance of Gripper.

7.2 Connectivity in Graphs

We now consider a graph problem that involves the connectivity of two designated vertices s and t. The domain D has constants s and t, a single binary predicate E(x, y), and a single action schema Link(x, y) that adds E(x, y) and has no precondition. The exact form of the initial situation or goal is not relevant in the following discussion.

The abstraction ¯Q defines two features: a boolean feature conn that is true iff s and t are connected, and a numerical feature n that counts the total number of edges in the graph. These features are defined with the concepts:

There is a single abstract action ¯a = 〈; n↑〉. Since conn exists as a feature in ¯Q and ¯a does not affect it, no instantiation of ¯a may modify the st-connectivity of the graph. The guarantee Φ¯a for ¯a is then

That is, a sufficient condition for Link(z1, z2) to instantiate ¯a, and thus increase n and leave conn intact, is that there should be no edge between z1 and z2, and there should be a path s ⇝ t if there are paths s ⇝ z1 and z2 ⇝ t. The first condition entails that the number of edges in the graph indeed increases after applying Link(z1, z2), while the second entails that the truth value of conn does not change with the application of the action: either it was true and remains true, or it was false and remains false.

On other hand, the synthesis of the necessary condition yields ¬E(z1, z2) which is quite weak. The reason is that the formula BS(a, p∗ ) in Table 1 is not strong enough. A better necessary condition is obtained when the following term is added to the disjunction in BS(a, p∗ ):

This term says that the action removes no edge from the graph, and adds one edge (u, v) for existing paths x ⇝ u and v ⇝ y. Clearly, if this condition is met, the graph has a path x ⇝ y after the application of the action. The resulting base thus remains valid for any domain D and, in some cases, it provides tighter conditions. Indeed, with this amendment, the necessary condition becomes equal to the sufficient condition Φ¯a.

Finally, observe that these conditions are not invariants. The reason is that the abstraction is not sound since there are configurations (states) in which no edge can be added to the graph without altering the st-connectivity. In such states, the abstract action ¯a is still applicable, as it does not have any precondition, but no Link(z1, z2) action instantiates it.

8 Discussion and FutureWork

Abstractions for generalized planning can be inductively obtained from small samples of transitions from one or several instances of planning problems. Although there are no guarantees on the soundness of the abstractions, we have shown that the abstractions contain usable information about the intended planning instances. Indeed, by analyzing the abstraction with respect to the planning domain, we have shown how to obtain formulas that capture some of the assumptions being made by the abstraction. These assumptions can be either sufficient or necessary. A sufficient condition is a guarantee for generalization. Necessary conditions may be used to show that an instance is not captured by the abstraction.

Sufficient conditions may also be used to improve the search for instantiations of an abstract action ¯a that is applicable in a state s in instance P. In the worst case, one needs to iterate over every grounded action a(¯ o) to find an instantiation of ¯a. However, if P satisfies the sufficient condition, it is enough to find a tuple of objects ¯ o such that s ⊨ Φ¯a(¯ o), something that may be easier to find than to iterate over the set of grounded actions.

The information provided by invariants has been exploited in planning for different purposes and it is essential in some planning paradigms. The automatic synthesis of invariants is a computationally hard problem, and many of the existing techniques are based on a generate and test approach that often yields an incomplete set of invariants [Fox and Long, 1998; Gerevini and Schubert, 1998; Rintanen, 2000; Rintanen, 2008; Helmert, 2009]. We have shown how to use the synthesis of guarantees for abstractions as a method for generating candidates for invariants. Hence, the computation of abstractions for generalized planning may be relevant even when the focus is to learn invariants rather than to solve generalized planning problems. As seen in the examples, some of these invariants are quite complex and out-of-reach for stateof-the-art methods for invariant synthesis.

There are clear directions for future work. First, come up with better bases for translation, based on either p+ or p∗ , and understand better the strengths and weaknesses of different bases. Second, even though we are able to handle concepts that are more general than those generated from concept grammars, we are not yet able to accommodate distance features as defined by Bonet et al. [2019a]. Finally, it may be the time to bring theorem provers into the pipeline of generalized planning: from samples we obtain abstractions ¯Q by an inductive process, a solution ¯π for ¯Q is computed with a FOND planner, and an instance P is then assured to be solved by ¯π if P satisfies the guarantee for ¯Q. The latter may be automated with the help of theorem provers.

Acknowledgments

B. Bonet is supported by a Banco Santander - UC3M Chair of Excellence Award. This work is partially funded by grants TIN2017-88476-C2-2-R and RTC-2017-6753-4 of the Spanish Ministerio de Econom´ıa, Industria y Competitividad.