A New Logical framework for Deductive Planning

1 Introduction

In this paper we present a logical framewor~ for defin­ ing consistent axiomatizations of planni~g domai~s . ~n effective mechanism for defining the basic operatiOns m a constructive way is embedded in a logic that allows properties of state spaces given by these actions to be proved. This not only includes the deductive g~ne!ation of plans; reasoning about the complete scenano IS also supported by this approach.

Our work follows the "Plans are Programs" paradigm. This approach is not new; in deductive planning, in particular, it has already been discussed by several au­ thors (cf. [Green, 1969; Rosensc~ein, 1981; Kau~z, 1982; Bibel, 1986; Manna and Waldmger, 1987; Bmndo et a/., 1992]). However, their contributions concentrated mainly on aspects of common control structures like se­ quential composition, conditional branching, and some­ times recursion. Less attention has been paid to the question of data structures. Our approach is based on the idea of treating relations used in the axiomatizations of planning scenarios in the same way data with an alge­ braic structure are treated in ordinary programming languages. In planning, situations are usually described by a set of relations between certain objects (blocks, rooms, robots etc.). These relations are flexible in the sense that they may change from one situation to another. The fact that these changes are local to a small section of the entire situation is not reflected in the basic seman­ tic concepts underlying most formalisms for deductive planning. So, for example, the blocks world operation unstack(a, b), (Genesereth and Nilsson, 1987], changes only the on-relation between a and b, the clear-property of b and the table-property of a. If the pile of blocks is just a part of some room, which in turn is j~st one .c~n­ stituent of a larger scene, the unstack-operatiOn exhibits very local behavior .

·This work was partly supported by the German Ministry for Research and Technology (BMFT) under contract ITW 9000 8.

A straightforward concept is to consider these rela­ tions as objects, like elements of (abstract) data types in ordinary programming languages. In the theory of abstract data types most often one only considers al­ gebraic structures where all elements are (freely) g.en­ erated by so-called constructors. In our case, restnct­ ing ourselves to finite relations, an appropriate set of "constructors" and "selectors" can easily be devised as well . Starting with the empty relation all finite n-ary relations can be generated by successive applications of an add- operation that adds an n-tuple to a given rela­ tion. As is the case with freely generated data types, we have to supply a corresponding delete-operation in order to compute with this data type. It seems rea­ sonable to take these two operations as the basis of a planning language designed to compute. changes of re­ lational structures. In our approach relations between unstructured objects correspond to data objects and are therefore considered to be finite . This .seems to be a realistic assumption in most applications. In the con­ text of recursive plans the finiteness of relations and its reflection by axioms becomes essential for termination proofs.

This approach, whereby one considers a fixed state space generated by add- (and delete-) operations, un­ derlies STRIPS-like [Fikes and Nilsson, 1971] planners. These systems also demand a complete description of the operations used in the planning process. In par­ ticular, they allow an efficient treatment of the frame problem [McCarthy and Hayes, 1969] since it is explic­ itly denoted which parts of a situation are changed. Our approach lends formal semantics to the basic concepts underlying the STRIPS approach and, While retaining its effectiveness, removes most of its limitations by pro­ viding a more general mechanism for defining operations and by embedding this mechanism in a logical frame­ work. This not only extends the STRIPS approach and makes it suitable for deductive planning but also allows whole planning environments to be set up in a provably consistent way.

Based on elementary add- and delete-operations with fixed semantics, we will begin with the definition of ba­ sic actions, and then use efficient control structures to build up more complex plans. Apart from the usual ones, these control structures include a new non-deterministic choose construct, necessary to select objects in a non­ deterministic way. Domain constraints are formulated as invariants of the basic actions and can be proved from their basic definitions, thus guaranteeing consistency of the whole planning environment. Due to the fixed se­ mantics of the elementary operations, as well as the con­ trol structures, "side effects" can be excluded in many cases, by a purely syntactical inspection of plans, thereby providing an efficient treatment of the frame problem.

