In Defense of PDDL Axioms

1 Motivation

It is not uncommon for planners to support derived predi­ cates, whose truth in the current state is inferred from that of some basic predicates via some axioms under the closed world assumption. While basic predicates may appear as ef­ fects of actions, derived ones may only be used in precon­ ditions, effect contexts and goals. Planners in this family include the partial order planner UCPOP [3], the HTN plan­ ner SHOP [18], and the heuristic search planner GPT [4], to cite but a few. The original version of PDDL [17], the Inter­ national Planning Competition language, also featured such axioms and derived predicates. However, these were never used in competition events, and did not survive PDDL2.1, the extension of the language to temporal planning [8].

This is unfortunate, as the lack of axioms impedes the abil­ ity to elegantly and concisely represent real-world domains. Such domains typically require checking complex conditions which are best built hierarchically, from elementary con­ ditions on the state variables to increasingly abstract ones. Without axioms, preconditions and effect contexts quickly become unreadable, or postconditions are forced to include supervenient properties which are just logical consequences of the basic ones-that is when extra actions do not need to be introduced or action descriptions customised. Moreover, axioms provide a natural way of capturing the effects of ac­ tions on common real world structures such as paths or flows, as we then need to reason about how the transitive closure of

*The full proofs of the theorems appear in the techreport: http : I I csl.anu.edu.aul"-'thiebauxlpapersltrarp0103.pdf.

Jorg Hoffmann and Bernhard Nebel

Institut fiir Informatik Universitiit Freiburg D-79110 Freiburg, Germany

<last-name>®informatik .uni-freiburg.de

a basic relation is affected. 1 There is no intuitive way to up­ date transitive closures in the body of a PDDL action, while it is easy to axiomatize them recursively by means of PDOL axioms (see [4] for a power flow example).

The most common criticism of the original POOL axioms was that their semantics was ill-specified, and that the condi­ tions under which the truth of the derived predicates could be uniquely determined were unclear. We remedy this by pro­ viding a clear semantics for POOL axioms while remaining consistent with the original description in [17]. In particular, we identify conditions that are sufficient to ensure that the ax­ ioms have an unambiguous meaning, and explain how these conditions can efficiently be checked.

Another common view is that axioms are a non-essential language feature which it might be better to compile away than to deal with explicitly, compilation offering the advan­ tage of enabling the use of more efficient, simple, standard planners without specific treatment [10; 9; 7] . We bring new insight to this issue. We give evidence that axioms add signif­ icant expressive power to PDDL. We take "expressive power" to be a measure of how concisely domains and plans can be expressed in a formalism and use the notion of compilability to analyse that [ 19]. As it turns out, axioms are an essen­ tial feature because it is impossible to compile them away­ provided we require the domain descriptions to grow only polynomially and the plans to grow only polynomially in the size of the original plans and domain descriptions. Of course, if we allow for exponential growth, then compilations become possible and we specifY one such transformation, which, un­ like those previously published [1 0; 9; 7], works without re­ striction. However, the above mentioned results suggest that it might be much more efficient to deal with axioms inside the planner than to compile them away. In fact, our experiments with FF [ 11] suggest that adding even a simple implementa­ tion of axioms to a planner clearly outperforms the original version of the planner solving the compiled problem.

2 Syntax and Semantics

We remain in the sequential planning setting of POOL2.1 Ievell, which is essentially that of the version of POOL with AOL actions used in the 2000 planning competition. See [2] for a description of the syntax. For clarity we do not consider types. Although we see axioms with conditions on numeric ftuents, such as those featured in PDDL2.1 level 2, as very desirable, we do not consider them here for simplicity.

1 In that respect, PDDL axioms offer advantages over the use of purely logical axioms as in the original version of STRIPS [14] .

Let B and V be two sets of predicate symbols with B n V = 0, called the set of basic and derived predicates, re­ spectively. Symbols in V are not allowed to appear in the initial state description and in atomic effects of actions, but may appear in preconditions, effect contexts, and goals. The domain description features a set of axioms A. These have the form(: derived (d ?x) (f ?x)), where dE V, and where f is a first-order formula built from predicate symbols in B U V and whose free variables are those in the vector x.

Intuitively, an axiom(: derived (d ?x) (f ?x)) means that when (f ?x) is true at the specified arguments in a given state, we should derive that ( d ? x) is true at those arguments in that same state. Unlike traditional implications, these derivations are not to be contraposed (the negation of f is not derived from the negation of d), and what cannot be derived as true is false (closed world assumption). Because of the closed world assumption, there is never any need to explicitly derive neg­ ative literals, so the constraint that the consequent of axioms be positive literals does not make us lose generality.

