Formal Theories of Action (Preliminary Report)

1. Introduction

We consider the problem of formalizing reasoning about action in the framework of the situation calculus of McCarthy and Hayes (1969). A situation is the complete state of the universe at an instant of time. A fluent is a function defined on situations. For instance, in the blocks world, the location of a given block x is a fluent whose values are the possible locations of blocks. In the language of the situation calculus, the value of this fluent at s for a block x is denoted by location(x,s). If sis a situation and a an action then result( a, s) stands for the situation that results when the action a is carried out starting in the situation s.

We are primarily interested · in the form of reason­ ing which Hanks and McDermott (1986) call "temporal projection": given some description of the current situ­ ation, some description of the effects of possib_le actions, and a sequence of actions to be performed, predict the properties of the world in the resulting situation.

A number of difficulties arise in attempts to describe the effects of actions in the situation calculus and in sim­ ilar formalisms. One of them, known as the qualification p:roblem, is related to the fact that the successful per­ formance of an action may depend on a large number of qualifications. As a consequence, the axiom describing the effect of such an action has to include a long list of assumptions. It is desirable to treat each qualification as a separate fact and describe it by a separate axiom.

This research was partially supported by DARPA under Contract N0039-82-C-0250.

FORMAL THEORIES OF ACTION (PRELIMINARY REPORT)

Vladimir Lifschitz

Computer Science Department Stanford University Stanford, CA 94305, USA

Another difficulty is that, in addition to the axioms describing how the properties of the current situation change when an action is performed, we need a large num­ ber of axioms listing the properties which are not affected by a given action. This is called the frame problem. For instance, when a robot is moving a block, appropriate "frame axioms" must guarantee that all the properties of the situation which are not related to the positions of _the robot and the block (for instance, the positions of all other objects) remain the same.

John McCarthy proposed approaching the qualifica­ tion problem and the frame problem using circumscrip­ tion (McCarthy 1980, 1986). We assume that the reader has some familiarity with this concept; for the definition, see (McCarthy 1986). With regard to the qualification problem, the idea is, instead of listing all the qualifica­ tions in the antecedent of one axiom, to condition the axiom on the fact that (a certain aspect of) the action is not "abnormal" in the situation in which the action is performed. For each qualifying condition, a separate axiom postulates that the condition implies the abnor·· mality of this aspect of the action. Circumscribing ab­ normality should ensure that the action has its expected effect whenever we are not in any of those exceptional sit­ uations which, according to the axioms, make the action abnormal.

For the frame problem, similarly, McCarthy proposes an axiom which guarantees that the location of x in the situation result( a, s) is the same as its location in the situations unless a certain aspect of a is abnormal. Then· circumscribing abnormality should allow us to prove that x does not change its position if the action consists of moving a block other than x, or in painting a block, etc., so that all "frame axioms" should become provable.

Further analysis has shown, however, that the result of minimizing abnormality relative to McCarthy's axiom set is not quite as strong as necessary for the successful formalization of the blocks world. The difficulty can be illustrated by the following example (McCarthy 1986). Consider the situations

S1 = 7'esult(move(A, top B), SO)