We will restrict ourselves to a formalization within a variant of Dynamic Logic (DL), although many of the ba­ sic ideas could be used in the context of other program­ ming logics as well (e.g., [Salwicki, 1977; Hare}, 1979; Manna and Pnueli, 1991; Kroger, 1987]). Not only does DL seem to be expressive enough for most applications in planning; this choice also allows an easy implemen­ tation of our formalism in an existing deductive system, the Karlsruhe Interactive Verifier (KJV) [Heisel et a/., 1990] . This system can be used as a logic-based shell for setting up planning environments. This includes the def­ inition of the basic actions, the proof of invariants and additionallemmmata, and on top of that the implemen­ tation of various planning strategies.

The paper is organized in the following way : section 2 introduces the semantic background of our theory. In section 3, we define the logic, including syntax and se­ mantics of the planning language. Section 4 shows how state invariants can be derived from the basic operator definitions; it also shows how the abstract operator de­ scriptions, already seen in other planning formalisms , can be obtained, and serve as the basis for deductive planning. Section 5 is devoted to the frame problem. In section 6 we discuss some aspects of the implementation within the KJV system. Section 7 refers to related work and finally, we conclude with some remarks in section 8.

2 State Spaces

Our logical language will be parameterized by an alpha­ bet of "user-defined" symbols. Since many different sorts of objects occur in most applications, our syntax is based on a finite set of sort symbols Z . There will be a fam­ ily of finite, disjoint sets, C = (Cz I .z E Z), the system of constants, and a family of denumerable, disjoint sets X = (Xz I z E Z), the system of variables. Both families are assumed to be disjoint . Atomic formulae are built up by the equality symbol "::" and "user-defined" relation symbols (e.g., on, clear , table etc.). These are given by a z·-indexed family'R = (Rz I i E z·) of disjoint sets, Rz being the set of relation symbols of type i . We assume that almost all sets Rz are empty and that all of them are finite, i.e., R := U{Rz I i E z·} is a finite set .

For a given triple (Z, 'R, C) a model (defining the state space) is denoted by a structure JC = (V, S, I), where 1) = (Dz I z E Z) is a system of carrier sets, S is a set of states (or situations) and I is a state-dependent interpretation that assigns an element of the appropriate carrier to each pair (s, c) and a relation of appropriate type to each pair (s, r). That is, for r E Rz and i = (z1, . . . ,zn), we have I(s, r) ~ Dz, X . .. X Dzn ·

In order to evaluate terms and formulae containing variables, we introduce valuations f3 : X -+ D that preserve sorts. Terms are either variables or constants. They are evaluated by (c]. ,p = I(s, c) and (x], ,p = f3(x), respectively. Satisfiability for first-order formulas in structures JC is defined by

where x E Xz and 13; is like f3 except that f3;(x) =d.

As mentioned in the introduction , we are interested in particular finitely generated state spaces given by so­ called natural models /Co = ('Do, So, Io) . 'Do is a family of at most countable sets. We define So to be the set of all mappings that map the relation symbols from R to finite relations on Do := U{Do. I z E Z} of appropriate type and set I 0(s, r) = s(r). In natural models, constants are interpreted in a state independent way, that is for some d we have I 0(s, c)= d for all s E S0 . Note that in natural models /Co we may drop the first index when evaluating terms.

The reason for introducing states was , of course, that we want to study operators that take us from one world to another . In particular , we are interested in a small set of operators that can be used as atomic constructs in our planning language, just as assignment statements are used in conventional programming languages. Looking at the state space given by a natural model /C0 it is more or less obvious how these elementary operations should look. They can be defined for arbitrary structures JC if treated as relations on S .

For each r E Rz and i = (z1, ... , Zn) let d- r and a-r

be defined as

and

Theorem 1

1) In natural models JC0 the relations a - r( ... ) and d- r( ... ) are total functions.

• 2} In natural models K0 for any two states s and s' there exists a finite sequence of elementary add -and delete­ operations op1, ... , opn 1 such that s op1 o ... o opn B 1 1 where 1 o 1 denotes the composition of relations.

