Automatic Verification for Soundness of Bounded QNP Abstractions for Generalized Planning

1 Introduction

Generalized planning (GP) studies the computation of general solutions for a set of planning problems [Srivastava et al., 2008; Hu and De Giacomo, 2011; Bonet and Geffner, 2018; Segovia et al., 2019; Illanes and McIlraith, 2019]. For example, the general solution "while the block A is not clear, pick the top block above A and place it on the table" will eventually meet the goal clear(A) no matter how many blocks the tower has. Computing general solutions with correctness guarantee has long been a key issue in GP. However, so far only limited correctness results have been obtained, mainly for the so-called 1d planning problems [Hu and Levesque, 2010] and extended-LL domains [Srivastava et al., 2011a].

∗Corresponding Author

Abstractions are widely used to solve GP problems. The idea is to develop an abstract model of the problem, which is easier to solve, and exploit a solution in the abstract model to find a solution in the concrete model. A popular kind of abstract models for GP are qualitative numerical planning (QNP) problems, introduced by [Srivastava et al., 2011b]: they showed that QNPs are decidable, and proposed a generate-and-test method to solve QNPs. Bonet and Geffner [2018] proposed solving a generalized classical planning problem by abstracting it into a QNP, they showed that if the abstraction is sound, then a solution to the QNP is also a solution to the original problem. Here, soundness of abstractions is the key to guarantee correctness of solutions to the original problem.

The automatic generation of sound abstractions for GP problems has attracted the attention of researchers in recent years. Bonet et al. [2019a] proposed learning a QNP abstraction for a GP problem from a sample set of instances, however, the abstraction is guaranteed to be sound only for the sample instances. Further, Bonet et al. [2019b] showed how to obtain first-order formulas that define a set of instances on which the abstraction is guaranteed to be sound. Illanes and McIlraith [2019] considered solving a class of GP problems by automatically deriving a sound QNP abstraction from an instance of the problem, by introducing a counter for each set of indistinguishable objects, however, this class of problems is too restricted.

Recently, Banihashemi et al. [2017] proposed an agent abstraction framework based on the situation calculus [Reiter, 2001] and Golog [Levesque et al., 1997]. They related a highlevel (HL) action theory to a low-level (LL) 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. Based on their work, Cui et al. [2021] proposed a uniform abstraction framework for GP. They formalized a GP problem as a triple of a basic action theory, a trajectory constraint, and a goal. They gave model-theoretic definitions of sound/complete abstractions of a GP problem, and showed that solutions to a GP problem are nicely related to those of its sound/complete abstractions. In particular, the refinement of any solution to a sound abstraction is a solution to the original problem.

The significance of the research line initiated by Bonet and Geffner [2018] is that soundness of abstractions together with correctness of high-level solutions guarantee correctness of low-level solutions. In this paper, based on Cui et al.'s work, we explore automatic verification of sound abstractions for GP. First of all, we give a proof-theoretic characterization of sound abstractions for GP in the situation calculus. Secondly, based on the characterization, we give a sufficient condition for sound abstractions. 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 address this, we exploit universal and existential extensions of regression, and develop methods to handle counting and transitive closure. Using the SMT solver Z3, we implemented a sound bounded QNP verification system and experimented with 7 domains: 5 from the literature and 2 made by us. Experimental results showed that our system was able to successfully verify soundness of abstractions for all domains in seconds.

2 Preliminaries

In this section, we introduce the situation calculus and Golog, regression and its two extensions, and a generalized planning abstraction framework.

2.1 Situation Calculus 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. A situation s is executable if it is possible to perform the actions in s one by one: Exec(s) .= ∀a, s′ .do(a, s′ ) ⊑ s ⊃ Poss(a, s′ ).

In the situation calculus, a particular domain of application can be specified by a basic action theory (BAT) of the following form: D = Σ ∪ Dap ∪ Dss ∪ Duna ∪ DS0 , where Σ is the set of the foundational axioms for situations; 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; Dss is a set of successor state axioms (SSAs), 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; Duna is the set of unique name axioms for actions; DS0 is the initial knowledge base stating facts about S0.

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 [De Giacomo et al., 2000]. In transition semantics, a configuration 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. 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 Trans and Final as follows: Do(δ, s, s′ ) .= ∃δ′ .Trans∗ (δ, s, δ′ , s′ ) ∧ Final(δ′ , s′ ), where, Trans∗ denotes the transitive closure of Trans.

2.2 Regression and Its Extensions

Regression is an important computational mechanism for reasoning about deterministic actions and their effects in the situation calculus [Reiter, 2001]. The following is the definition of a one-step regression operator:

Definition 1. Given a BAT D and a formula ϕ. We use RD[ϕ] to denote the formula obtained from ϕ by the following steps: for each term f(⃗t, do(α, σ)), replace ϕ with ∃y.ψf (⃗t, y, α, σ) ∧ ϕ[f(⃗t, do(α, σ))/y]1 ; replace each atom P(⃗t, do(α, σ)) with ϕP (⃗t, α, σ); replace each precondition atom Poss(A(⃗t), σ) with ΠA(⃗t, σ); and further simplify the result with Duna.

Luo et al. [2020] presented the existentially extended regression, notation RE [ϕ(s), δ] denotes a state formula expressing that there exists an execution of program δ starting from s making ϕ hold.

