A Formal Model for Classical Planning

1 Introduction

In this paper we investigate a formal model for a broad class of A.l. planning systems. We define the range of applicability of our model later; here, we simply note that it is relevant to such well-known "classical" planners as STRIPS [Fikes and Nilsson, 1971], NOAH [Sacerdoti, 1977], NONLIN [Tate, 1977], TWEAK [Chapman, 19~7] and SIPE [Wilkins, 1988] . Each of these planners has 1ts own very distinctive features. But there are also many similarities, and we can define a useful formal model of the concept of "plan" used by all of them.

The model can be used to provide semantics for much of the planning process. That is, we can develop a logic which is interpreted as making assertions about plans. Relative to the model and the logic, claims about par­ ticular plans or planning systems can be proven true or false. Section 3 gives a concrete application of this: we develop a truth criterion for a broad class of planning systems. The concept of a truth criterion (TC) is due to Chapman [Chapman, 1987] . In fact, many of the ideas in this paper were inspired by Chapman'~ work _and so we spend the rest of this introduction contrastmg the goals of his work and ours.

In general, a planner's truth criterion is the test it uses to check whether a particular proposition holds at some point in a proposed plan. It is easy to see h~w impor­ tant this test is. For example, we are always mterested

·The first author was partially supported by NASA Grant NCC2-494 and by Texas Instruments Contract No. 7554900. The second author is supported by an IBM Grad­ uate Fellowship.

tPresent address: Teknekron, 530 Lytton Ave, Palo Alto, CA 94301.

Adam Grove

Computer Science Department Stanford University Stanford, CA 94305 grove@cs.stanford.edu

in whether the goal propositions will be true after execu­ tion of a proposed plan. A truth criterion tells the plan­ ner when to stop planning for the current goal. Aside from computational efficiency, there are three desirable properties a truth criterion can have. First, it should be correct: when it tells us that a goal is achieved, we can safely stop planning (for this goal). Second, a TC can be sufficient: if the goal is achieved, it will tell us. Sufficiency makes planning faster, because we can avoid unnecessary work. Finally, and somewhat more vaguely, a truth criterion may be informative. By this we mean that, when a proposition fails to hold, the TC gives us information about why it does not and we can use this to guide further planning steps.

Chapman presented a model for one particular plan­ ning system (his "TWEAK" formalism). Using this model, assertions about plans such as "proposition p nec­ essarily holds after execution of action a" are given a precise meaning. Chapman gave an interesting test for the necessary truth of a proposition which is, relative to his model, provably correct and sufficient. Further­ more, this TC is informative; it is possible to "read off" all the useful modifications we might make to a plan to ensure the proposition's truth. Given any reasonable search strategy that explores the suggested possibilities, the resulting planner will be correct and complete. 1

We also give a precise semantic model for planning, in Section 2. However, whereas Chapman discusses just one, quite restrictive, planning system, we discuss a gen­ eral theory for all "classical" planners. This reflects our goal to develop a theory that is useful for comparing many different planners. In contrast, Chapman 1s able to develop a new, straightforward, and provably correct planner by taking advantage offeatures particular to the system he studies.

We discuss a logic for describing and reasoning about our models. The idea of using a logic was implicit in Chapman's work, but never developed; for although he attempts to give a version of his TC in "logical nota­ tion", the formula presented contains minor errors and so does not quite correspond to his criterion. This has no effect on his results, because the real criterion, its proof.

1 That is it always finds a working plan if this is possi­ ble, and ne~er terminates with a plan that doesn't satisfy all goals.

and all discussion of its application, are in English. But in general , a well-defined formal language is useful be­ cause it can prevent ambiguity. Furthermore, we can use a formal logic to give syntactic proofs of assertions about the planner (such as the correctness of a proposed truth criterion). Theorem proving is much easier to au­ tomate than subtle semantic arguments like those used by Chapman.

2 The Model and Logic

Our model applies to planning systems that depend on a single-agent and situation-based world model and work by refining nonlinear plans. Before presenting the model itself, we look at these issues.