In sum, axioms are essentially (function free) logic pro­ gram statements [15]. For example, from the basic predicate on and the predicate holding in Blocks World, we can define the predicate clear, as follows:

(:derived (clear ?x) (and (not (holding ?x)) (forall (?y) (not (on ?y ?x)))))) Another classic is above, the transitive closure of on, e.g.: (:derived (above ?x ?y) (or (on ?x ?y) (exists (?z) (and (above ?x ?z) (above ?z ?y)) )))

In a planning context, it is natural and convenient to re­ strict attention to so-called stratified axiom sets-stratified logic programs avoid unsafe use of negation and have an un­ ambiguous, well-understood semantics [ 1]. The idea behind stratification is that some derived predicates should first be defined in terms of the basic ones possibly using negation, or in terms of themselves (allowing for recursion) but without using negation. Next, more abstract predicates can be defined building on the former, possibly using their negation, or in terms of themselves but without negation, and so on. Thus, a stratified axiom set is partitionable into strata, in such a way that the negation normal form 2 (NNF) of the antecedent of an axiom defining a predicate belonging to a given stratum uses arbitrary occurrences of predicates belonging to strictly lower strata and positive occurrences of predicates belonging to the same stratum. Basic predicates may be used freely.

Definition 1 An axiom set A is stratified iff there exists a partition (stratification) of the set of derived predicates V into (non-empty) subsets {Vi, 1 ~ i ~ n} such that for all (:derived (di ?x) (f ?x)) E A:

1. if dj appears in NNF(j ?x), then di E Vi and dj E Vj such that j ~ i,
2. if dj appears negated in NNF(j ?x), then di E Vi and dj E Vj such that j < i.

2 In a formula in NNF, negation occurs only in literals.

Note that any stratification {Vi, 1 ~ i ~ n} ofV induces a stratification { Ai, 1 ~ i ~ n} of A in the obvious way: Ai = {(:derived (di ?x) (fi ?x)) E A I di E Vi}. Note also that when no derived predicate occurs negated in the NNF of the antecedent of any axiom, a single stratum suffices. Several planning papers have considered this special case [ 1 0; 9; 7].

Working through the successive strata, applying axioms in any order within each stratum until a fixed point is reached and then only proceeding to the next stratum, always leads to the same final fixed point independently of the chosen strati­ fication [1, p. 116]. It is this final fixed point which we take to be the meaning of the axiom set.

We now spell out the semantics formally. Since we have a finite domain and no functions, we identify the objects in the domain with the ground terms (constants) that denote them, and states with finite sets of ground atoms. More precisely, a state is taken to be a set of ground basic atoms: the derived ones will be treated as elaborate descriptions of the basic state. In order to define the semantics, however, we first need to consider an extended notion of "state" consisting of a set S of basic atoms and an arbitrary set D of atoms in the derived vocabulary. The modeling conditions for extended states are just the ordinary ones of first order logic, as though there were no relationship between Sand D. Where ?x denotes a vector of variables and t denotes a vector of ground terms, we define:

Definition 2

Applying axiom a = (:derived (d ?x) (f ?x)) in a state S augmented with derived atoms D, results in the set [a](S, D) of further derived atoms:

Definition 3

Given this, we associate stratum Ai with the function [A]i which maps a given basic state S to the least fixed point attainable by applying the axioms in Ai starting from the extended state consisting of S and of the set of ground derived atoms returned at the previous stratum by [A]i-l· The stratified axiom set A denotes the function [A] = [A]n:

Definition 4 Let { Ai, 1 ~ i ~ n} be an arbitrary stratifica­ tion for a stratified axiom set A. For each state S, let:

Finally, given a stratified axiom set A, we write S f=A f to indicate that a formula f composed of both basic and derived predicates holds in state S:

Definition 5 s FA f iff (S, [A](S)) I= f

This modeling relation is used when applying an action in state S to check preconditions and effect contexts, and to de­ termine whether S satisfies the goal. This is the only change introduced by the axioms into the semantics of PDDL and completes our statement of the semantics. The rest carries over verbatim from [2] .