Definition 2. Given a situation-suppressed formula ϕ and a Golog program δ, the extended regression RE [ϕ(s), δ] can be inductively defined as follows:

• RE [ϕ(s), α] = RD[P oss(α, s) ∧ ϕ(do(α, s))],
• RE [ϕ(s), ψ?] = ψ[s] ∧ ϕ(s),
• RE [ϕ(s), δ1; δ2] = RE [RE [ϕ(s), δ2], δ1],
• RE [ϕ(s), δ1|δ2] = RE [ϕ(s), δ1] ∨ RE [ϕ(s), δ2],

1ϕ[t′ /t] denotes that formula obtained from ϕ by replacing all occurrences of t′ in ϕ by t.

Proposition 2. Given a basic action theory D, a Golog program δ and a situation-suppressed formula ϕ, we have:

Li and Liu [2015] presented the universally extended regression, notation RU [ϕ(s), δ] denotes a state formula expressing that all executions of program δ starting from s making ϕ hold. To get the definition of universally extended regression, one can replace the symbols RE , ∧, ∨, and ∃ in Definition 2 with RU , ⊃, ∧, and ∀, respectively.

Proposition 3. Given a basic action theory D, a Golog program δ and a situation-suppressed formula ϕ, we have:

2.3 Generalized Planning Abstraction Framework

Situation calculus cannot express the property of termination, counting, transitive closure, and non-deterministic actions. Cui et al. [2021] extended the situation calculus for these four aspects: to represent the property of termination, following [Schulte and Delgrande, 2004], they use the situation calculus with infinite histories; to represent planning with non-deterministic actions, they treat a non-deterministic action as a non-deterministic program; to extended the situation calculus with counting, following the logic FOCN [Kuske and Schweikardt, 2017], they introduce counting terms of the form #¯ y.φ, meaning the number of tuples ¯ y satisfying formula φ; transitive closure is often used to define counting terms, following transitive closure logic [Immerman and Vardi, 1997], they introduced 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 φ.

Now we introduce the GP abstraction framework proposed in [Cui et al., 2021].

Definition 3. A GP problem is a triple 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 is a goal condition.

