Action Localness, Genericity and Invariants in STRIPS

1 Introduction

Among the earliest proposals for specifying actions is STRIPS, due to Fikes and Nilsson [Fikes and Nilsson 71]. STRIPS has the great merit of simplicity and ease of imple­ mentation. As an example and a quick review of it, here is how the action of picking up block A in a blocks world may be specified:

action: pick-up(A)

pre-condition: on(A,X), clear(A)

post-condition: add-list: inhand(A) delete-list: on( A,X)

In a Prolog setting, this is easily implemented by the rule: pick-up(A) :- on(A,X), clear(A), retract(on(A,X)), as­ sert(inhand(A)) assuming that the state of the blocks-world

Yan Zhang

Knowledge Systems Group Department of Computing University of Western Sydney, Nepean Kingswood, NSW 2747, Australia

is represented as a collection of Prolog facts. An immediate observation is that both the specification and the implemen­ tation describe a generic action that has A as a parameter, and that X is implicitly existentially quantified. Even this ex­ ample however is not as general as STRIPS can be, for it is possible to have first-order formulas in the pre-condition and post-condition. However, unless restrictions are observed, the inclusion of such formulas, as pointed out by Lifschitz [Lif­ schitz 86] can cause difficulties. Moreover, until that paper appeared, there was no proper logical semantics for STRIPS. Further, constraints or invariants (like "no block can be both inhand and on something") are observed either (a) by specifi­ cation or programming of the add-list and delete-list to ensure non-violation, or (b) by Prolog rules of the form: impossi­ ble:- inhand(A), on(A,X) where not( impossible) is used as a guard in the body of action rules.

A logical semantics of STRIPS should build upon the in­ sights of Lifschitz and also give an account of several other characteristics. Lifschitz showed that if states of the world are represented as sets of ground atoms, then his semantics of STRIPS is safe, and we will use this as a starting point because we are principally interested in understanding the ef­ ficacy of Prolog-like implementations that are based on such state representation. Designers of rules for such programs of­ ten draw pictures like that shown in figures 1 and 2 to reason about pre- and post-conditions, and to maintain constraints implicitly. The most striking characteristic of such pictures is the identification of 'localness' and 'genericity'. Localness has to do with the fact that an informal 'window' (see the dashed enclosures in the figures) is typically drawn around the objects relevant to the action instance. Genericity is the notion that each window to which an action can apply looks like any other similar window except for a change in parame­ ters. Another characteristic, noted by Lifschitz [Lifschitz 86] is that the constraints like the impossible rule above are often maintained implicitly by clever design of the add- and deletelists. In this paper we address these and related characteristics to provide a formal explication for why they work.

The organization of the paper is as follows. In section 2 we recapitulate a number of standard definitions, intro­ duce a formal counterpart of the 'window' idea and show how it accounts for pre-condition 'local ness'. We also pro­ vide the formal equivalent of 'genericity' for actions. In sec­ tion 3 we examine state change due to actions and show that post-condition 'windows' have the same boundary as the pre­ condition ones. We also identify two kinds of inertial assump­ tions that appear to be implicitly used by designers of action specifications. Section 4 considers intended design semantics in the add- and delete-lists, and shows how candidate action invariants can be derived from them depending on two kinds of inertial assumptions. Concluding the paper is section 5 which discusses what we are currently pursuing and what has yet to be done.

2 States, Actions and Windows

States of the world are describable formally in many ways, but a popular one is to represent them as collections of ground atoms. This is a particularly felicitous choice for databases, and for implementations in languages like Prolog. In this pa­ per we accept this choice as it will permit us to focus on the issues that really matter without being distracted by techni­ calities that may attend alternative choices. It has the virtue of simplicity and is sanctioned by earlier investigations by Lifschitz. To this end therefore, we will adopt a first-order language with equality as our descriptive medium. Section 2.1 recalls the logic and model theory needed.

Actions are state transformers. In the STRIPS tradition, for an action to apply in a state its pre-condition must be sat­ isfied by that state. Actions that are specified with parameters or variables have instances that are the result of instantiat­ ing or substituting constant names of objects in the state into the action pre-condition. If successfully applied, the post­ conditions of the action are actuated, i.e., the add-list and delete-list operations are performed on the representation. If states are theories, then actions so modelled are theory change operators. Such operators have been studied extensively in the logics of action from many perspectives (an example is [Lin 95]), but it is not the purpose of this paper to introduce yet another. Rather, we wish to examine a well-known system that has wide practical acceptance to see if its design heuris­ tics, particularly those with a diagrammatic flavor such as ex­ posited by Barwise [Barwise 95], can be given formal justifi­ cations.