Checking that the axiom set in a domain description is stratified and computing a stratification can be done in poly­ nomial time in the size of the domain description, using Algo­ rithm I . The algorithm starts by building a lVI x lVI matrix 3 R such that R[i, j] = 2 when it follows from the axioms that predicate i's stratum must be strictly lower than predicate j's stratum, R[i, j] = 1 when i's stratum must be lower than j's stratum but not necessarily strictly, and R[i ,j] = 0 when there is no constraint between the two strata (lines 2-15). R is first filled with the values encoding the status (strict or not) of the base constraints obtained by direct examination of the axioms (lines 5-10). Then, the consequences of the base con­ straints are computed, similarly as one would compute the transitive closure of a relation (lines 11-15). There exists a stratification iff the strict relation encoded in R is irreflexive, that is iff R[i, i] =F 2 for all i E V (line 16). In that case, the stratification corresponding to the smallest pre-order consis­ tent with R is extracted, i.e. predicates are put in the lowest stratum consistent with R (lines 17-26).

3 Axioms Add Significant Expressive Power

It is clear that axioms add something to the expressive power of PDDL. In order to determine how much power is added, we will use the compilability approach [19]. Basically, what we want to determine is how concisely a planning task can be represented if we compile the axioms away. Furthermore, we want to know how long the corresponding plans in the compiled planning task will become.

3 By I · I we denote the cardinality of a set.

In the following, we take a PDDLx planning domain de­ scription to be a tuple D. = (C, B, V , A, 0 ), where C is the set of constant symbols, B is the set of basic predicates, V is the set of derived predicates, A is a stratified axiom set as in Definition 1, and 0 is a set of action descriptions (with the mentioned restriction on the appearance in atomic effects of the symbols in V). A PDDLx planning instance or task is a tuple II = (D. , I, Q), where D. is the domain description, and I and g are the initial state (a set of ground basic atoms) and goal descriptions (a formula) , respectively. The result of applying an action in a (basic) state and what constitutes a valid plan (sequence of actions) for a given planning task are defined in the usual way [2], except that the modeling re­ lation in Definition 5 is used in place of the usual one. By a PDDL domain description and planning instances we mean those without any axioms and derived predicates, i.e. , a PDDL domain description has the form (C, B, 0, 0, 0 ).

We now use compilation schemes [19] to translate PDDLx domain descriptions to PDDL domain descriptions. Such schemes are functions that translate domain descriptions be­ tween planning formalisms without any restriction on their computational resources but the constraint that the target do­ main should be only polynomially larger than the original. 4

Definition 6 A compilation scheme from X to Y is a tuple of functions f = (hi, !;, f p) that induces a function F from X-instances II= (D.., I, 9) toY-instances F(II) as follows :

and satisfies the following conditions:

1. there exists a plan for II iff there exists a plan for F(II),
2. and the size of the results of j 0 , k and fg is polynomial in the size of their argument D..

In addition, we measure the size of the corresponding plans in the target formalism. 5

Definition 7 If a compilation scheme f has the property that for every plan P solving an instance II, there exists a plan P' solving F(II) such that liP' II ::; c x IIPII + kfor positive integer constants c and k, then f is a compilation scheme preserving plan size linearly, and ifiiP'II ::; p(JIPII, IIIIII)for some polynomial p, then f is a compilation scheme preserving plan size polynomially.

From a practical point of view, one can regard compilabil­ ity preserving plan size linearly as an indication that the target formalism is at least as expressive as the source formalism. Conversely, if a super-linear blowup of the plans in the target formalism is required, this indicates iliat the source formal­ ism is more expressive than the target formalism- a planning algorithm for the target formalism would be forced to gener­ ate significantly longer plans for compiled instances, making it probably infeasible to solve such instances. If plans are re­ quired to grow even super-polynomially, then the increase of expressive power must be dramatic. Incidentally, exponential growth of plan size is necessary to compile axioms away.

4 We use here a slightly simplified definition of compilability. 5 The size of an instance, domain description, plan, etc. is de­ noted by II · 11 .

In order to investigate the compilability between PDDL and PDDLx, we will analyze restricted planning problems such as the 1-step planning problem and the polynomial step plan­ ning problem. The former is the problem of whether there exists a 1-step plan to solve a planning task, the latter is the problem whether there exists a plan polynomially sized (for some fixed polynomial) in the representation of the domain description.'From the results on the computational complex­ ity of pure OAT A LOG and DATA LOG with stratified negation [6], the next theorem is immediate.

Theorem 1 The 1-step planning problem for PDDLx is EXPTIME-complete, even if all axioms are in pure DATALOG.