Plans are constructed for agents that operate in some well-defined environment. We only consider planners whose world model is like the situation calculus ([Mc­ Carthy, 1968]) . More precisely, we suppose that a par­ ticular state of the world is described by a set of objects, often called propositions, which throughout we consider to come from some fixed set P. 2 We say that a propo­ sition holds at, or is true in, a state if it is a member of that state. We assume that basic operations in the world, the actions, are functions mapping one state to another resulting state (i.e., they are functions from sub­ sets of P to subsets of P). Of the class of all possible actions, A, the agent we are planning for can presumably execute some known subset, say n. If the agent executes a sequence of actions starting in state I, the final state must be what results from applying the composition of the actions to I.

The purpose of a planner is to find a sequence of ac­ tions in n which ensures that, when the world contains a given collection of initial propositions, then after ex­ ecution it is certain that all of some given collection of goal propositions holds. We will call any sequence of actions, together with the set I, a complete plan. We are interested in planners that proceed by considering sets of complete plans, and slowly narrow the size of the sets until all the complete plans that remain guarantee the goals (i.e., this is the least-commitment approach to planning) . Because it is never practical to manipulate arbitrary sets of plans, a planner always uses some com­ pact representation system, which we will call the plan representation language, to describe such sets. Here, we make the assumption that the planners use a language which describes nonlinear plans. A nonlinear plan is given by:

• I ~ P, which is the initial state.
• A fixed, finite collection P of plan steps A1, ... , An. Each plan step is associated with a collection of ac­ tions inn (an action-set). Where there can be no confusion, we will blur the distinction between a plan step and its associated action-set.
• A partial order on plan steps, -< .

2 Propositions are often thought of as being formulas in some formal logic. However, it is not always possible or useful to take this view.

• A set of constraints on the n plan steps. The con­ straints specify which combinations of actions in A1 x A2 x . .. x An are actually permitted.

It is easy to see how a nonlinear plan describes a set of complete plans: it stands for all such plans obtainable by extending -< into a total order on the A;, and then choosing (subject to the constraints) one action from each A;. The term "nonlinear" is used because we need only give a partial order on the plan steps.

Virtually all the planners mentioned in Section 1 ma­ nipulate some form of nonlinear plan. 3 Within the framework described so far (which has just concerned itself with representations) planners differ in three main ways. First, many planners only allow certain special types of actions to occur in n. A very common restric­ tion on n is what we call the STRlPS assumption ([Fikes and Nilsson, 1971]). Under this assumption, an action a E n must have a very simple structure: in any situ­ ation, a has the effect of first removing some fixed set of propositions (traditionally called the delete list) then adding all of some other fixed set (the add list) . Sec­ ond, plan representation languages differ in how they describe the action-sets associated with a plan step in a partial plan. One common technique, used in Chap­ man's system among others, allows action "schemas" such as Puton(x,y) which stand for all actions obtained instantiating the variables x, y; we discuss such systems in somewhat more detail later. Finally, planners can differ significantly in their constraint schemes (for ex­ ample, Chapman uses a simple language that constrains the values his variables can be instantiated to) . Note that the constraint language and the action-set repre­ sentation language are interrelated.

In our model, these differences are represented within a uniform framework. We first define a partial plan, which is a tuple (I, P, -<) (where each component is as described above) . The structure of partial plans can be viewed as a plan representation language, but it is very weak because we make no provision for constraints. Our model is based on the observation that a nonlinear plan in a general language, possibly with constraints, can be described using a collection of partial plans.

3 Some of these planners, such as NOAH, NONLIN, and SIPE, also make use of a hierarchical structure on actions. That is, there is a concept of "high level" actions and/or propositions, which can be expanded into a more detailed and more complex objects at a lower abstraction level. Our model does not capture this aspect of a plan representation system. This does not invalidate its usefulness however, be­ cause, as Wilkins [Wilkins, 1988] points out, all hierarchical planners operate on a series of planning levels, where on any one level the degree of abstraction never changes. Within one level our model is usually applicable. Nevertheless, giving a deeper theory for these concepts would probably be the most interesting extension to the model we are proposing here.

