M. Fox and D. Long

Volume 9, 1998

**Links to Full Text:**

- PDF format
- PS format
- Appendix - TIM code and examples

As planning is applied to larger and richer domains the effort involved in constructing domain descriptions increases and becomes a significant burden on the human application designer. If general planners are to be applied successfully to large and complex domains it is necessary to provide the domain designer with some assistance in building correctly encoded domains. One way of doing this is to provide domain-independent techniques for extracting, from a domain description, knowledge that is implicit in that description and that can assist domain designers in debugging domain descriptions. This knowledge can also be exploited to improve the performance of planners: several researchers have explored the potential of state invariants in speeding up the performance of domain-independent planners. In this paper we describe a process by which state invariants can be extracted from the automatically inferred type structure of a domain. These techniques are being developed for exploitation by STAN, a Graphplan based planner that employs state analysis techniques to enhance its performance.

Journal of Artificial Intelligence Research 9 (1998) 367-421 Submitted 7/98; published 12/98 The Automatic Inference of State Invariants in TIM Maria Fox Derek Long Department of Computer Science University of Durham, UK maria.fox@dur.ac.uk d.p.long@dur.ac.uk Abstract As planning is applied to larger and richer domains the effort involved in constructing domain descriptions increases and becomes a significant burden on the human application designer. If general planners are to be applied successfully to large and complex domains it is necessary to provide the domain designer with some assistance in building correctly encoded domains. One way of doing this is to provide domain-independent techniques for extracting, from a domain description, knowledge that is implicit in that description and that can assist domain designers in debugging domain descriptions. This knowledge can also be exploited to improve the performance of planners: several researchers have explored the potential of state invariants in speeding up the performance of domain-independent planners. In this paper we describe a process by which state invariants can be extracted from the automatically inferred type structure of a domain. These techniques are being developed for exploitation by stan, a Graphplan based planner that employs state analysis techniques to enhance its performance. 1. Introduction Stan (Long & Fox, in press) is a domain-independent planner based on the constraint satisfaction technology of Graphplan (Blum & Furst, 1995). Its name is derived from the fact that it performs a variety of pre-processing analyses (STate ANalyses) on the domain description to which it is applied, that assist it in planning efficiently in that domain. Stan took part in the aips-98 planning competition, the first international competition in which domain-independent planners were compared in terms of their performance on well-known benchmark domains. Of the four planners that competed in the strips track, three were based on the Graphplan (Blum & Furst, 1995) architecture. The most important difference between stan and the other Graphplan-based planners was its use of state analysis techniques. Although these techniques were not, at that stage, fully integrated with the planning algorithm stan gave an impressive performance as can be determined by examination of the competition results. There is a description of the competition, its objectives and the results, at the aips-98 planning competition FTP site (see Appendix A). One of the most important of the analyses performed by stan is the automatic inference of state invariants. As will be described in this paper, state invariants are inferred from the type structure of the domain that is itself automatically inferred, or enriched, by stan. The techniques used are completely independent of the planning architecture, so can be isolated in a pre-processing module that we call tim (Type Inference Module). Tim can be used by any planner, regardless of whether it is based on Graphplan or on any other underlying cfl1998 AI Access Foundation and Morgan Kaufmann Publishers. All rights reserved. Fox & Long architecture. Tim has been implemented in c++ and executables and examples of output are available at our web site (see Appendix A) and in Online Appendix 1. Tim takes a domain description in which no type information need be supplied and infers a rich type structure from the functional relationships between objects in the domain. If type information is supplied tim can exploit it as the foundation of the type structure and will often infer an enriched type structure on this basis. State invariants can be extracted from the way in which the inferred types are partitioned. The consequence is that the domain designer is relieved of a considerable overhead in the description of the domain. Whilst it is easy to hand-code both types and state invariants for simple domains containing few objects and relations, it becomes progressively more difficult to ensure cross-consistency of handcoded invariants as domains become increasingly complex. Similarly, the exploitable type structure of a domain may be much richer than can easily be provided by hand. We have observed that tim often infers unexpected type partitions that increase the discrimination of the type structure and provide corresponding benefits to stan's performance. We therefore see tim as a domain engineering tool, helping to shift the burden of domain design from the human to the automatic system. The usefulness of both types and state invariants is well-documented. Types have been provided by hand since it was first observed that they reduce the number of operator instantiations that have to be considered in the traversal of a planner's search space. The elimination of meaningless instantiations is particularly helpful in a system such as Graphplan, in which the structure to be traversed is explicitly constructed prior to search. We believe that the benefits to be obtained from type inference in planning are similar to those obtained in programing language design: type inference is more powerful than type checking and can assist in the identification of semantic errors in the specification of the relational structure of the domain. Indeed, we have found tim to be a useful domain debugging tool, allowing us to identify flaws in some published benchmark domains. We also used tim to reveal the underlying structure of the Mystery domain, a disguised transportation problem domain, used in the planning competition. The Mystery domain is described in Appendix C.2. The use of domain knowledge can significantly improve the performance of planners, as shown by a number of researchers. Gerevini and Schubert (1996a, 1996b) have considered the automatic inference of some state constraints and demonstrated that a significant empirical advantage can be obtained from their use. Kautz and Selman (1998) have handcoded invariants and provided them as part of the domain description used by Blackbox. They demonstrate the performance advantages obtained and acknowledge the importance of inferring such invariants automatically. McCluskey and Porteous (1997) have also demonstrated the important role that hand-coded state invariants can play in domain compilation for efficient planning. Earlier work by Kelleher and Cohn (1992) and Morris and Feldman (1989) explores the automatic generation of some restricted invariant forms. We discuss these, and other, related approaches in section 5. In this paper we will describe the type inference process employed by tim and explain how four different forms of state invariant can be extracted from the inferred type structure. We will argue that tim is correct since it never infers sentences that are not state invariants. We will then provide experimental results demonstrating the performance advantages that can be obtained by the use of types. 368 Automatic Inference of State Invariants fuelled 1 unfuelled 1 at 1 at in load unload drive drive 1 1 Figure 1: A simple transportation domain seen as a collection of FSMs. 2. The Type Inference Module One way of viewing strips (Fikes & Nilsson, 1971) domains is as a collection of finite-state machines (FSMs) with domain constants traversing the states within them. For example, in a simple transportation domain there are rockets and packages, with rockets being capable of being at locations and of moving, by driving, from being at one location to being at another, and of being fuelled or unfuelled, and of moving between these two states. at can be seen as forming a one-node FSM, and fuelled and unfuelled as forming a two-node FSM. This view is depicted in Figure 1. 369 Fox & Long Packages can be at locations or in rockets, and can move between these states in the resulting two-node FSM. In this example, rockets can be in states that involve more than one FSM, since they can be both at and fuelled, or at and unfuelled. STRIPS domains have been seen in this way in earlier work (McCluskey & Porteous, 1997; Grant, 1996), as discussed in Section 5. 2.1 Types in TIM When two objects participate in identical FSMs they are functionally equivalent and can be seen to be of the same type. The notion of type here is similar to that of sorts in the work of McCluskey and Porteous (1997). A primary objective of the tim module is to automatically identify the equivalence classes that form the primitive types in a domain description and to infer the hierarchical type structure of a domain on the basis of the primitive types. The way this is done is discussed in Section 2.3. The primitive types are functional equivalence classes, and the objects of the domain are partitioned into these classes. Having identified the types of the domain objects tim infers the types of the parameters of all of the operators. State invariants are inferred as a final stage. The early parts of this process rely on three key abstract data types, the property space, the attribute space and the transition rule. Formal definitions of these components are provided in Section 2.3, but we provide informal descriptions here to support the following definitions. Transition rules represent the state transformations that comprise the FSMs traversed by the objects in the domain. Property spaces are FSMs, together with the objects that participate in them, the properties these objects can have and the transition rules by which they can acquire these properties. Attribute spaces contain collections of objects that have, or can acquire, the associated attributes. Attributes differ from properties because they can be acquired, or lost, without the associated loss, or acquisition (respectively), of another attribute. Attribute spaces also contain the transition rules that enable the acquisition (or loss) of these attributes. Once the state and attribute spaces have been constructed we assign types to the domain objects according to their membership of the property and attribute spaces. Any two objects that belong in identical property and attribute spaces will be assigned the same type. It is therefore very important to ensure that the property and attribute spaces are adequately discriminating, otherwise important type distinctions can be lost. Much of the subtlety of the algorithm described in Section 2.2 is concerned with maintaining adequate discrimination in the construction of these spaces. We present the following definitions here to support our informal characterisation of the roles of types in strips and in tim. The definitions are used again in Sections 2.4 and 2.6, which discuss how types are assigned to objects and operator parameters. Definition 1 A type vector is a bit vector in which each bit corresponds to membership, or otherwise, of a unique state or attribute space. The number of bits in the vector is always equal to the number of distinct state and attribute spaces. Definition 2 A type is a set of domain objects each associated with the same type vector. Definition 3 A type vector, V1, in which two distinct bits, si and sj, are set corresponds to a sub-type of the type associated with a vector, V2, in which only si is set (all other settings 370 Automatic Inference of State Invariants being equal). Then the type associated with V2 can be seen to be a super-type of the type associated with V1. Definition 4 A type structure is a hierarchy of types organised by sub-type relationships between the component types. Definition 5 A type structure is adequately discriminating if objects are only assigned to state (and attribute) spaces that characterize their state transitions (and attributes). Definition 6 A type structure is under-discriminating if it fails to distinguish types that are functionally distinct. Definition 7 A type structure is over-discriminating if functionally identical objects are assigned to different types. There are two distinct ways in which types play a role in the specification of a domain. They can restrict the set of possible operator instances to eliminate all those that are meaningless in the domain and hence improve efficiency by reducing the size of the search space, and they can eliminate unsound plans that could be constructed if they were not provided. The following examples clarify the difference between these two roles. The untyped schema: drive(X,Y,Z) Pre: at(X,Y), fuelled(X), location(Z) Add: at(X,Z), unfuelled(X) Del: at(X,Y), fuelled(X) permits more instances than the typed schema: drive(X,Y,Z) params: X:rocket,Y:package,Z:location Pre: at(X,Y), fuelled(X), location(Z) Add: at(X,Z), unfuelled(X) Del: at(X,Y), fuelled(X) but all meaningless instances will be eliminated during search because their preconditions will not be satisfiable. On the other hand, the typed schema: fly(X,Y,Z) params: X:aircraft,Y,Z:location Pre: at(X,Y) Add: at(X,Z) Del: at(X,Y) ensures that only aircraft can be flown, whilst the untyped schema: 371 Fox & Long fly(X,Y,Z) Pre: at(X,Y) Add: at(X,Z) Del: at(X,Y) allows flying as a means of travel for any object that can be at a location, including packages, and other objects, as well as aircraft. Tim is capable of automatically inferring all types playing the restrictive role indicated in the typed drive operator. However, tim cannot infer type information that is not implicit in the domain description. Thus, given the untyped f ly schema, there are no grounds for tim to infer any type restrictions. Tim will draw attention to unintended under-discrimination by making packages and aircraft indistinguishable at the type level, unless there is distinguishing information provided in other schemas. At the very least tim will make explicit the fact that packages are amongst those objects that can fly. This assists the domain designer in tracking errors and omissions in a domain description, but unstated intended distinctions cannot be enforced by tim. 2.2 An Overview of the TIM Algorithm Figure 2 gives a broad outline of the tim algorithm. A more detailed description is given in Appendix B. The role of each component of the algorithm is described, together with a commentary on discussing related issues and justifications, in Sections 2.3, 2.4 and 2.7. Broadly, tim begins with an analysis of the domain operators, extracting transition rules that form the foundations of the property and attribute spaces described previously. These rules are used to separate properties into equivalence classes from which the property and attribute spaces are constructed. Tim then analyses the initial state in order to assign the domain objects to their appropriate spaces. This analysis also identifies the initial properties of individual objects and uses them to form states of the objects in the property spaces. The initial states in a property space are then extended by the application of the transition rules in that space to form complete sets of states accounting for all of the states that objects in that property space can possibly inhabit. As described in Section 2.4, attribute spaces do not behave like FSMs, as property spaces do, and the extension of these is carried out by a different procedure: one that can add new objects to these spaces, rather than new states. Tim then assigns types to objects using the pattern of membership of the spaces it has constructed. Finally, tim uses the spaces to determine invariants that govern the behaviour of the domain and the objects in it. 2.3 Constructing the Transition Rules We begin by describing the process by which the transition rules are constructed. The following definitions are required. Definition 8 A property is a predicate subscripted by a number between 1 and the arity of that predicate. Every predicate of arity n defines n properties. Definition 9 A transition rule is an expression of the form: propertyLambda ) propertyLambda ! propertyLambda 372 Automatic Inference of State Invariants Construct base PRSs (Section 2.3) Split PRSs (Section 2.3) Construct transition rules (Section 2.3) Seed property and attribute spaces (Section 2.3) Assign transition rules (Section 2.4) Analyse initial state (Section 2.4) Extend property spaces (Section 2.4) Extend attribute spaces (Section 2.4) Identify types (Section 2.6) Construct invariants (Section 2.7) Figure 2: Outline of the tim algorithm. in which the three components are bags of zero or more properties called enablers, start and finish, respectively. The double arrow, ), is read enables and the single arrow, !, is read the transition from. So: E ) S ! F is read: E enables the transition from S to F. The properties in S are given up as a result of the transition. The properties in F are acquired as a result of the transition. The properties in E are not given up. If enablers is empty we write: start ! f inish If start is empty we write: Transition rule 1 enablers ) null ! f inish If finish is empty we write: Transition rule 2 enablers ) start ! null The bag null is the empty bag of properties. Its role is to emphasise that, in transition rule 1, nothing is given up as a result of the transition and, in transition rule 2, nothing is acquired. Rules that have a null start and a null finish are discarded because they describe null transitions. When the property bags contain more than one element they are separated by commas. The collection: pk; qm; ::: rn 373 Fox & Long is interpreted to mean that each of the properties in the collection can be satisfied as many times as they appear in the collection. The comma is therefore used to separate the elements of a bag. We use Phi to denote bag union, Psi to denote bag difference, Omega to denote bag intersection and v to denote bag inclusion. Definition 10 A Property Relating Structure (PRS) is a triple of bags of properties. The first stage of the algorithm constructs a set of transition rules from a set of operator schemas. Each operator schema is analysed with respect to each parameter in turn and, for each parameter, a PRS is built. The first bag of properties is formed from the preconditions of the schema, and the number used to form the property is the argument position of the parameter being considered. For example, if the precondition is on(X; Y ), and the parameter being considered is X, the property formed is on1. This bag, called precs, contains the enablers that will be used in the formation of the transition rules. The second bag, called deleted precs, of properties is formed from all of the preconditions that appear on the delete list of the schema (with respect to this same parameter). The third bag, called add elements, contains the properties that can be formed from the add list of the schema. The PRS contains no deleted elements component - it is assumed that every element on the delete list of a strips operator appears in the precondition list. This is a reasonable restriction given that strips operators do not allow the use of conditional effects. It is further assumed that every pair of atoms on the delete list of a schema will be distinct for all legal instantiations of the schema. This does not constitute a significant restriction since operator schemas can always be easily rephrased whenever this condition is violated. We now consider the process by which PRSs are constructed. Given the schema: drive(X,Y,Z) Pre: at(X,Y), fuelled(X), location(Z) Add: at(X,Z), unfuelled(X) Del: at(X,Y), fuelled(X) and considering the parameter X, the following PRS will be built: PRS 1 precs : at1; fuelled1 deleted precs : at1; fuelled1 add elements : at1; unf uelled1 By considering the parameter Y we obtain: PRS 2 precs : at2 deleted precs : at2 add elements : and by considering the parameter Z we obtain: 374 Automatic Inference of State Invariants PRS 3 precs : location1 deleted precs : add elements : at2 In constructing these structures we are identifying the state transformations through which the objects, instantiating the operator parameters, progress. Note that objects that instantiate X go from being fuelled and at somewhere to being unfuelled and at somewhere; objects that instantiate Y lose the property of having anything at them and gain nothing as a result of application of this operator, and objects that instantiate Z continue being locations and gain the property of having something at them. We now convert these structures into transition rules in order to correctly capture these state transformations. Our standard formula for the construction of rules from PRSs is: precs Psi deleted precs ) deleted precs ! add elements Thus, using the PRS 1 above, we could build the rule: at1; fuelled1 ! at1; unfuelled1 A potential problem with this rule is that it causes at1 and fuelled1 to be linked in state transformations, so that at1 and fuelled1 become associated with the same property space and, as a consequence, objects that can be at places, but that cannot be fuelled, may be indistinguishable from objects that require fuelling before they can be moved. In fact, we wish the transition rules to express the fact that being fuelled enables things to go from being at one place to being at another place, whilst not excluding the possibility that there may be other enablers of this transition. We therefore begin a second phase of PRS construction by identifying, for special treatment, PRSs in which a property appears in both the deleted precs and the add elements. This is a property that is exchanged on application of the operator. That is, the relation continues to hold between the identified argument and some other object or objects (not necessarily the same object or objects as before the application of the operator). For example, in PRS 1, the vehicle is at a new location after application of the operator, and no longer at the old location. We observe that the vehicle must be fuelled to make this transition. To separate the transition from this condition we split the PRS. Splitting identifies the exchanged properties in a PRS and creates one new PRS for each exchange and one for the unexchanged properties. Therefore, splitting a PRS always results in at most k + 1 (and at least k) new PRSs, where k is the number of exchanges that the PRS represents. By splitting PRS 1 we construct two new PRSs: one characterizing the exchange of the at property, and one characterising the fuelled to unfuelled transition. The first of the new PRSs is: PRS 4 precs : at1; fuelled1 deleted precs : at1 add elements : at1 375 Fox & Long from which the rule fuelled1 ) at1 ! at1 is constructed. It should be noted that the property of being fuelled is no longer seen as part of the state transformation but only as an enabler, which is why it does not appear in the deleted precs bag in the resulting PRS. The second new PRS captures the fact that at1 can be seen as an enabler for the transition from fuelled1 to unfuelled1: PRS 5 precs : at1; fuelled1 deleted precs : fuelled1 add elements : unfuelled1 In this PRS there are no further splits required since no other properties are exchanged in it. A more general example is as follows: PRS 6 precs : p1; p2 Delta Delta Delta pn deleted precs : p1 Delta Delta Delta pi pi+k Delta Delta Delta pm add elements : p1 Delta Delta Delta pi q1 Delta Delta Delta qk from which i PRSs would be constructed to deal with each of the i exchanged pairs and a final PRS, PRS 7, would be constructed to describe the remainder of the transition making i + 1 PRSs in total. PRS 7 precs : p1; p2 Delta Delta Delta pn deleted precs : pi+k Delta Delta Delta pm add elements : q1 Delta Delta Delta qk There is no need to consider additional pairings of add and delete-list elements, since these would not correspond to exchanges of properties. The splitting process is justified in Section 3.1. The standard rule construction formula can be applied to PRS 5, yielding the rule at1 ) fuelled1 ! unfuelled1 It should be observed that, even if the add elements bag contains multiple properties, a single rule will always be built when the standard construction formula is applied. On considering the remaining PRSs, 2 and 3, it can be observed that they each contain an empty field: in 2 the add elements field is empty and in 3 the deleted precs field is empty. When a PRS has an empty field special treatment is required. From PRS 2 we build the rule at2 ! null to represent the fact that the object that instantiates Y gives up the property of having something at it, and gains nothing in return. From 3 we build the rule location1 ) null ! at2 376 Automatic Inference of State Invariants to represent the fact that the object that instantiates Z gains the property of having something at it by virtue of being a location, and gives up nothing in return. These rules have a somewhat different status from the ones that characterize the exchange of properties. In these cases properties are being lost or gained, without exchange, so can be seen as resources that can be accumulated or spent by domain objects rather than as states through which the domain objects pass. For example, a location can acquire the property of having something at it, without relinquishing anything in return, whereas an object that requires fuel can only become fuelled by relinquishing the property of being unfuelled, and vice versa. Increasing and decreasing resources are identified as attributes and are distinguished from states. This distinction will later prove to be very important, since the generation of true state invariants depends upon it being made correctly. Properties that can increase and decrease without exchange are not invariant, and false assertions would be proposed as invariants if they were treated in the same way as state-valued properties. A rule of the form constructed from PRS 3 must be constructed separately for every property in the add elements bag because these properties must be individually characterized as increasing resources. Rules constructed using null are distinguished as attribute transition rules. If the null is on the left side of the ! the rule is an increasing attribute transition rule. If the null is on the right hand side then the rule is a decreasing attribute transition rule. A final case to consider during rule construction is the case in which a PRS has an empty precs field. This happens if the parameter, with respect to which the PRS was constructed, did not appear in any of the preconditions of the operator schema. In this case a set of rules is constructed, one for each property, a, in the add elements bag, of the form null ! a reflecting the fact that a is an increasing resource (the deleted precs field will necessarily also be empty in this case). Definition 11 A state is a bag of properties. When it is necessary to distinguish a bag from a set, square brackets will be used to denote the bag. Definition 12 A property space is a tuple of four components: a set of properties, a set of transition rules, a set of states and a set of domain constants. Definition 13 An attribute space is a tuple of three components: a set of properties, a set of transition rules and a set of domain constants. It is helpful to observe here that the state and attribute spaces represent disjoint collections of properties, and that these disjoint collections are formed from the transition rules by putting the start and f inish properties of each rule into the same collection. For example, given two rules: E1 ) [p1; p2; p3] ! [q1; q2] and E2 ) [r1; r2] ! [s1] 377 Fox & Long the collections [p1; p2; p3; q1; q2] and [r1; r2; s1] would be formed. If a property appears in the start or f inish of both rules then a single collection will be formed from the two rules. The last stage in the rule construction phase is to identify the basis for the construction of property and attribute spaces. This is done by uniting the left and right hand sides of the rules. Uniting forms collections of properties that each seed a unique property or attribute space. It is not yet possible to decide which of the seeds will form attribute spaces, so treatment of both kinds of space is identical at this stage. The enablers of the rules are ignored during this process. We do not wish to make enablers automatically fall into the same property spaces as the states in the transformations they enable. This could result in incorrect assignment of properties to property and attribute spaces since enablers only facilitate, and do not participate in, state transformations. The output of this phase is the collection of rules, with some properties marked as attributes, and the property space seeds formed from the uniting process. All properties that remain unassigned at this stage are used to seed separate attribute spaces, one for each such property. The role played by the second phase of PRS construction is to postpone commitment to the uniting of collections of properties so that the possibility of objects, which can have these properties, being associated with different property spaces is left open for as long as possible. It may be that consideration of other schemas provides enough information for this possibility to be eliminated, as in the following abstract example, but we support as much type discrimination as possible in the earlier phases of analysis. We consider this simple example to illustrate the problem. 2.3.1 Postponing Property Space Amalgamation Given a domain description containing the following operator schema: op1(X,Y,Z) Pre: p(X,Y), q(X,Y) Add: p(X,Z), q(X,Z) Del: p(X,Y), q(X,Y) the PRS: precs : p1; q1 deleted precs : p1; q1 add elements : p1; q1 will be constructed, during the first phase, for X. The properties p1 and q1 are bound together in this PRS, and the resulting rule would be: p1; q1 ! p1; q1 which forces objects that can have property p1 to occupy the same property space as objects that can have property q1. Since this PRS models the exchange of p1 we will split it, and replace it with two new PRSs: precs : p1; q1 deleted precs : p1 add elements : p1 378 Automatic Inference of State Invariants precs : p1; q1 deleted precs : q1 add elements : q1 We do not consider other pairings of p1 and q1, since these will be found in the PRSs of other operator schemas if the domain allows them. The two PRSs generated lead to the generation of the rules: q1 ) p1 ! p1 and p1 ) q1 ! q1 The two rules indicate that p1 and q1 should be used to form different property spaces since they could, in principle, be independent of one another. Then objects assigned to these two spaces can turn out to be of distinct types. However, if we add the following two schemas: op2(X,Y) Pre: q(X,Y) Add: p(X,Y) Del: q(X,Y) op3(X,Y,Z) Pre: p(X,Y) Add: q(X,Y) Del: p(X,Y) we generate, for X, the PRSs: precs : q1 deleted precs : q1 add elements : p1 and precs : p1 deleted precs : p1 add elements : q1 and the rules: q1 ! p1 and p1 ! q1 indicating that p1 and q1 should be united in the same set and hence form a single property space, and that objects that can have these properties are really of the same type. The uniting overrides the potential for separate property spaces to be formed but, in the absence of these two schemas, there would have been insufficient information available to determine the nature of the relationship between the two properties. 379 Fox & Long 2.4 Constructing the Property Spaces and Synthesising the Types The objective of this stage is to construct the type structure of the domain by identifying domain objects with distinct property spaces. Objects can appear in more than one property space, giving us a basis for deriving a hierarchical type structure. The first part of the process involves completing the seeded property spaces. The first task is to associate transition rules with the appropriate property space seeds. This can be easily done by picking an arbitrary property of the start or finish component of each rule and identifying the property space seed to which that property belongs. There can never be ambiguity because every property belongs to only one seed and uniting ensures that all of the properties referred to in a rule belong to the same seed. At this point the distinction between states and attributes becomes important. Any property space seed that has an attribute transition rule associated with it becomes an attribute space and is dealt with differently from property spaces in certain respects explained below. The next step is to identify the domain objects associated with each property space and attribute space. For each object referred to in the initial state we construct a type vector in which a bit is set if the corresponding space is inhabited by the object. An object can inhabit more than one space. Habitation is checked for by identifying all of the properties that hold, in the initial state, of the object being considered and allocating them as states, rather than as properties, to the appropriate state and attribute spaces. When every domain object has been considered a unique type identifier is associated with each of the different bit patterns. The next task is to populate the property spaces with states. The following definitions are required to support the explanation of this process. Definition 14 A world-state is a collection of propositions characterising the configuration of the objects in a given planning domain description. Definition 15 Given a world-state, W , a property space, P = (P s; T Rs; Ss; Os), or an attribute space, P = (P s; T Rs; Os), and an object o 2 Os, the P -projection of St for o is the bag of properties, possessed by o in W , each of which belongs to P s. The collection of properties of an object, o, in the initial state can be divided into a set of bags of properties, each bag corresponding to the P -projection of the initial state for o, for some property or attribute space P . Each bag is added to the state set of the corresponding property space, or discarded if the corresponding space is an attribute space. We now need to extend the spaces by, for each property space, adding states that can be inferred as reachable by objects within that space along transitions within that space. This is done for every state in the space, including states that are newly added during this process, until no further new states are reachable. The ordering of the properties within states is irrelevant, so two states are considered equal if they contain the same properties, regardless of ordering (they are considered order-equivalent). Since, when we come to use this information in parts of the process of invariant generation, we will not require knowledge of any inclusion relations between pairs of states, it is convenient to mark these at this stage. The addition of reachable states is important for the inference of state invariants, and their use will be discussed in Section 2.7. The attribute spaces receive different treatment at this point. The 380 Automatic Inference of State Invariants important difference to observe is that, since property spaces characterize the exchange of properties, objects in a property space must start off in the initial state as members of that property space. However, since attributes can be acquired without exchange, it is possible for objects that do not have particular attributes in the initial state to acquire those attributes later. This is only possible if the attribute space has an increasing attribute transition rule associated with it. We now, therefore, consider each attribute space to see whether further objects can be added by application of any corresponding increasing rule. An object can be added to an attribute space if it potentiates all of the enablers of an increasing rule in that attribute space. An object potentiates an enabling property if it is a member of the state or attribute space to which that property belongs. Membership of all of these spaces indicates that the object could enter a state in which it satisfies all of the enabling properties, which would justify an application of the increasing rule. Any enabling property that is not associated with a state or attribute space is a static condition, so the initial state can be checked to confirm that the property is true of the object being considered. A complication arises if any enabling property was itself used to seed an attribute space (in which case it is itself an attribute), because it is then necessary to identify all of the objects in its attribute space and consider them for addition to the current attribute space. Of course this could, in principle, initiate a loop in the process but we avoid this by marking attribute spaces as they are considered and ensuring, by iterating until convergence, that all of the attribute spaces in the loop are completely assigned. The correctness of this part of the procedure is discussed in Section 3. When this is done the state and attribute spaces are complete and the types of the domain objects can be extracted. The completeness of this construction phase is discussed in Section 3.1. 2.5 A Worked Example A fully worked example of all stages of the process will help to clarify what is involved. Consider a simplified version of the Rocket domain in which there are two operator schemas: drive(X,Y,Z) Pre: at(X,Y), fuelled(X), location(Z) Add: at(X,Z), unfuelled(X) Del: at(X,Y), fuelled(X) load(X,Y,Z) Pre: at(X,Y), at(Z,Y) Add: in(X,Z) Del: at(X,Y) and an initial state containing four constants: rocket, package, London and Paris, and the relations: at(rocket,Paris), fuelled(rocket) and at(package,London). It can be observed that this simplified Rocket domain has the rather odd feature that the load schema is not restricted to loading packages into rockets. This oddity will be highlighted by the analysis that is constructed, showing how the analysis performed by tim can help in understanding (and debugging) the behaviour of the domain. From the drive operator schema the following PRSs are constructed for variables X, Y and Z respectively: 381 Fox & Long precs: at1, fuelled1 deleted precs: at1, fuelled1 add elements: at1, unfuelled1 precs: at2 deleted precs: at2 add elements: precs: location1 deleted precs: add elements: at2 From the load operator schema the following PRSs are constructed for variables X, Y and Z respectively: precs: at1 deleted precs: at1 add elements: in1 precs: at2, at2 deleted precs: at2 add elements: precs: at1 deleted precs: add elements: in2 and the following rules are built. The first PRS generates the first two rules and subsequent PRSs each generate one rule. fuelled1 ) at1 ! at1 at1 ) fuelled1 ! unfuelled1 at2 ! null location1 ) null ! at2 at1 ! in1 at2 ) at2 ! null at1 ) null ! in2 We now construct the following united sets of properties: fat1; in1g ffuelled1; unfuelled1g fat2g fin2g 382 Automatic Inference of State Invariants These are used to seed property spaces. We first associate the rules with these property space seeds, resulting in the following assignment: fat1; in1g at1 ! in1; fuelled1 ) at1 ! at1 ffuelled1; unfuelled1g at1 ) fuelled1 ! unfuelled1 fat2g location1 ) null ! at2; at2 ) at2 ! null; at2 ! null fin2g at1 ) null ! in2 The last two spaces have been converted into attribute spaces by their association with attribute transition rules. The resulting spaces can now be supplemented with domain constants and their legal states. We first identify the subset of the legal states of the domain objects that are identifiable from the initial state. We do not use the goal state to provide further information about the properties of objects. The goal state might be unachievable because objects cannot obtain the required properties. This would invalidate tim's analysis of the domain. In the initial state the rocket has properties at1 and fuelled1, the package has property at1, London has property at2 and Paris has property at2. Using this information we associate domain constants with the developing state and attribute spaces to obtain: fat1; in1g at1 ! in1; fuelled1 ) at1 ! at1 frocket; packageg ffuelled1; unfuelled1g at1 ) fuelled1 ! unfuelled1 frocketg fat2g location1 ) null ! at2; at2 ) at2 ! null; fLondon; P arisg at2 ! null fin2g at1 ) null ! in2 The next step is to add the legal states of these objects, which are identifiable so far, to the property spaces. This results in the following structures, the first two of which can be extended by inference (as will be explained) into completed property spaces. The last two will be extended into completed attribute spaces by the addition of objects that can potentially acquire the associated attributes (also described below). fat1; in1g at1 ! in1; fuelled1 ) at1 ! at1 frocket; packageg [at1] ffuelled1; unfuelled1g at1 ) fuelled1 ! unfuelled1 frocketg [fuelled1] fat2g location1 ) null ! at2; at2 ) at2 ! null; fLondon; P arisg at2 ! null fin2g at1 ) null ! in2 The last stage in the construction of the two property spaces is to add any states that can be inferred as reachable, via transition rules, by objects in the property spaces. For example, packages can go from being at1 to being in1, by application of the rule at1 ! in1, and since that rule is available in the property space to which package belongs, and at1 is one of the legal states in that property space, we add in1 as a further legal state. In general, we construct the extension by, for each state in the space, identifying applicable rules and, for each rule, creating a new state by removing the properties in the start of the 383 Fox & Long rule and adding the properties in the finish of the rule. This is done until all further states are order-equivalent to those already generated. The enablers of the rules are ignored, with the consequence that some of the new states generated might be unreachable. When this process is completed in the current example the finished property spaces are as follows: Property space 1 fat1; in1g at1 ! in1; fuelled1 ) at1 ! at1 frocket; packageg [at1]; [in1] Property space 2 ffuelled1; unf uelled1g at1 ) fuelled1 ! unf uelled1 frocketg [fuelled1]; [unf uelled1] We now consider each attribute space in turn and add domain objects (not already members) that potentiate their increasing rules. No new domain objects can be added to the first attribute space since only London and P aris can potentiate the increasing rule, and they are already present. However, when the second attribute space is considered it can be observed that rocket and package both potentiate the increasing rule and are therefore both added as new members. The resulting attribute spaces are: fat2g location1 ) null ! at2; at2 ) at2 ! null; fLondon; P arisg at2 ! null fin2g at1 ) null ! in2 frocket; packageg The oddity of the load operator is revealed at this stage, since both package and rocket have been assigned as members of the in2 attribute space (meaning that they both can have the attribute of having things in them). The number of distinct bit patterns that are constructed, indicating object membership of the state and attribute spaces, determines the number of distinct types that exist in the domain. Hence, in this simplified encoding of the Rocket domain, there are three distinct types. The rocket has type [1101], the package has type [1001] and P aris and London both have type [0010]. These types are given abstract identifiers, T0; T1 and T2, but might be more meaningfully interpreted as the types of: movable object requiring fuel, movable object and location respectively. As expected, London and P aris are of type location, whilst the package is of type movable object and the rocket is of type movable object requiring fuel, which is a sub-type of movable object. The distinction we have made between state and attribute spaces is further exploited in the process of inferring state invariants, discussed in Section 2.7. 2.6 The Assignment of Types to Operator Parameters Types are assigned to the parameters of the operators in the following way. Given an operator schema and a collection of property spaces and attribute spaces we allocate a type vector to each of the variables in the schema. The membership in the state and attribute spaces of each of the properties of a given variable is recorded by setting the appropriate bits in the vector for that variable. Only the properties that appear in the preconditions of the 384 Automatic Inference of State Invariants schema are considered, because any object that can satisfy the preconditions of an operator can have the properties represented by the postconditions and is therefore of the right type for instantiation of the operator. When a type is associated with the vector the union of all of its sub-types is taken. This union is then the type assigned to the variable. Any domain object, the type of which is a sub-type of the type associated with the variable, can then be used to instantiate that variable. To see how this process works, consider the variable X in the drive schema above. The precondition properties of X are: at1, fuelled1. These are members of the two property spaces 1 and 2. Therefore, the type vector associated with X is [1100]. It can be observed that the type vector associated with the rocket is [1101], so that the type of rocket is a sub-type of the type of X. This is the only sub-type, so the union of sub-types contains only T0, the type of rocket. This means that X can be instantiated by rocket, but not by any other domain constant, since no other domain constant has a type in the appropriate sub-type relation. To type the operator parameters we introduce new type variables, Tk::Tn for unused values between k and n, where k is the number of existing types and n is k plus the number of variables in the schema being considered. The type vector for variable Y will be [0010] and Z will have no type vector because location is a static relation and Z does not appear as an argument to any other predicate in the preconditions. Z therefore acquires the same type as London and P aris, the only two objects for which location is true in the initial state. T4 is a super-type of T2. After taking the unions of the sub-types we can now specify the drive schema in the following way: drive(X,Y,Z) Params: X:T0 Y:T2 Z:T2 Pre: at(X,Y), fuelled(X), location(Z) Add: at(X,Z), unfuelled(X) Del: at(X,Y), fuelled(X) stan exploits the sub-typing relations that have been inferred when constructing instances of the drive operator. Any variable that appears in a schema but does not appear in its preconditions can be instantiated by objects of any type. This is because the domain description contains no basis for inferring type restrictions in this case. No variable can appear on the delete list without appearing on the precondition list, since we assume that all delete list elements appear as preconditions. So such a variable would have to occur on the add list. This would mean that, regardless of the properties holding of the object used to instantiate that variable, in the initial state, it can acquire that add list property freely. Since this acquisition would occur irrespective of the type of the object, such variables are essentially polymorphic. 2.7 The Inference of State Invariants The final phase of the computation of tim is the inference of the state invariants from the property spaces. The attribute spaces are not used for the inference of invariants: incorrect invariants would be proposed by tim if attribute spaces were inadvertantly used. This explains the importance of identifying the attribute spaces in the earlier stages of the algorithm. The current version of tim is capable of inferring four kinds of invariant, three of which are inferred from the property spaces (identity invariants, state membership invariants and 385 Fox & Long invariants characterizing uniqueness of state membership) and one of which is inferred from the operator schemas and initial state directly (fixed resource invariants). In the simplified Rocket domain, considered above, an example of an identity invariant is: 8x : Tk:8y:8z:(at(x; y) ^ at(x; z) ! x = z) A state membership invariant is: 8x : Tk:(9y : Tn:at(x; y) . 9y : Tm:in(x; y)) A uniqueness invariant is: 8x : Tk::(9y : Tn:at(x; y) ^ 9y : Tm:in(x; y)) To infer the identity invariants each property space is considered in turn, with respect to their properties and states. If a property, for example Pk with P of arity n ? 1, occurs at most once in any state an invariant of the following form, in which _y and _z are vectors containing n Gamma 1 values, can be constructed: 8x:8_y:8_z:(P (y1::kGamma 1; x; yk::nGamma 1) ^ P (z1::kGamma 1; x; zk::nGamma 1) ! _y = _z) The form of this invariant can be generalised to deal with the case where there are at most m ? 1 occurrences of Pk in any state in the space. In this case we build the following expression, in which we have assumed that k = 1, for simplicity. 8x:8_y1:::_ym:(P (x; _y1) ^ ::: ^ P (x; _ym) ! (_y1 = _y2 . _y1 = _y3 . ::: . _ymGamma 1 = _ym)) The state membership invariants are of the form: 8x:(Disjunct1 . :: . Disjunctn) where each disjunct is constructed from a single state. Thus, if a property space contains k states there will be at most k disjuncts in the invariant constructed for that property space. Only one state membership invariant is constructed for each property space. Given the collection of states in a property space we first identify those that are supersets of other states in the collection. All supersets are discarded, since the invariants that would be built from them would be logically equivalent to those built from their subset states. Each remaining state is used to build a single disjunct. If the state being considered contains a single property, Pk with P of arity n, then the expression 9_y:P (y1::kGamma 1; x; yk::nGamma 1) is constructed. Of course, if n = 1 then there is no existential quantifier and the disjunct is just P (x). If the state contains more than one property, say m of them denoted P 1::P m, then we build (again, assuming that k = 1 for simplicity): 9_y1:::_ym:(P 1(x; _y1) ^ P 2(x; _y2) ^ ::: ^ P m(x; _ym)) The uniqueness invariants are constructed in a similar way. For each property space we begin by analysing the superset states to identify non-exclusive pairs of subset states. For 386 Automatic Inference of State Invariants example, given the subset states fat1g and fin1g and the superset state fat1; in1g, it can be observed that the two subset states are not mutually exclusive since at1 and in1 can be simultaneously held. Having done this analysis and identified all mutually exclusive pairs of states we mark the subset states as unusable for generation of invariants. The remaining states are considered in all possible pairings. For every pair of states, P; Q, we generate an invariant of the following form assuming, for simplicity, that x is in the first position in P 1::P n and Q1::Qm. The form of the invariant is easily generalised, as before. 8x::(9_y1:::_yn:(P 1(x; _y1) ^ P 2(x; _y2) ^ ::: ^ P n(x; _yn)) ^(9_y1:::_ym:(Q1(x; _y1) ^ Q2(x; _y2) ^ ::: ^ Qm(x; _ym)))) The fourth kind of invariant can be inferred from the structure of the operator schemas without reference to the property spaces or domain type structure. We call these invariants fixed resource invariants since they capture the physical limitations of the domain. Fixed resource invariants cannot be inferred from the state and attribute spaces because they describe properties of the domain rather than of objects within it. The following schema from the Gripper domain provides an example of why fixed resource invariants are distinguished from the other three kinds: move(X,Y) Pre: at robot(X), room(Y) Add: at robot(Y) Del: at robot(X) The PRSs that would be built from this operator are: precs : at robot1 deleted precs : at robot1 add elements : precs : room1 deleted precs : add elements : at robot1 and the rules constructed from these are: at robot1 ! null and room1 ) null ! at robot1 It can be observed that both of these rules are attribute transition rules and that at robot1 is attribute rather than state-valued. This means that no invariants of the first three kinds discussed would be constructed. The reason for the lack of invariants of the first three forms is that the encoding of the robot is embedded in a predicate, so the robot cannot participate directly in state transitions. An obvious invariant of the robot, which would naturally be true of this domain, is that the 387 Fox & Long robot is always in exactly one room but this cannot be inferred using the techniques so far described. In fact, this is an axiom about the world, or domain, rather than specific objects within it, and has to be obtained from information other than the state transformations of the objects. It can be seen from the operator schemas for the Gripper domain that at robot1 is balanced. That is, it is always deleted whenever it is added and added whenever it is deleted. This means that the number of occurrences of at robot in the initial state determines the number of occurrences that are possible in any subsequent state. This leads to the construction, for this domain, of the invariant jfx : at robot(x)gj = 1 since there is only one at robot relation in the initial state. The form of fixed resource invariants is always equational. Such an invariant states that the size of the set of combinations of objects satisfying a certain predicate is equal (or, in some cases, less than or equal) to a certain positive integer. Because this integer can be very large it is more convenient to write an equation than it would be to write a logical expression. The information encoded in the fixed resource invariants is very useful for identifying unsolvable goal sets without attempting to plan for them. For example, in the ICPARC version of the three-blocks Blocks world (Liatsos & Richards, 1997), in which there are only three table positions, there must always be exactly three clear surfaces. Any goal specifying more than three clear relationships can be identified as unachievable from the fixed-resource invariants for that domain. The fixed-resource and uniqueness invariants produced by tim can be seen as providing a form of multi-mutex relations, in contrast to the binary mutex relations inferred during the construction of the plan graph in Graphplan-based planners (Blum & Furst, 1995). Binary mutex relations indicate that two actions or facts are mutually incompatible, whilst multimutex relations indicate that larger groups of actions or facts are collectively incompatible. Binary mutex relations, preventing a fact that can be true of only one object from holding of two different objects simultaneously, can be extracted from the identity invariants that tim infers. Multi-mutex relations are more powerful than binary ones. Stan can detect unsolvable goal-sets by using the fixed-resource and uniqueness invariants even when the binary mutex relations at the corresponding level do not indicate that any problem exists. To infer these invariants we examine the predicates in the language to see whether they are exchanged on the add and delete lists of the operator schemas. If a predicate is exchanged equally in all schemas (it always appears the same number of times on the add list as on the delete list of a schema) then the predicate corresponds to a fixed resource. If a single schema upsets this balance then the predicate is not treated as fixed. Given a fixed resource predicate, it can be inferred that there can never be more combinations of objects satisfying that predicate than there are in the initial state. Because of the slightly odd encoding of the rocket world considered in this paper, only location is a fixed resource. at is not fixed because it is not equally exchanged in the load schema. Examples of fixed resource invariants inferred from various standard domains are provided in Appendix C. There are certain circumstances under which it is necessary to infer the weaker invariant that jfx : P (x)gj ^ k 388 Automatic Inference of State Invariants for some positive integer k. If P holds of multiple objects in the initial state then it is possible for subsequent state transformations, or attribute acquisitions, to result in states in which two or more instances of P collapse into one. If P holds multiply often in the initial state (or in any other reachable state) then it is necessary to build the invariant using ^ instead of =. If P is state-valued, and multiple instances never occur in any state in its property space, then it is safe to assert equality in the construction of the invariant. Automatic inference of the first three kinds of invariants relies on the construction of the property spaces as discussed in Section 2.4. As has been discussed, the distinction between state and attribute spaces is critical for the inference of correct invariants. However, using just the techniques described so far, tim would lose information from which it could construct useful invariants. To give an example of how this could occur we now consider the following simple encoding of the standard Blocks world: move(X,Y,Z) Pre: on(X,Y), clear(X), clear(Z) Add: on(X,Z), clear(Y), clear(table) Del: on(X,Y), clear(Z) In this operator, used by Bundy et al. (1980), the add list element clear(table) makes reference to a constant. If the operator schema were to be submitted to our analysis in its current form no PRS would be built for the constant, so the rules that would be constructed, and hence the state and attribute spaces constructed, would fail to record the fact that every application of move results in a state in which the table is clear. The resulting analysis would result in incorrect invariants and types. Grant (1996) identifies this version of the move operator as flawed, because of the need to maintain state correctness by the addition of the invariant clear(table) to the add list. However, we can analyse this schema correctly if we first abstract it to remove the constant, yielding the following new schema: move(X,Y,Z,T) Pre: on(X,Y), clear(X), clear(Z), table(T) Add: on(X,Z), clear(Y), clear(T) Del: on(X,Y), clear(Z) Now, given an initial state in which blockC is on blockA and blockB is on the table, we add the proposition table(table) (so that the new precondition can be satisfied) and the property and attribute spaces that are constructed are as follows: fon1g clear1 ) on1 ! on1 fblockA; blockB; blockCg [on1] fon2; clear1g on2 ! clear1; clear1 ! on2; fblockA; blockB; blockC; tableg table1 ) null ! clear1 The second of these is an attribute space, so our invariant extraction algorithm is not applied to it. Consequently, the only invariants we can infer are those that characterize the positions of blocks (every block is on exactly one surface). This is a pity, as there is information available in the attribute space that could yield useful extra invariants. In particular, we would like to infer the invariant that every block can be either clear or have 389 Fox & Long something on it, but it cannot be both clear and have something on it. The reason we cannot infer this as an invariant is because it would be asserted to hold for every object in the attribute space, including the table, even though it is not actually true of the table (the table can have things on it and still be clear). 2.7.1 Sub-space Analysis on Property and Attribute Spaces The solution to the problem of loss of invariants is to decompose any property or attribute space that contains k ? 1 object types into k sub-spaces. A property sub-space is structurally identical to a property space. Attribute sub-spaces are identified but not used, as no invariants can be obtained from them. Property sub-spaces can be obtained by analysis on attribute spaces, as the following example will show. The reason for distinguishing sub-spaces from property and attribute spaces is that the properties are not partitioned in sub-spaces as they are in the property and attribute spaces. The original property or attribute space is not discarded and the sub-spaces are not used for determining the types of objects. The only role of the sub-space analysis is to enable the construction of additional invariants. We now consider the Blocks domain described in the previous section as an example of the benefits of sub-space analysis. At the point of invariant construction the types of the domain objects have been identified by their property and attribute space membership, so table is already known to be of a different type to that of the blocks. This is because table is not a member of the property space for on1. Therefore, two sub-spaces can be constructed from the attribute space, one for the type [11], of blocks, and one for the type [01], of tables. No sub-spaces can be constructed from the property space because it contains only one type of object. The rules associated with the sub-spaces will be all of the rules from the original attribute space that are enabled by objects of the appropriate type. The second of the two sub-spaces is an attribute sub-space because of the inclusion of the increasing attribute transition rule. At this stage the two sub-spaces are as follows: fon2; clear1g on2 ! clear1; clear1 ! on2 fblockA; blockB; blockCg fon2; clear1g table1 ) null ! clear1; on2 ! clear1; ftableg clear1 ! on2 The attribute sub-space will not be used for invariant construction because it contains an attribute transition rule and would result in incorrect invariants (as is the case for attribute spaces), so there is nothing to be gained from developing it further. However, the state sub-space is now completed by the addition of the states associated with the objects in the space, both in the initial state and by extension. The resulting sub-spaces are: fon2; clear1g on2 ! clear1; clear1 ! on2 fblockA; blockB; blockCg [on2]; [clear1] fon2; clear1g table1 ) null ! clear1; on2 ! clear1; ftableg clear1 ! on2 From the new state sub-space we can infer the following invariants, using the type name Block to stand for the type vector [11]. We infer the identity invariant: 8x : Block Delta (8y Delta 8z Delta (on(y; x) ^ on(z; x) ! y = z)) 390 Automatic Inference of State Invariants the state membership invariant: 8x : Block Delta (9y : Block Delta on(y; x) . clear(x)) and the unique state invariant: 8x : Block Delta :(9y : Block Delta (on(y; x) ^ clear(x))) Although there is an additional invariant, that the table is always clear, we cannot infer this at present. 2.8 The Problem of Mixed Spaces It can happen that the encoding of a domain conceals the presence of attributes within schemas until the point at which property space extension occurs. This can prevent the property space extension process from terminating. For example, a simple lightswitch domain contains the following two schemas: switchon(X) Pre: off(X) Add: on(X), touched(X) Del: off(X) switchoff(X) Pre: on(X) Add: off(X), touched(X) Del: on(X) and an initial state in which switchA is on. Two PRSs are constructed: precs : off1 deleted precs : off1 add elements : on1; touched1 precs : on1 deleted precs : on1 add elements : off1; touched1 giving rise to two rules: off1 ! on1; touched1 and on1 ! off1; touched1 Uniting then seeds one property space containing all three properties. After addition of the rules the property space is as follows: fon1; off1; touched1g off1 ! on1; touched1; fswitchAg on1 ! off1; touched1 [on1] 391 Fox & Long It is at the point of extension of the space that the problem arises. The following states are added: [off1; touched1], [on1; touched1; touched1], [off1; touched1; touched1; touched1] and so on. We cannot simply avoid adding properties that are already in the state being extended because the two, apparently identical, properties might in general refer to different arguments. The problem here is due to the fact that touched1 is actually an increasing attribute but this does not become apparent in the PRSs. The consequence is that mixed spaces are constructed. A mixed space is a property space containing hidden attributes. Tim detects hidden attributes by checking, on extension, that no new state contains a state already generated from the same initial state starting point. Thus, on extension of the mixed space above, tim would detect the hidden attribute when the state [on1; touched1; touched1] is constructed, because this state contains the state [on1] that initiated this extension. Having detected the hidden attribute there are two possibilities: either tim can convert the mixed space into an attribute space, in which case no invariants will be constructed, or it can attempt to identify the attribute and split the mixed space into an attribute space and a property space containing the state-valued components of the mixed space. We take this option and split the state. This allows us to infer invariants concerning the state-valued properties. tim takes the difference between the including and included states and, for each distinct property in the difference, processes the rules by cutting any rule containing that property into two rules, at least one of which will be an attribute rule. The following method is used to cut the rules. In the following, attr+ indicates one or more occurrences of the attribute-valued property and the comma is overloaded to mean both bag conjunction and bag union. If the rule is of the form: enablers ) start ! adds; attr+ then the two new rules will be of the forms: enablers; start ) null ! attr+ and enablers ) start ! adds If the rule is of the form: enablers ) attr+; precs ! adds then the two new rules are of the forms: enablers; precs ) attr ! null and enablers; attr ) precs ! adds The rule cutting separates the attribute-valued properties from the state-valued properties. Now pure attribute and property spaces can be constructed. However we do not discard the original mixed space because it has been used in determining the type structure of 392 Automatic Inference of State Invariants the domain. Any additional type information that could be extracted from the state and attribute spaces built following this analysis is not currently exploited. When this analysis is applied to the lightswitch domain, the following new property space and attribute space are built: fon1; off1g off1 ! on1; on1 ! off1 fswitchAg [on1]; [off1] ftouched1g off1 ) null ! touched1; on1 ) null ! touched1 fswitchAg Using Lightswitch to stand for the type [11], the following state membership invariant can be constructed from the property space: 8x : Lightswitch Delta (on(x) . off(x)) tim also constructs the uniqueness invariant: 8x : Lightswitch Delta :(on(x) ^ off(x)) 3. Properties of TIM The correctness of tim relies on it constructing only necessarily true invariants. The demonstration that only true invariants are constructed guarantees the construction of an adequately discriminating type structure. We cannot guarantee against under-discrimination but we argue that over-discrimination does not occur in the type structures generated by tim. These properties were defined in Section 2.1. Over-discrimination would be the result of distinguishing functionally identical objects at the type level. This would occur if tim placed objects that participate in identical state transitions in different property spaces but, because of the underlying partitioning of properties between property spaces, this cannot happen. Further, membership of different property spaces requires that there be distinguishing state transformations, which there are not in functionally identical objects. Flawed assignment (assigning an object to a property space without its corresponding state transformations), should simply be seen as erroneous, rather than as over-discrimination. The possibility of this occurring can be excluded because property and attribute space construction and extension are shown to be correct in Section 3.1. A failure to detect type differences (under-discrimination) in the domain will result in weak invariants, and over-discrimination, if it could occur, would lead to over-targeted invariants that would still be true, but only for a subset of the objects they ought to cover. Flawed assignment would clearly lead to the construction of false invariants. Underdiscrimination, which can arise, therefore affects the completeness of the state-invariant inference procedure. It can also lead to over-generalisation of the operators since the types assigned to the operator parameters will be equally under-discriminating. This can enable meaningless instances to be formed, needlessly increasing the size of the search space that must be explored by the planner. This clearly raises efficiency issues but it does not undermine the formal properties of the planner that exploits tim. As observed, the consequence of under-discrimination is the construction of weak (but valid) invariants. The following example illustrates how under-discrimination can occur. Given a schema: 393 Fox & Long op(X,Y) Pre: p(X,Y) Add: q(X,Y) Del: p(X,Y) and an initial state in which p(a; c); p(b; c); q(b; d) hold, the following two property spaces are constructed: fp1; q1g p1 ! q1 fa; bg [p1]; [q1]; [p1; q1]; [q1; q1] fp2; q2g p2 ! q2 fc; dg [q2]; [p2; p2]; [q2; p2]; [q2; q2] Given these property spaces it is impossible to distinguish a from b or c from d, even though analysis of the operator schema and initial state reveal that a is functionally distinct from b and c from d. It can be seen that, although a must always exchange a p1 for a q1, b can have both p1 and q1 simultaneously. A similar observation can be made for c and d. However, the process by which invariants are constructed cannot gain access to this information. An identity invariant constructed for the first property space is: 8x : T Delta 8y Delta 8z Delta 8u Delta (q(x; y) ^ q(x; z) ^ q(x; u) ! y = z . y = u . z = u) This invariant is weaker than is ideal, because a can participate in only one q relation (b can participate in two simultaneously). A state membership invariant for this property space is: 8x : T Delta ((9y : T1 Delta p(x; y)) . 9y : T1 Delta q(x; y)) which understates the case for b, which can have p1 and q1 simultaneously. No unique state invariant is constructed for this property space, because p1 and q1 are not mutually exclusive. 3.1 Correctness and Completeness of the Transition Rule Construction Phase The correctness of the algorithm used in tim depends on two elements. Firstly, the property spaces identified by the algorithm must be correctly populated. That is, no objects should be assigned to property spaces to which they do not belong and every achievable state must be included in the appropriate property space. Secondly, these property spaces must only support the generation of correct invariants. This second element is examined in Section 3.2. An interesting relationship exists between the states in a property space and the invariants generated from the space. Incorrect invariants will be contructed if a property space is missing achievable states. This is because the state membership invariants assert that each object in the property space must be in one of the states in the property space. If states are missing then this invariant will be false. We now prove that all achievable states will be in the appropriate property space. Theorem 1 Given an initial state, I, a collection of operator schemas, O, a property space, P = (P s; T Rs; Ss; Os), generated by tim when applied to I and O, and any state, St, which 394 Automatic Inference of State Invariants is reachable from I by application of a valid linearised plan formed from ground instances of operator schemas in O, then for any o 2 Os, the P -projection of St for o, StoP , is in Ss. Proof: The proof is by induction on the length of the plan that yields the state St. In the base case the plan contains no operator instances so St = I. The P -projection of I for o is in Ss, by definition of the first phase of the property space construction process described in Section 2.4. Suppose St is generated by a plan of length k + 1, with last step a and penultimate state pre-St. Let the P -projection of pre-St for o be pre-StoP . By the inductive hypothesis, this state is in Ss. If a does not affect the state of o, then the P -projection of St for o will be pre-StoP , and therefore in Ss trivially. Otherwise, consider the operator schema, Op 2 O, from which a is formed. As described in Section 2.7, no constants appear in Op and all variables in the body of Op are parameters of Op. Let the initial collection of PRSs constructed from Op, for those parameters instantiated with o in the creation of a, be the set PRS1:::PRSn where every PRSi has the form: precs : Pi deleted precs : Di add elements : Ai and the initial collection is the collection formed prior to splitting. For each value of i the ith PRS will lead to the construction of k + 1 transition rules, where k is the size of the bag intersection, Xi, of Di and Ai. The k rules will be of the following form: 8c 2 Xi Delta (Pi Psi fcg ) c ! c) and the remaining rule will be of the form: Pi Psi (Di Psi Xi) ) (Di Psi Xi) ! (Ai Psi Xi) We refer to the latter rule for PRSi as the ith complex rule. A subset of the n complex rules will contain a property in P s in either the start or the finish and will, therefore, be relevant to the transition from pre-St to St. It can be observed that these m complex rules (PRS1:::PRSm without loss of generality) must be in P because of the uniting process described in 2.3. We define pres(a)oP to be the P -projection of the preconditions of a for o. Similarly, adds(a)oP and dels(a)oP are defined to be the P -projections of the add and delete lists respectively. By construction of the PRSs, defined in Section 3.1, pres(a)oP = mM 1 Pi adds(a)oP = mM 1 Ai dels(a)oP = mM 1 Di 395 Fox & Long Because of the restriction that delete lists must be a subset of preconditions, and the fact that a is applicable to pre-St, it follows that dels(a)oP v pres(a)oP v pre-StoP . Since v represents bag inclusion it can be seen that all of the separate bags Di are included in pre-StoP without overlap. The extension process involves the iterated application of the rules as explained in Section 2.4 and indicated in the pseudo-code algorithm presented in Appendix B. For a rule to be applicable to a state its start must be included in the state. Therefore the m complex rules are all applicable, regardless of the sequence of application, to pre-StoP . It follows that the state (pre-StoP Psi mM 1 (Di Psi Xi)) Phi mM 1 (Ai Psi Xi) is generated in the extension process. By definition of Xi, and the fact that Di v pre-StoP , this state can be written as: (pre-StoP Psi mM 1 Di) Phi M Ai which, as observed above, is just: (pre-StoP Psi dels(a)oP ) Phi adds(a)oP which equals StoP by the standard semantics of operator application in strips. 2 The proof demonstrates that splitting, discussed in 2.3, does not result in the generation of invalid invariants. However, splitting can compromise the completeness of the invariantgeneration process. It can result in the inclusion of unreachable states in property spaces, with the consequence that the identity and state membership invariants that are generated are weaker than would otherwise be the case. This is further discussed in Section 3.2. We now explain the role of splitting in the PRS construction phases. Each domain object in a strips domain has an associated finite automaton in which the states consist of the properties (for example, at1) it can have, either initially or as a result of the application of an arbitrary length sequence of operators. Objects that can be observed to be of the same type will have identical automata at the property level. The PRSs capture the ways in which operator applications modify the configurations of individual objects and hence provide an encoding of these automata. The PRSs are built in two phases. In the first phase, all of the parameters in all of the schemas are considered, so all possible object state transitions are captured. However, some of these transitions conceal the functional distinctions inherent in the domain description and would lead to premature amalgamation of property spaces, as was observed in the discussion of the Rocket domain in Section 2.5. In that example it was observed that use of our standard formula for the construction of rules from these PRSs alone would result in the failure to detect the type distinction between rockets and packages. The second phase assists the type inference processes in avoiding under-discrimination by distinguishing enablers of a state transformation from the properties that are exchanged 396 Automatic Inference of State Invariants during the transformation. Each PRS characterizing the exchange of k properties is split to form at most k + 1 new PRSs. The PRSs 4 and 5, given in Section 2.3, show how two PRSs are constructed from a single PRS containing a single exchanged property. This is a simple example, as only one split is required to remove exchanges. In general it might be necessary to split repeatedly until all exchanges are removed, as shown in the example given by PRS 6 in Section 2.3. No non-exchange combinations of the properties in deleted precs and add elements should be considered during splitting. The resulting PRSs lead to the construction of transition rules which allow generic state transformations, such as movement from one location to another, to be separated from the specific nature of the objects that can make those transformations. It can be observed that the rules that result from the splitting process are more general than the rules that would have been obtained from the PRS prior to splitting. They distinguish more precisely between the properties that take part in state transitions and the properties that simply enable those transitions, allowing finer type distinctions to be inferred on the basis of the functionalities of the objects in the domain. Finer distinctions are made during the process of seeding property and attribute spaces by uniting. This is because uniting merges, into single equivalence classes, all of the properties that appear in both the start and finish of a rule. We argue that all state transformations are accounted for by the end of this second phase. The result of the second phase is that the automata formed during the first phase are separated into collections of simpler automata where possible, so that no transitions are lost but there is a finer grained encoding of the possible transitions that can be made by objects with appropriate properties. The PRSs constructed in this phase support the construction of rules that allow objects making these transitions to occupy different property spaces. Some of the second phase PRSs may be under-constraining, in the sense that analysis of subsequent schemas might eliminate the possibilities they are keeping open, as in example 2.3.1, but the set of PRSs obtained at the end of the second phase cannot be over-constraining because all of the first phase PRSs are considered for splitting. A subtlety concerns the consequence, at the type level, of assigning two functionally distinct objects to the same state or attribute space. For example, in example 2.5, rocket and package are both assigned to the property space for fin1; at1g and the attribute space for fin2g. However, because rocket can be fuelled or unfuelled, and the package cannot, there is a distinction between them that emerges in the property and attribute membership vectors associated with the rocket and package objects. Membership of the additional property space for ffuelled1; unfuelled1g means that rocket is assigned a type that is a sub-type of the type of package and the functional distinctness of rocket and package is recognised. As discussed, there is an oddity in this encoding that results in the package being assigned membership of the fin2g attribute space. Furthermore, at1 and in1 were united, with the effect that rockets can make the at1 ! in1 transition and can be used to instantiate variables of type movable object, even when variables of this type are intended only to be instantiated with the package. There is nothing in the domain description to prevent this interpretation. A more conventional encoding of the load schema would prevent the rocket from being loaded into any other object, and this would cause a refinement in the type structure that would identify loadable objects, and would prohibit the use of the rocket in forming instances of operators that should be restricted to operating on those objects. 397 Fox & Long The construction of transition rules follows a simple rule whereby any undeleted preconditions are used to enable a transformation from a state in which the deleted preconditions of a PRS hold to one in which the added elements of the PRS hold. Given the assumption that all deleted atoms in an operator schema must appear as preconditions in that schema, these rules correctly characterize strips-style state transformations. All possible transformations are captured because of the second phase of PRS construction. A complete set of correct transition rules is therefore constructed. Given the correctness and completeness of the transition rule construction phase, correct initial allocation of objects to spaces depends simply on correctly checking membership of the initial properties of the object in the property sets, formed by uniting the rules, that are used to seed the spaces. Extension of the property spaces is done by straightforward application of the transition rules, so all configurations of properties that can be occupied by the objects in the property space will have been added by the end of the extension phase. Extension of the attribute spaces is unproblematic in the cases where no potential enabler is itself an attribute. If one is, then the process by which the attribute space of that enabler is completed could, it appears, initiate a loop in the attribute space extension process. In fact, this does not happen as tim is able to detect when a loop has occurred and avoid repeatedly iterating over it. The following example illustrates the problem and the way it is solved in tim. Suppose we have three attribute spaces: Attribute space 1 fq1g p1 ) null ! q1 fa; bg Attribute space 2 fr1g q1 ) null ! r1 fcg Attribute space 3 fp1g r1 ) null ! p1 fdg These spaces are extended by the addition of objects that potentiate their increasing rules, as discussed in Section 2.4. No problem arises if the enablers of these rules are states, and not attributes, but in the extension of attribute space 1 above the enabler, p1, is an attribute. The attribute space for p1 has not yet been extended, so it is necessary to complete that space before using it to complete 1. Extension of 3 requires the extension of 2, for the same reason, and that requires the extension of 1 which requires the extension of 3, and so on. The way tim avoids re-entering this loop is by marking each space, as it is considered, as having been seen on this iteration. When a marked space is encountered it is not extended but is used as if it is already complete. Then a second iteration is required to extend any spaces that still require completion. Subsequent iterations will be required until the process converges. Our experiments suggest that it is unusual for there to be more than two iterations required. A worst case upper bound is o Lambda As, where o is the number of domain constants and As is the number of attribute spaces (which is limited by the number of properties), and hence quadratic in the size of the domain description. 398 Automatic Inference of State Invariants If the extension process starts with attribute space 1, in the above example, attribute space 1 will be marked as having been seen on the first iteration. Tim then goes on to extend space 3 because the extension of space 1 depends upon space 3 being complete. Space 3 is marked as having been seen on this iteration and space 2 is considered. Space 2 is marked and space 1 is revisited. Because space 1 is marked tim infers that a loop has been entered. Its objects are added to space 2 without extension and the objects of space 2 are then added to space 3. Finally, the objects of space 3 can be added to space 1 and the first iteration is complete. fq1g p1 ) null ! q1 fa; bg [ fc; dg fr1g q1 ) null ! r1 fcg [ fa; bg fp1g r1 ) null ! p1 fdg [ fc; a; bg However, space 2 is not yet complete, so a second iteration is required. This iteration starts in the same place as the first and the process is repeated, except that no further iterations will be required in this example. 3.2 Correctness of the State Invariants We now argue for the correctness of the invariant inference procedure by considering each of the four kinds of invariant in turn. The following arguments rely upon correctly distinguishing property spaces from attribute spaces, since the invariant analysis cannot be performed on attribute spaces. The only scope for confusing this distinction is in the extension of mixed spaces, but we extract attributes from mixed spaces by checking for inclusion of existing states in the new states generated during extension. This process was discussed in Section 2.8. Definition 16 Given a property space P = (P s; T Rs; Ss; Os), Ss can be partitioned into three disjoint sets: Sssubs and Sssups that contain all of the states in Ss that are included (as bags) or that include (as bags), respectively, at least one other state in Ss and Ssind that contains all of the independent states in Ss that are neither in Sssubs nor in Sssups. Theorem 2 Given a property space P = (P s; T Rs; Ss; Os), in which the set of states Ss is a union of the three disjoint sets of states Ssind, Sssubs and Sssups, for each object, o, in Os the following families of invariants will hold: 1. identity invariants; 2. state membership invariants; 3. unique state invariants. as defined in Section 3.2. Proof: We address each kind of invariant in turn. By Theorem 1 every object in Os must be in a state in Ss. Furthermore, all states of each object in Os, with respect to each property in P s, will be in Ss. This follows because the properties are partitioned between the spaces 399 Fox & Long during the seeding process. Therefore, the maximum number of occurrences of a property p in P s, possessed by any object in Os in any state of the world, will be bounded by the maximum number of instances of that property in any state in Ss (these maximum values might not be equal since Ss can contain inaccessible states). The identity invariants simply express this bound on the properties of the objects in Os. Every object in Os must be in a state in Ssind[Sssubs. This follows by definition of these sets in Definition 16 and by Theorem 1. The state membership invariants assert that every object in Os must be in at least one of these states, with each disjunct in the invariant corresponding to the assertion of membership of one of these states. To argue for the correctness of the unique state invariants, we observe that the proposed invariants would only be false if they paired states that were not mutually exclusive. In this case, either the state extension process would have put properties that could be simultaneously held into the same bag, or such properties would be simultaneously held in the initial state and hence would appear in the same bag on initial construction of the property space. In either case, a state will exist in the property space that is a superset of both of the non-exclusive states. However, uniqueness invariants are generated for pairs of states drawn only from Ssind [ Sssups so these non-exclusive pairs of states will not lead to the generation of incorrect invariants. 2 The fixed resource invariants are always associated with a particular predicate. If atoms built with that predicate are balanced on the add and delete lists of all of the operator schemas then the number of occurrences of these atoms in the initial state is fixed over all subsequent states. This is what the invariant expresses. An invariant is constructed for every predicate that forms balanced atoms. Since no new techniques are required to infer invariants from sub-spaces, no further argument is required to support correctness of the invariants formed following sub-space analysis. Although Theorem 2 demonstrates the correctness of the invariants inferred by tim it is possible for weak invariants to be inferred from the presence of unreachable states in Ss. Weak identity invariants are inferred if an unreachable state is generated, during extension, containing more instances of a property than are contained in any reachable state. When this happens an identity invariant will be generated that is weaker than would be ideal, but is still valid. Further, if a property space contains unreachable states they will cause the inclusion of additional false disjuncts in the state membership invariants, but since these false disjuncts will not exclude satisfying assignments their presence will not invalidate the invariants. Unreachable states cause additional tautologous uniqueness invariants to be generated but do not affect the strength of the invariants that refer only to reachable states. Clearly we cannot hope to identify all of the unreachable states, as such an analysis would be as hard as planning itself. Because no invariants are generated for attribute spaces tim cannot be claimed to be complete. Sub-space analysis rectifies this to some extent by identifying property spaces that exist within attribute spaces and allowing further invariants to be generated. This analysis could be further refined. 400 Automatic Inference of State Invariants 3.3 Effects of TIM on the Properties of the Planner Tim is itself sound, so no planner that uses tim is in danger of losing soundness as a result. Tim is certainly not complete for all domain axioms because there are invariant properties of other kinds that cannot be extracted by the current version. For example, Kautz and Selman (1998) identify optimality conditions and simplifying assumptions amongst the different kinds of axioms that might be inferred from a domain. An optimality condition in the Logistics domain might be: a package should not be returned to a location it has been removed from. A simplifying assumption in the same domain might be: once a truck is loaded it should immediately move (assuming all necessary loads can be done in parallel). These constraints require a deeper analysis of the domain than is currently performed by tim, but we intend to characterise them and infer them in our future work. We cannot guarantee that the type structure inferred by tim is always fully discriminating, although we do guarantee that it is not over-discriminating. However, failure on tim's part to infer all of the structure that is there to be inferred does not impact on the completeness of a planner using tim because, in these cases, tim will return an unstructured domain and the planner can therefore default to reasoning with the unstructured domain when necessary. 4. Experimental Results An examination of tim's performance can be carried out on several dimensions. We consider three specific dimensions here: the viability of the analysis on typical benchmark domains; the scalability of the analysis and the utility of performing the analysis prior to planning. Its general performance on standard benchmark problems provides an indication of the scale of the overhead involved in using tim as a preprocessing tool. All experiments were performed under Linux on a 300MHz PC with 128 Mb of RAM. Figure 3 shows that, even on large problem instances, the overhead is entirely acceptable. All of the Mystery problems listed in this table are very large (involving initial states containing hundreds of facts) and could not be solved by stan, ipp (Koehler, Nebel, & Dimopoulos, 1997) or Blackbox (Kautz & Selman, 1998) in the aips-98 competition. The nature of the Mystery domain is described in Appendix C. This emphasises the relative costs of the preprocessing and planning efforts. The selection of problems used to construct table 3 is justified as follows. In the Blocks world we have used a representative example from each of three encodings supplied in the pddl release. These are: the simple encoding (prob12), the att encoding (prob18) and the snlp encoding (prob23). The Hanoi set contains a collection of reasonably sized problems. A representative group of relatively large Mystery instances was chosen from the pddl release. The two Tyre world instances are the only two strips instances available in the release. The three Logistics problems are the three largest for the simple strips encoding included in the pddl release. The second dimension is scalability of the analysis. An analytic examination of the algorithm can determine an upper bound on performance that is polynomial in all of the key domain and problem components, including number of operator schemas, number of literals in operators, numbers of objects and facts in the initial state and the number and arities of predicates in the language. Figure 4 shows that the performance of tim is roughly quadratic in the size of the problem specification. In the graph, size is crudely equated with 401 Fox & Long Domain and problem Parse time Analysis time Output time Total Blocks prob12.pddl 2 0 2 5 prob18.pddl 3 1 2 7 prob23.pddl 2 1 1 5 Hanoi 3-disc 2 1 4 7 4-disc 2 1 4 7 5-disc 3 1 4 8 6-disc 3 1 4 9 7-disc 4 2 4 11 Mystery prob060.pddl 17 15 9 43 prob061.pddl 48 82 29 160 prob062.pddl 26 37 10 74 prob063.pddl 11 7 8 27 prob064.pddl 21 21 10 52 Tyre-World prob01.pddl 5 2 28 36 prob02.pddl 6 2 28 37 Logistics prob04.pddl 4 2 5 12 prob05.pddl 4 2 6 12 prob06.pddl 4 2 6 13 Figure 3: Table showing tim's performance in milliseconds on standard domains and problems. All timings are elapsed times and minor discrepancies in totals arise from rounding. 402 Automatic Inference of State Invariants 0 2000 4000 6000 8000 10000 12000 0 10000 20000 30000 40000 50000 60000 70000 80000 Millisecs Size of file Tim Analysis of Mystery Domain Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Pi Figure 4: Graph showing tim's performance on Mystery problems, plotting time against size (in characters) of problem file. The solid line is a plot of a quadratic function. the number of characters in the specification file. This graph was constructed by running tim on all of the strips Mystery domain problems in the pddl release. The increasing sizes of the problem specifications reflect increases in any and all of the various categories of objects in the domain and corresponding facts to describe their initial states. Figure 5 shows the effect on tim's performance as the number of operator schemas increases. This graph was constructed using an artificial domain in which each new operator causes two new state transitions described by two new literals. Thus, both number of operators and number of properties is increasing whilst the number of objects stays constant. The domain is described in detail in Appendix E. The graph indicates the linear growth of cost of analysis. The final dimension for evaluating tim is the effect of exploitation of its output by a planner. Gerevini and Schubert (1998) and Kautz and Selman (1998) provide convincing evidence supporting the powerful role of state invariants in enhancing the performance of SAT-based planning. In Figure 6 we demonstrate the power of inferred types by showing the advantage that stan with tim obtains over stan without tim on untyped Rocket domain problems. Figure 6 shows the effect on performance of increasing the number of packages to be transported. The time taken by stan with tim grows linearly, whilst stan without tim follows a cubic curve. If there are p packages in a problem instance then stan with tim constructs 4(p+1) operator instances while stan without tim constructs (p+3)2(p+5)+2p instances. This demonstrates that type information is the most significant factor in the advantage depicted in the graph. Figure 7 demonstrates that a similar improvement is obtained in the Logistics domain. In this graph a series of sub-problems were considered in 403 Fox & Long 20 25 30 35 40 45 50 55 60 65 70 0 2 4 6 8 10 12 14 16 Millisecs Number of operators Tim Performance with Increasing Number of Operators 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 Figure 5: Graph showing the consequences of increasing the number of schemas and inferrable property spaces. 0 2000 4000 6000 8000 10000 12000 0 5 10 15 20 25 30 35 40 Millisecs Number of packages The Effect of Tim on the Performance of Stan STAN without TIM 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 STAN with TIM + + + + + + + + + + + + + + + + + + + + Figure 6: Graph showing comparison between stan with and stan without tim on Rocket domain problems generated from the Rocket domain provided in Appendix D. 404 Automatic Inference of State Invariants 0 2000 4000 6000 8000 10000 12000 1 1.5 2 2.5 3 3.5 4 4.5 5 Millisecs Number of sub-problems The Effect of Tim on the Performance of Stan STAN without TIM STAN with TIM Figure 7: Graph showing comparison between stan with and stan without tim on Logistics domain problems. which each sub-problem involves the independent transportation of a single package between two cities. In very simple domains, the overhead of carrying out this analysis can outweigh the advantages offered. For example, in the Movie domain used in the competition stan gained no benefits from using tim but paid the overhead to the detriment of its performance on instances from that domain. However, in general we observe that the benefits of this analysis increase with the increasing complexity of domains. 5. Related Work Although the importance of state invariants for efficient planning has been observed there has been relatively little work on automatic inference of invariants. The published work that most closely resembles the research described in this paper is the state constraint inference system discoplan, of Gerevini and Schubert (1998). Discoplan enables the inference of sv-constraints that correspond to a subset of our identity invariants. The reason that discoplan is restricted to a subset is that it generates sv-constraints only for pairs of literals (one on the addlist of a schema and the other on the delete list) in which the arguments vary in only one place. Tim can infer identity invariants in which vectors of arguments vary, as shown in Section 2.7. Discoplan cannot currently infer all singly varying constraints (although the techniques described by Gerevini and Schubert (1996a) are not yet fully implemented in discoplan). For example, discoplan cannot infer that all blocks can only 405 Fox & Long be on one surface, in its analysis of the Blocks world domain cited in the paper. Tim can infer these invariants from its sub-space analysis. Gerevini and Schubert (1996a, 1996b) have also examined the potential for inferring parameter domains that are similar to the operator parameter types inferred by tim. Their domains are inferred by an iterative process of accretion which is similar to the attribute space extension process of tim. However, the accretion process they describe is synthetic, in that the parameter domains are synthesised directly from the operator descriptions and initial state. Tim is an analytic system that constructs its types from an analysis of the functional properties of the domain objects. This analytic approach provides a rich information source from which other structures, including the domain invariants, can be derived. Some of the implicative constraints inferred by discoplan correspond to an implicit type assignment and would arise in the type structure built by tim. A further implicative constraint generated by discoplan refers to the separation of functional roles of objects. In particular, the irreflexivity of on, as in: 8x Delta 8y Delta (on(x; y) ! :(x = y)) can be captured using this kind of constraint. Tim cannot currently infer these invariants. Because tim uses an analysis based on the state view of objects in the domain it is able to generate a broader collection of invariants, including state membership and unique state invariants currently not produced by discoplan. Although discoplan can deal with negative preconditions and tim cannot yet manage them, the invariants they produce overall are currently less powerful than those inferred by tim. Apart from the work of Gerevini and Schubert, there is some older work on the inference of invariants which also relies on the generation of candidate invariants which are then confirmed by an inductive process against the domain operators. Two examples are the work of Kelleher and Cohn (1992) and Morris and Feldman (1989). The former work concentrates on identifying directed mutual persistence relations, which hold between pairs of facts in a domain when, once both are established, the second continues to hold while the first does. The use of these relations leads to the inference of a collection of constraints which fall into the uniqueness invariants inferred by tim. In the work described in (Morris & Feldman, 1989) the authors build invariants by using truth counts which are counts of the number of propositions from particular identified sets which must be true in any state of the domain. Sets for which this count is 1 can then be used to build invariants which are a subset of the state membership and uniqueness invariants. The authors describe methods for attempting to identify the sets of facts from which to work. This work, in common with that of Kelleher and Cohn and of Gerevini and Schubert, builds invariants by first hypothesising a possible seed for the invariants and then determining their validity by analysing the effects of the operators on these seeds. In contrast to this generate-and-test strategy, tim produces only correct invariants which it infers from a deep, structural analysis of the domain. The inference of invariants does not exhaust the possibilities of this analysis. For example, the type structure is inferred automatically during this analysis, which has been shown to have dramatic potential for the efficiency of planning. The relationship between enablers, and the state transitions they enable, determines an ordering on the satisfaction of goals, which also has significance for efficiency. Further, the state-based view of the behaviour of 406 Automatic Inference of State Invariants domain objects would allow the techniques described by McCluskey and Porteous (1997) to be automated. McCluskey and Porteous (1997) have proposed and explored an object-centred approach to planning. This approach is based on the provision, by a domain engineer, of a rich collection of state invariants for object sorts participating in functional relationships in the domain. These invariants are then exploited in a domain compilation phase to facilitate an efficient planning application to that domain. Tim infers precisely the sorts and collections of state invariants that McCluskey and Porteous provide by hand. Grant (1996) generates state invariants from state descriptions, provided by hand, and then uses these invariants to build operator schemas. His approach is clearly related even though the objectives of his analysis are different. Grant is concerned with the automatic synthesis of domain descriptions from a rich requirements specification provided by an expert user. Our concern is with reverse-engineering a domain description to obtain the information that can help increase the efficiency of planners applied to that domain. Although the primary objectives in the use of tim are to enhance the performance of planning within a domain, tim also provides a valuable tool in the construction of domain descriptions by revealing the underlying behaviours that the domain engineer has implicitly imposed, and helping with the debugging of domain descriptions. 6. Conclusion Tim is a planner-independent set of techniques for identifying the underlying structure of a domain, revealing its type structure and a collection of four different kinds of invariant conditions. One important application of these techniques is as a domain debugging aid during the construction of large and complex domains. Using tim has revealed many anomalies in domains encoded by us and by others, and has greatly assisted us in understanding stan's performance on many domains and problems. Another important application is in increasing the efficiency of planners by making explicit to the planner information about the domain that it would otherwise have to infer, from the domain representation, during planning. Tim generates a rich collection of invariants containing many that are not inferrable by related systems, as discussed in the previous section. The results presented by Gerevini and Schubert (1998) suggest that a marked improvement can be obtained from the use of invariants in the performance of planners based on SAT-solving techniques. No analysis has yet been done to determine what advantages might be obtainable by using invariants in planners based on other architectures. Stan does not yet exploit all of the invariants produced by tim during planning. It uses the type structure and the fixed resource invariants and we are currently developing an extension of stan that will fully exploit the other kinds of invariant. We expect to be able to use the uniqueness and identity invariants to shortcut the effort involved in deducing a significant subset of the necessary mutex relations during graph construction. The analysis performed by tim is efficient, growing more slowly than a quadratic function of the size of the initial state being analysed. Our empirical analysis does not consider the effect on tim's performance of increasing numbers of operator schemas. However, the argument presented in Section 4 shows that tim's analysis grows linearly with the number 407 Fox & Long of operator schemas, linearly with the number of domain constants and linearly with the size of the initial state. There are other factors to take into account, but this confirms a polynomial performance as the size (and related structure) of the domain increases. The type analysis performed by tim differs, in some important respects, from the various forms of type analysis performed during the compilation of programs written in strongly typed languages. In the latter context the type-correctness of a program is judged with respect to an imposed context of basic types. Tim infers the basic types from the domain description so it is impossible for a domain specification not to be well-typed. Consequently we do not attempt to type-check domain descriptions using tim. This is a direction in which we hope to move in the near future, because type-checking will enable some unsolvable problems to be detected as unsolvable statically rather than at planning time. We currently focus only on type inference and the exploitation of the inferred type structure in the management of the search space of the planner. 7. Acknowledgements We would like to thank Alfonso Gerevini, Gerry Kelleher and the anonymous referees for useful discussions and helpful comments on earlier drafts of this paper. Appendix A. FTP and Web Sites The aips-98 Planning Competition FTP site is at: http://ftp.cs.yale.edu/pub/mcdermott/aipscomp-results.html. Our web site, on which stan and tim executables can be found, is at: http://www.dur.ac.uk/,dcs0www/research/stanstuff/planpage.html Appendix B. The TIM Algorithm The following is a pseudo-code description of the tim algorithm. fConstruct base PRSs (Section 2.3)g Ps := fg; for each operator schema, O, for each variable in O, x, construct a PRS for x from O and add to Ps; fSplit PRSsg for each PRS in Ps, P, if a property, p, appears in P in both the adds and deleted precs fields then split P over p, into P' and Q and replace P with P' and Q in Ps, where to split P over p: construct PRS Q with the same precs as P, deleted precs and adds both set to fpg; construct PRS P' from P by removing p from deleted precs and adds of P; fConstruct transition rules (Section 2.3)g Ts := fg; for each PRS in Ps, P, construct a transition rule for P and add to Ts; fSeed property and attribute spaces (Section 2.3)g let each property be initially assigned to a separate equivalence class; for each rule, r, in Ts merge together (unite) the equivalence classes for all the properties in the start and finish of r; 408 Automatic Inference of State Invariants construct a separate space for each equivalence class of properties; fAssign transition rules (Section 2.4)g for each rule, r, in Ts place r in the space associated with the equivalence class containing the properties in the start (and finish) of r, s; if r is an increasing or decreasing rule then mark s as an attribute space; fAnalyse initial state (Section 2.4)g for each object, o, in the domain identify the bag of initial properties of o, I(o); for each space, s, construct the bag of properties from I(o) which belong to the equivalence class associated with s, b; if b is non-empty then add o to the space s; if s is not an attribute space then add b as a state in s; fExtend property spaces (Section 2.4)g for each property space, p, while there is an unextended state in p, s, mark s as extended; newgen := fg; for each rule in p, r, if the start of r is included in s then add the state snew = (s ominus start oplus end) to newgen; if snewis a superset of any state in newgen then mark p is an attribute space and exit the analysis of p; add newgen to the states in p; fExtend attribute spaces (Section 2.4)g changes := TRUE; while changes, changes := FALSE; for each unmarked attribute space, a, extend a where to extend a: mark a; for each rule in a, r, for each property in enablers of r, p, if p's equivalence class is associated with an unmarked attribute space, a', then extend a'; add all objects that appear in every space associated with an enabling property for r to a; if objects are added then changes := TRUE; fIdentify types (Section 2.6)g for each object in the domain, o, identify the pattern of membership of spaces for o, tt; associate the type pattern, tt, with o; for each operator schema, O, for each argument of O, x, identify the pattern of membership of spaces for x implied by the properties of x in the preconditions of O, tt; associate type pattern, tt, with x in O; fConstruct invariants (Section 2.7)g for each property space, P, for each property in P, p, construct an identity invariant for p; construct a state membership invariant for P; construct a uniqueness invariant for P; 409 Fox & Long Appendix C. Example Output The following output was produced by tim and can be found, along with other examples, on the stan webpage. These examples show the details of the analysis performed on each of three domains: a Flat-tyre domain, a Mystery domain and a Logistics domain. The analysis is done with respect to an initial state and a set of operator schemas. The operator schemas used in these three domains are those provided with the pddl strips releases for these domains. The initial states were taken from the pddl release. The pddl release can be found at http://www.cs.yale.edu/HTML/YALE/CS/HyPlans/mcdermott.html. C.1 The Tyre World TIM: Type Inference Mechanism - support for STAN: State Analysis Planner D. Long and M. Fox, University of Durham Reading domain file: domain01.pddl Reading problem file: prob01.pddl TIM: Domain analysis complete for flat-tire-strips TIM: TYPES: Type T0 = -wrench"" Type T1 = -wheel2"" Type T2 = -wheel1"" Type T3 = -trunk"" Type T4 = -the-hub"" Type T5 = -pump"" Type T6 = -nuts"" Type T7 = -jack"" It will be noticed that the two wheels are separated into different types. This is because one wheel is intact and the other is not intact, and there is no operator for repairing wheels that are not intact. The tools have each been given different types. This is because they each appear as constants in different operators and therefore are functionally distinct. TIM: STATE INVARIANTS: FORALL x:T4. (on-ground(x) OR lifted(x)) FORALL x:T4. NOT (on-ground(x) AND lifted(x)) FORALL x:T3. (closed(x) OR open(x)) FORALL x:T3. NOT (closed(x) AND open(x)) 410 Automatic Inference of State Invariants FORALL x:T1 U T2. (deflated(x) OR inflated(x)) FORALL x:T1 U T2. NOT (deflated(x) AND inflated(x)) The invariants for hubs (below) suggest that almost anything could be on a hub. Since this is not the case the type structure is under-discriminating. However, the additional invariants drawn from the sub-space analysis provide enough information, in principle, to discriminate more fully between the types. This information is not yet being fully exploited. FORALL x:T4. FORALL y1. FORALL z1. on(y1,x) AND on(z1,x) =? y1 = z1 FORALL x:T4. (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. on(y1,x) OR free(x)) FORALL x:T4. NOT (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. on(y1,x) AND free(x)) FORALL x:T4. FORALL y1. FORALL z1. tight(y1,x) AND tight(z1,x) =? y1 = z1 FORALL x:T4. FORALL y1. FORALL z1. loose(y1,x) AND loose(z1,x) =? y1 = z1 FORALL x:T4. ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. tight(y1,x) AND fastened(x)) OR (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. loose(y1,x) AND fastened(x)) OR unfastened(x)) FORALL x:T4. NOT ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. tight(y1,x) AND fastened(x)) AND (Exists y1:T0 U T1 U T2 U T5 U T6 U T7. loose(y1,x) AND fastened(x))) FORALL x:T4. NOT ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. tight(y1,x) AND fastened(x)) AND unfastened(x)) FORALL x:T4. NOT ((Exists y1:T0 U T1 U T2 U T5 U T6 U T7. loose(y1,x) AND fastened(x)) AND unfastened(x)) TIM: DOMAIN INVARIANTS: ---x0: container(x0)""-- = 1 ---x0: hub(x0)""-- = 1 ---x0: intact(x0)""-- = 1 ---x0: jack(x0)""-- = 1 ---x0: nut(x0)""-- = 1 ---x0: pump(x0)""-- = 1 ---x0: unlocked(x0)""-- = 1 ---x0: wheel(x0)""-- = 2 ---x0: wrench(x0)""-- = 1 TIM: ATTRIBUTE SPACES: 411 Fox & Long The attribute space for the properties in the first of these groups is subjected to a much more rigorous analysis in the sub-space invariants below. Objects, x, in T0 U T1 U T2 U T5 U T6 U T7 can have property: Exists y1:T3. in(x,y1); Exists y1:T4. on(x,y1); Exists y1:T4. tight(x,y1); Exists y1:T4. loose(x,y1); have(x); Objects, x, in T3 can have property: Exists y1:T0 U T1 U T2 U T5 U T6 U T7. in(y1,x); Objects, x, in T3 all have property: container(x); Objects, x, in T4 all have property: hub(x); Objects, x, in T1 all have property: intact(x); Objects, x, in T7 all have property: jack(x); Objects, x, in T6 all have property: nut(x); Objects, x, in T5 all have property: pump(x); Objects, x, in T3 all have property: unlocked(x); Objects, x, in T1 U T2 all have property: wheel(x); Objects, x, in T0 all have property: wrench(x); TIM: OPERATOR PARAMETER RESTRICTIONS: inflate(x1:T1) put-on-wheel(x1:T1 U T2,x2:T4) remove-wheel(x1:T1 U T2,x2:T4) put-on-nuts(x1:T6,x2:T4) remove-nuts(x1:T6,x2:T4) jack-down(x1:T4) jack-up(x1:T4) tighten(x1:T6,x2:T4) loosen(x1:T6,x2:T4) put-away(x1:T0 U T1 U T2 U T5 U T6 U T7,x2:T3) fetch(x1:T0 U T1 U T2 U T5 U T6 U T7,x2:T3) close-container(x1:T3) open-container(x1:T3) cuss() TIM: ADDITIONAL STATE INVARIANTS, USING SUB-SPACE ANALYSIS: We report here only the additional state invariants that add information to the invariants already listed. TIM currently reports invariants that are subsumed by the earlier collection. It should be observed that the first wheel is intact but the second is not, and this gives rise to the following new invariant for wheels of the second type. 412 Automatic Inference of State Invariants FORALL x:T2. (deflated(x)) The first attribute space, which contains all objects except the trunk and the hub, is now subjected to sub-space analysis yielding a rich new collection of invariants. FORALL x:T0. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =? y1 = z1 FORALL x:T0. (Exists y1:T3. in(x,y1) OR have(x)) FORALL x:T0. NOT (Exists y1:T3. in(x,y1) AND have(x)) FORALL x:T1. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =? y1 = z1 FORALL x:T1. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) =? y1 = z1 FORALL x:T1. (Exists y1:T3. in(x,y1) OR have(x) OR Exists y1:T4. on(x,y1)) FORALL x:T1. NOT (Exists y1:T3. in(x,y1) AND have(x)) FORALL x:T1. NOT (Exists y1:T3. in(x,y1) AND Exists y1:T4. on(x,y1)) FORALL x:T1. NOT (have(x) AND Exists y1:T4. on(x,y1)) FORALL x:T2. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =? y1 = z1 FORALL x:T2. FORALL y1. FORALL z1. on(x,y1) AND on(x,z1) =? y1 = z1 FORALL x:T2. (Exists y1:T4. on(x,y1) OR have(x) OR Exists y1:T3. in(x,y1)) FORALL x:T2. NOT (Exists y1:T4. on(x,y1) AND have(x)) FORALL x:T2. NOT (Exists y1:T4. on(x,y1) AND Exists y1:T3. in(x,y1)) FORALL x:T2. NOT (have(x) AND Exists y1:T3. in(x,y1)) FORALL x:T5. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =? y1 = z1 FORALL x:T5. (Exists y1:T3. in(x,y1) OR have(x)) FORALL x:T5. NOT (Exists y1:T3. in(x,y1) AND have(x)) FORALL x:T6. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =? y1 = z1 FORALL x:T6. FORALL y1. FORALL z1. tight(x,y1) AND tight(x,z1) =? y1 = z1 FORALL x:T6. FORALL y1. FORALL z1. loose(x,y1) AND loose(x,z1) =? y1 = z1 FORALL x:T6. (Exists y1:T4. tight(x,y1) OR Exists y1:T4. loose(x,y1) OR have(x) OR Exists y1:T3. in(x,y1)) FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND Exists y1:T4. loose(x,y1)) FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND have(x)) FORALL x:T6. NOT (Exists y1:T4. tight(x,y1) AND Exists y1:T3. in(x,y1)) FORALL x:T6. NOT (Exists y1:T4. loose(x,y1) AND have(x)) FORALL x:T6. NOT (Exists y1:T4. loose(x,y1) AND Exists y1:T3. in(x,y1)) FORALL x:T6. NOT (have(x) AND Exists y1:T3. in(x,y1)) 413 Fox & Long C.2 The Mystery Domain The Mystery domain was devised by Drew McDermott for the aips-98 planning competition. His intention was to conceal the structure of the problem domain by employing an obscure encoding of a transportation domain. The code replaces locations with the names of foods and the routes between them with eats relations. The transports are pleasures while cargos are pains. Cargos and transports can be at locations, with the at relation encoded as craves. A cargo is either at a location or in a transport encoded by the fears relation. Transports have restricted capacity encoded by planets and consume fuel in travelling between locations. Fuel exists in limited quantities at locations measured by provinces. Using TIM we were able to decode the domain and identify the roles played by each of the components of the encoding. TIM: Domain analysis complete for mystery-strips (prob048.pddl) TIM: TYPES: It should be noted that provinces (types T6, T7 and T8) are divided into three separate types because they form a sequence, defined by the attacks relation, in which the first and last have a slightly different functional role to the others. The same is true of the planets (types T1, T2 and T3). Type T0 = -beef,cantelope,chocolate,flounder,guava,mutton,onion, pepper,rice,shrimp,sweetroll,tuna,yogurt"" Type T1 = -saturn"" Type T2 = -pluto"" Type T3 = -neptune"" Type T4 = -achievement,lubricity"" Type T5 = -abrasion,anger,angina,boils,depression,grief,hangover, laceration"" Type T6 = -alsace,bosnia,guanabara,kentucky"" Type T7 = -goias"" Type T8 = -arizona"" TIM: STATE INVARIANTS: FORALL x:T4. FORALL y1. FORALL z1. harmony(x,y1) AND harmony(x,z1) =? y1 = z1 FORALL x:T4. (Exists y1:T1 U T2 U T3. harmony(x,y1)) FORALL x:T0. FORALL y1. FORALL z1. locale(x,y1) AND locale(x,z1) =? y1 = z1 FORALL x:T0. (Exists y1:T6 U T7 U T8. locale(x,y1)) FORALL x:T4 U T5. FORALL y1. FORALL z1. fears(x,y1) 414 Automatic Inference of State Invariants AND fears(x,z1) =? y1 = z1 FORALL x:T4 U T5. FORALL y1. FORALL z1. craves(x,y1) AND craves(x,z1) =? y1 = z1 FORALL x:T4 U T5. (Exists y1:T0. craves(x,y1) OR Exists y1:T4. fears(x,y1)) FORALL x:T4 U T5. NOT (Exists y1:T0. craves(x,y1) AND Exists y1:T4. fears(x,y1)) TIM: DOMAIN INVARIANTS: ---(x0,x1): attacks(x0,x1)""-- = 5 ---(x0,x1): eats(x0,x1)""-- = 36 ---x0: food(x0)""-- = 13 ---(x0,x1): harmony(x0,x1)""-- = 2 ---(x0,x1): locale(x0,x1)""-- = 13 ---(x0,x1): orbits(x0,x1)""-- = 2 ---x0: pain(x0)""-- = 8 ---x0: planet(x0)""-- = 3 ---x0: pleasure(x0)""-- = 2 ---x0: province(x0)""-- = 6 TIM: ATTRIBUTE SPACES: Objects, x, in T1 U T2 U T3 can have property: Exists y1:T4. harmony(y1,x); Objects, x, in T6 U T7 U T8 can have property: Exists y1:T0. locale(y1,x); Objects, x, in T4 can have property: Exists y1:T4. fears(y1,x); Objects, x, in T0 can have property: Exists y1:T4 U T5. craves(y1,x); Objects, x, in T6 U T7 all have property: Exists y1:T6 U T8. attacks(x,y1); Objects, x, in T6 U T8 all have property: Exists y1:T6 U T7. attacks(y1,x); Objects, x, in T0 all have property: Exists y1:T0. eats(x,y1); Objects, x, in T0 all have property: Exists y1:T0. eats(y1,x); Objects, x, in T0 all have property: food(x); Objects, x, in T2 U T3 all have property: Exists y1:T1 U T2. orbits(x,y1); 415 Fox & Long Objects, x, in T1 U T2 all have property: Exists y1:T2 U T3. orbits(y1,x); Objects, x, in T5 all have property: pain(x); Objects, x, in T1 U T2 U T3 all have property: planet(x); Objects, x, in T4 all have property: pleasure(x); Objects, x, in T6 U T7 U T8 all have property: province(x); TIM: OPERATOR PARAMETER RESTRICTIONS: succumb(x1:T5,x2:T4) feast(x1:T4,x2:T0,x3:T0) overcome(x1:T5,x2:T4) TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS: These additional invariants show that the transports are always at a location and never loaded into other transports. FORALL x:T4. FORALL y1. FORALL z1. craves(x,y1) AND craves(x,z1) =? y1 = z1 FORALL x:T4. (Exists y1:T0. craves(x,y1)) C.3 The Logistics Domain TIM: Domain analysis complete for logistics-strips (prob05.pddl) TIM: TYPES: Type T0 = -bos-truck,la-truck,pgh-truck"" Type T1 = -bos-po,la-po,pgh-po"" Type T2 = -bos-airport,la-airport,pgh-airport"" Type T3 = -bos,la,pgh"" Type T4 = -package1,package2,package3,package4,package5,package6, package7,package8"" Type T5 = -airplane1,airplane2"" TIM: STATE INVARIANTS: FORALL x:T0 U T4 U T5. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) =? y1 = z1 FORALL x:T0 U T4 U T5. FORALL y1. FORALL z1. in(x,y1) AND in(x,z1) =? y1 = z1 FORALL x:T0 U T4 U T5. (Exists y1:T1 U T2. at(x,y1) 416 Automatic Inference of State Invariants OR Exists y1:T0 U T5. in(x,y1)) FORALL x:T0 U T4 U T5. NOT (Exists y1:T1 U T2. at(x,y1) AND Exists y1:T0 U T5. in(x,y1)) TIM: DOMAIN INVARIANTS: ---x0: airplane(x0)""-- = 2 ---x0: airport(x0)""-- = 3 ---x0: city(x0)""-- = 3 ---(x0,x1): in-city(x0,x1)""-- = 6 ---x0: location(x0)""-- = 6 ---x0: obj(x0)""-- = 8 ---x0: truck(x0)""-- = 3 TIM: ATTRIBUTE SPACES: Objects, x, in T1 U T2 can have property: Exists y1:T0 U T4 U T5. at(y1,x); Objects, x, in T0 U T5 can have property: Exists y1:T0 U T4 U T5. in(y1,x); Objects, x, in T5 all have property: airplane(x); Objects, x, in T2 all have property: airport(x); Objects, x, in T3 all have property: city(x); Objects, x, in T1 U T2 all have property: Exists y1:T3. in-city(x,y1); Objects, x, in T3 all have property: Exists y1:T1 U T2. in-city(y1,x); Objects, x, in T1 U T2 all have property: location(x); Objects, x, in T4 all have property: obj(x); Objects, x, in T0 all have property: truck(x); TIM: OPERATOR PARAMETER RESTRICTIONS: drive(x1:T0,x2:T1 U T2,x3:T1 U T2,x4:T3) fly(x1:T5,x2:T2,x3:T2) unload(x1:T0 U T4 U T5,x2:T0 U T5,x3:T1 U T2) load-plane(x1:T4,x2:T5,x3:T1 U T2) load-truck(x1:T4,x2:T0,x3:T1 U T2) TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS: 417 Fox & Long The following invariants add the constraints that trucks and airplanes must always be at a location and never loaded into one another. FORALL x:T0. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) =? y1 = z1 FORALL x:T0. (Exists y1:T1 U T2. at(x,y1)) FORALL x:T5. FORALL y1. FORALL z1. at(x,y1) AND at(x,z1) =? y1 = z1 FORALL x:T5. (Exists y1:T1 U T2. at(x,y1)) Appendix D. The Rocket Domain The Rocket domain used in the construction of Figure 6 is as follows: (define (domain rocket) (:predicates (at ?x ?y) (in ?x ?y) (fuelled ?x) (unfuelled ?x) (loc ?x) (obj ?x) (container ?x)) (:action fly :parameters (?x ?y ?z) :precondition (and (at ?x ?y) (loc ?z) (fuelled ?x)) :effect (and (not (at ?x ?y)) (at ?x ?z) (unfuelled ?x) (not (fuelled ?x)))) (:action load :parameters (?x ?y ?z) :precondition (and (obj ?x) (container ?y) (at ?x ?z) (at ?y ?z)) :effect (and (in ?x ?y) (not (at ?x ?z)))) (:action unload :parameters (?x ?y ?z) :precondition (and (at ?y ?z) (in ?x ?y)) :effect (and (at ?x ?z) (not (in ?x ?y))))) Appendix E. Operator Test Domain This domain is an artificial domain used to test the effects of increasing operators and literals in the domain encoding on the performance of TIM. This example is the third instance - the variation was achieved by adding more operator schemas in the pattern of those included here. 418 Automatic Inference of State Invariants (define (domain od) (:predicates (p1 ?x ?y) (q1 ?x ?y) (p2 ?x ?y) (q2 ?x ?y) (p3 ?x ?y) (q3 ?x ?y) (p4 ?x ?y) (q4 ?x ?y) (p5 ?x ?y) (q5 ?x ?y) (p6 ?x ?y) (q6 ?x ?y) (p7 ?x ?y) (q7 ?x ?y) (p8 ?x ?y) (q8 ?x ?y) (p9 ?x ?y) (q9 ?x ?y) (p10 ?x ?y) (q10 ?x ?y) (p11 ?x ?y) (q11 ?x ?y) (p12 ?x ?y) (q12 ?x ?y) (p13 ?x ?y) (q13 ?x ?y) (p14 ?x ?y) (q14 ?x ?y) (p15 ?x ?y) (q15 ?x ?y) (p16 ?x ?y) (q16 ?x ?y) (p17 ?x ?y) (q17 ?x ?y) (p18 ?x ?y) (q18 ?x ?y) (p19 ?x ?y) (q19 ?x ?y) (p20 ?x ?y) (q20 ?x ?y)) (:action o1 :parameters (?x ?y ?z) :precondition (and (p1 ?x ?y) (q1 ?x ?z)) :effect (and (not (p1 ?x ?y)) (not (q1 ?x ?z)) (p1 ?x ?z) (q1 ?x ?y))) (:action o2 :parameters (?x ?y ?z) :precondition (and (p2 ?x ?y) (q2 ?x ?z)) :effect (and (not (p2 ?x ?y)) (not (q2 ?x ?z)) (p2 ?x ?z) (q2 ?x ?y))) (:action o3 :parameters (?x ?y ?z) :precondition (and (p3 ?x ?y) (q3 ?x ?z)) :effect (and (not (p3 ?x ?y)) (not (q3 ?x ?z)) (p3 ?x ?z) (q3 ?x ?y)))) The problem instance was fixed as follows: (define (problem op) (:domain od) (:objects a b c) 419 Fox & Long (:init (p1 a b) (q1 a c) (p2 a b) (q2 a c) (p3 a b) (q3 a c) (p4 a b) (q4 a c) (p5 a b) (q5 a c) (p6 a b) (q6 a c) (p7 a b) (q7 a c) (p8 a b) (q8 a c) (p9 a b) (q9 a c) (p10 a b) (q10 a c) (p11 a b) (q11 a c) (p12 a b) (q12 a c) (p13 a b) (q13 a c) (p14 a b) (q14 a c) (p15 a b) (q15 a c) (p16 a b) (q16 a c) (p17 a b) (q17 a c) (p18 a b) (q18 a c) (p19 a b) (q19 a c) (p20 a b) (q20 a c)) (:goal (and (p1 a c) (q1 a b)))) References Blum, A., & Furst, M. (1995). Fast Planning through Plan-graph Analysis. In IJCAI. Bundy, A., Burstall, R., Weir, S., & Young, R. (1980). Artificial Intelligence: An Introductory Course. Edinburgh University Press. Fikes, R., & Nilsson, N. (1971). STRIPS: A New Approach to the Application of TheoremProving to Problem-Solving. Artificial Intelligence, 2 (3). Gerevini, A., & Schubert, L. (1996a). Accelerating Partial Order Planners: Some Techniques for Effective Search Control and Pruning. JAIR, 5, 95-137. Gerevini, A., & Schubert, L. (1996b). Computing Parameter Domains as an Aid to Planning. In AIPS-96. Gerevini, A., & Schubert, L. (1998). Inferring State Constraints for Domain-Independent Planning. In AAAI. Grant, T. J. (1996). Inductive Learning of Knowledge-based Planning Operators. Ph.D. thesis, Rijksuniversiteit Limburg de Maastricht. Kautz, H., & Selman, B. (1998). The Role of Domain Specific Knowledge in the Planning as Satisfiability Framework. In The Fourth International Conference on Artificial Intelligence Planning Systems. 420 Automatic Inference of State Invariants Kelleher, G., & Cohn, A. (1992). Automatically Synthesising Domain Constraints from Operator Descriptions. In Proceedings ECAI92. Koehler, J., Nebel, B., & Dimopoulos, Y. (1997). Extending Planning Graphs to an ADL Subset. In Proceedings of 4th European Conference on Planning. Liatsos, V., & Richards, B. (1997). Least Commitment: An Optimal Planning Strategy. In Proceedings of the 16th Workshop of the UK Planning and Scheduling Special Interest Group. Long, D., & Fox, M. (in press). The Efficient Implementation of the Plangraph in stan. In JAIR. McCluskey, T. L., & Porteous, J. (1997). Engineering and Compiling Planning Domain Models to Promote Validity and Efficiency. Artificial Intelligence, 95 (1). Morris, P., & Feldman, R. (1989). Automatically Derived Heuristics for Planning Search. In Proceedings of the 2nd Irish Conference on Artificial Intelligence and Cognitive Science, School of Computer Applications, Dublin City University. 421