If we now consider PDDL planning tasks, it turns out that the planning problem is considerably easier, even if we allow for polynomial length plans. Since guessing a plan of poly­ nomial size and verifYing it can easily be done in polynomial space, the polynomial step PDDL planning problem is obvi­ ously in PSPACE. Taking in addition Vardi's [20] result into account that first-order query evaluation over a finite database is PSPACE-complete, hardness follows as well.

Theorem 2 The polynomial step planning problem for PD D L is ?SPACE-complete.

From these two statements it follows immediately that it is very unlikely that there exists a polynomial time compilation scheme from PDDLx to PDDL preserving plan size polyno­ mially. Otherwise, it would be possible to solve all prob­ lems requiring exponential time in polynomial space, which is considered as quite unlikely. As argued, however, by Nebel [19], if we want to make claims about expressiveness, then we should not take the computational resources of the compila­ tion scheme into account but allow for computationally un­ constrained transformations. Interestingly, even allowing for such unconstrained compilation schemes changes nothing.

Theorem 3 Unless EXPTIME = PSPACE, there is no compi­ lation scheme from PDDLx (even restricted to pure DATALOG axioms) to PDDL preserving plan size polynomially.

Proof Sketch. We use a proof idea similar to the one Kautz and Selman [13] used to prove that approximations of logi­ cal theories of a certain size are not very likely to exist. By using a DATALOG theory in order to describe all instances of the linearly bounded alternating Turing machine accep­ tance problem up to a certain size, which in its general form is EXPTIME-complete [5], we get a polynomial advice string [12] if a compilation scheme from PDDLx to PDDL preserv­ ing plan size polynomially exists. This would imply that EX­ PTIME ~ PSPACE/poly. However, by Karp and Lipton's [12] results, this implies that EXPTIME = PSPACE. ·

4 Compilations with Exponential Results

While it is impossible to find a concise equivalent PDDL plan­ ning instance that guarantees short plans, it is possible to come up with a poly-size instance which may have expo­ nentially longer plans in the worst case. Such compilation schemes have been described by e.g. Gazen and Knoblock [10] and Garagnani [9] under severe restrictions on the use of negated derived predicates. Specifically, these schemes do not work if negated derived predicates appear anywhere in the

Figure 1 PDDL instances induced by f

