How to Progress a Database II: The STRIPS Connection

1 Preliminaries

The language C of the situation calculus is first-order, many-sorted, with sorts state for situations, action for actions, and object for everything else. It has the fol­ lowing domain independent predicates and functions: a constant So of sort state denoting the initial state; a binary function do( a, s) denoting the state resulting from performing the action a in the state s; a binary predicate Poss(a, s) meaning that the action a is pos­ sible (executable) in state s; and a binary predicate <: state x state. s < s' means that s' can be reached from s by a sequence of executable actions. We assume a finite number of state independent predicates with ar­ ity objectn, n ~ 0, a finite number of state independent functions with arity objectn -+ object, n ~ 0, and a finite number of fiuents which are predicate symbols of arity objectn x state, n ~ 0. We denote by £ 2 the second-order extension of C. Our foundational axioms for the situation calculus will be in £ 2 (Lin and Reiter [7]), because we need induction on situations (Reiter [12]).

*Fellow of the Canadian Institute for Advanced Research

Often, we must restrict the situation calculus to a par­ ticular situation. For instance, the initial database is a finite set of sentences in .C that do not mention any state terms except S0 , and do not mention Pass and <. For this purpose, for any state term st, we define .Cst to be the subset of .C that does not mention any other state terms except st, does not quantify over state variables, and does not mention Pass or <.

We use c;t to denote the second-order extension of Cst by predicate variables of arity objectn, n ~ 0. So the second-order sentence (3p)('v'x).p(x) = F(x, So) is inC~ , but (3p)('v'x)(3s).p(x, s) ::::: F(x, S0 ) is not, since the l~tter quantifies over a predicate variable of arity object x state.

Our situation calculus theory of actions, V, will have the form (cf. Reiter [13) and Lin and Reiter [7]) V = "E U 'Dss U 'Dap U 'Duna U Vs 0 , where

• "E is the set of foundational axioms for the situation calculus (Lin and Reiter [6)). These play no role in the current paper, so we omit them.
• 'Dss is a set of successor state axioms, one for each fluent F(x, s), of the form:

where <l>p(X,a,s) is in £ 5 · Successor state axioms embody a solution to the frame problem, as de­ scribed in Reiter [11).

• Vap is a set of action precondition axioms, one for each action A(x), of the form:

where 'l!A(x,s) is in Cs.

• 'Duna is the set of unique names axioms for actions: for any two different actions A ( x) and A' (y) we have A(x) =1= A'(Y), and for any action A(x), we have 1

• Vs 0 , the initial database, is a finite set of first-order sentences in .Cs 0 ·

1 In what follows, x = y is an abbreviation for X1 = Yl 1\ ···1\xn=Yn·

Example 1.1 The following blocks world will provide a running example for this paper:

Actions

• move(x, y, z): Move the block x from blocky onto block z, provided both x and z are clear and block x is on top of block y.
• movefromtable(x, y): Move the block x from the table onto block y, provided x is clear and on the table, and block y is clear.
• movetotable(x, y): Move block x from blocky onto the table, provided x is clear and x is on y.

Fluents

• clear(x, s): Block x has no other blocks on top of it, in state s.
• on(x, y, s): Block xis on (touching) blocky, in state s.
• ontable(x, s): Block xis on the table, in states.

This setting can be axiomatized as follows:

Action Precondition Axioms

Poss(move(x, y, z), s) = clear(x, s) 1\ clear(z, s) 1\ on(x, y, s) 1\ xi= y 1\ xi= z 1\ y i= z,

Poss(movefromtable(x, y), s) = clear(x, s) 1\ clear(y, s) 1\ ontable(x, s) 1\ xi= y,

Poss(movetotable(x, y), s) = clear(x, s) 1\ on(x, y, s) 1\x i= y.

Successor State Axioms