In general structures K, if )..x.I(s, x) = )..x.I(s', x) im­ plies s = s 1 1 the relations a - r( ... ) and d - r( ... ) are partial functions. A more serious restriction is imposed by requiring the add- and delete-operations to be total functions. This means that no interesting domain con­ straints will hold for the whole state space. But what can we do then if we are interested only in states where, for example, we have on(y, x) /1. on(z, x) - y = z ? The answer is simply to check whether the set of states with the above property is closed under the basic actions we want to use in our plans. That is, we treat domain constraints as invariants of the basic actions. Since the concept of invariant is broader than the concept of do­ main constraint-domain constraints must, of course, be invariants of the basic actions-our approach does not impose any restriction on the formulation of planning problems. It offers, as we shall discuss in section 4, the advantage of proving formulae to be invariant, thereby ensuring the soundness of the whole axiom system.

It can be proved (in a way which would have to be made precise) that all structures K where the constants are rigid symbols and I(s, r) is always a finite relation are "contained" in a natural model K0 . Hence, the only crucial question is whether we can define (or "program" ) sufficiently many actions in a sufficiently (!.bstract way. The property stated in part two of the theorem guaran­ tees that the basis of our planning language is power­ ful enough: All states can be reached from each other by applying finite sequences of basic add- and delete­ operations. Of course, this does not mean that all actions can be "programmed" in a satisfactory way. Indeed it turns out that the control structures have to be carefully designed. In particular, we need a non-deterministic choose construct in connection with recursive actions. The choose construct will be introduced in section 3.

3 The Logic

We start with the definition of the syntax of our plan­ ning language. Actions 1r and action abstractions 1 are defined relative to a vocabulary given by (Z, C, R, X). In addition, we use a system A = (Az I z E Z*) of names for abstractions.

where cp is a first-order formula and r is a relation symbol from R. We impose the usual type constraints. The oc­ currence of x following choose is a binding occurrence, the scope of which consists of the plan enclosed by "be­ gin" and "end" .

Let K = (V,S,I) be a structure for (Z,C,'R). The semantics of plans 1r is given by a valuation [ .. .]p, where ( 7r )p ~ S X S.

We have defined the semantics for arbitrary structures K . However, the reader should bear in mind that we are interested only in natural models K0 , where the add- and delete-operations are total functions on the set of states.

rec a(x1, .. . ,xn).7r is a recursive action x1 , ... ,xn be­ ing the formal parameters and 1r being the body of that action. To simplify our exposition we restrict ourselves to simple recursive actions, an extension to mutually re­ cursive ones being straightforward. The semantics (and proof theory) of recursive abstractions relies on finite approximations. As can be seen from the semantic defi­ nitions above recn a(x1, . .. , Xn).7r denotes the n'th ap­ proximation of the meaning of rec a( x 1 , ... , x n). 1r . U n­ interpreted reasoning is achieved by using induction on the indices of approximations in order to prove state­ ments about recursive actions.

The language is referentially transparent with respect to variables. Side effects occur only on the level of re­ lations (states). This is reflected in the axiomatization which, in this aspect, is simpler than that of ordinary DL and close to that given in [Kautz, 1982].

The choose construct guesses a new element by chang­ ing the valuation (environment) that is used to evaluate the subsequent action. However, this change of environ­ ments as in the case of parameter passing follows a strict stack discipline, that is, the effect of choosing a new ele­ ment can not work outside the plan enclosed by "begin" and "end" . The choose construct is necessary to "move" in structures.

To be able to reason about these changes, we follow the approach taken in Dynamic Logic, in that we extend the predicate logic used so far by formulae [1r]cp and [?r(6, .. . , ~n)]cp, where r is a relation symbol and the ~; are either terms or "placeholders" e.

The formal semantics of this new type of formulas is given by

Intuitively, [1r]cp has to be read: "If 11' terminates, cp holds afterwards." The dual operator < 1r>, defined by < 1r>cp :+-+ ...,[ 11' ]...,cp has to be read: "1r terminates with cp." The (modal) operator [?- r(6, ... , ~n)] refers to all states that differ from the given one in at most the value of r, where some argument positions are fixed. For ex­ ample, [? - on( e, e] cp means that cp holds in all states that differ from the given one in at most the on-relation whereas [?-on( T1, Tn)]cp means that cp holds in all states that differ from the given one in at most the on-relation between the objects denoted by T1 and Tn . In ordinary DL, this is achieved by quantifying on program variables. A kind of "quantification" like the one above increases the expressive power of the formalism in general and is necessary for inductive proofs.

The axiomatization follows the paradigm of so-called uninterpreted reasoning, where we do not rely on the ex­ pressive power of the underlying data structure. The semantics and proof theory of recursive actions (plans) is outside the scope of this paper, however, a general introduction to uninterpreted reasoning, as it is imple­ mented in the KIV system, can be found in [Heisel eta/., 1989] . An axiomatization of a very powerful procedure concept for imperative programming languages is given in [Stephan, 1989]. Here we present only some axioms for the non-standard constructs.

As is the case with assignments in ordinary program­ ming languages, the effects of the add- and delete­ operations on first-order formulae can be described in an exhaustive way.

Theorem 2 Let cp be a formula such that all bound variables are distinct from the variables occurring in T1, ... , Tn . Then the weakest precondition (in the sense of [Dijkstra, 1976]} of cp with respect to delete-r( T1, .. . , Tn) and add-r( T1, ... , Tn) are the for­ mulae '{; and <p, respectively, where '{; results from cp by replacing all atomic subformulae

Analogous to the well known assignment axioms we have

In addition to that, uninterpreted reasoning requires ax­ ioms like:

[choose x begin 11' end]cp +-+ 'v'y . [1r~]cp ,

where y is a fresh variable. The axioms for the simple structured commands are as usual. Examples for general (modal) axioms are

where x must not occur free in 11', and

where Tis free for x in cp, and cp; denotes the substitution ofT for all free occurrences of x in cp.

4 Actions and Plans

We are now going to outline how planning domains can consistently be defined in our theory. In section 6 we will discuss briefly the technical aspects of a logic based shell for planning and the implemention of planning strategies within such a system. Our treatment of the frame prob­ lem will be discussed seperately. The main concern of this section is to demonstrate how basic actions can be defined in an abstract way and that domain constraints can be treated adequately.

There is no technical distinction between basic actions and derived plans composed out of them. The latter can be used without restriction as basic operations for higher levels of the planning process. However, we have to start out with some set of basic actions that are hand­ coded. The first step involves fixing the set of relation symbols we want to use. At the end of this section we will discuss how defined notions, like above in the blocks world scenario can be added to the theory.

The unstack operation, for example, can be defined as a simple abstraction run 0

In most applications, the state space is restricted by so­ called domain constraints. In the blocks world, for example, we have 'v'x (clear( x) +-+ -,3y on(y, x)) .

In our setting, domain constraints are treated as invari­ ants. For cp being the equivalence above, we can prove the assertion cp --> [run(x, y)]cp. If a similar assertion holds for all basic actions, we can use the domain con­ straint tp in all states reached by arbitrary plans made up of these basic actions, provided tp has been included in the description of the initial state. This fact can be proved formally in our setting.

The great advantage is that adding domain constraints in such a way guarantees consistency with the definition of the basic actions and, with that, consistency of the whole planning environment. Having deduced a set of domain constraints, we may also simplify the descrip­ tion of the basic actions to be used in the planning pro­ cess. From the definition given above, a sufficient ( ab­ stract) description of the unstack operation (in the style of [Kautz, 1982]) would be:

As another example, suppose we have a world where blocks have colours and let red, black, and white be the only colours that occur. An operator paintblack [Bibel et al., 1989] that changes the colour of any block to black is defined by the abstraction "Ypb

rec paintb(x) . add- black(x); delete- white( x); delete - red( x) .

If we can prove that the formula

Vx (red(x)Vblack(x)Vwhite(x)), stating that every block has exactly one of the three colours, is an invariant of all basic actions, then <"Ypb(x) > black(x) sufficiently describes our action.

Note that it is not necessary to specify adding or delet­ ing negative facts in our approach. So, even without the domain constraint above, -,white( x) as well as ...,red( x) can be proved to hold after the execution of "Ypb.

Definitions of basic actions can be more complex than those presented above. Using the choose construct we are able to define, for example, the non-deterministic dump operator [Kautz, 1982], that transfers all blocks from a certain box into another by

rec dump(x, y) . if 3 z in(z, x) then choose z begin if in(z, x) end else skip fi then add- in(z, y); delete- in(z,x); dump(x, y) else abort fi

and prove theorems about it .

The language introduced above can also 'be used to treat "recursively defined notions", like the above rela­ tion in the blocks world scenario. This kind of relations often causes problems in planning environments, see for example [Kautz, 1982]. Let "Yab be the recursive abstrac­ tion

Using this piece of program the relation above can be defined by

We are then able to prove lemmata like

where E is the set of domain constraints.

5 The Frame Problem

Considering the unstack-operation and analyzing its def­ inition reveals the fact that the only relations affected by unstack are table, clear, and on. This, in particular, means that unstack has no side effects on, for example, the colours of blocks. Thus,

appears to be a valid (frame) assertion. This observation leads us to an efficient treatment of the frame problem, which has the following proper foundation.

In our approach, the basic actions of a planning do­ main are defined as abstractions, the bodies of which in simple cases merely contain the elementary add- and delete-operations. From these definitions of basic ac­ tions, frame assertions can be inferred using uninter­ preted reasoning. Clearly, we have to use the basic ax­ ioms for the add- and delete-operations, respectively, in these deductions. In general, frame assertions are of the form

where the condition f consists of inequalities. In fact, another frame assertion for the unstack:-operation would be:

Of course, the frame assertions can be proved for com­ plete plans as well.

One main advantage of our approach, however, is that a comprehensive subset of valid frame assertions can be obtained in a non,.deductive way by. an algorithm that analyzes the syntactical str.ucture of plans. Assertions generated by this algorithm can be proved in a uniform way, that is, we can provide a proef procedUre (tactic in KIV) that automatically generates a proof for each such assertion. We shall, now outline the basic ideas: underllf­ ing tihis algerit:hm.

In order to formulate the genetal method for. comput­ ing sound frame· asserti0ns (for general plans)., we have to analyze the semantics of our planning language. It turns out that for each plan 1r and each relation symbol r, the formal execution tree of 1r contains only a finite number of different applications of the elementary op­ erations .. - r( .. . ), if we do not take into account those arguments that are program variables bound by a choose construct. In such a generalized 'call' .. - r( f1 , .. . , fn), we write f; = 0, iff; is such an argument . Let Ra(1r, r) and Ra ( 1r, r) denote the set of all applications of elemen­ tary add- and delete-operations that are reachable by 1r, respectively. Using this notation we get the following result .

Theorem 3 For each 1r and each relation symbol r the following implications are provable in our axiornatization

Clearly, the extensive use of the choose construct re­ duces the number of computed frame axioms . All cases not covered by these computed frame axioms have to be proved in a non-uniform way.

6 Implementation

Although this paper is mainly devoted to the presen­ tation of our theory, we will shortly describe how a logic based planning environment can be implemented within an (existing) tactical theorem proving system. The paradigm of tactical theorem proving seems to be especially well suited to the kind of environment we have in mind (see also [Guinchiglia et al., 1992]). Based on a general logical framework, derived rules and tactics can be defined and are then used to implement efficient planning strategies or other reasoning methods on plans.

Like many other systems in the area of tactical theo­ rem proving the KIV system is based on a sequent cal­ culus. Program (plan) synthesis, [Heisel et al., 1991], is supported by so-called meta variables. Given plan­ ning problems by sets of formulae r and Ll, we start with the goal E, r => <?a > !\ Ll , and instantiate the metavariable ?a during a goal-directed (backward­ chaining) proof. E is the set of domain constraints. Strategies like progression and regression ( cf. [Kautz, 1982]) can easily be implemented on the basis of a set of suitable derived rules and tactics. For example, our treatment of domain constraints can be implemented by a derived scheme like E => [1r] !\E. These strategies can use the "computed" frame assertions to determine the invariant part of a pre- or postcondition.

In this way, we obtain considerable efficient implemen­ tations that can be easily changed, extended, and com­ bined and that are guaranteed to be sound with respect to the basic formalism.

7 Related Work

Rosenschein and Kautz were the first using Dynamic Logic in planning [Rosenschein, 1981; Kautz, 1982].

They define basic actions as atomic constituents of their planning language that are axiomatized freely by de­ scribing their preconditions and effects, respectively. Our approach goes beyond this by providing a STRIPS­ like way of defining basic actions and setting up con­ sistent planning scenarios on top of that . The logical formalism is extended to reason about these basic ac­ tions as well as about composite plans built out of them. In both cases this includes recursive definitions.

With the work of Pednault [Pednault, 1986; Pednault, 1989] the approach we presented in this paper shares the idea of describing basic actions in a STRIPS-like manner, that is, by giving add and delete lists for rela­ tions. Moreover, both approaches embed these descrip­ tions into a logical formalism that can be used to rea­ son about plans. We begin with the observation that the appropriate semantical background for integrating this STRIPS approach into deductive planning are mod­ els based on finitely generated relations. While ADL uses a fixed form of conditional add and delete lists our approach allows to program basic operations in a carefully chosen programming language that covers ADL schemata in a straightforward way. In our approach it is easy to add non-determinism and also in the determinis­ tic case we can do without auxiliary relations which seem to be necessary in ADL to describe more complicated actions . In our setting we start out with the definition of basic actions. The defining programs always have a precise meaning in the underlying semantical structures. From these definitions which in addition are independent of each other we then prove domain constraints, derived descriptions, and frame assertions. These issues are not addressed in the ADL work. In addition, we have out­ lined a method to generate certain frame assertions even for composite plans by a purely textual analysis. Al­ though many ideas presented above are independent of the logical basis we want to stress that the ability to rea­ son about the structure of (possibly) recursive definitions (programs) is essential in this context.

As already mentioned above, our formalism is based on the STRIPS ideas that have been given formal semantics by Lifschitz [Lifschitz, 1986]. We feel that our formalism in some sense "proceduralizes" Lifschitz's approach and extends it in some way; e.g. as far as the treatment of negative effects etc. is concerned. However, investigating this relationship in more detail goes beyond the scope of this paper. Separate work will be devoted to that issue.

8 Conclusion

Combining characteristic features of conventional plan­ ning with techniques borrowed from programming logics, we have introduced a new theory of action based on a special variant of Dynamic Logic. Plans may be con­ structed using rich control structures including recur­ sion, non-deterministic branching, and a special choose construct. In our approach, we start out by the defini­ tion of basic actions and are then able to prove prop­ erties about the state space generated by these actions. This includes frame assertions and domain constraints. In this way, we prevent our planning environment from running into inconsistencies. These are possible in other systems where frame assertions and domain constraints are considered to be axioms. An efficient treatment of the frame problem is provided by a method to generate most frame assertions non-deductively (with the possi­ bility of a uniform formal proof within the system) . Our theory of action clearly is not restricted to blocks-world­ type planning domains. One could equally well define a theory for an intelligent help system context where the planning domain is a command language environment . There the ability of reasoning about recursive plans is essential. Implementing our logical framework in the KIV system provides the basis not only for a deductive planning system, but also for a complete deductive plan­ ning environment, i.e., a system that also assists a user in developing a consistent axiomatization of his plan­ ning domain. Furthermore, this notion of environment can be extended by implementing tactics for temporal projection, plan validation and other reasoning methods. Further work is devoted to the automated generation of recursive plans and an extension of the logical framework to parallelism.