2.1 Basic Definitions and Constructions

Since ground atoms are the basis of state descriptions, in or­ der to evaluate formulas with respect to states we need to know when an atom does not hold. The simplest assump­ tion to achieve this is to use the version of the closed world assumption [Reiter 78] in the absence of constraints.

Definition 1 If .6. is a set of ground atoms of C, then the closed world assumption applied to .6. is CWA(-6.) = .6. U { -,£1£ fl. .6. and Lis a ground atom}.

This is actually a simplification of the original definition which involves state constraints, but here .none are assumed to be (explicitly) available. A potential problem with this as­ sumption is inconsistency when the description is indefinite [Zhang and Foo 96], e.g. there is a constraint of the form p V q where p and q are atoms, and neither of them appear in the state description. The indefiniteness of actions in terms of their pre- or post-conditions is known to be problematic [Zhang and Foo 96]. For pre-conditions it is possible to avoid it by refining the action ontology to "split" the indefinite ac­ tion into definite ones, but for post-conditions no such easy way is known. To circumvent this for the purpose of focusing on the main ideas, we shall therefore assume that all descrip­ tions for states as well as for actions are definite. Then, using the closed world assumption, all states are ground complete, i.e., for each ground atom, either it or its negation holds in a state.

Formally, complete states are structures in model theory and logic, so we shall use the terms state and structure inter­ changeably. The next three definitions are paraphrased from [Enderton 72; Chang and Keisler 73]. (As it gets tedious to make distinctions between predicate (constant) symbols and the relations (domain elements) they denote, we will not ob­ serve these distinctions later.)

Definition 2 Suppose Cis a first-order language with equal­ ity. An £-structure U is a triple (A, R, C) where A is a non­ empty set called the domain of U, R is a map that assigns relations of the appropriate arity on A to predicate symbols in C, and C is a map that assigns elements of A to constant symbols in C.

Definition 3 IfU1 and U2 are C structures with domains A1 and A2 respectively such that A1 ~ A2, and the relation and constant assignment maps of ul are that of u2 restricted to A1, then U1 is a substructure ofU2, and conversely U2 is an extension ofUl.

Definition 4 Two C structures U1 and U2 are elementarily equivalent, written U1 =: U2, if for every sentence¢ E C, U1 F= ¢ if!U2 F= ¢.

Two elementarily equivalent structures satisfy exactly the same set of sentences, and are therefore indistinguishable by sentences. To look ahead a little, our interest in sub­ structures arises from the intuition that they are the 'win­ dows' within pictures of states to which actions are locally applied. The construction of these windows is determined by the arguments or parameters of the action pre-condition, and the objects of relevance are accumulated via a closure opera­ tion. This closure has the effect of accruing, to the constants that instantiate a pre-condition, other constants that may be needed to evaluate predicates in the pre-condition. For in­ stance, if V X P(X, b) is a component of a pre-condition and b is a constant instantiated into it as an action parameter, we would need to accrue all constants c in the (domain of the) structure for which P( c, b) holds in order to evaluate the com­ ponent. This motivates the closure definition below.

Definition 5 Given a set S of constants in U, the expansion of S by n-ary predicate Pin U, denoted closure(U, S, P), is U{ {a1, ... , an} I some ai is inS, andU f= P(a1, ... , an)}. The notation closure(U, S, P1, ... , Pk) has the obvious gen­ eralization to several predicates.

In fact, this closure is a special case of a more general clo­ sure which is suggested by the notation closure(U, S, P, k) where k is the level of transitivity of P used in the expansion of S, e.g., if a E Sand Pis binary with P(a, b) and P(b, c) holding in U (while neither b nor c is in S), both b and c will be in closure(U, S, P, 2). Our closure is fork = 1, and we confine attention to this case simply because the key ideas in this paper are thereby not obscured by technical detail, and moreover for most practical applications k = 1 suffices. The generalization to arbitrary k is conceptually easy. The con­ struction of the closure implies the following lemma.

