System Assistance in Structured Domain Model Development

1 Introduction

As soon as we aim at using planning systems in the con­ text of realistic applications, the task of generating the underlying domain model becomes increasingly crucial. It is not only difficult to overlook the great amount of object types, relations, and actions involved when speci­ fying such a model. It is also difficult to keep consistency in mind, which is of particular importance if the applica­ tion domain is a safety-critical one. Consequently, sys­ tem assistance in constructing safe models of complex planning domains would be of real help.

Our work is motivated by the experiment of using a de­ ductive planning system in the simulation of a safety­ critical application, namely a chemical warehouse. This planning domain is quite complex and it has turned out that the construction of a clearly structured, adequate, and consistent model would have been almost infeasi­ ble if done without any system support. The reason is that specifying a complex planning domain is an iterative process which includes frequent modifications of already specified parts and attempts to extend parts and finally put them together.

*This work has partly been supported by the Federal Min­ istry of Education, Science, Research, and Technology under grants ITW 9404 and ITW 9600.

In this paper, we introduce a domain modeling tool (DMT) that supports users in the incremental and mod­ ular development of safe, i.e. provably consistent, mod­ els of planning domains. It relies on the concept of systematic domain model construction proposed by [Bi­ undo and Stephan, 1996] : This approach- based on a modal temporal logic- considers domain models as for­ mal structures. Domain models consist of signatures, action definitions, and domain constraints. The well­ defined operations of union, extension, and refinement allow for building complex domain models out of already existing simpler ones. We have improved this domain modeling concept in order to make it really useful for practical applications. We have introduced the notion of static constraints, in addition to domain constraints and have extended the operations on models . These improve­ ments grew out of a large case study, which- in a some­ what simplified version- is used as the example domain throughout this paper. Based on the modified concept, we have implemented the DMT system that supports the process of domain modeling. It does syntactic anal­ yses of domain specifications given by a user and has a deductive component which automatically performs the proofs necessary to guarantee both the consistency of single models and the safety of the union, extension and refinement operations . Finally, we have used the system for modeling a complex, safety-critical planning domain.

The paper is organized as follows. In Section 2 we give a short introduction into the basic temporal logic formal­ ism on which the domain modeling process relies. Our formal concept of domain model development and the domain modeling tool that implements this concept are presented in Section 3. We give an overview of the chem­ ical warehouse planning domain CHEW in Section 4 and demonstrate the structured development of a CHEW do­ main model by means of examples in Section 5.

2 The Logical Setting

