Compiling Control Knowledge into Preconditions for Planning in the Situation Calculus

1 Introduction

One of the strategies used in planning to mitigate the com­ plexity of the general problem is to employ some form of domain specific knowledge to assist the search for a plan. For instance, Hierarchical Task Network (HTN) planning systems [Sacerdoti, 1974; Wilkins, 1988; Erol eta!., 1996] use domain specific procedural knowledge in the form of task decomposition methods. The forward-chaining planners TLPlan [Bacchus and Kabanza, 2000], TALPlanner [Kvam­ strom and Doherty, 2000] and the SAT based planner SAT­ Plan [Kautz and Selman, 1998] use domain knowledge in the form of declarative constraints expressed in a logical lan­ guage. This strategy has been shown experimentally to yield remarkable improvements in performance. Both TLPlan and TALPlanner use control constraints expressed in the form of temporal logic formulas. These formulas are used to elim­ inate plan prefixes which will lead to a suboptimal plan or cannot be extended into a complete plan at all.

Most practical planning systems use STRIPS, ADL or ex­ tensions of these to describe actions and their effects. How­ ever, the first formal specification of the classical planning problem, due to [Green, 1969], was postulated in the lan­ guage of the situation calculus [McCarthy, 1963]. The sit­ uation calculus has proven to be a very powerful formalism and has been employed in the formalization of many differ­ ent aspects of dynamical systems (see e.g. [Reiter, 2001]). In this paper, we use the situation calculus as our formal framework and consider how to incorporate search control into action theories. Specifically, we show that control for­ mulas with a certain syntactic form can be incorporated into nonMarkovian action theories in the situation calculus, as re­ cently introduced in [Gabaldon, 2002], in a similar way as [Lin and Reiter, 1994] treat qualification state constraints. In these nonMarkovian action theories, the effects and precon­ ditions of actions are not assumed to depend solely on the current situation, but on any past situation. This nonMarko­ vian property of the theories allows an easier incorporation of dynamic constraints into database specifications, a more nat­ ural and concise axiomatization of nonMarkovian operations like rollback in transaction systems and other domains with nonMarkovian properties. In this paper, we are concerned with another problem where these theories are useful: incor­ porating search control knowledge by treating it as dynamic, qualification state constraints. Dynamic in the sense that they may refer to the current and any past situation, as opposed to static state constraints which refer only to the current state. Moreover, they are understood as qualification constraints be­ cause they pose further restrictions on the "executability" of actions. (We do not consider the use of these constraints for expressing ramifications, i.e. indirect effects of actions.)

Furthermore, we present a transformation from nonMarko­ vian action theories into Markovian ones. This transforma­ tion takes an action theory with nonMarkovian axioms and by applying regression steps and introducing additional flu­ ents and their corresponding successor state axioms, produces a classical Markovian theory as introduced by [Reiter, 1991]. We then show how this transformation can be used for com­ piling search control knowledge into normal action precondi­ tions. This nonMarkovian to Markovian transformation pro­ cedure is of independent interest. Toward the end we extend this approach for theories with explicit time and close with a discussion.

2 Formal Preliminaries

In this section we give an overview of the situation calculus and the main definitions necessary for action theories without the Markov assumption.

2.1 The Situation Calculus

The situation calculus is a first order logic language with three basic components: actions, situations, and fluents. Ac­ tions are responsible for all the changes in the world. Situa­ tions are sequences of actions which represent possible his­ tories of the world. Fluents are properties of the world that change from situation to situation as a result of the execu­ tion of actions. Formally, the language has three sorts: ac­ tion, situation and fluent. In addition to variables of these sorts, the language includes functions such as move(x, y) to represent actions, a constant So and a function do( a, s) for situations such as do(move(x, y), S0 ), and predicates for representing fluents such as atLocation(x, l, do( a, s)) . The initial situation, or empty history, is denoted by the constant S0 . Non-empty histories are built by means of the function do. For a complete description see [Pirri and Reiter, 1999; Reiter, 2001].

A situation calculus axiomatization of a domain, includes the following set of axioms:

1. For each action function A(x), an action precondi­ tion axiom of the form: Poss(A(x1, ... , Xn), s) = ITA ( x1, ... , Xn, s) where s is the only term of sort situ­ ation in IIA(xl, ... , Xn, s).
2. For each fluent F(x, s), a successor state axiom of the form: F(x1, ... , Xn, do( a, s)) = <I>F(Xl, ... , Xn, a, s) where s is the only term of sort situation in <l>F(Xl, . .. ,Xn,a,s).
3. Unique names axioms for actions. For instance: move(x, y) =f. pickup(x).
4. Axioms describing the initial situation of the world: a finite set of sentences whose only situation term is the constant So.