Lemma 1 Assume the notation as in definition 5. If U f= Q(b, xl, .. . ,xk, al, ... , am)

for all b in closure(U, { a1, ... , am}, Q) then U f= 'v'YQ(Y,X1, ... , Xk, a1, ... , am)·

This lemma is the basis for an induction that establishes the corresponding lemma in which Q above is replaced by gen­ eral formulas called D-formulas in definition 6 below, where D is { a1, ... , am} in the present context.

2.2 Blocks World Example

The blocks-world structure (state) illustrated by figures I and 2 will motivate much of the later development. All of figure 1 shows a world Win which£ has predicate symbol on(·,·), constant symbols {a, b, c, d, e, table}. Letting the constant symbols name their domain elements and the predicate sym­ bol name its relation, the theory T2 (subtheory of T1, to be in­ troduced shortly) of the structure is axiomatizable by the set { on(a, b), on(c, d), on(e, table), on(b, table), on(d, table)} . The dashed part of figure 1 shows a substructure of T2 with the theory T1 axiomatizable by {on( a, b), on(b, table), on( e, table)}. Already, if one accepts that the dashed part is a sub-structure of the entire structure, from well-known preser­ vation theorems [Chang and Keisler 73] we can conclude the following: the universal sentence 'v'x-,on(x, a) holds in T2, so by the fact above, it also holds in T1 ; the (trivially) exis­ tential sentence on( a, b) holds in T1, so it also holds in T2. However, it will turn out that these conclusions from stan­ dard model theory are special cases of the main theorem of this section. This example is much simplified, for in practice we may need more predicates than shown, e.g., clear, block etc. By the CWA the negative ground literals are implied and not shown. As a result, the formula 'v' X -,on (X, a) holds in this structure. Observe that this is the intended meaning of the predicate clear( a) in practice, so clear(·) is eliminable in a language with the on(·,·) predicate.

2.3 What Is A Window?

We are now ready to formalize the informal notion of a 'window' for an action instance. Let the pre-condition of action A be ¢(X1 , ... ,Xn). If A applies in state U with substitutions a1 , ... , an for X1 , ... , Xn respectively, construct a sub-structure W of U by letting the do­ main of W be closure(U, {a1, ... , an}, P1, ... , Pk) where P1 , ... , Pk are the predicates that occur in ¢. In or­ der to emphasize the origins of W, it is convenient to also write it as window( ¢[a1 , ... , an], U) or alternatively by window(A[a1, ... ,an],U), being careful to remember that the domain of this structure includes constants beyond a1, ... , an by virtue of closure.

Example 1 Suppose the pre-condition of action move( A, B) in the blocks world is 'v'X-,on(X,A) /1. 'v'X-,on(X,B) /1. on(A, Y) /1. on(B, Z) and it is applied to the structure U in figure 1 with the substitutions A/ a, B / e, then the substruc­ ture W will have closure domain {a, e, b, table}, and rela­ tions restricted to these.

This example explains the motivation for the name window. In figure 1 the objects in the dashed line box constitute the domain of W. This window of the action move( a, e) en­ closes all the objects that could possibly be relevant in a test of the applicability of this action. The extent of the window is determined here by the fact that its pre-condition is a {a, e }­ formula, as specified in the definition below.

Definition 6 Given a set D of domain constants in £, the D­ formulas are (partly) grounded formulas in which each pred­ icate must have at least one argument that is from D.

It appears that most practical pre-conditions of actions have as instances D-formulas where D is the set of substituted con­ stants in the particular instance of the action. For example, in the instance of the action move( a, e), the pre-condition 'v'X-,on(X,a) /1. 'v'X-,on(X,e) /1. on(a,Y) /1. on(b,Z) is a {a, e }-formula. Note that this definition effectively enforces !-transitivity in P. A 2-transitive formula would have (for a binary P) a subformula instance of the form P(a, X) /1. P(X, Y)-or some such permutation thereof-where a is in D, and unless Y is instantiated to some bin D, this subfor­ mula violates the definition of a D formula since P(X, Y) does not have a D constant. However, if indeed Y is some such b, the subformula reads P(a, X) 1\ P(X, b) and is !­ transitive.

So, because of the above reasons, we shall assume the fol­ lowing:

Assumption 1 (D-formula Assumption) If ¢ is a pre­ condition of action A[a1, ... , an], then ¢[a1, ... , an] is a { a1, ... , an}-formula.

The formal reason for why windows work in practice is pro­ vided by the next theorem.

Theorem 1 (Pre-condition Conservative Extension) Let ¢[a1 , ... , an] be a pre-condition of an action instance to be applied to state U. If o: is any { a1, ... , an}-formula, then U f= o: iff window( ¢[a1, ... , an], U) f= o:.

Proof: We proceed by induction on the complexity of a. For atomic a it suffices to consider by example the case of P( a1, X) as more general cases follow the same pattern. U f= P(a1,X) iff U f= VXP(a1,X) iff for all b in the domain of U, U f= P(a1 , b) . By the con­ struction of window(¢[a1, ... ,an],U) and lemma 1 the last assertion is equivalent to window( ¢[a1, ... , an], U) f= P(a1 , X). The inductive steps in the proof of the equiv­ alence is straightforward for the 1\ connective. For the V connective the inductive proof has the same structure as the atomic case. Finally U f= -.o: iff U ~ o: iff (by the inductive hypothesis) window(¢[a1, . . . , an],U) ~ o: iff window( ¢[at, ... , an], U) f= -.a. D

In other words, the theory of U is a conservative ex­ tension [Chang and Keisler 73; Enderton 72] of that of window(¢[a1, . .. ,anJ,U) for {a1, . . . ,an}-formulas. This theorem is the essence of why the pictorial idea of a 'win­ dow' cut out of a picture of a state is intuitively appealing. We claim that it captures the notion of 'local ness' in such pic­ tures. The theorem states that an instantiated pre-condition is satisfied by the objects in the window if and only if it is satis­ fied by the entire picture.

3 State Change

Consider now figure 2 which intuitively represents the resul­ tant state of the move( a, e) action applied to the state in fig­ ure 1. Note that the window boundary is unchanged from figure 1. This is another characteristic of 'localness' that is captured. We now turn to a formal account of these obser­ vations based on the post-conditions of the action instance. Our first assumption is that all the objects and predicates of direct interest in the post-condition are already named in the pre-condition, i.e.,

Assumption 2

(Post-condition Assumption) If A[a1 , ... , an] is an action in­ stance with pre-condition¢[ a1 , ... , an]. then all constants of this instance in the post-condition are among the a1, ... , an. and all the predicates in the post-condition are among those of the pre-condition.

The next assumption is the interpretation of what it means to add and delete atoms in the corresponding lists. Lifs­ chitz [Lifschitz 86] proposes the very reasonable one that, for atomic add and delete lists, amounts to the:

Assumption 3 (Inertia Assumption) Let action instance A transform state (structure) U to state (structure) U1 . Then (i) u F= p implies ul F= p for any atom p not in the delete­ list of A- this is the idea of inertia or persistence by default; (ii) ifQ is an atom in the add-list, then ul F= Q.

In practice, the second condition seems to apply by default to atoms Q already known to be such that U f= -.Q. If the Inertia Assumption is understood to dominate pre-conditions to the extent that no atom that persists can be in the add-list (this is not required by the semantics of Lifschitz [Lifschitz 86]), and no atom that does not hold in u and ul is in the delete-list, then we have:

Assumption 4 (Strong Inertia Assumption) This is as in the Inertia Assumption, except that in (i) we add the qualifier, "and only for atoms P not in the delete-list", and in (ii) we strengthen the consequent to "U1 f= Q and U ~ Q ".

For strong inertia then, nothing is in the add- or delete-list un­ less it has changed signs in the course of the action. Strong in­ ertia was implicitly used by Reiter in [Reiter 91] in his formu­ las 'Y~ and 'Yp which combined explanation closure (due to Schubert) and result closure (due to Pednault) in his solution to the frame problem. It is tempting to think that this should be the natural default for designers of specifications. While inertia is a reasonable guide to the design of action specifica­ tions in practice, we shall see an example in section 4.2 that strong inertia does not appear to be the intended designer se­ mantics in some STRIPS specifications, i.e. that sometimes (weak) inertia has significance.

For non-atomic add- and delete-lists, we might as well go the whole hog and consider post-conditions which are formu­ las. Bearing in mind the cautionary statements from [Lifs­ chitz 86], it is prudent to consider only such formulas that are definite so that they in effect define a set of ground liter­ als, whose predicate names and constants are subject to the Post-condition Assumption above. Then we apply the Inertia Assumption as before.

The result is that the Post-condition Assumption coupled with these remarks implies:

Theorem 2 (Post-condition Conservative Extension) If ¢1 and 'ljJ are the pre- and post-conditions of action instance A respectively, then with the notation above (i) subject to the Post-condition Assumption the domain of window( 1/J, U1) is a subset of the domain ofwindow(¢[al, .. . ,an],U); (ii) in addition, if subject to the Inertia Assumption, the Pre­ condition Conservative Extension theorem also holds for window('lj;,UI) with respect to U1 .