Example 1. In the blocks world, an agent can perform two kinds of actions: mt(x) (move x to the table, provided x is being held, and unstack(x, y) (unstack x from y, provided x is clear and x is on y.There are four fluents: clear(x), ontable(x), on(x, y), and holding(x). In this problem, the trajectory constraint C is ⊤, the goal state G is clear(A), some example axioms from D are as follows:

Precondition Axioms.

Successor State Axioms.

Initial Situation Axiom.

where the formula on+(x,A) is a transitive closure formula, which means that the block x is above block A.

Abstractions for GP problems are specified by the following notion of refinement mapping:

Definition 4. A function m is a refinement mapping from Gh= ⟨Dh,Ch,Gh⟩ to Gl= ⟨Dl,Cl,Gl⟩ if for each HL deterministic or non-deterministic action type A, m(A(⃗x)) = δA(⃗x), where δA(⃗x) is a LL program; for each HL relational fluent P, m(P(⃗x)) = ϕP (⃗x), where ϕP (⃗x) is a LL situation-suppressed formula; for each HL functional fluent f , m(f(⃗x)) = τf (⃗x), where τf (⃗x) is a LL (counting) term.

Given a refinement mapping m, they introduced an isomorphism relation, called m-isomorphic, between a HL and a LL situation as follows:

Definition 5. Given a refinement mapping m, a situation sh of a model Mh is m-isomorphic to a situation sl in a model Ml, written sh ∼m sl, if: for any HL relational fluent P, and variable assignment v, we have Mh, v[s/sh] |= P(⃗x, s) iff Ml, v[s/sl] |= m(P)(⃗x, s); for any HL 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.

To relate HL and LL models, they defined two relations: m-simulation and m-back-simulation. Intuitively, simulation means: whenever a refinement of a HL action can occur, so can the HL action, and back-simulation means the other direction. Here we only present the definition of m-simulation relation, m-back-simulation relation can be defined symmetrically. In the following, ∆MS denotes the situation domain of M; SM 0 stands for the initial situation of M; the notation Term(δ, s, C) means starting in situation s, program δ terminates under constraint C:

Definition 6. A relation B ⊆ ∆Mh S ×∆Ml S is anm-simulation relation betweenMh andMl, if ⟨SMh 0 , SMl 0 ⟩ ∈ B and the following hold: (1) ⟨sh, sl⟩ ∈ B implies that: sh ∼m sl; for any HL action type 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 HL 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.

Based on the notions above, they defined sound/complete abstraction on model and theory level. Sound abstraction means that HL behavior entails LL behavior, and complete abstraction means the other direction.

Definition 7. Mh is a sound m-abstraction of Ml, if there is an m-back-simulation relation B between Mh and Ml.

Definition 8. Mh is a complete m-abstraction of Ml, if there is a m-simulation relation B between Mh and Ml.

On the theory level, sound and complete abstractions are defined as follows:

Definition 9. Gh is a sound m-abstraction of Gl, if for any model Ml of Dl:

• there is a model Mh of Dh such that: (1) Mh is a sound m-abstraction of Ml via B1; (2) for any situations sh in Mh, sl in Ml, if ⟨sh, sl⟩ ∈ B1 and Mh, v[s/sh] |= Gh[s], thenMl, v[s/sl] |= Gl[s], and,
• there is a model M ′h of Dh such that: (1) M ′h is a complete m-abstraction of Ml via B2; (2) for any situations sh inM ′h , sl inMl, if ⟨sh, sl⟩ ∈ B2 andM ′h , v[s/sh] |= Gh[s], thenMl, v[s/sl] |= Gl[s].

Definition 10. Gh is a complete m-abstraction of Gl, if for any model Mh of Dh:

• there is a model Ml of Dl such that: (1) Mh is a complete m-abstraction of Ml via B1; (2) for any situations sh in Mh, sl in Ml, if ⟨sh, sl⟩ ∈ B1 and Ml, v[s/sl] |= Gl[s], thenMh, v[s/sh] |= Gh[s], and,
• there is a model M ′ l of Dl such that: (1) Mh is a sound m-abstraction of M ′ l via B2; (2) for any situations sh in Mh, s′l inM ′ l , if ⟨sh, s′l ⟩ ∈ B2 andM ′ l , v[s/s′l ] |= Gl[s], thenMh, v[s/sh] |= Gh[s].

3 Proof-Theoretic Characterization

In this section, we give proof-theoretic characterizations of abstractions for GP.

First of all, we introduce some notations and conventions. We define the program of doing any HL action sequence and its refinement as follows:

We call a situation s s.t. Do(anyllps, S0, s) holds an executable refinement of a HL situation, ER in short. The following notation Infexe(δ, h,C) means h is an infinite execution of program δ satisfying trajectory constraint C:

Infexe(δ, h,C) .= C(h) ∧ ∀s′ ❁ h∃δ′ . Trans∗ (δ, S0, δ′ , s′ ). We introduce an abbreviation R(s, s′ ), which means that situations s and s′ result from executing the refinement of the same HL action sequence:

Let ϕ be a HL formula uniform in a situation. We use m(ϕ) to denote the formula resulting from replacing each high-level symbol in ϕ with its LL definitions. We now define m(C) for a HL trajectory constraint C. For this purpose, we first define a normal form for trajectory constraints.

Definition 11. Let C be a trajectory constraint. We say that C is in normal form if C contains no occurrence of action variables or Poss, and any appearance of do must be in the form of s′ = do(A(⃗t), s), where s and s′ are variables.

Proposition 4. Any trajectory constraint can be converted to an equivalent one in normal form.

Proof. First, note that there are a finite number of action functions A1, . . . ,An, and hence we have ∀a ∨ni=1 ∃⃗x.a = Ai(⃗x). Thus, quantification over action variables can be removed as follows: replace ∃aϕ(a) with ∨ni=1 ∃⃗xϕ(Ai(⃗x)). Then Poss(Ai(⃗t), σ) can be replaced with the instantiated RHS of the action precondition axiom for Ai. Let C be the resulting trajectory constraint. Let do(A(⃗t), σ) be an appearance of do not in the required form. We replace C by ∃s.s = do(A(⃗t), σ) ∧ C[do(A(⃗t), σ)/s], where C[t1/t2] denotes the formula obtained from C by replacing any appearance of t1 by t2. We repeat this process until any appearance of do is in the required form.

Definition 12. Let C be a HL trajectory constraint. We first convert it into an equivalent one C ′ in normal form. We let m(C) denote the LL constraint obtained from C ′ as follows: first replace any appearance of ∃s ❁ h with ∃s ❁ h.Do(anyllps, S0, s), then replace any appearance of s′ = do(A(⃗t), s) with Do(m(A(⃗t)), s, s′ ), and finally replace any high-level symbols with its LL definitions.

We now extend the m-simulation or m-back-simulation relation B to infinite histories, and show that if a HL infinite history hh and a LL infinite history hl are B-related, then hh satisfies a constraint C iff hl satisfies m(C).

Definition 13. Let Mh be a sound or complete abstraction of Ml via B. Let hh and hl be infinite histories of Mh and Ml, respectively. We write ⟨hh, hl⟩ ∈ B if the following hold: for any sh ❁ hh, there is an ER sl ❁ hl s.t. ⟨sh, sl⟩ ∈ B; and for any ER sl ❁ hl, there is sh ❁ hh s.t. ⟨sh, sl⟩ ∈ B.

Proposition 5. Let Mh be a sound or complete abstraction of Ml via B. Let ⟨hh, hl⟩ ∈ B. Let C be a HL trajectory constraint. Then Mh, v[h/hh] |= C(h) iff Ml, v[h/hl] |= m(C)(h).

Proof. WLOG, we assume that C is in normal form. We prove by induction that for any sub-formula C ′ of C, for any free variables ⃗s and ⃗x, and for any sub-situations ⃗sh of hh and any ER sub-situations ⃗sl of hl s.t. ⟨sih , sil ⟩ ∈ B for any index i, we have Mh, v[h/hh,⃗s/⃗sh] |= C ′ iff Ml, v[h/hl,⃗s/⃗sl] |= m(C ′ ). The base cases are of the following forms s ⊑ s′ , s′ = do(A(⃗t), s), P(⃗x, s), and f(⃗x, s) = y. All these cases can be easily proved. The induction cases are those of ¬, ∧, ∃x, and ∃s ❁ h. We only prove the last case, the other cases are easy. So suppose Mh, v[h/hh, ⃗s/⃗sh] |= ∃s ❁ h.C ′ . Then there is sh ❁ hh s.t. Mh, v[h/hh,⃗s/⃗sh, s/sh] |= C ′ . By Definition 13, there is an ER sl ❁ hl s.t. ⟨sh, sl⟩ ∈ B. By induction hypothesis, Mh, v[h/hh,⃗s/⃗sh, s/sh] |= C ′ iff Ml, v[h/hl,⃗s/⃗sl, s/sl] |= m(C ′ ). Thus Ml, v[h/hl,⃗s/⃗sl] |= ∃s ❁ h.Do(anyllps, S0, s) ∧ m(C ′ ), which is m(∃s ❁ h.C ′ ). The other direction can be similarly proved.

Non-deterministic actions in [Cui et al., 2021] are treated as non-deterministic Golog programs. In particular, each non-deterministic action A has a definition in the form A(⃗x) .= π⃗u.Ad(⃗x, ⃗u), where Ad is a deterministic action. We let ΠA(⃗x, s) denote ∃⃗u.ΠAd (⃗x, ⃗u, s), let ϕP,Ad (⃗y, ⃗x, ⃗u, s) denote ϕP (⃗y, Ad(⃗x, ⃗u), s) simplified by using Duna, and let ψf,Ad (⃗y, z, ⃗x, ⃗u, s)) denote ψf(⃗y, z,Ad(⃗x, ⃗u), s) simplified by using Duna.

We now introduce the following abbreviations:

where, ψT says that the refinement of any HL action terminates in s under Cl; ξP and ξf says that for any HL action A(⃗x), if its refinement transforms situation s to s′ , then there is ⃗u s.t. the mapping of all SSAs instantiated with Ad(⃗x, ⃗u) hold for s and s′ .

The following theorem gives a proof-theoretic characterization for sound abstractions, where Item 1 and Item 6 are easy to understand; Item 2 says that Dl entails that for any ER, i.e., executable refinement of a HL situation, the executability of the refinement of any HL action implies its mapped precondition; Item 3 says that Dl entails that for any ER, the mapped precondition of any HL action implies that the executability of its refinement holds in some R-related situation; and Item 5 says that Dl entails that the existence of an infinite execution of anyllps satisfing the LL constraint is equivalent to the existence of one satisfying the mapped HL constraint.

Theorem1. Gh is a soundm-abstraction of Gl iff the following conditions hold:

1. DS0 l |=m(ϕ), where ϕ ∈ DS0 h ;
2. Dl |= ∀s.Do(anyllps, S0, s) ⊃ ∧A∈Ah ∀⃗x, s′ .Do(m(A(⃗x)), s, s′ ) ⊃ m(ΠA(⃗x, s));
3. Dl |= ∀s.Do(anyllps, S0, s) ⊃ ∧A∈Ah ∀⃗x.m(ΠA(⃗x, s)) ⊃ ∃s′ , s′′ .R(s, s′ ) ∧ Do(m(A(⃗x)), s′ , s′′ );
4. Dl |= ∀s.Do(anyllps, S0, s) ⊃ ψT ∧ ξP ∧ ξf ;
5. Dl |= ∃hl.Infexe(anyllps, hl,Cl) ≡ ∃hl .Infexe(anyllps, hl , m(Ch));
6. Dl |= ∀s.Do(anyllps, S0, s) ∧m(Gh)[s] ⊃ Gl[s].

Proof. (sketch) ⇒: Item 1 and 6 are easy to prove. For Item 2 and 4, according to Definition 9, for each model Ml of Gl, there exist a model Mh of Gh s.t. Mh is a complete abstraction of Ml via a m-simulation relation B1. Let sl be a LL situation which satisfies Do(anyllps, S0, s), then based on Definition 6, there is a HL situation sh s.t. ⟨sh, sl⟩ ∈ B1, and for any HL action type A: if m(A(⃗x)) is executable in sl, then A(⃗x) is executable in sh, thus, sl satisfies m(ΠA(⃗x, s)); sl satisfies Term(m(A(⃗x)), s,Cl); if there exists a LL situation s′l satisfies Do(m(A(⃗x)), sl, s′l ), then there exists an action A(⃗x, ⃗u) and a HL situation s′h , s.t. ⟨s′h , s′l ⟩ ∈ B1, furthermore, if sh and s′h satisfy the HL fluent-action related SSAs, then sl and s′l satisfy the mapped HL fluent-action related SSAs. For Item 3, we can prove that Mh is also a sound mabstraction of Ml via a m-back-simulation relation B2, then for ⟨sh, sl⟩ ∈ B1, there also exists a LL situation s′l , such that ⟨sh, s′l ⟩ ∈ B2, thus, sl and s′l are R-related, furthermore, A(⃗x) is executable in sh, then m(A(⃗x)) is executable in s′l . Finally, let hl be a LL infinite history, then there exists a HL infinite history hh, based on the relation B2, we can construct another LL infinite history h′l , this coupled with Proposition 5 can imply Item 5.

⇐: For any LL model Ml, by using refinement mapping, we first construct a HL model Mh, then based on the Item 1, 2, 4, and 5, we can construct a m-simulation relation B1 between Mh and Ml. Similarly, based on the Item 1, 3, 4, and 5, we can construct a m-back-simulation relation B2 between Mh and Ml. Then, we can get that Gh is sound abstraction of Gl based on Item 6 and Definition 9.

Complete abstraction on the theory level means that for each HL model Mh, there exist two LL models Ml, M ′ l s.t. Mh is a sound abstraction of Ml, and a complete abstraction of M ′ l . However, in this case, Ml and M ′ l may be different, and thus we cannot give a proof-theoretic characterization for complete abstractions. Nonetheless, we give a sufficient and necessary condition for complete abstractions in terms of the existence of two LL models Ml and M ′ l satisfying 5 conditions where Item 2 says that Ml satisfies for any ER, ψT , ξP , and ξf hold, and the LL goal implies the mapped HL goal, and the executability of the refinement of any HL action implies its mapped precondition; Item 3 says that M ′ l satisfies that there exists a set P of situations including the initial situation such that for any P-situation, ψT , ξP , and ξf hold, and the LL goal implies the mapped HL goal, and the mapped precondition of any HL action implies that its refinement is executable and leads to a P-situation.

Theorem 2. Gh is a complete m-abstraction of Gl iff for any model Mh of Dh, there are two models Ml, M ′ l of Dl s.t.

1. SMh 0 ∼m SMl 0 , SMh 0 ∼m SM′ l 0 ;
2. Ml |= ∀s.Do(anyllps, S0, s) ⊃ ∧A∈Ah [∀⃗x, s′ .Do(m(A(⃗x)), s, s′ ) ⊃ m(ΠA(⃗x, s))] ∧ψT ∧ ξP ∧ ξf ∧ [Gl[s] ⊃ m(Gh)[s]];
3. M ′ l |= ∃P.P(S0) ∧ ∀s.P(s) ⊃ ∧A∈Ah ∀⃗x.m(ΠA(⃗x, s)) ⊃ ∃s′ .Do(m(A(⃗x)), s, s′ ) ∧P (s′ ) ∧ ψT ∧ ξP ∧ ξf ∧ [Gl[s] ⊃ m(Gh)[s]];
4. if Ml |= ∃hl.Infexe(anyllps, hl,Cl), thenMh |= ∃hh.Infexe(anyhlas, hh,Ch);
5. if Mh |= ∃hh.Infexe(anyhlas, hh,Ch), then M ′ l |= ∃hl.Infexe(anyllps, hl,Cl).

Proof. (sketch) ⇒: Item 1 is easy to prove. For Item 2, according to the Definition 10, we know that for each HL model Mh of Dh, there exist a LL model Ml, such that Mh is a complete abstraction of Ml via a m-simulation relation B1. Let sl be a LL situation which satisfies Do(anyllps, S0, s), then based on Definition 6, there is a HL situation sh s.t. ⟨sh, sl⟩ ∈ B1, and for any HL action type A: if m(A(⃗x)) is executable in sl, then A(⃗x) is executable in sh, thus, sl satisfies m(ΠA(⃗x, s)); sl satisfies Term(m(A(⃗x)), s,Cl); if there exists a LL situation s′l satisfies Do(m(A(⃗x)), sl, s′l ), then there exists an action A(⃗x, ⃗u) and a HL situation s′h , s.t. ⟨s′h , s′l ⟩ ∈ B1, furthermore, if sh and s′h satisfy the HL fluentaction related SSAs, then sl and s′l satisfy the mapped HL fluent-action related SSAs; if sl satisfies Gl, then sh satisfies Gh, and hence, sl satisfies m(Gh). For Item 3, according to the Definition 10, we know that for the HL model Mh, there is another LL model M ′ l , such that Mh is a sound abstraction of M ′ l via a m-back-simulation relation B2. We construct the situation set P of M ′ l based on the following two steps: (i) SM′ l 0 ∈ P; (ii) for any LL program anyllps, if there is a situation sl satisfies Do(anyllps, SM′ l 0 , sl), then sl ∈ P. Now we let sh be a reachable situation of Mh via executing anyhlas, then according to the construction of P, there is a situation sl ∈ P of M ′ l , such that ⟨sh, sl⟩ ∈ B2, and for any HL action type A: if A(⃗x) is executable in sh, then m(A(⃗x)) is executable in sl, thus, sl satisfies m(ΠA(⃗x, s)); sl satisfies Term(m(A(⃗x)), s,Cl); if there exists a HL situation s′h satisfies Do(A(⃗x), sh, s′h ), then there exists an action A(⃗x, ⃗u) and a LL situation s′l ∈ P, s.t. ⟨s′h , s′l ⟩ ∈ B2, furthermore, if sh and s′h satisfy the HL fluent-action related SSAs, then sl and s′l satisfy the mapped HL fluent-action related SSAs; if sl satisfies Gl, then sh satisfies Gh, and hence, sl satisfies m(Gh). Item 4 and 5 can be proved by using the Definition 8 and 7, respectively.

⇐: For the model Mh and Ml, based on the Item 1, 2, and 4, we can construct a m-simulation relation B1 between Mh and Ml. Similarly, based on the Item 1, 3, and 5, we can construct a m-back-simulation relation B2 between Mh and Ml. Then, we can get that Gh is complete abstraction of Gl based on the Definition 10.

4 Automatic Verification for Soundness of Bounded QNP Abstractions

In this section, we explore how to automatically verify the soundness of bounded QNP abstractions with theorem provers. To this end, we first introduce some restrictions in Theorem 1, and give a sufficient condition for sound abstractions, which is verifiable in first-order logic with counting and transitive closure. Then, based on the sufficient condition, we present the methodology of sound bounded QNP abstraction verification with theorem provers. Particularly, we develop methods to handle counting and transitive closure.

4.1 A Sufficient Condition for Sound Abstraction

We first discuss how to obtain a sufficient condition for sound abstractions from Theorem 1:

• (1). Situations that satisfy Do(anyllps, S0, s) are all executable. State constraints are formulas that hold in all executable situations. Given a BAT D and a formula ϕ(s), ϕ(s) is a state constraint for D if D |= ∀s.Exec(s) ⊃ ϕ(s). Thus, we can replace the condition Do(anyllps, S0, s) by providing LL state constraints in tasks 2, 3, 4 and 6 in Theorem 1. We use Dsc to denote a set of state constraints, and abuse Dsc as the conjunction of its elements;
• (2). Determining whether a given program terminates is the quintessential undecidable problem. We assume that any HL action refinement does not involve iterations. Then, the formula ψT in task 4 is true trivially;
• (3). We restrict that each HL action is deterministic, thus, we can ignore trajectory constraints, and then ignore task 5;
• (4). Since tasks 2 and 3 involve the reasoning about LL Golog programs, we use existentially extended regression to compute executability conditions of Golog programs.

Given a program δ and a situation s, the executability condition pre(δ, s) of δ in the situation s can be computed as RE [⊤(s),A(⃗x)]. Thus, in tasks 2 and 3, we can equivalently replace Do(m(A(⃗x), s, s′ )) by pre(m(A(⃗x)), s). In addition, we introduce the following abbreviation:

which means that for any HL action A(⃗x) and a LL situation s, m(A(⃗x)) is executable in s if and only if s satisfies the refinement of precondition of the action A(⃗x). Then, for getting a sufficient condition for sound abstractions, we verify a stronger task which can implies both task 2 and 3: |=foct ∀s.Dsc(s) ⊃ ξA, where, |=foct denotes the entailment in first-order logic with counting and transitive closure;

(5). For further discussion, we introduce two more abbreviations as follows:

ζP .= ∧A∈Ah ∀⃗x.pre(m(A(⃗x), s))

• ⊃ ∧P ∈Ph ∀⃗y.[RE [m(P (⃗y))[s], m(A(⃗x))]
• ⊃ m(ϕP,A(⃗x, ⃗y, s))] ∧ [m(ϕP,A(⃗x, ⃗y, s))
• ⊃ RU [m(P (⃗y))[s], m(A(⃗x))],

ζf .= ∧A∈Ah ∀⃗x.pre(m(A(⃗x), s))

• ⊃ ∧f∈Fh ∀⃗y, z.[RE [m(f (⃗y) = z)[s], m(A(⃗x))]
• ⊃ m(ψf,A(⃗x, ⃗y, z, s))] ∧ [m(ψf,A(⃗x, ⃗y, z, s))
• ⊃ RU [m(f (⃗y) = z)[s], m(A(⃗x))]],

where, ζP says that if the LL programm(A(⃗x)) is executable in situation s, then there exists an execution of m(A(⃗x)) starting from s making m(P(⃗y)) hold, and all executions of m(A(⃗x)) starting from s making m(P(⃗y)) hold. ζf and ζP have similar meaning.

Based on the two extended regression definitions, we can get that task 4 is equivalent to |=foct ∀s.Dsc(s) ⊃ ζP ∧ ζf . Finally, we can get the following corollary.

Corollary 1. Given a GP problem Gl and its abstraction Gh, suppose that all the HL actions are deterministic and their refinements do not involve iteration, then Gh is a sound abstraction of Gl if:

1. DS0 l |=foct m(ϕ), where ϕ ∈ DS0 h ;
2. |=foct ∀s.Dsc(s) ⊃ ξA;
3. |=foct ∀s.Dsc(s) ⊃ ζP ∧ ζf ;
4. |=foct ∀s.Dsc(s) ∧m(Gh)[s] ⊃ Gl[s].

Note that when conditions of Corollary 1 do not hold, we cannot determine whether an abstraction is sound.

4.2 Sound Bounded QNP Abstraction Verification

QNPs are classical planning problems extended with nonnegative real variables and non-deterministic actions that increase or decrease the values of variables by positive indeterminate amounts. QNPs were first introduced by Srivastava et al. [2011b], and nowadays, they have been widely used for modeling abstractions of GP problems.

Given a set of propositional variables F and a set of nonnegative numerical variables V , we refer to p and ¬p for p ∈ F as the F-literals, v > 0 and v = 0 for v ∈ V as the V -literals. A pair of complementary literals has the form {p, ¬p} for p ∈ F, or {v > 0, v = 0} for v ∈ V . A set of literals is consistent if it does not contain complementary literals. Let LX (resp. LF ) denote the set of all consistent sets of literals from F ∪ V (resp. F).

Definition 14. A QNP problem Q = ⟨F, V, I, O, G⟩ consists of F , a set of propositional variables; V , a set of non-negative real variables; I ∈ LX, a set of initial true literals; G ∈ LX, the set of goal literals; and O, a set of actions. Every a ∈ O has a set of preconditions pre(a) ∈ LX, a set of propositional effects eff (a) ∈ LF , and a set of numerical effects N(a) which contain special atoms of the form inc(v) or dec(v) to increase or decrease v by some arbitrary amount for v ∈ V . Actions with the dec(v) effect must feature the precondition v > 0 for any variable v ∈ V .

Many abstraction models of GP problems involve integer variables. For example, Bonet and Geffner [2018] proposed abstracting generalized classical planning problems into a variant of QNPs where the numerical variables of QNPs are all non-negative integer variables. In this work, we consider that abstractions of GP problems are bounded QNPs where integer variables can be incremented or decremented by one.

Definition 15. A bounded QNP problem is a 5-tuple Q = ⟨F, V, I, O, G⟩ where F is a set of propositional variables; V is a set of non-negative integer variables; I ∈ LX is a set of initial true literals; G ∈ LX is the set of goal literals; and O is a set of actions. Every a ∈ O has a set of preconditions pre(a) ∈ LX, a set of propositional effects eff (a) ∈ LF and a set of numerical effects N(a) of the form v ↑ (v ↓) for v ∈ V , which means that v is incremented (decremented) by 1. Actions with the v ↓ effect must feature the precondition v > 0 for any variable v ∈ V .

Example 1 cont'd. An abstraction for the GP problem ClearA is a bounded QNP Q = ⟨F, V, I,O,G⟩, where F = {H} contains a propositional variable H that means the agent holding a block; V = {n} contains a numerical variable n that means the number of blocks above A; the initial state I is n > 0 ∧ ¬H; the goal state G is n = 0; the actions in O = {pickabove, putaside} are defined as follows:

In the bounded QNP abstraction case, the verification for tasks 1 and 2 can be easily transformed into two first-order theorem proving tasks with transitive closure; the verification for task 3 in Corollary 1 can be more specific, concretely, it can be divided as the following two tasks:

For each HL relational fluent p ∈ Ph, and HL action A ∈ Ah, A makes p true (the false case can be discussed similarly) means that in LL, all the executions of m(A) make m(p) true, then we have the following task 3∗ :

where, the notation |=fot means the first-order entailment with transitive closure.

For each HL functional fluent n ∈ Fh, and HL action A ∈ Ah, if A makes n increase by 1 (the decrease case can be discussed similarly), then for any LL situation s and any situation s′ that is arrived by executing m(A(⃗x)) from s, we have m(n)[s′ ] = m(n)[s] + 1. Assuming that m(n) = #x.ϕ(x), we have the following formula Ψ holds:

which means that there exists only one object that makes ϕ(x) true from false after the execution of the program m(A(⃗x)). Then based on Proposition 3, we have the following task 3#:

Transitive closure formulas are often used to define counting terms. Thus, task 3# may involve regression about transitive closure. In fact, the definition of one-step regression of transitive closure formulas is the same as Definition 1.

Example 1 cont'd. Given the successor state axiom of fluent on(x, y, s) in Example 1, and a transitive closure formula ϕ: [TCx,yon(x, y)](x,C, s′ ), the regression result RD[ϕ] of ϕ related to the concrete action unstack(A, B) is as follows:

Existing first-order theorem provers cannot express the transitive closure of formulas with the form [TCx,yφ](u, v). To handle this case, we first define the formula φ(x, y) as a new relation P(x, y), then equivalently replace the formula [TCx,yφ](u, v) with P +(x, y), and finally feed it into a theorem prover. Furthermore, existing theorem provers cannot express the minimality of transitive closure as well, thus, we can only verify the weak transitivity.

5 Verification System and Experiment Results

In this section, we designed a sound bounded QNP abstraction verification system 2 . The inputs of our system include a GP problem coupled with state constraints, a refinement mapping, and an abstraction problem. The output of our system is True / Unknown. GP problems in our system take the form of STRIPS-like problems. The only extension of GP problems to STRIPS problems is that their initial states can be first-order formulas with transitive closure (see Example 1). The formalization of bounded QNP abstractions in our system is similar to that in [Bonet and Geffner, 2020].

The workflow of our verification system is as follows:

Step 1. Given the input GP problem, the system automatically generates the LL BAT;

Step 2. Based on the abstraction problem, refinement mapping, LL BAT, and LL state constraints, the system generates the verification tasks that we mention in Corollary 1. Concretely, the system generates task 1 for the HL and LL initial states; task 2 for each HL action; task 3∗ for each pair of HL relational fluent and action; task 3# for each pair of HL functional fluent and action; task 4 for the HL and LL goals.

Step 3. The system feeds all the tasks above into the Z3solver (version 4.8.10.0) [de Moura and Bjørner, 2008] for verification. If all these tasks can be verified, then the system returns True, else returns Unknown.

We use the following example to demonstrate the verification process of our system:

2 The system is available at https://github.com/sysulic/AVS.

Example 2. This problem involves a robot with two grippers whose goal is to move some balls from room R into room D. Each gripper may carry one ball at a time. The LL predicates are: at(r), in(b, r), free(g), and carry(g, b). Actions are: move(r, r′ ), pick(b, r, g), and drop(b, r, g). The initial state is at(R) ∧ ∀g.f ree(g) ∧ ∃b.in(b, R).

The domain constraint Dsc of this problem is as follows:

• ∀g∃b.carry(b, g) ≡ ¬free(g),
• at(R) ≡ ¬at(D), ¬at(R) ≡ at(D),
• ∀b, g.in(b,R) ≡ ¬in(b,D) ∧¬carry(b, g),
• ∀b, g.in(b,D) ≡ ¬in(b,R) ∧¬carry(b, g),
• ∀b, g.carry(b, g) ≡ ¬in(b,R) ∧¬in(b,D),
• ∀b1, b2, g.carry(b1, g) ∧ carry(b2, g) ⊃ b1 = b2.

The bounded QNP problem in HL involves three numerical variables B, C, and G that denote, respectively, the number of balls at the source room, the number of balls carried by grippers, the number of free grippers. Boolean variable T means the robot is in the target room. The initial state is B > 0 ∧ C = 0 ∧ G > 0 ∧ ¬T , and the goal condition is B = 0. Actions are as follows:

• Move : ⟨¬T; T⟩, Leave : ⟨T; ¬T⟩,
• Pick : ⟨¬T,B > 0,G > 0;B -1,C +1,G-1⟩,
• Drop : ⟨T,C > 0; C -1,G+1⟩.

The refinement mapping is as follows:

• m(B) = #b.in(b, R), m(G) = #g.free(g),
• m(C) = #b.∃g.carry(b, g), m(T ) = at(D),
• m(Move) = (at(R))?;move(R,D),
• m(Leave) = (at(D))?; move(D, R),
• m(Drop) = πb, g.(carry(b, g) ∧ at(D))?; drop(b, D, g)
• m(Pick) = πb, g.(at(R) ∧ in(b, R) ∧ f ree(g))?; pick(b, R, g).

The system automatically generates 13 tasks for this problem, some of them are as follows:

• verification involves initial state: |=foct Dsc ∧ at(R) ∧ ∀g.free(g) ∧ ∃b.in(b, R) ⊃ ∃b.in(b, R)∧¬∃b, g.carry(b, g)∧∃g.f ree(g)∧¬at(D),
• verification involves goal state: |=f oct Dsc ∧ ∀b.in(b, D) ⊃ ∀b.¬in(b, R) ∧ ∀g.f ree(g),
• verification involves precondition of Pick:

|=foct Dsc ∧ ∃b, g.in(b, R) ∧ at(R) ∧ f ree(g)

• ⊃ ¬at(D) ∧ ∃b.in(b, R) ∧ ∃g.f ree(g),
• verification involves the fluent-action pair (T,Move): |=foct ∀s.Dsc(s) ∧ pre(m(Move), s) ⊃ RU [m(T (s)), m(Move)], where,
• pre(m(Move), s) ≡ at(R),
• RU [m(T(s)),m(Move)] ≡ at(R) ⊃ (at(R) ⊃ (¬at(D) ∧ D = D) ∨ (at(D) ∧ ¬D = R)).

Our verification system was also tested on other 6 domains. Abstractions of ClearA, OnAB come from [Bonet et al., 2019a]. Abstractions of other problems are provided by us.

OnAB is about achieving the goal On(A,B) in blocksworld domain where a gripper is initially empty, and the blocks A and B are in different towers with blocks above them; Logistics involves a vehicle whose goal is to load goods from the source location and transport them to the target location; GetLast and FindA are both linked list domain problems. The predicate and the action sets of these two problems are the same. The goal of GetLast is to traverse all the elements in a linked list, while FindA aims at finding the element A in a linked list; Corner contains instances that an agent needs to navigate in a rectangle grid and arrive at the point (0, 0) from any other points (x, y).

Our experiments were run on a Windows machine with a 3.7GHz CPU and 16GB RAM, the default time limit of each subtask was 15s. We summarize the experimental results in Table 1. #A is the number of HL actions. #F is the number of HL functional fluent F . #P is the number of HL relational fluent P. T is the total time costs of all verification tasks. Experimental results showed that our systemwas able to successfully verify soundness of abstractions for all domains in a reasonable time.

6 Conclusion

In GP, solutions of sound abstractions are those with correctness guarantees for the original problems. In this paper, based on Cui et al.'s work, we explored automatic verification of sound abstractions for GP. We gave a proof-theoretic characterization of sound abstractions for GP in the situation calculus. Then, we got a sufficient condition for sound abstractions. To implement it in the bounded QNP abstraction case,we exploited regression extensions and presented methods to handle counting and transitive closure. In the future, we are interested in automatic verification concerning trajectory constraints for non-deterministic abstractions, such as FOND. We are also interested in automatic learning abstractions and abstraction revision based on the verification of sound abstraction.

Acknowledgments

We acknowledge support from the Natural Science Foundation of China under Grant No. 62076261.