4 In addition, we sometimes specify a set of preconditions, which are propositions that must be true before an action is regarded as being truly executable. Consideration~ of exe­ cutability are ignored in the model we present (and, m effect , this is also true for Chapman's model) . During planning, pre­ conditions become (sub-)goals that must be achieved, and so typically only influence the goal selection component of the planner.

Definition: A plan-structure is a finite tree, where the nodes are partial plans. If n; =(I;, P;, ~;) is an an­ cestor of, or equal to, n; = (I;, P;, ~i ), then we write n; - n; and say that n; is a specialization of n; . When­ ver this is the case, we insist that ~i ~ ~i, I; ~ I;, and P; = P; . However, although P; = P;, we do not as­ sume that the action-sets associated with a particular plan step A; are identical in the two partial plans, but we do require that the action-set for A; in n; is a super­ set of the corresponding action-set in n;, for all i. From this condition it follows that complete plans (i.e., partial plans that represent a single complete plan) must be leaf nodes in the tree. Conversely, we also require that every leaf must be complete.

From any n; there are a large number of potential specializations (formed by constraining the partial order in some way, and restricting the action-sets associated with some of the plan steps). However, not all these possibilities can be considered by the planner. This is because the planner has a limited language for describ­ ing action-sets, so that not all possible subsets of n can be captured, and also because of constraints. This is perhaps the key point: the main differences between dif­ ferent planners' representations system can be captured by differences in how the specialization relation works.

We can define a formal language, which makes asser­ tions about plan-structures. Because the model is so general, the language covers many planning systems. To shorten the presentation, we introduce our language in­ formally. The key features are:

• The language is a based on a sorted first-order logic, with the usual connectives, and quantification for the two sorts plan-steps and propositions. At any node in the model, the domain of plan-steps is, of course, just the plan-steps at the node, and the do­ main of the sort propositions is P. 5
• The language has two primitive modal operators, Ds and D. At a node in a plan, Ds¢J is true just if ¢J is true in all nodes which are specializations of the first, and O¢J is true if ¢J holds in all specializations which are complete plans. We read D¢J as "¢J is nec­ essarily true". The "necessary" modality is the key to our logic; a necessary property of a nonlinear plan is true of all the complete plans it describes. The truth criterion we give later is of interest because it shows that, sometimes, we can discover whether a formula is necessarily true without considering all these complete plans individually.

We sometimes use the duals of 0 and Ds, written <> and <>s, which are defined in the usual way as <> = ...,o..., and <>s = ...,os..., respectively.

• There is a binary predicate ~ between plan steps. At n, a~b if in fact the plan step (denoted by) a

5 Note tha.t these doma.ins a.re independent of the node in a. pla.n-structure. In a. presentation of the formal proper­ ties of the logic (for which we ha.ve insufficient spa.ce here) this observation has some importa.nt consequences (such as the truth of the "Ba.rca.n" a.xiom; see [Hughes a.nd Cresswell, 1968]).

precedes b.

• There is one unary predicate Initially on propo­ sitions. If p is a term denoting a proposition, lnitially(p) is true at a node if the denotation of p is in I (for that node).
• There are three binary predicates, Asserts, Denies and Holds which relate propositions to plan steps. First suppose that n is a complete plan, say (I,P,~), and that p denotes a proposition in P . Then Holds(p, a) is true at n if the proposition de­ noted by p is true immediately prior to the plan step denoted by a. This is well defined because of the nature of complete plans, and because we know the initial state I . In a complete plan, Asserts(a,p) is true if Holds(p, a) is false but p holds immediately after a is executed. (Denies is defined similarly; p must be true before a but false afterwards.)

When n is not complete, the denotations of Asserts, Denies and Holds can be defined arbitrarily.

There are several interesting formulas that are valid in all plan-structures. One of the most important is the following axiom, that captures the fundamental connec­ tion between Asserts, Denies, Holds, and Initially as we have defined them.

Later, we will refer to this formula as the Holds axiom.

All nonlinear planning languages share some common weaknesses and our language can help make these pre­ cise. For example, it is a consequence of the use of partial orders on plansteps that formulas like the following are valid:

That is, using partial orders does not allow us to impose a constraint that simply says "x must come immediately before z"; we must also commit to whether x and z are before or after every other action y.

There are also many formulas that are not valid in the general case, but are true of particular systems. If the STRIPS assumption about actions inn is assumed, then additional axioms like the following hold.

Such formulas say that the propositions asserted (or de­ nied) by an action are essentially independent of the ordering imposed on plan-steps. This is a very strong property which simplifies planning enormously when it is reasonable. Most planners use STRIPS-like actions .

Another special axiom that is true in systems like Chapman's TWEAK is:

(In this axiom, Ensures(z, p) is simply an abbreviation for Asserts(z,p) V Holds(p, z).) This axiom can be un­ derstood as showing that the constraint language in TWEAK is rather weak; it cannot be used to constrain a group of actions to assert p, except in the rather trivial case where one particular action is guaranteed to assert p anyway. We have insufficient space to explain in detail how such axioms arise in Chapman's system. In brief, Chapman's action-set language makes use of "proposi­ tions" with variables, which are essentially placehold­ ers that are instantiated during planning. For example, in the "blocks world" a plan step might be associated with action schema Pickup(z), with add list Holding(z) (and perhaps some preconditions, such as Clear(z)). This stands for all actions in n obtainable by instantiating z to a real object. 6 It turns out to be very important for Chapman's TC that variables can be instantiated in infinitely many ways; and the reason for this is essen­ tially to guarantee the truth of axioms like the above, although this can appear quite mysterious until Chap­ man's proof is read. In our language we express many of the important properties Chapman required without using planner specific features such as variables. It is not possible to reprove Chapman's TC exactly in our system, because his TC makes use of features specific to TWEAK. However, a TC which is very similar in spirit can be proven just by making assumptions, such as the formula just given, whose truth can be tested for any nonlinear planning system.

3 Truth Criterion

Chapman proved that his TWEAK truth criterion is cor­ rect and sufficient for his model. However, as he points out, this criterion fails for any planning system just somewhat more expressive than his. One basic short­ coming of Chapman's truth criterion is its requirement that, whenever a proposition necessarily holds at some point in the plan, it is necessarily asserted by one partic­ ular plan step. But in general, it is possible for multiple plan steps to act together to guarantee the truth of a proposition, even where no one step alone is enough.

In this section, we discuss a new truth criterion that is correct and sufficient for any planning system within the scope of our model.

3.1 Presentation

Intuitively our truth criterion can be read as follows . A proposition p is necessarily true immediately before plan step a iff, in all specializations of the plan, two conditions hold: (1) If a is necessarily the first plan step, then it is necessarily the case that p is initially true, and (2) whenever there is a plan step c that is necessarily immediately before a, then if c does not possibly assert p then p must hold at c and not possibly be denied by c. In our logic this TC is given as:

6 Note that expressions like Holding(x) are part ofthe plan representation language, and are meaningless unless consid­ ered in the context of the planning process. This contrast with true propositions in 1', for example Holding(BLOCKA), which can be used to describe the state of the world. In lan­ guages like Chapman's, it is important to keep in mind that "variables" like x are just formal objects used by the planner, and do not connote any formal first-order quantification.

Using our logic, it is possible to give a (lengthy) syn­ tactic proof showing that the TC holds if and only if DHolds(p, a) (see [Christensen, 1990]). In principle, this proof could be checked by an automatic theorem prover, and perhaps even generated by one. Here; we simply give a sketch of a semantic proof.

We first show that whenever DHolds(p, a) fails to hold, our TC is false also. So suppose -,0Holds(p, a). Consider one of the completions where -,Holds(p, a). There are two cases: either a is the first step of the plan or it is not. If the former, the Holds axiom shows that ....,Jnitially(p). But then our TC fails since this completion is a spe­ cialization where a is necessarily the first plan step and ....,oJnitially(p) .

If a is not the first plan step then there must be some other plan step, c, which is immediately be­ fore a; then the Holds axiom shows that ...... Asserts(c,p) and either ....,Holds(p,c) or Denies(c,p) . It follows that ...... oAsserts(c,p) holds in this completion, but one of DHolds(p, c) and ...... ooenies(c,p) is false. Therefore our TC does not hold.

Next, we show if our TC does not hold, then nei­ ther does DHolds(p, a). Suppose the TC is false in a partial plan. Then there must be some specializa­ tion of the plan where either ( 1) a is necessarily the first plan step and ....,oJnitially(p) or (2) there is some plan step c immediately before a with ...... oAsserts(c,p) and either ODenies(c,p) or ....,oHolds(p, c) . If (1), there must be a completion where a is the first plan step and ....,Jnitially(p) . Then, by the HoldS axiom, ....,Holds(p,a) is true in this completion and therefore ....,oHolds(p, a) holds in our plan. If (2) there must be some completion where either (i) there is some plan step c immediately before a and ...... Asserts(c,p) and Denies(c,p) or (ii) there is some plan step c immediately before a and ...,Asserts( c, p) and ....,Holds(p, c). In either case, by the Holds axiom, ....,Holds(p, a), which implies that -.DHolds(p, a).

3.2 Algorithm for Checking our Truth Criterion

The straightforward implementation of our TC involves examining every specialization of a plan. This is clearly not desirable. In fact, the most naive truth criterion, namely applying the Holds axiom to every completion of a partial plan, is no less efficient. However, the po­ tential for efficiency improvements results from noticing two important properties. First, we only need to exam­ ine those specializations where the following holds:

In the following, we will refer to the expression inside the initial Ds of our TC as CTC(p, a) . It is easy to see To test if DHolds(p, a) :

For every weakest specialization such that there is a plan step c necessarily immediately before a which does not possibly assert p:

Check that c does not possibly deny p and necessarily Holds(p, c) .

For any weakest specialization such that a is the first plan step:

Check that lnitially(p) necessarily holds .

that if the above expression does not hold in a special­ ization then CTC(p, a) must hold there.

Second, we only need to examine the weakest such spe­ cializations. A specialization is weaker than another if the latter is a specialization of the former. If CTC(p, a) does not hold in such a specialization we can stop, since in that case ...,osCTC(p, a). If CTC(p, a) does hold in such a specialization then it holds for all specializations of that specialization. For a proof of this, see [Chris­ tensen, 1990]. Using these two properties we arrive at the algorithm in figure 1.

The algorithm for checking the truth criterion re­ quires time exponential in the length of the plan. Chap­ man proved that determining DHolds(p, a) in any system where the schema representation is sufficiently strong to include conditionals is NP-Hard. 7 It is therefore ex­ tremely unlikely that any polynomial time algorithm will ever be found for verifying the truth criteria of such sys­ tems. However, our algorithm will often be considerably more efficient than the application of the Holds axiom to all the completions of a plan, as we shall see shortly. Furthermore, as we discuss later, it represents a good starting point in the development of incomplete or un­ sound algorithms which might overcome the complexity barrier.

3.3 Restricted Ranges of Variables

Chapman gives an example of an extension to TWEAK that causes his TC to fail. Recall that TWEAK uses "variables" , which are placeholders the planner uses to reason about groups of actions. If TWEAK is ex­ tended with a mechanism for restricting the range of variables, then Chapman's TC is no longer sufficient. For example, in TWEAK, if CLEAR(x) is denied by a TWEAK plan step, this step can be specialized into in­ finitely many actions which deny propositions that sat­ isfy the CLEAR(x) schema, e.g. CLEAR(A), CLEAR(B), CLEAR(C), CLEAR(Harry), etc., where A, B, C, and Harry are constants. Restricting the range of variables might be desirable to ensure that variables adhere to a certain type, e.g. we might wish to restrict variable x to the values {A, B, C}, thereby eliminating the possibility CLEAR(Harry) .

Suppose we have the plan in figure 2. In this example, Punch( Bob, John) necessarily holds in the final situation.

7 Conditional actions, which can be modeled in our system, will be described later.

Figure 2: Example where Chapman's TC fails .

However, it is not necessarily asserted by any one step, and so fails Chapman's truth criterion.

On the other hand, our truth criterion succeeds. Fur­ thermore, our truth criterion algorithm requires that only two specializations of the plan be checked. To see this let us step through the algorithm. We would be­ gin by evaluating Holds(Punch(Bob, John),C) . Clearly, there are no specializations where C is the first plan step. However, there are two distinct weakest specializa­ tion such that there is a plan step immediately before C and that plan step does not possibly assert Punch(Bob, John). These are simply the specializations where the constraints y 'I Bob and x 'I John have been respec­ tively added. We will examine the former specialization. In this specialization plan step B must not possibly deny Punch(Bob, John). This is in fact so, since plan step B does not deny anything.

Furthermore, we want DHolds(Punch(Bob, John) , B) . This is checked with another application of the TC. There are no specializations where B is the first plan step. However, in this case there are no specializations where there is a plan step immediately before B that does not possibly assert Punch( Bob, John) . To guarantee this would mean adding either x 'I Bob or y 'I John . If we add the former then both y and x must denote John , which is not allowed. If we add the latter then y can't possibly denote any object , which is also disallowed.

The evaluation of the other specialization proceeds in an analogous manner. As can be seen from stepping through the algorithm, it is somewhat reminiscent of resolution theorem proving, in that we continually at­ tempt to disprove the proposition until a contradiction is found. It is different from resolution theorem proving in that it is guaranteed to terminate if a contradiction is not found in this manner.

3.4 Conditional Actions

Figure 3 shows a plan which, while simple, cannot be represented by TWEAK, or by most other classical plan­ ning systems. One exception is [Pednault, 1988], who presents a plan language that supports conditional ac­ tions and a method for synthesizing linear plans using these actions .

The actions in figure 3 might be described as being conditional, because their effect depends on the statP of the world in which they are executed. In contrast.

Dey I 6otO(Beedl) I H-6oodTime >

STRIPS-like actions have a constant effect (in any world where their preconditions are true). 8 In the figure, one can always go to the beach; there are no executabil­ ity preconditions as such. However, nothing will be achieved at night. This is a very simple conditional ac­ tion representation and nothing in our model precludes us from having arbitrarily complex conditional actions; our model allows any action that is a function mapping states to states.

The algorithm for determining our truth criterion would begin by considering one of the specializations where there is an action immediately before the fi­ nal situation which does not possibly assert HaveG­ oodTime. Assume it considers Goto(Beach) first. We must constrain -,day to be true, or else HaveGood­ Time would possibly be asserted. Then, we verify that Goto(Beach) cannot deny HaveGoodTime and recurse on Holds(HaveGoodTime,Goto(Party)). However, there are no specializations with an action immediately be­ fore Goto(Party) where HaveGoodTime is not possibly as­ serted. If there were then both ...,night and -,day must hold, which is impossible.

3.5 Conclusion and Further Work

In practical terms, one might argue, our truth criterion is not useful since the algorithm for verifying it appears to be inherently exponential. This contrasts with Chap­ man's truth criterion, which can be verified in polyno­ mial time. However, the value of a polynomial time truth criterion is somewhat questionable, given that the plan­ ning process is still undecidable. Furthermore, TWEAK achieves efficiency in the truth criterion at the cost of limitations in expressive power.

As domains become more complex it becomes less and less likely that the TWEAK representation can be used to adequately model them. For example; TWEAK is unable to efficiently model HACKERS cubical blocks world, and completely unable to solve problems whose solution requires conditional actions.

There is an interesting tradeoff between expressivity of a planning language and the search process using that language. As expressivity is added to the language the number of choice points at each plan node in the search tree increases. Furthermore, efficient truth criteria such as Chapman's are less likely to exist. On the other hand, because of the finer resolution greater expressivity al­ lows, over-commitment is more easily avoided, and so the amount of backtracking can be reduced. Also, the increased expressivity allows more knowledge to be en­ coded at each node, thereby allowing for possibly more informed choices. So it is far from clear what the op­ timal point along this spectrum of expressivity is. We note that much of planning research has concerned itself with developing planners which support powerful plan representations.

8 The idea of modifying the STRIPS paradigm, to allow for "preconditions" which determine action's effects, can be found occasionally in the literature; for instance, these are Pednault's secondary preconditions.

Of course, such planners are generally not based on provably correct truth criteria. Our truth criterion could in principle be used instead. However, for efficiency rea­ sons, it is likely that the actual algorithm used would be tailored to take advantage of the planner's specific plan representation. It might even be the case that com­ pleteness, or even in some circumstances, correctness, is sacrificed in order to achieve efficiency gains . However, the designer of the truth criterion would have a sound and complete reference point from which to start, and would therefore be well aware of the corners that were cut 'to achieve efficiency. It remains to be seen what the appropriate tradeoff between efficiency, correctness, completeness, and expressive power of the plan represen­ tation is.