Assertion (i) is trivial. Assertion (ii) follows from the Iner­ tia Assumption and reasoning similar to the Pre-condition Conservative Extension theorem. Together, the two theo­ rems confirm that the window construction captures the in­ tuitive notion of 'localness'. The 'genericity' of actions is captured by the following observation (see [Enderton 72; Chang and Keisler 73] for the definition of isomorphism be­ tween structures) and the fact that isomorphic structures are elementarily equivalent (see definition 4).

Observation 1 (Isomorphism of Windows ) Any two in­ stances of an applicable action has isomorphic pre-condition, and correspondingly isomorphic post-condition, windows.

4 Action Invariants

Zhang and Foo [Zhang and Foo 96] have used persis­ tence to derive action invariants from definite pre- and post­ conditions. Since the Inertia Assumption is accepted in our formalization, one should expect that a similar derivation is possible here. If so, it would give a formal account of how STRIPS rule designers, ·for reasons of implementation effi­ ciency, avoid having to specify the impossible predicates as action guards by clever selection of add- and delete-lists.

Definition 7 An invariant of an action A is a formula f3 s. t. , for all instances of A, if /3 holds in the state (structure) before A is applied, f3 will hold in the resulting state (structure).

In the context of several actions (not merely different in­ stances) constraints are simply the set of invariants common to all of them. So, it suffices to search for candidate invari­ ants for each action in order to discover system constraints. In practice, designers of action specifications know many con­ straints, but they may not be aware;; of others that are implicit in the action specifications. Conversely, known constraints can be used to specify conditions for actions. In this section we indicate how invariants depend on action specifications.

The notions of pre- and post-condition windows introduced in the earlier sections provide the justification for localized reasoning about action invariants. While this section reports preliminary work toward the elimination of the impossible rules, the ideas proposed are prompted by the preceding for­ mal development. We are currently investigating systematic algorithms to fulfill this work.

4.1 Ontological Primacy of Atoms

In many knowledge representation systems there is an im­ plicit priority given to those facts of the world that can be expressed positively as ground atoms. This is a linguistic convention seldom breached, and no doubt there are strong psychological and cognitive reasons for it. Not being experts in these disciplines, we adduce evidence for what might be called a principle of the ontological primacy of atoms by re­ counting some facts that are widely known in our AI and KR community. First, databases (both deductive and otherwise) record atoms as the primary data. So do pure logic programs. Herbrand models are standard in KR semantics, and many of the characterization theorems of non-monotonic reasoning systems are expressed in terms of properties of such models. The bias toward positivity appears to be widespread even in formal approaches.

We therefore advance the following hypothesis, and then formalize it in the next definition.

Assumption 5 (Positive Literal Bias) In an action specifica­ tion the add-list of atoms are determinants of the delete-list of atoms in the presence of constraints.

Definition 8 Let C be a set of formulas that express the con­ straints of the system. A set r of atoms determines another set A if C u r f= A.

The Positive Literal Bias hypothesis then translates to this formal proposal. Let A be an action that is applied to state U with resultant state ul' and with add-list r of atoms, delete­ list A of atoms. Let C be (possibly unknown) system con­ straints. Then C U r f= .., V A, which is equivalent to C f= 1\ r :::> .., V A. The notation V A means the disjunction of the atoms in the set A. This means that 1\ r :::> .., VA is a candidate invariant for the action A if its constants are gener­ alized. This generalization is possible because of observation 1 on isomorphisms of windows.

Our proposal is in the spirit of Explanation Closure at­ tributed to Schubert [Reiter 91]. Indeed the assertion Cur f= .., V A has the structure of an abduction of the negative literals in terms of the positive ones with respect to C.