I. (: predicates ; all predicates in B U TJ 2. (done1 ) . ·· (done0 ) 3. (fixed0 ) ·. . (fixed.) 4. (neY)) for each i E {1 , ... , n} 5. (: action stratum1 6. : parameters () 7. : precondition (and (fixed1_.) (not (fixed1))) 8. : effect (and (done1)) 9. (for all (x',,t) 10. (Yhen (and (f 1 ,1 ?x1 ,1 ) (not (d,, , ?i,,t))) II. (and (d1 ,1 ?x1 , .) (neY)))) (forall (x1 .~, 1 ) 12. 13. 14. 15. (Yhen (and (f 1 , ~ 11 ?x1 . ~~~) (not (d1 . ~,1 ?x1 ,~,1 ))) 16. (: action f i xpoint1 (and (d1 . ~ 1 1 ?x1 . ~ 1 1 ) (neY)))))) 17. : parameters () 18. : precondition (done1 ) 19. :effect (and (Yhen (not (ney)) (fixed,)) 20. (not (neY)) 21. (not (done,)))) for each o E 0 22. (: action NAME(o) 23. :parameters PARAMETERS(o) 24. : precondition (and PRECONDITION( a) (fixed,)) 25. : effect (and EFFECT(o) 26. (not (fixed. )) ... (not (fixed. )) 27. (not (done. )) . . . (not (done.)) 28. (forall x. ,, (not (d. ,1 ?x. ,t))) 29. 30. (for all Xn, ~nl (not (dn, ~nl ?xn , ~nl ))))) Where k = max( {i I some d;,j occurs in PRECONDITION(o)}u{O}) and m = min( { i I a predicate in some f ;,j is modified in EFFECT( a) }u{ n+l }) 31. (: init I U (fixedo )) 32. (: goal (and Q (fixed.)) )

planning task, 6 and the latter scheme [9] is further restricted to pure DATALOG axioms.

An interesting contrasting approach is that of Davidson and Garagnani [7]. They propose to compile pure DATALOG ax­ ioms solely into conditional effects, which means that the re­ sulting plans will have exactly the same length. However, as is implied by Theorem 3, their domain description suffers a super-polynomial growth.

We now specifY a generally applicable compilation scheme producing poly-size instances, which we will use as a base­ line in our performance evaluation. In contrast to the schemes mentioned above, it complies with the stratified semantics specified in Section 2 while dealing with negated occurrences of derived predicates anywhere in the planning task.

Theorem 4 There exists a polynomial time compilation scheme f = (fti, k f 9 ), such that for every PDDLx do­ main description!::.. = (C, B, 'D, A, 0 ): llfi (t::..)l l = c 1 and 11!9 (!::..)11 = c2for some constants c 1 and c2, and fti(!::..) = (C, B', 0, 0, 0') is a PDDL domain with IB'I :S IBI +3 I'DI +2 and with 110'11 :S p(IIOII, IIAII)for some polynomial p.

Proof Sketch. Figure 4 shows the main elements of the PDDL instances induced by f. f computes a stratification {Ai , 1 ::=:; i ::=:; n} of the set of axioms A , as explained in Section 2, where in stratum i , each axiom ai,j is of the form (:derived (di,j ?xi,j) (fi, j ?xi,j )) for 1 ::=:; j :SI Ai 1. f encodes each stratum as an extra action stratum; (see lines 5-15 in Figure 4) which applies all axioms a; ,j at this stratum in parallel, records that this was done ( donei) and whether anything new (new) was derived in doing so. Each ai, j is encoded as a universally quantified and conditional effect of stratumi-see lines 9-15. To ensure that the precedence be­ tween strata is respected, stratumi is only applicable when the fixed point for the previous stratum has been reached (i.e. when fixedi-l) and the fixed point for the current stratum has not (i .e. when (not (fixedi)))-see line 7. f encodes the fixpoint computation at each stratum i using an extra action f ixpoint; , which is applicable after a round of one or more applications of stratumi (i.e., when donei is true), asserts that the fixed point has been reached (i.e. fixedi) whenever nothing new has been derived during this last round, and re­ sets new and done; for the next round-see lines 16-21. Next, the precondition and effect of each action description o E 0 are augmented as follows (see lines 22-30). Let 0 ::::; k ::::; n be the highest stratum of any derived predicate appearing in the precondition of o, or 0 if there is no such predicate. Before applying o, we must make sure that the fixed point for that stratum has been computed by adding f ixedk to the precon­ dition. Similarly, let 1 ::::; m ::::; n + 1 be the lowest stratum such that some predicate in the antecedent of some axiom in Am is modified in the effect of o, or n + 1 if there is none. After applying o, we may need to re-compute the fixed points for the strata above m, that is, the effect must reset fixed, done, and the value of all derived propositions, at strata m and above. Finally, f ixed0 holds initially, and the goal re­ quires f ixedn to be true. The fact that f preserves domain description size polynomially, and the bounds given in theo­ rem 4, follow directly from the construction. ·

6 This remains true even if negation is compiled away as per the Gazen and Knoblock method [10].

It is obvious that a plan P for a planning task II can be recovered from a plan P' for the compiled planning task F(II), by simply stripping all occurrences of stratum and fixpoint actions. In the worst case of course, there is no polynomial p such that IIP'II ::::; p(IIPII , IIIIII) . Indeed, the worst-case is obtained when, initially and after each ac­ tion from P, all derived predicates need to be (re)computed and only one proposition is ever derived per application of stratumi actions. Even if the planner is able to interleave as few fixpointi actions as possible with the stratumi ac­ tions, this still leads to a plan of length IIP'II = IIPII + (IIPII + 1)(2:~~ (IVi l +3)) = IIPII + (IIPII + 1)(3n+ lVI) , where V denotes the set of all instances of predicates in V . Observe that V is not polynomially bounded in lVI and ICI-

5 Planning: With or Without Axioms?

The absence of a polynomial time compilation scheme pre­ serving plan size linearly not only indicates that axioms bring (much needed) expressive power, but it also suggests that ex­ tending a planner to explicitly deal with axioms may lead to much better performance than using a compilation scheme with the original version of the planner. To confirm this hy­ pothesis, we extended the FF planner [11] with a straight­ forward implementation of axioms-we call this extension FF x-and compared results obtained by FF x on POOLx in­ stances with those obtained by FF on the POOL instances pro­ duced via compilation with f.

FF x transforms each axiom (: derived( d ? x) (f ? x)) into an operator with parameters (?x) , precondition (f ?x) and effect ( d ?x), with a flag set to distinguish it from a "normal" operator. During the relaxed planning process that FF per­ forms to obtain its heuristic function, the axiom actions are treated as normal actions and can be chosen for inclusion in a relaxed plan. However, the heuristic value only counts the number of normal actions in the relaxed plan. During the for­ ward search FF performs, only normal actions are considered; after each application of such an action, the axiom actions are applied so as to obtain the successive fixed points associated with the stratification computed by Algorithm 1.

One domain we chose for our experiments is the usual Blocks World (BW) with 4 operators. In contrast to most other common benchmarks, in BW there is a natural distinc­ tion between basic and derived predicates; in particular BW is the only common benchmark domain we are aware of where the stratification of the axioms requires more than one stra­ tum. The basic predicates are on and ontable, and the de­ rived ones are above and holding (stratum 1), as well as clear and handempty (stratum 2) whose axiomatisations use the negation of holding. above is only used in goal descriptions. For the experiment labelled BW-1 in the fig­ ures below, we generated 30 random initial states for each size n = 2 . .. 10 and took the goal that any block initially on the table had to be above all those that were initially not. Note that expressing the resulting goal using on and ontable would require exponential space, highlighting once more the utility of derived predicates. As shown in the figure, the me­ dian run-time of FF x shows a significant improvement over that of FF+f. The plans found by FF+f in this experiment were an order of magnitude longer than those found by FF x . The experiment labelled BW-2 shows, for n = 2 .. . 42, the spe­ cial case of those instances for which the initial state has only one tower. Here the improvement in run time is dramatic, as FF x finds the optimal plans whose length is only linear in n.

Another domain we ran experiments on is the challenging Power Supply Restoration (PSR) benchmark [4], which is de­ rived from a real-world problem in the area of power distribu­ tion. The domain description requires a number of complex, recursive, derived predicates to axiomatize the power flow, [ 4]. We considered a version of the benchmark wiiliout any uncertainty for which the goal is to resupply all resuppliable lines. For each number n = 1 to 7 feeders, we generated 100 random networks with a maximum of 3 switches per feeder and with 30% faulty lines. The third figure above compares the median run times of FF x and FF+f as a function of n. Again the improvement in performance resulting from han­ dling axioms explicitly is undeniable. In this experiment, the plan length does not vary much with n: with our parameters for the random instances generation, it is clustered around 5 actions for POOLx instances, and around 50 for the compiled instances. Yet this makes all the difference between what is solvable in reasonable time and what is not.

Although the domains in these experiments are by no means chosen to show off the worst-case for the compilation scheme, they nevertheless illustrate its drawbacks. The dif­ ference of performance we observe is due to the facts that compilation increases the branching factor, increases the plan length, and obscures the computation of the heuristic.

Other published compilation schemes [10; 9] are not ap­ plicable to the above domains whose descriptions involve negated derived predicates. The exponential space transfor­ mation by Davidson and Garagnani [7] is applicable to BW, but was unable to cope with problems larger than n = 4 be­ cause it substitutes for their definitions all occurrences of non­ recursive derived predicates until none remains. This turns preconditions into ADL constructs that quickly become too complex for FF's pre-processing step to compile them away in reasonable time, in difference to the experiments described above where pre-processing time was negligible.

6 Conclusion

As reflected by recent endeavours in the international plan­ ning competitions, there is a growing (and, in our opinion, de­ sirable) trend towards more realistic planning languages and benchmark domains. In that context, it is crucial to determine which additional language features are particularly relevant. The main contribution of this paper is to give theoretical and empirical evidence of the fact that axioms are important, from both an expressivity and efficiency perspective. In addition, we have provided a clear formal semantics for PDDL axioms, identified a general and easily testable criterion for axiom sets to have an unambiguous meaning, and given a compilation scheme which is more generally applicable than those previ­ ously published (and also more effective in conjunction with forward heuristic search planners like FF).

Future work will include more extensive empirical stud­ ies involving a more elaborate treatment of axioms within FF and planners of different types, as well as the extension of derived predicates and axioms to the context of the numeri­ cal and temporal language features recently introduced with PDDL 2.1. Axioms have long been an integral part of action formalisms in the field of reasoning about action and change where, much beyond the inference of derived predicate con­ sidered here, they form the basis for elegant solutions to the frame and ramification problems, see e.g. [16] . It is our hope that the adoption of PDDL axioms will eventually en­ courage the planning community to make greater use of these formalisms.

Acknowledgements

Thanks to Blai Bonet, Marina Davidson, Stefan Edelkamp, Maria Fox, John Lloyd, and John Slaney for fruitful discus­ sions which helped to improve this paper.