The logical representation formalism is a subset of the temporal planning logic TPL introduced in [Stephan and Biundo, 1996). We extend this formalism by the concept of nondeterministic (random) assignments, but do not consider recursive actions or plans. TPL is an interval­ based modal temporal logic. It relies on a many-sorted first-order language that provides flexible and rigid func­ tion and relation symbols. The modal operators in­ clude 0 (weak next) , 0 (strong next), D (always) , 0 (sometimes), and the binary operator ; (chop). TPL formulae are interpreted over intervals. Intervals a are nonempty sequences of states (a=<a1,a2 .. . > ). States (J; are interpretations of the flexible symbols. A first­ order formula ¢ holds in an interval a iff it holds in the first state of that interval. Ot.p holds in a iff a is a single-state interval (a=<a1 >) or t.p holds in the greatest proper suffix of a (which is <a2' ... >). 0 false means that there exists no such suffix. An interval a satisfies 0t.p iff a is not a single-state interval and sat­ isfies Ot.p, i.e., a has a greatest proper suffix that sat­ isfies t.p. Dt.p and 0 t.p hold in a iff t.p holds in every suffix of a and iff there exists a suffix of a that satis­ fies t.p, respectively. The chop-operator is interpreted as the sequential composition of formulae: t.p ; 'lj; holds in a= <a1 , a2 , .. . , an , . . . > iff either a is infinite and sat­ isfies t.p or a can be split into two successive intervals u'=<al , a2, .. . 'an> and a"=<an, .. . >- which overlap in one state- such that u' satisfies t.p and a 1 ' satisfies 'lj;.

In addition to these modalities, a programming lan­ guage is embedded in TPL. This programming language is used to specify the effects of basic actions. It provides elementary operations add- .. , delete- .. , and := (up­ date), which represent single-step transitions described by 0 . As for control structures , ; is used as sequential composition and the following axioms are given.

Actions are defined by expressions like a(x1 , . .. ,xn) <== 1r, where 'a' is the action name, (x1 , ... ,xn) are the param­ eters , and 1r is a program. Programs are built using elementary operations, action calls a(x1 , . . . ,xn) <== 1r (t1 , .. . , tn) , and control structures. Programs are TPL formulae. In general, these programs are used to de­ scribe not only actions but also composite plans.

The elementary operations are characterized by axioms 1 , like

1 We refer to these as the "wp-axioms" .

where r (f) is a flexible relation (function) symbol and x : z is a fresh variable of type z . f( .. . ) :=? : z repre­ sents the random assignment. ¢is the formula resulting from the first-order formula ¢ by replacing each occur­ rence of the atomic subformula r(s1 , ... , sn) by ((t1 f. S1 V ... V tn :f: sn)-+ r(sl , ... ,sn)) and ¢results from¢ by replacing j (s 1 , .· . , sn) = s by ((J(sl , . . . , Sn) = S 1\ (xl :f: S1 V ... V Xn :f: Sn)) . ¢ and ¢ are the weakest preconditions of ¢ w.r.t. the respective elementary operation 2 . Please note that el­ ementary operations describe single state transitions, whereas actions and plans are composed of many of them using the chop-operator , thereby specifying intervals of arbitrary length.

Finally, for action calls we have the equivalence 3

3 The Domain Modeling Tool

In [Biundo and Stephan, 1996), we proposed a formal concept for the construction of provably consistent plan­ ning domain models. It provides well-defined operations on models that allow for the structured and incremental development of domain models by combining and ex­ tending already existing ones in a sound manner. We extend this concept by introducing the notion of static constraints and by extending the refinement operation in a way such that also abstract relations can be "imple­ mented" by concreter ones.

A domain model M is a data structure <Z, Sig, SC, DC, A>, where Z is a set of sort symbols , Sig is a signature, SC and DC are sets of static constraints and domain constraints, and A is a set of action definitions. SC and DC consist of first-order formulae , whereby only rigid symbols" are allowed in SC. Static constraints serve to describe unchangeable domain features, whereas domain constraints reflect essential changeable facts that nev­ ertheless have to hold in each situation. Domain con­ straints therefore contain flexible symbols. A domain model is consistent if it is syntactically sound (i.e. sym­ bols are used in a unique way and terms and formulae are well-formed) and if each domain constraint is invari­ ant against each action (i.e. it holds after the execution of an action iff it has held before). Please note that the latter trivially holds for static constraints.

Operations on domain models are union, extension, and refinement. The operations are safe. They guarantee that only consistent models develop, given consistent ones as input.

2 The wp-axioms for ordinary assignments and the delete operation are omitted, due to lack of space.

3 x (t) denotes a vector of variables (terms) .

Union . (1±1) combines two domain models M1 and M2, provided:

• Z1, Sig1 and Z2, Sig2 agree on common sorts, i.e.: common sorts are identical w.r.t. subsort and supersort relationships and the signatures match w .r.t . symbols ranging over common sorts.
• Actions from A1 UA2 that use function and relation symbols from both Sig1 and Sig2 are in A1nA2.
• Formulae from SC1USC2 (DC1UDC2) that use func­ tion and relation symbols from both Sig1 and Sig2 are in sc1nsc2 (DC1nDC2).

M11±1M2:=<Z1UZ2, Sig1 EBSig2, SC1USC2, DC1UDC2, A1UA2>, where EB denotes the union of signatures. The consistency of M11±1M2 is given by the consistency of M1 and M2. In particular , the invariance of DC1-DC2 (DC2DC1) against the actions A2 (A1) is guaranteed as these actions and formulae have no symbols in common.

Extensions (6) add new sorts, symbols, actions, or con­ straints to a model M = <Z, Sig, SC, DC, A> . Let E = <Ze, Sige, SCe, DCe, Ae>· M can be extended byE if:

• Z and Ze agree on common sorts.
• Sig and Sige have no symbols in common.
• Ae are action definitions over SigEBSige.
• SCe and DCe are constraints over SigEBSige.

ML".E:=<ZUZe, SigEBSige, SCuSCe, DCuDCe, A'UAe>, where A' results from A by extending (some) action defi­ nitions by parts that change only symbols from Sige and also by perhaps restricting their applicability. In order to guarantee consistency of ML".E (given that M and E are consistent), it has to be proved that the actions A' (Ae) are invariant against DCe (DCUDCe)·

Refinements (\7) allow for the replacement of abstract scenarios by more concrete ones. Let M be given. In a first step M is extended by some E yielding ML".E, like above. In particular this means that some of the previous actions a are extended to a'. In addition to that there are completely new actions using only sym­ bols from Sige.

In a second step we want to forget about some of the previous symbols and actions. In a sense these sym­ bols and also some of the actions using them will be implemented in terms of new concepts which in turn means that facts about the abstract scenario are pre­ served in a somewhat modified form. Let the symbols we want to implement (and then forget about) be given by SigJ and let RP = {Vx(r(x) +-* <Pr) I r E Sig 1 } U {Vxy(f(x) = y +-* ¢J) If E Sig 1 }, where the <Pr (¢J) are first-order formulae not containing symbols from Sig/. The formulae in RP have to be proved to be invariants of the actions in ML".E. However, some of the actions in A' shall no longer be available on the concrete level , i.e. in the refined model. These are given by A1 ~A'. We then replace atomic formulae containing the symbols from Sig/ in each constraint ¢ of ML".E by the equivalences given in RP. This can be done by a straightforward algorithm. Let ¢* be the formula resulting from ¢ after this step. For an action a the transformed version a· is obtained by translating the tests in the way described above and by removing all elementary operations that affect symbols from Sig/. If function symbols from Sig1 occur in arguments of the remaining elementary opera­ tions, these have to be eliminated by using the choose construct. We end up with a set of actions (A'-AJ)*. The refinement finally is (ML".E) \7 <SigJ ,RP,AJ>:= <ZUZe, (SigEBSige)-Sigf, (SCUSCe)*, (DCUDCe)* ,(A'­ AJ)*UAe>.

Based on this formal concept of domain model con­ struction, we have implemented a deduction-based do­ main modeling tool (DMT) that supports the modeling process by carefully analyzing an user's inputs and by au­ tomatically performing the necessary proofs . The system has components for both syntactic analysis and deduc­ tion. Syntactic analysis guarantees well-formedness of terms and formulae and proves that no flexible symbols occur in static constraints and that no rigid symbols are manipulated by update-, add-, or delete-operations. In order to prevent the user from specifying an action that causes undesired effects or no effects at all, the system does the following analysis in addition. It checks the pre­ condition and body of each action. If it detects flexible terms in the precondition that are identical with terms being manipulated in the action body, it tries to prove that the values they have before and after the action ex­ ecution differ. This is done by the deductive component of DMT which tries to derive this fact from the pre­ conditions, using the static constraints and the domain constraints. The deductive component is an automated theorem prover for TPL.

4 The Chemical Warehouse Scenario

The chemical exchange warehouse (CHEW) was devel­ oped at the Hazardous Waste Management Division (HWM) of the Lawrence Livermore National Lab 4 . The CHEW concept is part of a programme for the environ­ mentally sound, cost effective and legal management of chemical waste. It is devoted to the storage of excess usable chemicals, the resale of inquired substances, and the disposal of unsaleable ones. Dealing with danger­ ous materials, the chemical warehouse is a safety-critical environment. The HWM concept takes this fact into account by specifying a collection of safety conditions that must not be violated by anyone who acts in this environment. We have implemented a simulation of the CHEW warehouse (cf. Figure 1) where- in contrast to what the HWM concept says- we assume that a robot is used for the transportation of barrels. Barrels containing chemicals are delivered at the ramp. First, the barrels are proved and their content is analyzed. The barrels are then stored in suitable cells from where they can be retrieved as soon as respective inquiries have been sub­ mitted. A deductive planning system is used to generate plans that enable the robot to act safely in this (simu­ lated) environment by executing provably correct plans that in particular meet the required safety conditions .

4 http://www.llnl.gov /es_and_h/hwmJwme/hwm.html

As a prerequisite for using our planning system, we had to set up a model of this domain. In order to obtain a suitable and consistent, comprehensive model we have constructed a development tree using the DMT domain modeling tool. This tree reflects how separate parts of

the model have been specified, flexibly extended and re­ fined, and finally tied together. Figure 2 shows a (sim­ plified) part of this development tree and Section 5 gives some detailed examples on the development steps.

5 A Structured Domain Model Development

We start developing the CHEW model by first speci­ fying some basic components of the warehouse building and its equipment . There are rooms, doors , and a robot . The rooms are connected by doors and the robot is able to move from one room to another. We set up a do­ main model MI = <ZI, Sigi, SCI , DCI, AI >, where Z1 = {room , door , robot}. The signature Sig1 consists of Rr={ connects(door,room,room) } , F t={ in-rrobot-+roam}, Fr={rob-+robot }; Rt={}. There is only one robot sup­ posed to be in our scenario; it is denoted by a constant . We have two static constraints saying that a door con­ nects two different rooms, and that the connects rela­ tion is symmetric w.r.t. the room arguments: scl {\ld,rl, r2(connects(d,r1,r2) -t r1 of. r2),

\ld, r 1, r2 (connects ( d, r1, r2) H connects( d, r2, rl) ) } . As the TPL representation formalism allows for the use of flexible function symbols , we are able to repre­ sent unique relations like in-r by functions. This pre­ serves us from specifying and maintaining a domain con­ straint explicitely stating the uniqueness of in-r, namely \lr1,r2((in-r(rob,rr) 1\ in-r(rob, r2 )) -t r1 = r2) . Fi­ nally, we define an action that allows the robot to move from one room to another: A1 consists of

move(r1 :room, r2 :room) ¢= choose d : connects(d, r1, r 2) begin if in-r(rob) = ri then

in-r(rob) := r 2 else skip fi. end

As already explained in Section 3, the DMT tries to prevent the user from specifying an action that causes undesired effects or no effects at all. In our example, the system detects a flexible term in the precondition of 'move' that is changed in the action body, namely in­ r(rob). Therefore, it tries to derive the unequality of the respective values from the preconditions using the static constraints: SC 1- \1 r 1, r2, d ( (connects( d, r1, r2) 1\ in­ r(rob) = rl) -t r1 of. r2). The system succeeds with this proof as the first static constraint in SC states that the rooms connected by a door are different. This way, static constraints serve to keep certain (static) facts out of preconditions which helps to make action definitions simpler.

In a second step, we concentrate on the treatment of chemicals in our warehouse scenario. We specify the re­ spective objects and, among others, an action that rep­ resents the analysis of the content of a delivered barrel. The analysis process is modeled on an abstract level , be­ cause in reality it is carried out by a human. Thus , the analysis device is considered to be a black box. In or­ der to analyze its content a barrel has to be put in the device. After the analysis process the barrel is put out and has a color mark indicating the type of chemical it contains ( cf. Figure 3) .

We set up the domain model M2 = <Z2, Sig2, SC2, DC2, A2>, where Z2 = {barrel , color , dejault.color , new.color , device }. Here, we have a hierarchy of sorts. color has two subsorts: dejault .color and new.color.

Sig2 consists of Rt={ in( barrel), out(barrel), clear­ in( ) , clear-out( ) } , Rr={}, F 1 ={paintbarrel-+color}, and F r= { dev-+device, blue-+new.color, red-+new. color, green-tnew.color, yellOW-tnew.color, grey-tdefault .color} · As static constraints we have that different constant symbols denote different objects, also known as unique name assumption. In order to correctly model our plan­ ning domain, we have to make sure that the model re­ flects essential properties of that domain, like "a bar­ rel cannot be located at the input- and output position of the device at the same time" . Therefore, suitable domain constraints are introduced. We have DC2 = { Vb' -,(in(b') 1\ out(b')), clear-in +-+ -,:J b in(b), clear­ out +-+ -,:J b out(b)}. The analysis action is defined as follows.

analyze(b:barrel) ¢::

As we proceed on the assumption that the content of a barrel is not known unless it has been analyzed, the action is formulated as a nondeterministic one. It as­ signs an "unknown" value? to paint(b). As one effect of this action, we have that there exists an object of type new.color that equals paint(b). In addition, we have ac­ tions for loading and unloading the device. 'load', for example, reads:

load(b:barrel) ¢::

if clear-in then

delete-clear-in ; add-in( b) else skip fi

During the specification of M2, DMT provides type checks and proves syntactical soundness of terms and formulae. In addition, it has to process the domain con­ straints. This means, the domain constraint

of DC2 has to be proved invariant against 'analyze', for example. To do so, the system generates the invariance assertion 5 :

(<p 1\ analyze(b)) -+ 0 (0 false 1\ <p) stating: If <p holds in a state where we execute 'analyze', then we end up in a state where <p holds again.

5 analyze(b) abbreviates the action call analyze(b:barrel) ¢:: 1r (b) , the variable b being the actual parameter.

In order to prove this formula, the system first ap­ plies the axioms for control structures given in Section 2. Then it iteratively computes weakest preconditions of <p w.r.t. the elementary operations in the body of 'ana­ lyze', using the wp-axioms. As a result it obtains the first-order implication

Vb ((Vb' -,(in(b') 1\ out(b')) 1\ in(b)) -+

Vb' -,(in(b') 1\ bi-b' 1\ out(b'))).

It is easy to see, that this formula can be simplified to true.

In the next step, we want to combine M1 and M2, thereby introducing the concepts of barrels and their analyses into the model of the building. The combina­ tion of these models is achieved by applying the union operation for models. The prerequisites for this opera­ tion are obviously satisfied : The models have no sorts in common and with that differ also in signatures, actions, and constraints. We obtain M3 = M1 l±J M2, where Z3 = z1 u z 2, Sig3 = Sig1 EB Sig2, sc3 = sc1 u sc2 , DC3 = DC2, and A3 = A1 u A2.

Now, we extend M3 by modeling the transporta­ tion of barrels using the robot. We define the ex­ tension E = <Z3, Sig, {}, DC, A>. Sig has the flexible symbols: Rt={held(barrel)> handempty( )} and F 1 = { in-bbarrel-+room} . There are no static constraints, but three domain constraints: DC = {handempty +-+ -,:J b held(b),

Vb (held(b) -+ in-r(rob) = in-b(b)) ,

V b1,b2 ((held(bi) 1\ held(b2)) -+ b1 = b2)} . Note that we have used a flexible relation symbol for the unique relation held, in contrast to what has been done in the cases of in-r and in-b and at the cost of needing a do­ main constraint explicitely stating the uniqueness. The reason is that using a flexible function symbol instead (describing the held property by formulae like held=b) would have required the int roduction of a so-called error element, like empty-barrel , in order to express the fact that nothing is held by the robot. This in turn would have required an expensive exception handling in the body of actions that manipulate barrels, like case analy­ ses of the form if b i- empty-barrel then ... else skip. A contains the actions for picking up and putting down barrels. 'pickup' reads:

pickup(b : barrel) ¢::

The DMT syntax check detects no errors and the sys­ tem also succeeds in proving the domain constraints DC invariant against 'pickup' and 'putdown'. Now we can extend M3 byE as the prerequisites of the extension op­ eration 6 are satisfied: The signatures are disjoint and A and DC are built over Sig3 EB Sig. We generate the extension M3 6 E = M4 where Z4 = Z3, Sig4 = Sig3 EB Sig, SC4 = SC3, DC4 = DC3 U DC, and A4 =A~ U A.

A3 results from A3 by inserting some expressions from Sig into the definition of 'move':

move(r1 : room,r2 :room) {::: choose d: connects(d, r1, r2) begin if in-r( rob) = r 1 then in-r(rob) := r2; choose b: held(b) begin in-b(b) := r 2 end else skip fi end

This modification is necessary, in order to get the second domain constraint of DC invariant against 'move'. With that, the system succeeds in performing the proof obli­ gations that guarantee safety of our extension, namely: DC3 are invariants w.r.t. A ('pickup' and 'putdown' ma­ nipulate only symbols from Sig) and DC are invariants w.r.t. A3 ('analyze', 'load', and 'unload' do not affect symbols occurring in DC). So, M4 is accepted by the system.

Finally, we will show how our new model M4 is refined to a more concrete one by introducing the notion of loca­ tion that serves to represent the various positions inside the building at which movable objects, like barrels and the robot, could be located. This notion will enable the specification of "moving inside a room"' for example.

As described in Section 3, the operation of domain model refinement comprises extension as well as the elimination of actions and symbols. Assume we first extend M4 by some E = <Z, Sig, SC, DC, A>, where Z = {location} and among the rigid symbols we have entrancedevice-+location' exitdevice-+location' and arealocation-+room· The flexible symbols include at­ rrobot-+location and at-bbarrel-+location· We add also ac­ tions for moving inside a room and for passing a door, respectively. After the extension step, we want to for­ get about the previous 'move' action of M4 as well as about the relations in and out, originating from M2 . Let RP contain the formulae V b (in(b) t-t at-b(b) = entrance(dev)) and V b (out(b) t-t at-b(b) = exit(dev)). It turns out that 'analyze' is among the actions of A4 that have to be modified in order to enable the invari­ ance proof of the RP formulae: We have to consider locations here:

analyze(b:barrel) {:::

if in(b) 1\ clear-out 1\ at-b(b) = entrance(dev) then delete-in(b) ; add-clear-in ; paint(b) :=? ; add-out(b) ; delete-clear-out ; at-b(b) := exit(dev) else skip fi

It is easy to see that the first formula of RP still cannot be proved to be invariant against 'analyze' unless we have added the state constraint entrance(dev) f:. exit(dev) . As can be seen (torn this example, the generation of sound models can be a tricky task, the deductive support of which is really useful. In this case an analysis of the failed invariance proof has helped us modifying the ex­ tension accordingly unless we ended up with a correctly refined domain model.

6 Related Work and Conclusion

The question of knowledge acquisition and knowledge base maintenance for planning has hardly been ad­ dressed in the literature. Recently, [Chien, 1996] has in­ troduced an approach to the analysis of planning knowl­ edge bases. This mechanism detects goals that are not achievable by actions and supports the user in detecting modeling errors by allowing the generation of automati­ cally completed plans. In the work of [Cesta and Oddi, 1996], a formal domain description language has been proposed, which is especially well suited for the descrip­ tion of physical planning domains. This approach also considers domain model construction based on a formal semantics.

In this paper, we have introduced the domairi mod­ eling tool DMT that assists users in the modular and structured development of verified domain models. It provides well-defined operations for the extension, re­ finement, and combination of existing models and au­ tomatically performs the proofs that are necessary to guarantee the safety of these operations.

Although our system uses the TPL planning logic, DMT can easily be adapted- by restricting the logical language- to construct safe domain models for operator­ based planning systems that rely on different formalisms; examples being systems using STRIPS-like operator de­ scriptions or systems based on ADL, like UCPOP [Pen­ berthy and Weld, 1992].