4.2 Generating Candidate Invariants

Let us now apply the above proposal to a few examples. Sev­ eral caveats will be revealed in the process, which is to be thought of as a procedure for generating plausible guesses at invariants which will be correct if the Positive Literal Bias hypothesis holds along with some weak requirements.

For the move( a, e) action, the add-list is on( a, e) and the delete-list is on( a, b) , so by the proposal we have the candi­ date invariant on( a, e) :::> -,on( a, b), which generalizes (us­ ing unique names) to (X '/= Y) :::> (on(A, X) :::> -,on( A, Y)) which is just a fancy way of saying that no block is in different places, i.e., the Pro log rule: impossible:- on( A, X), on( A, Y), X =J Y used as a guard for checking the move action. However, the generalization implies that every block has been moved before, since the generalization relies on an isomorphism of result windows and these are the effects of the action. This motivates the following definition.

Definition 9 A ground atom P is actualised by an action A if it was false in some initial window satisfying the pre­ condition of A but true in the resulting window.

By earlier remarks, we cari replace 'window' by 'state', and equivalently say P satisfies the post-condition of A. Then the proposed candidate invariant is plausible for every A­ actualised atom. The soundness of the proposed invariant is not in question for the following reasons. Let P1 , ... , Pn be the add-list of an instance of action A, and Ql, ... , Qm be the delete-list. Then in the resultant state it is the case that /\:~~Pi 1\ /\:~';' -,Qi and this implies the candidate invari­ ant in our proposal, which is /\!~~Pi :J /\!~';' -,Qi. In fact, if we assume strong inertia as in assumption 4, then all of P1 , .. . , Pn would have been false in the initial state, so the conjunctive formula/\!~~ Pi 1\ /\:~';' -,Qi is false in it, and cannot be an invariant, while the weaker formula in question holds in it. To confirm that this is actually an invariant in our formalization an induction is necessary, but in [Zhang and Foo 96] a persistence logic has been used to verify it.

One final remark: the clear predicate used in some imple­ mentations has not been used in the blocks-world example here as it is eliminable. For technical reasons our proposal requires non-eliminable predicates.

4.3 Weak Inertia

In this rather preliminary subsection we show an exam­ ple where strong inertia is not the intended semantics of a STRIPS specification.

Example 2 Consider a duopoly law for the ownership of a television station. Current owners may sell to others, but at all times there must be two owners. Here is the STRIPS specification for the action buy( A, E) meaning informally that owner A is selling his share of the station to E.

action: buy(A,E)

pre-condition: own(B,T), own(E,T), A f E post-condition: add-list: own( A, T)

delete-list: own( E, T)

Please note the formal similarity of this situation with that of move( a, e) that we discussed earlier. In any instance of buy( a, e), the window of the action will contain in addition to own( a, t) an instance own(b, t) which will persist through the action but is not in the add-list. However, the candi­ date invariant using strong inertia is formally similar to that of the move action in the blocks world, viz., (A f B) :J (own( A, T) :J -,own(B, T)) which is too weak to prevent a monopoly.

Consider now how weak inertia may be used here. If we change the add-list to own(A, T), own(B, T), a candidate in­ variantisown(A,T)/\own(B,T)A(E f AI\E f BI\A f B) :J -,own(E, T) which is intuitively what the specifier in­ tended under the unique names assumption. Evidently, weak inertia has different designer semantics.

5 Conclusion

We have provided a formalizations of the ideas of 'localness', 'genericity', and 'implicit constraints' in ~TRIPS-like spec­ ifications of actions. The first two are very faithful to the intuitions of designers, but the third is not quite settled as it appears that two different kinds of inertia are assumed. The first two formalizations have potential uses in diagrammatic reasoning, while the third suggests opportunities for identi­ fying the psychology of action specifications with appropri­ ate model classes for which inductive proofs of candidate in­ variants can be avoided. There is an increasing interest in diagrammatic reasoning [Barwise 95] in AI and we shall be extending the window semantics in this direction. We are cur­ rently pursuing the identification of dynamic system classes in the spirit of Sandewall [Sandewall 94] to see how invari­ ants can be extracted completely from specifications without induction. There appear to be at least three notions of com­ pleteness for invariants that can be formalised.