A set of these axioms, together with a set of domain inde­ pendent foundational axioms ~. is called a (Markovian) basic action theory.

2.2 A nonMarkovian Situation Calculus

For a basic action theory without the Markov assumption, we need some definitions. These are based on those in [Gabal­ don,2002].

We will use the following abbreviations in the definitions to follow:

where ,...., stands for either C or = and variable s appears in 0' 11 · If 0' 1 is So then we may write (3s : 0' 11 ,...., 0') W and (V s : 0' 11 ,...., 0') W instead.

Definition 1 (Bounded Formulas) For n > 0, let 0' be a term do([a1, ... , an], A) rooted at A. The formulas of L sitcalc bounded by 0' are the smallest set of formulas such that:

1. If W is an atom whose situation terms are all rooted at A, then W is bounded by 0'.
2. If W', W" are formulas bounded by situation terms rooted at s and A, respectively, then (3s : 0' 1 C 0' 11 ,...., 0') W and (V s : 0' 1 C 0' 11 ,...., 0') W are formulas bounded byO', where0' 11 isrootedatsand W = (·)(W' A W").
3. If W1, W2 are formulas bounded by situation terms rooted at A, then -.., W1, W1 A W2 and (3v) W1, where v is of sort action or object, are formulas bounded by 0'.

The set of formulas strictly bounded by 0' is similarly de­ fined by requiring in item (1) above that all situation terms of W be subterms of 0', in item (2) that W' be strictly bounded by a subterm of 0' 11 and W" by a subterm of 0'; and in item (3) that wl, w2 be strictly bounded by subterms of(]',

Example 1 Past temporal logic connectives can be expressed in the situation calculus with strictly bounded formulas as fol­ lows:

NonMarkovian basic action theories differ from those which include the Markov assumption in that preconditions and ef­ fects of actions may depend on any past situation, not only on the current one.

Hence the rhs, IIA(x1, ... , Xn, s), of action precondition axioms in a nonMarkovian basic action theory are formulas bounded by situation term s which do not mention predicate Pass and may refer to past situations. Similarly, the rhs, <I> F ( x1, ... , Xn, a, s) of successor state axioms are formulas strictly bounded by s.

2.3 Regression

For basic action theories with the Markov assumption, [Pirri and Reiter, 1999] define a provenly correct regression mech­ anism that takes a situation calculus sentence and, under cer­ tain restrictions on the form of this sentence, transforms it into an equivalent sentence whose only situation term is 80. This allows proving sentences without appealing to the foun­ dational axioms ~ which include a second order axiom. This regression operator was generalized for nonMarkovian theo­ ries in [Gabaldon, 2002].

In a nutshell, the regression operator, denoted by R, takes a sentence and recursively replaces each flu­ ent atom F(i', do( a, 0')) by its definition according to its successor state axiom, i.e. by <I>F(i',a,O'). Atoms Poss(A(i) ,do(a,O')) are similarly replaced by their defini­ tions given by the action precondition axioms. Regression recursively replaces these atoms until all the situation terms are reduced to S0 . For lack of space we refer the reader to [Pirri and Reiter, 1999; Reiter, 2001; Gabaldon, 2002] for the formal details.

In the transformation operator we introduce later, we will use a one-step version of the regression operator: R 1 [W[do(a,O')]] stands for the regression of a sentence W[do(a, 0')] bounded by do( a, 0') that results in a sentence bounded by 0'.

3 Control Knowledge and the Qualification Problem

As mentioned earlier, the use of search control knowledge has proven to be a promising recourse for improving the per­ formance of planning systems. Both TLPlan [Bacchus and Kabanza, 2000] and TALPlanner [Kvamstrom and Doherty, 2000] use declarative control knowledge in the form of tem­ poral logic and have shown substantial computational im­ provement.

Since our goal is to compile search control into precon­ ditions, we express control knowledge in terms of the past, not the future as it is done in TLPlan and TALPlanner (this is further discussed in the last section). However, declarative search control knowledge is typically expressed in a future temporal logic and we believe that obtaining preconditions from knowledge in that form is an important problem. In the last section we comment on how we are approaching this.

From the point of view oflogical theories of action, such as the situation calculus axiomatizations we discuss in this pa­ per, taking control knowledge into account is closely related to the classical qualification problem [McCarthy, 1977]. This is the problem of determining all the conditions that need to be satisfied for an action to be executable and control knowl­ edge is effectively a set of additional constraints on the exe­ cutability of actions, i.e. on what actions can be considered part of an executable plan.

Lin & Reiter [1994] have considered the qualification prob­ lem for situation calculus basic action theories with state con­ straints, which are formulas of the form (V s) Q ( s), uniform in s. Their solution is to add the qualifications to the precondi­ tion axiom of each action type:

where IIQ = R 1 [Q(do(A(x), s))]. After adding the qualifi­ cations to the precondition axioms, one can discard the con­ straints if two conditions are satisfied: all the state constraints hold initially, i.e. Q(So) holds for each Q; and the domain closure assumption on actions is included in the theory.

Control formulas are similar to state constraints in that they pose additional qualifications on actions, but they are more general since they may quantify over past situations.

In the nonMarkovian situation calculus, successor state ax­ ioms and action precondition axioms can refer to past situa­ tions in addition to the current situation. This permits con­ trol knowledge to be incorporated into action precondition axioms in the same way Lin & Reiter do. Formally, ifC(s) is a formula bounded by s representing some piece of con­ trol knowledge, we take this into account by adding it as an additional precondition for actions:

Precondition axioms in nonMarkovian action theories allow situation terms rooted at s such as do(A(x), s) to appear in their rhs, so we can add C(do(A(x),s)) directly without modification. By including the domain closure assumption on actions, we are then guaranteed that a situation is executable only if it satisfies the constraints.

Example 2 (Logistics domain constraint) Consider a con­ straint from a logistics domain, which involves vehicles de­ livering packages to locations, saying that a truck must re­ main in a location if there is a package at that location and it's never been in the truck (so it hasn't just been delivered and needs to be moved):

Suppose that the action precondition axiom for driveTruck(t, Zoe), driving a truck t to a location Zoe IS:

We can add the control formula as a new con­ junct in the rhs after simply replacing s with s* do( driveTruck(t, Zoe), s ):

In the next section, we introduce an operator which takes a ba­ sic action theory with such nonMarkovian axioms, and trans­ forms it into one with Markovian' ones.

4 Transforming a nonMarkovian Theory into Markovian

In order simplify the presentation, let us first make some sim­ plifying assumptions on the form and the nesting of formulas on which we define the transformation.

Formally, in reference to item (2) of Definition 1, we will assume that formulas are of the forms:

where all (if any) free variables of W2 are among the free variables of the full formula. Other combinations of quanti­ fiers and logical connectives reduce to these two cases. The restriction on the free variables ofW2 does make the transfor­ mation simpler. We treat the general case in the full version of this paper. Next, we restrict the nesting of formulas in the following way. By definition, W2 must itself be of the form ( ·)(W' 1\ W") where W' is bounded by s" and W" by s. We will restrict W2 by requiring it to be of the form ( ·) W', i.e. without the conjunct W".

Notice however that, even with this restrictions, arbitrary nesting of the past temporal logic abbreviations (Example 1) is still expressible.

The transformation performs a combination of regression and of replacement of formulas by new ftuents:

Definition 2 Let <p be an Lsitcalcformula bounded by s. We define a formula M [<p] obtained from <p recursively as fol­ lows. By Definition I, formula <p must be of one of the follow­ ing forms:

1. An atom whose only situation term is s. Then M[<p] = <p.
2. A formula of the form (2). Then, M[<p] = P'P(x, s) which is a new fluent with successor state axiom:

where M[W1] Pw 1 (x1, s) and M[Wz] Pw 2 (iz, s).

Initially, the new fluent is set to false, i.e. (\li)-,P"'(x, So) E Ds 0 ·

1. A formula of the form (3) . Then, M[<p] = P'P(x, s) which is a new fluent with successor state axiom:

where M[W1] Pw 1 (x1 , 8) and M[Wz] Pw 2 ( xz, s) as before, and the new fluent is initially set to true, i.e. (\lx)P"'(x, So) E Ds 0 ·

Theorem 1 Let <p denote a formula of the form (2) or (3) and V'P be the basic action theory obtained from 1J by adding the fluents and axioms resulting from applying M to <p. Then,

Now, we can apply the transformation to a nonMarkovian action theory 1J whose action precondition axioms have as an additional condition a constraint C(s), and obtain a Marko­ vian theory IJM that enforces the constraint. This produces a theory with precondition axioms of the form:

Theorem 2 Let C(8) be a control knowledge formula bounded by s and let 1J be a nonMarkovian basic action theory whose precondition axioms have the form ( 1) and in­ cludes domain closure axioms for actions. Then,

Example 3 Consider again the logistics domain control for­ mula from Example 2. Let <p1 and <pz stand for premise and consequence, respectively. Both formulas are of form (2). The premise <p1 stands for:

Applying operator M on <p1 produces three new fluents H (p, t , Zoe, s ), Pz(p, t, Zoe, s) and P'P 1 (p, t, Zoe, s) with the following successor state axioms:

The result of M on <p2 is similar. Then the constraint be­ comes:

Finally, we add the constraint to action precondition axioms:

Example 4 (Closed form solution for a fluent) Consider a fluent F(x, s) and its closed form solution [Reiter, 2001]:

Clearly, the rhs of the above sentence is formed by F(x, So) and two formulas which are almost of the form (2). The difference is in the ~·s immediately after the existen­ tial quantifiers on situations 8 1 , 8 2 , which would need to be strict C to fit form (2), and the subformulas of the form (3a', 8 1 )do( a', s') = s. The latter will be simplified away. Further, it is easy to modify the transformation on (2) to handle the ~·s. In general, all we need to do is replace Pw 1 (x1, 8) with R. 1 [Pw 1 (x1, do( a, s))]. However, in this ex­ ample the one step regression won't be necessary.

Applying the transformation to the subformula

results in a predicate P'P 1 (x, 8) with successor state ax­ iom (after simplifying) P'P 1 (x, do( a, 8)) = IF (x, a, 8) V P"'1 (x, 8)

The transformation of subformula <p2 =

results in a predicate P'P 2 (x,s) with successor state ax­ iom (after simplifying) P'P 2 (x,do(a,s)) = lf(i,a,s) V ..,,j;(x, a, s) 1\ P"' 2 (x, s)

Noticeably, this successor state axiom for P'P 2 (x,s) is al­ most identical to the canonical form successor state axiom for F(x,s) which is F(x,do(a,s)) = lf(i,a,s) v F(x,s) 1\ ..,,j;(x,a,s).

Finally, after applying the transformation to subformulas <p1, <pz of the closed form formula ( 4 ), we obtain the follow­ ing equivalent sentence:

The transformation comes close to producing a canoni­ cal Markovian successor state axiom. It does not because the closed form solution formula uses information about the value ofF in the initial situation.

5 Constraints with explicit time

In this section, we extend our approach to search con­ trol knowledge with explicit time. In the temporal sit­ uation calculus [Reiter, 2001], actions have an additional temporal argument denoting the time of occurrence, e.g. drive(truck, loc, 3.2) for driving a truck to a location Zoe at time 3.2. There are also some additional axioms: time(A(x, t)) = t specifying the occurrence time for each action A, and start( do( a, s)) = time( a) specifying the start time of situations.

We will use [h , t2] + t to denote [t1 + t , t2 + t] and t E [t1 , t2] to denote t1 :::; t A t :::; t2. So start( s) E [h , t2] + start(s') stands for start(s') + t 1 :::; start(s) A start(s) :::; start(s') + t2 which means that s' precedes s by at least t 1 and at most t2.

Analogous to forms (2) and (3), we have:

For a formula <p of the form (5), M yields a predicate Pcp (x, t, s) with a successor state axiom:

andM[(5)] =Pcp (x, t ,s)Astart(s) E [h , t2]+t. Theinitial database would include ('Vt)·Pcp (x, t, So) .

For a formula of the form (6), the successor state axiom for P"'(x, t , s) is:

with M[(6)] = Pcp (x, t, s) A start(s) E [t1, t2] + t. The initial database would include ('Vt)Pcp(x, t, So).

The statement of the following theorem, which establishes the correctness of the transformation, requires adding the con­ junct t = start(s') to formulas (5) and (6): 1

Theorem 3 Let <p denote a formula of the form (5) or (6) and define VM as before. Then,

6 Discussion and conclusion

We have shown that incorporating control knowledge as addi­ tional preconditions in nonMarkovian action theories is triv­ ial when this knowledge is in the form of bounded formu­ las (which include encodings of Past temporal logic modali­ ties) . We then introduced an operator for transforming non­ Markovian basic action theories into Markovian ones. This operator introduces into a theory the additional fluents and axioms needed for keeping track of the relevant past infor­ mation. We then showed how this operator can be used for compiling TLP!an style search control knowledge into action preconditions in the situation calculus.

1 The variable tis a fresh new variable so there is no effect on the meaning of the formulas.

In the TLP!an system, control knowledge is expressed in terms of linear (future) temporal logic, that is, temporal modalities next, always in the future, until, and sometime in the future are used. Every time a new operator is added to the plan prefix being considered, a control formula is pro­ gressed through it. If the formula is progressed into false, the plan prefix is pruned since a plan with this prefix will violate the constraint. Although it is easy to write situation calculus formulas corresponding to future temporal logic, re­ gression cannot be used on them. However, we argue that if instead of progression, as in TLP!an, we evaluate the control formulas against plan prefixes, it is reasonable to use a logic that refers to past situations instead of future situations. In­ deed, all the reasoning used by a planning system to decide if a partial plan should be discarded or not must be done relative to the properties of the partial plan itself. Furthermore, some future temporal formulas are satisfied by all plan prefixes (e.g. "sometime in the future ¢" where¢ is not unsatisfiable) and are not useful for search control. Thus it seems to us that restricting control formulas to refer exclusively to the past is appropriate.

Moreover, using past temporal logic is semantically cleaner for the following reason. The semantics of future tem­ poral logic is defined in terms of infinite sequences of states. However, plans are finite sequences of actions and thus pro­ duce a finite sequence of states. In order to deal with this tech­ nical difficulty, TLP!an makes the assumption that the world never changes after the plan is completely executed and tht>re­ fore the last state infinitely repeats. This assumption is rea­ sonable under another assumption typically made in classical planning: that the agent executing the plan is the only agent that changes the world, so when this agent terminates execut­ ing its plan, the world remains unchanged. This assumption is unnecessary if using past temporal logic or bounded situation calculus formulas.

Nevertheless, it would be convenient to be able to handle control knowledge expressed in future temporal logic. We are currently working on developing a procedure that would allow us to take a future temporal logic control formula, such as this Briefcase domain one:

goal(at(x, loc)) :::::J

atBriefcase(loc) Until-.inBrief case(x)

and produce a bounded situation calculus formula:

that a plan prefix must satisfy. In tum, we can then apply the procedure introduced in this paper to compile these formulas into the preconditions of actions.

Bacchus & Kabanza [1998] have also extended their sys­ tem for planning with temporally extended goals, which are conditions on sequences of states and not only on the final state as in classical planning. They use a first-order exten­ sion of the Metric Interval Temporal Logic (MITL) [Aiur et al., 1991] to specify the temporally extended goals. Defin­ ing plan correctness with respect to MITL formulas as goals again requires one to make the assumption that the world re­ mains unchanged after the plan is executed. In the case of temporally extended goals this is a further complication since testing if the current state satisfies the goal ¢ means checking whether ¢ is true if the world were to indefinitely remain as it currently is. (Past) MITL formulas can be encoded as for­ mulas of the situation calculus with explicit time as discussed in the previous section. Hence our approach also shows a way to reduce planning with temporally extended goals into planning with classical goals.

Some preliminary experiments by Bacchus & Ady [1999] have shown that compiling search control knowledge into ac­ tion preconditions can result in better performance compared to systems such as TLPlan which keep control knowledge as a separate set of formulas. A general method for compiling temporal formulas into preconditions in their framework has not yet been developed.

The work of [Rintanen, 2000] is also concerned with the use of control knowledge as additional preconditions of plan operators. He uses "auxiliary facts" which is a similar to our introduction of new fluents in the transformation. Like Bac­ chus & Kabanza, Rintanen uses future linear temporal logic for representing control knowledge for planers with ADL-like operators. With the help of these auxiliary facts, he then com­ piles the control knowledge into the operators. The main dif­ ference between his work and ours is that his framework is propositional, while ours is in the more expressive first order situation calculus. Furthermore, he does not allow nesting of temporal operators-in our framework this would correspond to disallowing nesting of quantifiers on situations-which we do allow. Also related but with a different approach, is the work of Sierra [1998]. There, domain knowledge in the form of action selection rules is used for controlling a STRIPS planner. Analyzing the relationship of Sierra's work with ours is among our future work.