Pass( a, s) :J [clear(x, do( a, s)) =

1. M' and M interpret all predicate and function sym­ bols which do not take any arguments of sort state identically.
2. M and M' agree on all fluents at So:: For every fluent F, and every variable assignment a,

If M' "'Sa M, then M' agrees with M on So: on fluents and state independent predicates and functions, but is free to vary its interpretation of everything else on all other states. In particular, they can interpret Pass and do differently.

Definition 1.1 A set of sentences Dsa in £t is a pro­ gression of the initial database Ds 0 to So: {with respect to D) iff for any structure M, M is a model of Dsa iff there is a model M' ofV such that M "'SaM'.

Notice that the new database is defined only up to log­ ical equivalence. The new database is allowed to contain second-order sentences because, as shown in (Lin and Reiter [6]), progression is not always first order defin­ able, but Dsa can always be captured by a set of second order sentences. However, Lin and Reiter specify some important special cases, which we shall exploit in this paper, for which progression is first order definable.

Our intuition about the semantics of STRIPS opera­ tors is that they are mechanisms for progressing situation calculus databases. This is the central idea of this paper, which is devoted to making this intuition precise.

(3y,z)a = move(y,x,z) V (3y,z)a = move(x,y,z) V

(3y)a = movetotable(x, y) V (3y)a = movetotable(y, x) V 2

(3y)a = movefromtable(x, y) V

clear(x, s) 1\ ·(3y, z)a = move(y, z, x) 1\

·(3y)a = movefromtable(y, x)],

Poss(a, s) :J [on(x, y, do( a, s)) = (3z)a = move(x, z, y) V a= movefromtable(x, y) V on(x, y, s) 1\ a i= movetotable(x, y) 1\ ·(3z)a = move(x, y, z)],

The central concept of (Lin and Reiter [6]) is this: Imagine performing an action a in an initial database Ds 0 · Let So: denote the resulting situation do( a, So). Imagine a database, Ds", which can act as a new initial database in the sense that

1. Dsa is a set of sentences about state So: only, i.e., in £sa or in £t.
2. For all queries about the future of So:, V is equiva­ lent (in a suitable formal sense) to I: U Dss U Dap U Duna U Dsa·

In other words, Ds" acts like the new initial database with respect to all possible future evolutions of the the­ ory following a. Dsa is said to be a progression of Ds 0 with respect to action a. To define progression formally, Lin and Reiter first introduce an equivalence relation over structures. Let M and M' be structures for £ 2 with the same domains for sorts action and object. De­ fine M' ,...., sa M iff the following two conditions hold:

STRIPS

Following Lifschitz ([4]), define an operator description to be a triple (P, D, A), where Pis a sentence of a first order language LSTRIPS and D (the delete list) and A (the add list) are sets of sentences of £sTRIPS· A world description W is any set of sentences of £sr RIPS. A STRIPS system consists of:

1. A world description W0 , called the initial world description,
2. A binary relation !> ~ 2CsrRIPs x £sTRIPs?
3. A set Op of symbols called operators, and
4. A family of operator descriptions {(Po:, Do:, Ao:)}o:EOp·

With each operator a is associated a world description Wa, the successor world description of Wo, defined by Wa = (Wo - Da) U Aa. A successor world description Wa is admissible iff Wo !> Pa.

Sometimes, but not always, !> will be the standard en­ tailment relation for the first order language £sTRIPS· In this case, admissibility simply corresponds to the fact that the precondition Po: is entailed by the initial world description W0 , in which case, on the standard view of STRIPS, the operator a is applicable. However, our in­ tuitions about STRIPS are not standard, and we prefer to leave open the interpretation of the "entailment" re­ lation !>.

2 In his treatment of STRIPS, Lifschitz does not provide for the relation !>.

Our semantics for STRIPS systems is indirect; we de­ fine certain classes of theories in the situation calculus and show how to associate suitable STRIPS systems with those theories. Only STRIPS systems associated with such situation calculus theories will, on our account of STRIPS, be assigned a semantics. This leaves many STRIPS systems (namely those without an associated situation calculus theory) without a semantics; we are not very distressed by this, given that STRIPS systems, in their full generality, do not currently have coherent semantics anyway.

3 Two Versions of STRIPS

The STRIPS systems we derive apply only to a restricted class of situation calculus action theories for which the successor state axioms have a particular syntactic form, which we now define. A successor state axiom is context free iff it has the form:

Here the A's and B's are function symbols of sort action, not necessarily distinct from one another. The [ and ij are sequences of distinct variables which include all of the variables of x; the remaining variables of the [ and ij are those being existentially quantified by the v and w, respectively. x could be the empty sequence. 3 The successor state axioms of our running blocks world example are context free. The following successor state axiom is not context free:

This is because the action tiptable does not have x as a parameter.

The STRIPS systems which we shall characterize will be for languages £ 2 whose orily function symbols of sort object are constants. Therefore, consider a ground action term a, and the context free successor state axiom (1) for fluent F, relativized to the initial state So. How does a affect the truth value of fluent F in the successor state do( a, S0 )? By the unique names axioms for actions, together with the assumption that the successor state axioms are context free, this relativized axiom will be logically equivalent to a sentence of the form:

Here the X and Y are tuples of constants of £ 2 obtained from those mentioned by the ground action term a. If we assume further that the action a is possible in the initial state, i.e. that V f= Foss( a, S0 ), this is equivalent to:

3 Notice that this is a slightly more restricted definition for context free successor state axioms than that of (Lin and Reiter [6)) . Specifically, we did not require that each action term A;({(i)) and B;(i{il) mention all of the variables of x in the variables {(i) and rfil.

Example 3.1 Consider Example

1.1 under the "generic" ground action move (X, Y, Z). The corresponding instances of (2) for the fluents clear, on and ontable are logically equivalent to:

3.1 OCF-STRIPS: Open World, Context Free STRIPS

Our point of departure is an action theory V = 'EUV8 8 U Vap U Vuna U Vs 0 , with the following properties:

1. The only function symbols of sort object that the second order language £ 2 possesses are constants. 4
2. Each state dependent sentence of Vs 0 is a ground fluent literal, i.e. of the form F(C, Sa) or -.F(C, Sa) for fluent F and constants C of sort object.
3. Vs 0 contains unique names axioms for constants of sort object: For each pair of distinct constant names C and C' of sort object, the axiom C 'I C'.
4. Vs 0 contains no pair of complementary literals.
5. Each successor state axiom of Vss is context free.
6. We are progressing with respect to a, a ground ac­ tion term, and a is possible initially:

1. For each fluent F, the following consistency condi­ tion (Reiter [11]) is satisfied:

where F's successor state axiom has the form

4 Recall that £ 2 is the language in which V is expressed.

The consistency condition (3) deserves a brief expla­ nation. Following Pednault [9] and Schubert [14], Reiter [11] provides a solution to the frame problem in the ab­ sence of state constraints which syntactically transforms a pair of effect axioms for a given fluent F into a succes­ sor state axiom for F. The effect axioms are assumed to have the syntactic forms:

and

Reiter applies the explanation closure idea of Schubert [14] to obtain the following frame axioms for F:

The successor state axiom (4) is logically equivalent to the conjunction of the above four sentences, whenever the consistency condition (3) holds. Notice that the consistency condition makes good sense: If it were violated, so that for some X, A, S we have Poss(A, S), !f(X,A,S), and r"F(X,A,S), then we could derive an immediate inconsistency from the above two effect ax­ ioms.

It is easy (but tedious) to verify that each fluent of Example 1.1 satisfies the consistency condition.

In keeping with our intuition that STRIPS systems are mechanisms for progressing situation calculus databases, we want now to characterize the result of progressing Vs 0 under the effects of the ground action a in the case of action theories of the above kind. This turns out to be easy, since the necessary work has already been done (Lin and Reiter [6], Section 6).

Let S be the following set of sentences:

1. InitializeS to {<p E Vs 0 I <pis state independent}.
2. For each fluent F do (with reference to the instance (2) ofF's successor state axiom):
3. (a) Add to S the sentence F(X(i), do( a, S0 )), i = 1, ... ,m.
4. (b) For each ground instance F(C, So) E Vs 0 add to S the sentence F(C, do( a, S0 )), whenever C is a tuple of constants different from each y(i), i = 1, ... , n. (Here, we invoke the unique names axioms for constants of sort object).
5. (c) Add to S the sentence ·F(Y(i), do( a, S0 )), i = 1, ... ,n.
6. (d) For each ground instance ·F(C, So) E Vs 0 add to S the sentence ·F(C, do( a, S0 )), when­ ever C is a tuple of constants different from each _i(i), i = 1, ... , m. (We again invoke the unique names axioms for constants of sort ob­ ject).

The resulting set S enjoys the property that S U Vuna is a progression of Vs 0 under action a (Lin and Reiter

[6], Theorem 4). 5 Moreover, the state dependent sen­ tences of S are all ground literals, and the results of Lin and Reiter [6] guarantee that S contains no pair of com­ plementary literals. It follows that S can serve as a new initial database for the purposes of iterating the above progression mechanism.

Now we interpret the above construction of the setS as a STRIPS operator. Imagine suppressing the state argument 80 of all the ground literals of Vs 0 · Now ask what sequence of deletions and additions of ground lit­ erals must be performed on the state-suppressed version of Vs 0 in order to obtain the state-suppressed version of S (i.e. S with the state argument do( a, S0 ) suppressed in its sentences). The deletions and additions necessary to achieve this state-suppressed transformation of Vs 0 to S will define the delete and add lists for the STRIPS operator a.

It is easy to see that the following deletions and addi­ tions, when applied to V0 , the state-suppressed version of Vs 0 , yields the state-suppressed version of S:

For each fluent F do (with reference to the instance (2) ofF's successor state axiom):

1. Delete from V 0 the sentences ·F(f(il), i = 1, ... ,m.
2. Delete from V 0 the sentences F(f(il), i = 1, ... ,n.
3. Add to V 0 the sentences F(f(il), i = 1, ... , m.
4. Add to V0 the sentences ·F(Y(il), i = 1, ... , n.

It is now clear how to define a STRIPS system and its associated operator for a: 6

1. The language .Csr RIPS is the state-suppressed ver­ sion of .C 2 · 7
2. The initial world description is V 0 .
3. t> is ordinary logical entailment; for a world de­ scription W and sentence a E .CsrRI ps, W !>a iff W f=a.
4. a's precondition is the state-suppressed version of the right hand side of the equivalence in a's situa­ tion calculus action precondition axiom.
5. For each fluent F, include in a's add and delete lists those literals specified above for obtaining the state suppressed version of S.

To our knowledge, OCF-STRIPS is the only variant of STRIPS which specifically provides for an incomplete database of ground literals, and which is provably correct with respect to a logical specification.

Example 3.2 Continuing with our blocks world exam­ ple, we can "read off" the OCF-STRIPS operator schema for move from the instances of the successor state axioms given in Example 3.1:

5 The consistency condition (3) was inadvertently omitted from the assumptions underlying Theorem 4 of Lin and Reiter [6].

6 See Section 2 for the relevant definitions.

7 We take it as self evident what is meant formally by the language obtained by suppressing objects of sort state from the language £ 2 .

move(X, Y, Z) 8

The operator description schemas for movefromtable and movetotable are obtained in the same way:

movefromtable(X, Y)

P: clear(X) 1\ clear(Y) 1\ ontable(X) 1\ X =P Y.

movetotable(X, Y)

P: clear(X) 1\ on(X, Y) 1\ X=/; Y.

A: clear( X), clear(Y), ·on( X, Y), ontable(X).

3.2 RCF-STRIPS: Relational, Context Free STRIPS

This version of STRIPS derives from action theories V of the form V = ~ u v ·· u Vap u Vuna u Vs 0 , with the following properties:

1. The only function symbols of sort object that the second order language £ 2 possesses are constants.
2. Vs 0 contains one sentence of the following form, for each fluent F:

where the C(i) are tuples of constant symbols of sort object. These are the only state dependent sentences of Vs 0 · (Initial databases of this form are special cases of the relatively complete databases defined in (Lin and Reiter [6]).) The case n = 0 is permitted, in which case this axiom is F(x, So) = false. For example, if an agent's hand is initially empty:

If initially, block A is on B, D is on A, C is on E, and no other block is on a block:

1. Vs 0 contains unique names axioms for constants of sort object.
2. Each successor state axiom of v ·· is context free.
3. We are progressing with respect to a, a ground ac­ tion term, and a is possible initially:

Notice that the single sentence (5) is logically equivalent to:

8 Notice that these are schemas, standing for the family of operators obtained by instantiating the "variables" X, Y and Z of the schema by constants of our situation calculus language.

Notice also that, given all the positive instances (6) ofF, we can trivially determine the sentence (7) . So it is suf­ ficient to represent a database of this form (say for com­ putational purposes) by the set of all positive instances of F. This, we claim, is what some versions of STRIPS do (but suppressing the state argument). This is also what relational databases do; in fact, the unique names assumption together with the condition (5) on Vs 0 are the defining properties for a relational database (Reiter [10]). The relational tables are just the ground instances of the fluents F. (But bear in mind that logically, the database consists of the table for F, together with the axiom (7) and unique names axioms.)

As we did in the previous section, we want now to characterize the result of progressing Vs 0 under the ef­ fects of the ground action a in the case of action theories of the above kind. To do so, we appeal to the results in (Lin and Reiter [6], Section 5). Consider the context free successor state axiom (2) for fluent F which we rel­ ativized to the initial state S0 . By our assumption (5) on the syntactic form of Vs 0 , (2) is equivalent to:

Let (7(1), ... , C(r) be all the C(k) that are different tuples than all of the y(i). Then, by unique names axioms for constant symbols of sort object, the above sentence will be logically equivalent to

Let S be the following set of sentences:

1. Initialize S to { cp E Vs 0 I cp is state independent}.
2. For each fluent F do: Add the sentence (8) to S.

The resulting set S enjoys the property that S U Vuna is a progression of Vs 0 under action a (Lin and Reiter [6], Theorem 3). Moreover, S has the same syntactic form as Vs 0 , and so can serve as a new initial database for the purposes of iterating the above progression mechanism.

Now we interpret the above construction of the setS as a STRIPS operator. Imagine representing the state dependent sentences

by the state-suppressed relational database of ground instances F(C(ll) , .. . , F(C(n)) . We emphasize that this representation is merely a shorthand for the sentence (9). Now ask what sequence of deletions and additions of ground literals must be performed on V 0 , the state­ suppressed relational database version of Vs 0 in order to obtain the state-suppressed relational version of S. The deletions and additions necessary to achieve this trans­ formation of Vo to the corresponding representation of S will define the delete and add lists for the STRIPS operator a.

It is easy to see that the following deletions and ad­ ditions, when applied to V 0 , yield the state-suppressed, relational database representation of S:

For each fluent F do (with reference to (2)):

1. Delete from V 0 the sentences F(Y(il), i = 1, . . . , n.
2. Add to V 0 the sentences F(X(il), i = 1, .. . ,m.

It is now clear how to define a STRIPS system and its associated operator for a: 9

1. The language .Csr RIps is the state-suppressed ver­ sion of £ 2 .
2. The initial world description is V 0 .
3. For a sentence u E .CsrRIPS, W t> u iff R(W) f= u . Here, W is a world description in relational database form for all its fluents, i.e. the only sentences in W that mention a fluent are ground atoms of that fluent. R(W) is the translation of the relational database part of W to its full logical form as follows: R(W) consists of the sentences of W that do not mention a fluent, together with those sentences of the form

where F(C(ll) , . . . ,F(C(n)) are all the ground in­ stances of a fluent Fin W .

1. a's precondition is the state-suppressed version of the right hand side of the equivalence in a's situa­ tion calculus action precondition axiom.
2. For each fluent F , include in a's add and delete lists those literals specified above for obtaining the state suppressed relational database representation of S.

Example 3.3 Consider the same actions, fluents and axioms as in Example 1.1, except treat this setting now as an instance of an RCF-STRIPS situation calculus specification. In this case, as before, we can "read .off" the RCF-STRIPS operator schema for move from the instances of the successor state axioms of Example 3.1:

move(X, Y , Z)

The operator description schemas for movefromtable and movetotable are obtained in the same way:

m ove fromtabl e(X, Y)

P: clear ( X) 1\ clear(Y) 1\ ontable(X) 1\ X f. Y.

D: clear(Y) , ontable(X) .

A: clear( X), on( X, Y) .

m ovetotable(X, Y)

P: clear(X) 1\ on(X, Y) 1\ X f. Y.

D: on(X, Y) .

A: clear(X), clear(Y), ontable(X).

4 Pednault's ADL

The only prior literature similar to our progression se­ mantics for STRIPS-like systems is by Pednault ([9], [8]). Like us, Pednault relates a STRIPS database to the ini­ tial state of a situation calculus axiomatization. But our interpretation of such a database, namely as a state­ suppressed situation calculus theory, distinguishes our approach from Pednault's, in which these databases are first order structures. So for Pednault, STRIPS is a map­ ping from first order structures to first order structures , where this mapping is defined by the addition and dele­ tion of tuples applied to the relations of the structure. ADL, Pednault's generalization of STRIPS, is just such a mapping between structures. For us, as for Lifschitz [4], STRIPS is a mapping from first order theories to (possibly second order) theories, where this mapping is effected by add and delete lists of sentences applied to the theory. The problem with the ADL view on STRIPS is that it does not provide a feasible mechanism for ap­ plying a STRIPS operator in the case that the database is a logically incomplete theory (e.g. OCF~STRIPS of Section 3.1). For in such a case, every model of this theory must be mapped by an ADL operator into its transformed structure, and it is the set of all such trans­ formed structures which represents the effect of the ADL operator. When there are infinitely many such models, or even when they are finite in number but numerous, ADL becomes an unattractive STRIPS mechanism. In contrast, our focus is on STRIPS mechanisms that oper­ ate on logical theories, and hence operate on the single sentential representations of these many models.

9 See Section 2 for the relevant definitions.

5 Conclusions

1. On our view STRIPS is a mechanism for progress­ ing a situation calculus theory, and its semantics can best be understood with reference to a suitable sit­ uation calculus axiomatization of actions and their effects.
2. With this notion of progression in hand, it becomes possible to formulate various STRIPS-like systems, and prove their correctness with respect to our pro­ gression semantics. In this paper we have done just that for two different STRIPS systems (OCF and RCF-STRIPS). In this connection OCF-STRIPS is of particular interest because it provides for a (lim­ ited) form of logical incompleteness of the database.
3. Notice that it is a completely mechanical process to obtain the OCF -STRIPS operators from a situa­ tion calculus axiomatization of some domain. Simi­ larly for RCF-STRIPS. In other words, these purely declarative situation calculus specifications can be compiled into appropriate STRIPS systems.
4. The connection of RCF -STRIPS to relational databases (Section 3.2) suggests a natural gener­ alization of STRIPS operators to allow for arbi­ trary relational algebra operators (not just adds and deletes) in defining the operator's effects. This can indeed be done, and an appropriate semantics de­ fined in terms of a situation calculus axiomatization that relaxes the context free restriction on successor state axioms of Section 3.2 (Lin and Reiter [5]: the full version of this paper).
5. We have considered only STRIPS systems that com­ pute the full result of progression. Sometimes, for

instance for computational purposes, it may be bet­ ter to compute only that part of the progression that is relevant to the goals of interest. For example, if our blocks world includes a fluent for the colors of blocks, then there are no need to progress this fluent if our goals have nothing to do with colors.

Formally, we say that a given STRIPS system is sound with respect to a consistent action theory V = ~ U 'Dss U 'Dap U 'Duna U 'Ds 0 iff: For any fi­ nite (including empty) sequence 6 of operators in the STRIPS system, there is a corresponding finite sequence T of action in the situation calculus such that if the world description W0 after performing 6 on Wo is admissible, then T is executable in So and 'DT ~ Th(W0), where VT is the result of sup­ pressing states in the progression of Vs 0 to ST, and Th(Wo) = { cp I Wo t> cp }.

Generally, if a STRIPS system is sound with respect to an action theory, then any goal that is achievable in the STRIPS system is also achievable in the ac­ tion theory. However, the converse is not true in general. We say a STRIPS system is adequate for a given goal if the converse is true, i.e. whenever the goal is achievable in the situation calculus theory by a sequence of actions, it is also achievable by a sequence of operators in the STRIPS system.

With these definitions in hand, we can show (Lin and Reiter [5): the full version of this paper) that, with respect to a suitable action theory, the main example STRIPS system considered in (Fikes and Nilsson [3)) is both sound, and adequate for the class of goals considered there. This is of interest because it shows that our semantics is sophisticated enough to handle the concepts of non-literal and/or non-essential formulas considered in Lifschitz's [4) analysis of this same example.

Acknowledgements:

Thanks to the other members of the University of Toronto Cognitive Robotics Group (Yves Lesperance, Hector Levesque, Richard Mann, Daniel Marcu and Richard Scher!) for their comments and suggestions. This research was sup­ ported by grants from the Natural Sciences and Engineering Research Council of Canada, the Institute for Robotics and Intelligent Systems of the Government of Canada, and the Information Technology Research Centre of the Government of Ontario.