where SO is a situation with exactly blocks A and B on the table. We expect circumscription to guarantee that_ ~ the first action, move( A, top B), is "normal", so that A is on top of B in situation Sl. In view of that, the second action is "abnormal" (so that the positions of the blocks in situation S2 will be impossible to predict lm the ba­ sis of McCarthy's axioms). However, if the first move is "abnormal" (for some unspecified reason), the positions of the blocks after the first action may remain unchanged, so that the second move may succeed after all. This ob­ servation shows that the intended model of McCarthy's axioms is not the only one in which the set of abnormal objects is minimal. In the intended model, the first ac­ tion is normal, and the second is not; in the other model, it is the other way around. Using circumscription, we can only prove the common properties of all minimal models; minimizing abnormality will only give a disjunction.

Another example of such an "overweak disjunction", for an even simpler system of actions, is discussed in (Hanks and McDermott 1986). There are three possi­ ble actions: load (a gun), wait, and shoot (an individual, whose name, according to some accounts, is Fred). Nor­ mally, waiting does not cause any changes in the world, but shooting leads to Fred's death, provided, of course, that the gun is loaded. Assume that all three actions are performed, in the given order. An axiom set simi­ lar to McCarthy's axioms for the blocks world is shown to have an unintended minimal model, in which the gun mysteriously gets unloaded on the waiting stage, so th~t the shooting does not kill Fred. In the intended model, wait does not change the world, but shoot does; in the unintended model, it is the other way around. In either case, abnormality is minimal. Here again, the result of circumscription is too weak.

It is easy to notice that, in both exam~hj!s, there is a

conflict between minimizing abnormality at two instants of time. In the intended model, minimization at the ear­ lier instant is preferred. But circumscription knows noth­ ing about time; it interprets minimality of a predicate as the minimality of its extension relative to set inclu­ sion. This, according to Hanks . and McDermott, is the reason why circumscription does not live up to our ex­ pectations in application to temporal reasoning: " ... the class of models we want our logic to select is not the "minimal models" in the set-inclusion sense of circum­ scription, but the "chronologically minimal" (a term due to Yoav Shoham): those in which normality assumptions are made in chronological order, from earliest to latest, or, equivalently, those in which abnormality occurs as late The paper by Hanks and McDermott was presented at the AAAI conference in 1986, and three more talks given at the same conference, (Kautz 1986), (Lifschitz 1986) and (Shoham 1986), met their challenge by formal­ izing, in somewhat different contexts, the idea of chrono­ logical minimization. As could be expected, all of them had to use forms of logical minimization more general than circumscription in the sense of (McCarthy 1986).

In this paper we argue that formalizing chronological minimization is not the easiest way to solve the tempo­ ral projection problem. We start with another view on the difference between the intended and the unintended models of the axioms for actions: in the intended model, all changes in the values of fluents are caused by actions, whereas in other models this is not the case. To express this distinction formally, we add new primitive predicates to the language. · With this different choice of primitive concepts, the effects of actions can be charaCterized by simple axioms in the language of the situation calculus plus traditional circumscription. The axiomatic treat­ ment of causality is the main distinctive feature of our approach.**

The method is illustrated by formalizing two exam­ ples: the shooting problem and the blocks world. The formalizations are reasonably complete, in the sense that they allow us to predict the effect of the execution of any sequence of actions. They are also computationally tractable, in the sense that, in. both cases, the result of circumscription can be determined by simple syntactic methods (such as predicate completion). Proofs of these facts will be given in the full version of the paper (Lifs­ chitz 1987).

2. The Yale Shooting Problem

To formalize the shooting story from the Hanks­ McDermott paper, we use object variables of four sorts: for truth values (v), for actions (a), for situations (s), and for truth-valued fluents (f). The object constants are: truth values false and true, actions load, wait and shoot, situation SO and fluents loaded and alive. The bi­ nary situation-valued function result must have an action term and a situation term as arguments. Finally, there are three predicate constants: holds(!, s) expresses that f is true in the situation s; causes( a, J, v) expresses that a causes the fluent f to take on the value v; precond(f, a) expresses that f is a precondition for the successful exe­ cution of a.·

· An early attempt to describe causation by axioms was made by Patrick Hayes (1971); see also (McDermott 1982).

** A similar solution was independently found by Brian Haugh (1987).

Our axioms for the shooting problem can be clas­ sified into three groups. The first group describes the initial situation:

Th~ second group tells us how the fluents are affected by act10ns:

These axioms describe the effects of successfully per­ formed actions; they do not say when an action can be successful. This information is supplied separately:

The last group consists of two axioms of a more general nature. We use the abbreviations:

One axiom describes how the value of a fluent changes after an action affecting this fluent is carried out:

(Recall that v can take on two values here, true and false; the equivalence in the consequent of Y3.1 reduces to holds(!, result( a, s)) in the first case and to the nega­ tion of this formula in the second.) If the fluent is not affected then its value remains the same:

· Notice that, syntactically, the variables for actions are obje~t variables, not function variables, even though each act10n a has a function associated with it: the sit­ uational fluent s - result( a, s ). Similarly, the variables ~or truth-valued fluents are object variables, not pred­ Icate variables. The value of f at s is represented by holds(!, s ).

This axiom set obviously does not include a number of assumptions that may be essentiaL The axioms do not tell us, for instance, whether fal se and true are different from each other and whether there are any truth values other than these two; we do not know whether load, shoot and wait are three different actions, etc. In this prelimi­ nary discussion, instead of making all these assumptions explicit, vye limit our attention to the term models of the axioms, in which every element of the universe is repre­ sented by a ground term of the language, and different terms represent different objects. (Such models are also called Her brand models in case of universal theories). We will identifyJthe universe of a term model with the set of ground terms.

It remains to specify how circumscription is used. We circumscribe causes and precond, with the remaining predicate holds allowed to vary, relative to the conjunc­ tion Y of the axioms Yl.l- Y3.2. This will lead us to the conclusion that causes and precond are true only when thi6 is required by the axioms of the second group, Y2. The minimization of causes will imply, in view of axiom Y3.2, that the only changes taking place in the world are those corresponding to axioms Y2.1-Y2.3. This solves the frame problem. The minimization of precond, in view of the definition of success, will imply that the only un­ successful actions are those in which precondition Y2.4 is violated. This solves the qualification problem.

The main technical difference between this formula­ tion and other attempts to apply circumscription to the situation calculus is that the predicates which we circum­ scribe, causes and precond, are not fluents, they do not , have situation arguments. The predicate success, which does have a situation argument, is defined in terms of the minimized primitive precond. Since the.minimized pred­ icates have no situation arguments, the conflict between minimizing in earlier and later instants of time simply cannot arise.

It is n6t difficult to prove that this circumscription Y has. a unique term model Mo . In this sense, it completely determines whether any given sentence is .true or false. In particular, the formula

holds( alive,

result( shoot, result( wait , result( load, SO))))

is false in Mo. The predicates causes and precond can be described in Mo by explicit definitions:

The definitions can be obtained by applying the predicate completion procedure to axioms Y2. They can be also characterized as the result of circumscribing the predicates causes and precond relative to Y2. These predicates occur both in Y2 and in Y3, but we see that axioms Y3 can be ignored when the result of circumscrip­ tion is determined.

The interpretation of holds in M0 can be viewed as the description of the work of a deterministic finite au­ tomaton A with 4 internal states, corresponding to all possible combinations of values of the fluents loaded and alive. The initial state of A is (false, true). Its input symbols are load, wait, shoot. Strings of input symbols are "plans", and the goal condition of a planning prob­ lem would define a set of final states. For example, the goal ...,alive corresponds to selecting (Jalse,false) and (true, false) as the final states, and the plan load, wait, shoot is accept~d by A with this set of final states. Each state of A corresponds to a set of situations which are in­ distinguishable in terms of the fluents loaded and alive.

3. An Alternative Formulation

The formalization of the Yale shooting problem pro­ posed above has two defects. First, we were only able to show that actions lead to the expected results in term models of the circumscription, not in arbitrary models. Second, we exploited some special features of the prob­ lem that are not present in more complex problems of this kind. Now we will consider an improved, though some­ what less economical, formalization of the shooting story. Here are the main differences between the two versions.

1. Since it is essential in the first solution that, in a term model, different ground terms have different values, we will need some uniqueness of names axioms, expressing this property. The following notation will be useful: if c1 , ... , Cn are constants of the same sort then U[c1, ... , cn) stands for the set of axioms c; =/= Cj (1 ~ i < j ~ n). For instance, U[l.oad, wait, shoot) is

load=/= wait, load=/= shoot, wait=/= shoot.

1. It is also essential in the first solution that every situation in the term model is the result of executing a sequence of actions in SO. · We see several ways to deal with this problem, all of them, admittedly, somewhat un­ intuitive. In the new solution we choose to restrict axioms .. Y3 to a subclass of relevant situations; we will postulate

· This fact allows us to define the interpretation of holds in Mo by recursion on the second argument.

that SO is relevant and that the result of executing an action in a relevant situation is relevant also.

1. The only precondition in the Yale shooting prob­ lem (given by axiom Y2.4) is extremely simple: loaded is one of the "coordinate fluents" defining the state of the corresponding automaton (see the end of Section 2). Even in the blocks world, we need preconditions of a more complex nature, such as clear 1 and clear top b for the ac­ tion move(b, 1), where clear is explicitly defined in terms of primitive fluents. Accordingly, in the second solution we explicitly distinguish between fluents in the general sense and primitive fluents. Only a primitive fluent can occur as the second argument of causes, but precondi­ tions do not have to be primitive.
2. The value which a causes f to take on may de­ pend on the situation in which a is executed. For in­ stance, toggling a switch may cause its status to change in two different ways, depending on its current status. · Accordingly, we will allow a truth-valued fluent (not nec­ essarily primitive), rather than a truth value, to be the last argument of causes; the value of that fluent in the situation s is the value that f will take on in the situa­ tion result( a, s ), provided a is successful. The effect of toggling a switch can be described then by an axiom such as

causes( toggle, on, not on)

(not is the function which transforms a fluent into its negation) .

In the new formalization of the Yale shooting we have an additional sort of variables, primitive fluents. On the other hand, we do not need variables for truth values any more. Thus the language has variables for actions (a), for situations (s), for truth-valued fluents (f), and for primi­ tive truth-valued fluents (p). This last sort is considered a subtype of fluents , so that a term representing a primitive fluent can be used wherever the syntax requires a fluent. (Accordingly, in a structure for the language the domain of primitive fluents must be a subset of the domain of fluents ).

The object constants are the same as in the language of Section 2. As before, load, wait and shoot are action constants and SO a situation constant; loaded and alive are . primitive fluents and false and true are fluents (in­ tuitively, the identically false fluent and the identically true fluent). The only function constant, result, and the predicate constants holds and precond are used as in the first formulation. The arguments of causes must be an action, a primitive fluent and a fluent. In addition, we need the unary predicate relevant, whose argument must be a situation term.

· This problem was pointed out by Michael Georgeff.

The axioms of the first two groups, Yl and Y2 (Section 2) are included in the new formulation with­ out change. (It is easy to see that all of them are well­ formed formulas of the new language). The definitions of success and affects remain the same, except that vari­ ables of different sorts are required now in the definition of affects:

The counterpart of Y3.1 is the following Law of Cbange:

Y3.2 becomes the Commonsense Law of Inertia:

In addition, we need a few axioms which have no counterparts in the first version. Let Act be the list of actions load, wait, shoot, and let Fl be the list of ftuents

We need the following uniqueness of names axioms:

Axiom U3 represents the assumption that a situa­ tion includes a complete description of its history, i.e., uniquely defines what action has led to it and in what situation the action was performed.

We also need to assume that the non-primitive ftuent constants

denote objects which do not belong to the subdomain of primitive ftuents. If this list is denoted by N P F then this assumption can be expressed by

The next group of axioms consists of the fluent def­ initions for the non-primitive ftuents:

Finally, there are 3 axioms for the new predicate relevant:

Axioms Rl, R2 imply

relevant s

for any situation term s without variables. Axiom R3 guarantees, in the presence of Rl and R2, that a sequence of actions cannot possibly lead from SO back to SO (i.e., SO is not "in the future" of SO).

By Y' we denote the conjunction of the axioms Yl, Y2, LC, LI, U, FD, R. The predicates causes and precond are circumscribed now relative to Y', with the remaining predicates holds and relevant allowed to vary. This circumscription has many non-isomorphic models. But in all of them the predicates causes and precond satisfy the following conditions (essentially identical to their definitions in the model Mo of Y):

Moreover, every ground atom is either true in all .models of this circumscription, or false in all of them. Thus our "circumscriptive theory" is sufficiently strong to decide any sentence without variables.

4. The Blocks World

Now we are ready to consider a slightly larger exam­ ple: a blocks world in which blocks can be moved and painted, as in (McCarthy 1986). Even though the object domain is now entirely different, the primitive concepts result, holds, causes and precond will be used again, and some axioms (notably, the law of change and the law of inertia) will be included in the axiom set for the blocks world in exactly the same form. These axioms represent the general properties of actions which are likely to be useful for constructing axiomatic descriptions of many different object domainf\o

As before, we have variables for actions (a), for sit­ uations ( s ), for truth-valued ftuents (f), and for prim-· itive truth-valued ftuents (p ), the last sort being again a subtype of ftuents. In addition, there are 3 "domain­ specific" sorts: blocks (b), locations (I) and colors (c).

Object constants: So, true, false, blocks Block1, .. . , BlockN (where N is a fixed positive integer), location Table, and, finally, colors Red, White and Blue. Here is the list of function constants, along with the sorts of their arguments and values:

The predicate constants are the same as in Section 3: holds, causes, precond and relevant.

The first group of axioms contains som<l general facts about blocks, their locations and colors:

Initially, all blocks are white and on the table:

The effects of actions:

(It is impossible to move a block onto its own top). Ax­ ioms B2.2 and B2.4 may seem redundant: we already know from axioms B0.2 and B0.3 that a block cannot possibly be at two places or have two colors simultane­ ously. But our method requires that all changes of all primitive fluents caused by an action be described explic­ itly. It does not solve the "ramification problem" in the sense of (Finger 1986) and (Ginsberg and Smith 1986).·

· I am indebted to Matthew Ginsberg for this impor­ tant observation.

The laws of change and inertia LC and LI are for­ mulated as in Y' above. To state the counterparts of the uniqueness of names 11-Xioms from Y', we define Act and Fl for the blocks world .language as follows:

Now the list Act consists of the symbols for functions returning actions, not of object constants, as in Y'. Fl contains both object constants and function constants. We will extend the definition of U[ . . . ] to the case when some or all of its arguments are functions. We can treat constants as 0-ary functions and thus define the meaning of U[b, .. . ,f,.], where b, ... , f,. are functions returning values of the same sort. By definition, this stands for the following set of axioms:

for all i < j, and

for all f; of arity k > 0, where x 1 , · · · , y1 , · ·. are variables of appropriate sorts. These axioms express that b, ... , f,. are injections with disjoint ranges. If each f; is an object constant then we get the special case defined in Section 3 above. Example: Axiom U3 can be written in this notation as U[result] .

N P F is defined as the list of terms

Now axioms U1-U4 are expressed exactly as in Section 3. In addition, we have 3 domain-specific uniqueness ax­ ioms:

The fluent definitions include, in addition to F D.true and FD.false, the definition of clear:

Finally, the axioms R are formulated as in Y'.

By B we denote the conjunction of all these ax­ ioms. As before, we circumscribe causes and precond, with holds and relevant allowed to vary. It turns out that in each model of this circumscription the minimized predicates satisfy the formulas obtained by "completing" axioms B2: causes( a, p, f) is equivalent to

Every ground atom is either true in all models of this circumscription, or false in all of them, so that this "cir­ cumscriptive theory", like the theory from Section 3, is complete on the level of atomic formulas.

Acknowledgements

This paper is an outgrowth of ideas developed by John McCarthy in his research on commonsense and non­ monotonic reasoning, and I am grateful for the opportu­ nity to discuss my work with him. I have also bene­ fitted from discussions with David Etherington, Michael Gelfond, Michael Georgeff, Matthew Ginsberg, Robert Givan, Brian Haugh, Patrick Hayes, Robert Kowalski, Drew McDermott, Nils Nilsson, Donald Perlis, Raymond Reiter and Yoav Shoham.