An abstract planning is the first phase of the web service composition in the Planics framework. A user query specifies the initial and the expected state of a plan in request. The paper extends Planics with a module for temporal planning, by extending the user query with an LT Lk X formula specifying temporal aspects of world transformations in a plan. Our solution comes together with an example, an implementation, and experimental results.
Web service composition within Service-Oriented Architecture (SOA) [
In this paper, we follow the approach of the system Planics [
2011/01/B/ST6/01477.
two approaches: one based on a translation to SMT-solvers [
We propose a novel approach based on applying SMT-solvers. Contrary to a number of other approaches, we focus not only on searching for a single plan, but we attempt to find all significantly different plans. We start with defining the abstract planning problem (APP, for short). Then, we present our original approach to APP based on a compact representation of abstract plans by multisets of service types. We introduce the language of LT Lk X for specifying the temporal aspects of the user query. This approach is combined with a reduction to a task for an SMT-solver. The encoding of blocking formulas allows for pruning the search space with many sequences which use the same multiset of service types in some plan already generated. Moreover, we give details of our algorithms and their implementations that are followed by experimental results. To the best of our knowledge, the above approach is novel, and as our experiments show it is also very promising.
The rest of the paper is organized as follows. Related work is discussed in Section 2. Section 3 deals with the abstract planning problem. In Section 4 the temporal planning is presented. An example of an abstract temporal planning is shown in Section 5. Section 6 discusses the implementation and the experimental results of our planning system. The last section summarizes this paper and discusses a further work. 2
A classification matrix aimed at the influence on the effort of Web service
composition is presented in [
Most of the applications of SMT in the domain of WSC is related to the
automatic verification and testing. For example, a message race detection
problem is investigated in [
Recently, there have also appeared papers dealing with temporal logics in
the context of WSC. Bersani et al. in [
Searching for plans meeting temporal restrictions is also a topic of interest of
a broad planning community. The PDDL language [
The OWL language [
Thing
Stamp Artifact
Service
The branch of classes rooted at Artifact is composed of the types of the objects, which the services operate on. Each object consists of a number of attributes, whereas an attribute consists of a name and a type. Note that the types of the attributes are irrelevant in the abstract planning phase as they are not used by the planner. The values of the attributes of an object determine its state, but in the abstract planning it is enough to know only whether an attribute does have some value (i.e., is set), or it does not (i.e., it is null). The Stamp class and its descendants define special-purpose objects, often useful in constructing a user query, and in the planning process. A stamp is a specific type aimed at a confirmation of the service execution. The specialized descendants of the Service class can produce the stamp being an instance of any subtype of Stamp and describing additional execution features. Note that each service produces exactly one confirmation object. The classes derived from Artifact and Stamp are called the object types.
Each class derived from Service, called a service type, stands for a description of a set of real-world services. It contains a formalized information about their activities. A service type affects a set of objects and transforms them into a new set of objects. The detailed information about this transformation is contained in the attributes of a service type: the sets in, inout, and out, and the Boolean formulas pre and post (pre and post, for short). These sets enumerate the objects, which are processed by the service. The objects of the in set are read-only, i.e., they are passed unchanged to the next world. Each object of inout can be modified - the service can change some values of its attributes. The objects of out are produced by the service. Let I denote the set of all identifiers used as the type names, the objects, and the attributes. In APP we deal with abstract values only, the types of the attributes are irrelevant, and we identify the attributes with their names. Moreover, we denote the set of all attributes by A, where A ⇢ I. An object type is a pair (t, Attr), where t 2 I, and Attr ✓ A. That is, an object type consists of the type name and a set of the attributes. By P we mean a set of all object types. Example 1. Consider the following exemplary ontology containing in addition to Thing also the class Artifact and Stamp. The class Artifact corresponds to the object type (Artif act, {id}) (the only attribute is an identifier) while the class Stamp corresponds to the object type (Stamp, {serviceClass, serviceId, level}), introducing the attributes describing the service generating the stamp, and the position of this service in an execution sequence we consider.
We define also a transitive, irreflexive, and antisymmetric inheritance relation Ext ✓ P ⇥ P, such that (t1, A1), (t2, A2) 2 Ext iff t1 6= t2 and A1 ✓ A2. That is, a subtype contains all the attributes of a base type and optionally introduces more attributes. An object o is a pair o = (id, type), where id 2 I and type 2 P. By type(o) we denote the type of o. The set of all objects is denoted by O. Amongst all the objects we distinguish between the artifacts (the instances of the Artifact type) and the stamps (the instances of the Stamp type). The set of all the stamps is denoted by ST, where ST ✓ O. Moreover, we define the function attr : O 7 ! 2A returning the set of all attributes for each object of O. Service types and user queries. The service types available for composition are defined in the ontology by service type specifications. The user goal is provided in a form of a user query specification, which is then extended by a temporal formula. Before APP, all the specifications are reduced to sets of objects and abstract formulas over them. An abstract formula over a set of objects O and their attributes is a DNF formula without negations, i.e., the disjunction of clauses, referred to as abstract clauses. Every abstract clause is the conjunction of literals, specifying abstract values of object attributes using the functions isSet and isN ull. In the abstract formulas used in APP, we assume that no abstract clause contains both isSet(o.a) and isN ull(o.a), for the same o 2 O and a 2 attr(o). For example (isSet(o.a) ^ isSet(o.b)) _ isN ull(o.a) is a correct abstract formula. The syntax of the specifications of the user queries and of the service types is the same and it is defined below.
inout, out are pairwise disjoint sets of objects, and pre is an abstract formula defined over objects from in [ inout, while post is an abstract formula defined over objects from in [ inout [ out.
A user query specification q or a service type specification s is denoted by specx = (inx, inoutx, outx, prex, postx), where x 2 {q, s}, resp. In order to formally define the user queries and the service types, which are interpretations of their specifications, we need to define the notions of valuation functions and worlds.
Definition 2. Let ' = Wi=1..n ↵ i be an abstract formula. A valuation of the attributes over ↵ i is the partial function v↵ i : So2 O{o} ⇥ attr(o) 7 ! {true, f alse}, where: • v↵ i(o, a)= true if isSet(o.a) is a literal of ↵ i, and • v↵ i(o, a)= f alse if isN ull(o.a) is a literal of ↵ i, and • v↵ i(o, a) is undefined, otherwise. We define the restriction of a valuation function v↵ i to a set of objects O ⇢ O as v↵ i (O) = v↵ i So2 O{o}⇥ attr(o). The undefined values appear when the interpreted abstract formula does not specify abstract values of some attributes, which is a typical case in the WSC domain. The undefined values are used also for representing families of total valuation functions. Next, for a partial valuation function f , by total(f ) we denote the family of the total valuation functions on the same domain, which are consistent with f , i.e., agree on the values defined of f . Moreover, we define a family of the valuation functions V' over the abstract formula ' as the union of the sets of the consistent valuation functions over every abstract clause ↵ i, i.e., V' = Sin=1 total(v↵ i ). The restriction of the family of functions V' to a set of objects O and their attributes is defined as V' (O) = Sn
i=1 total(v↵ i (O)).
Definition 3. A world w is a pair (Ow, vw), where Ow ✓ O and vw = v(Ow) is a total valuation function equal to some valuation function v restricted to Ow. The size of w, denoted by |w| is equal to |Ow|.
That is, a world represents a state of a set of objects, where each attribute is either set or null. By a sub-world of w we mean a world built from a subset of Ow and vw restricted to the objects from the chosen subset. Moreover, a pair consisting of a set of objects and a family of total valuation functions defines a set of worlds. That is, if V = {v1, . . . , vn} is a family of total valuation functions and O ✓ O is a set of objects, then O, V(O) means the set { O, vi(O) | 1 i n}, for n 2 N. Finally, the set of all worlds is denoted by W.
Now, we are in a position to define a service type and a (basic) user query as an interpretation of its specification. In the next section the user query is extended to a temporal version.
Definition 4. Let specx = (inx, inoutx, outx, prex, postx) be a user query or a service type specification, where x 2 {q, s}, resp. An interpretation of specx is a pair of world sets x = (Wpxre, Wpxost), where: – Wpxre = inx [ inoutx, Vpxre , where Vpre is the family of the valuation funcx tions over prex, – Wpxost = inx [ inoutx [ outx, Vpxost , where Vpost is the family of the valuation x functions over postx.
An interpretation of a user query (service type) specification is called simply a user query (service type, resp.).
For a service type (Wpsre, Wpsost), Wpsre is called the input world set, while Wpsost - the output world set. The set of all the service types defined in the ontology is denoted by S. For a user query (Wpqre, Wpqost), Wpqre is called the initial world set, while Wpqost - the expected world set, and denoted by Wiqnit and Weqxp, respectively. Abstract Planning Overview. The main goal of APP is to find a composition of service types satisfying a user query, which specifies some initial and some expected worlds as well as some temporal aspects of world transformations.
Intuitively, an initial world contains the objects owned by the user, whereas an expected world consists of the objects required to be the result of the service composition. To formalize it, we need several auxiliary concepts.
Let o, o0 2 O and v and v0 be valuation functions. We say that v0(o0) is compatible with v(o), denoted by v0(o0) obj v(o), iff the types of both objects are the same, or the type of o0 is a subtype of type of o, i.e., type(o) = type(o0) or (type(o0), type(o)) 2 Ext, and for all attributes of o, we have that v0 agrees with v, i.e., 8 a2 attr(o)v0(o0, a) = v(o, a). Intuitively, an object of a richer type (o0) is compatible with the one of the base type (o), provided that the valuations of all common attributes are equal.
Let w = (O, v), w0 = (O0, v0) be worlds. We say that the world w0 is compatible with the world w, denoted by w0 wrlw, iff there exists a one-to-one mapping map : O 7 ! O0 such that 8 o2 Ov0(map(o)) obj v(o). Intuitively, w0 is compatible with w if both of them contain the same number of objects and for each object from w there exists a compatible object in w0. The world w0 is called subcompatible with the world w, denoted by w0 swrlw iff there exists a sub-world of w0 compatible with w.
World transformations. One of the fundamental concepts in our approach concerns a world transformation. A world w, called a world before, can be transformed by a service type s, having specification specs, if w is sub-compatible with some input world of s. The result of such a transformation is a world w0, called a world after, in which the objects of outs appear, and, as well as the objects of inouts, they are in the states consistent with some output world of s. The other objects of w do not change their states. In a general case, there may exist a number of worlds possible to obtain after a transformation of a given world by a given service type, because more than one sub-world of w can be compatible with an input world of s. Therefore, we introduce a context function, which provides a strict mapping between objects from the worlds before and after, and the objects from the input and output worlds of a service type s.
injection, which for a given service type s and a set of objects O assigns an object from O to each object from ins, inouts, and outs.
Now, we can define a world transformation.
Definition 6. Let w, w0 2 W be worlds, called a world before and a world after, respectively, and s = (Wpsre, Wpsost) be a service type. Assume that w = (O, v), w0 = (O0, v0), where O ✓ O0 ✓ O, and v, v0 are valuation functions. Let ctxsO0 be a context function, and the sets IN , IO, OU be the ctxsO0 images of the sets ins, inouts, and outs, respect., i.e., IN = ctxsO0 ins , IO = ctxsO0 inouts , and OU = ctxsO0 outs . Moreover, let IN, IO ✓ (O \ O0) and OU = (O0 \ O).
We say that a service type s transforms the world w into w0 in the context ctxsO0 , denoted by w s,c!txsO0 w0, if for some vpsre 2 Vpsre and vpsost 2 Vpsost, all the following conditions hold: 1. IN, v(IN )
wrl ins, vpsre(ins) , 2. (IO, v(IO)) wrl inouts, vpsre(inouts) , 3. (IO, v0(IO)) wrl inouts, vpsost(inouts) , 4. (OU, v0(OU )) wrl outs, vpsost(outs) , 5. 8 o2 (O\IO) 8 a2 attr(o) v(o, a) = v0(o, a).
Intuitively, (1) the world before contains a sub-world built over IN , which is compatible with a sub-world of some input world of the service type s, built over the objects from ins. (2) The world before contains a sub-world built over IO, which is compatible with a sub-world of the input world of the service type s, built over the objects from inouts. (3) After the transformation the state of objects from IO is consistent with posts. (4) The objects produced during the transformation (OU ) are in a state consistent with posts. (5) The objects from IN and the objects not involved in the transformation do not change their states.
In the standard way we extend a world transformation to a sequence of world transformations seq. We say that a world w0 is transformed by the sequence seq into a world wn, denoted by w0 seq wn, iff there exists a sequence of worlds ⇢ = (w0, w1, . . . , wn) such that 8 1 i n wi 1 si,c!txsOii wi = (Oi, vi) for some vi. Then, the sequence seq = (s1, . . . , sn) is called a transformation sequence and ⇢ is called a world sequence.
Having the transformation sequences defined, we introduce the concept of user query solutions or simply solutions, in order to define a plan. Definition 7. Let seq be a transformation sequence, q = (Wiqnit, Weqxp) be a user query. We say that seq is a solution of q, if for w 2 Wiqnit and some world w0 such that w seq w0, we have w0 swrlweqxp, for some weqxp 2 Weqxp. The world sequence corresponding to seq is called a world solution. The set of all the (world) solutions of the user query q is denoted by QS(q) (W S(q), resp.). Intuitively, by a solution of q we mean any transformation sequence transforming some initial world of q to a world sub-compatible to some expected world of q. Plans. Basing on the definition of a solution to the user query q, we can now define the concept of an (abstract) plan, by which we mean a non-empty set of solutions of q. We define a plan as an equivalence class of the solutions, which do not differ in the service types used. The idea is that we do not want to distinguish between solutions composed of the same service types, which differ only in the ordering of their occurrences or in their contexts. So we group them into the same class. There are clearly two motivations behind that. Firstly, the user is typically not interested in obtaining many very similar solutions. Secondly, from the efficiency point of view, the number of equivalence classes can be exponentially smaller than the number of the solutions. Thus, two user query solutions are equivalent if they consist of the same number of the same service types, regardless of the contexts.
Definition 8. Let seq 2 QS(q) be a solution of some user query q. An abstract plan is a set of all the solutions equivalent to seq, denoted by [seq]⇠ . It is important to notice that all the solutions within an abstract plan are built over the same multiset of service types, so a plan is denoted using a multiset notation, e.g., the plan [2S + 4T + 3R] consists of 2 services S, 4 services T , and 3 services R.
In order to give the user a possibility to specify not only the initial and expected states of a solution, we extend the user query with an LT Lk X formula ' specifying temporal aspects of world transformations in a solution. Then, the temporal solutions are these solutions for which the world sequences satisfy ' . This is formally introduced in the next section. 4
In this section we extend the user query by an LT Lk X temporal formula and a solution to a temporal solution by requiring the temporal formula to be satisfied. The choice of linear time temporal logic is quite natural since our user query solutions are defined as sequences of worlds. The reason for disallowing a direct use of the operator X (by removing it from the syntax) is twofold. Firstly, we still aim at not distinguishing sequences which differ only in the ordering of independent service types. Secondly, if the user wants to introduce the order on two consequtive service types he can use formulas involving level constraints. On the other hand our language and the temporal planning method can be easily extended with the operator X.
We start with defining the set of propositional variables, the level constraints, and then the syntax and the semantics of LT Lk X . 4.1
Let o 2 O be an object, a 2 attr(o). The set of propositional variables P V = {pEx(o), pSet(o.a), pNull(o.a) | o 2 O, a 2 attr(o)}. Intuitively, pEx(o) holds in each world, where the object o exists, pSet(o.a) holds in each world, where the object o exists and the attribute a is set, and pNull(o.a) holds in each world, where the object o exists and the attribute a is null.
In addition to P V we use also the set of level constraints LC over the stamps ST, defined by the following grammar:
lc ::= lexp ⇠ lexp lexp ::= c | s.level | lexp lexp (1) where s 2 ST, c 2 Z, 2 {+, , ·, /, %}, ⇠ 2 { , <, =, >, }, and /, % stand for integer division and modulus, respectively.
Intuitively, s.level < c holds in each world, where the stamp s exists and the value of its level is smaller than c. 4.2
The LT Lk X formulae are defined by the following grammar:
' ::= p | ¬p | lc | ¬lc | ' ^ ' | ' _ ' | ' U<k' | ' R<k' . where p 2 P V , lc 2 LC, and k 2 N.
Observe that we assume that the LT Lk X formulae are given in the negation normal form (NNF), in which the negation can be only applied to the propositional variables and the level constraints. The temporal modalities U<k and R<k are named as usual k-restricted until and release, respectively. Intuitively, ' U<k means that eventually, but in less than k steps, holds and always earlier ' holds. The formula ' R<k expresses that either for the next k 1 states holds or in less than k steps, ' holds and always earlier holds. The derived basic temporal modalities are defined as follows: F<k' d=ef trueU<k' and G<k' d=ef f alseR<k' .
Definition 9. A model is a pair M = (⇢, V ⇢ ), where ⇢ = (w0, w1, . . . , wn) is a world solution with wi = (Oi, vi) for 0 i n, and V⇢ : Sin=0{wi} ⇥ ST ! N [ {1} is the function over the worlds of ⇢ valuating the expressions of the form stamp.level, defined as follows: – V⇢ (wi, s.level) = 1 if s 62 Oi, – V⇢ (wi, s.level) = 0 if s 2 O0, – V⇢ (wi, s.level) = j if s 2 Oj and s 62 Oj 1, for some 1 j i. The intuition behind the definition of V⇢ is as follows. If a stamp s is not an element of a world w, then the value of s.level in w does not exist, and this is denoted by 1 . If a stamp s is an element of the world w0, then the value of s.level is 0 in all the worlds. If wj is the world, where s appears for the first time, then the value of s.level is equal to j in wj as well as in all further worlds.
Before defining the semantics of LT Lk X we extend the stamp.level valuation function V⇢ from ST to the level expressions as follows: – V⇢ (wi, c) = c, – V⇢ (wi, lexp
V⇢ (wi, lexp0), – V⇢ (wi, lexp lexp0) = V⇢ (wi, lexp)
V⇢ (wi, lexp0) if V⇢ (wi, lexp) 6= 1 6 = lexp0) = 1 if V⇢ (wi, lexp) = 1 or V⇢ (wi, lexp0) = 1 , We say that an LT Lk X formula ' is true in M = (⇢, V ⇢ ) (in symbols M |= ' ) iff w0 |= ' , where for m n we have: – wm |= pEx(o) iff o 2 Om. The semantics of the propositions follows their definitions, for the level constraints the semantics is based on the valuation function V⇢ , whereas for the temporal operators the semantics is quite standard. Note that we interpret our language over finite sequences as the solutions we are dealing with are finite.
Now, by a temporal query we mean a query (as defined in the former section) extended with an LT Lk X formula ' . The temporal solutions are these solutions for which the world sequences satisfy ' . A temporal plan is an equivalence class of the temporal solutions, defined over the same multiset of services. 5
This section contains an example showing how the abstract temporal planning can be used in practice for a given ontology and user (temporal) queries.
Consider the ontology depicted in Fig. 2. In the Artif act branch one can see several types of objects, like, e.g., Arbour (the main point of interest of this example), which is a subclass of W are, P aintableArtif act, and Construction. At the left hand side the Service branch and its subclasses are located. The service Select (St) is able to search any W are, Selling (Sg) allows to purchase it, while T ransport (T ) can be used to change its location. The P ainting (P ) service is able to change colour of any P aintableArtif act, but it needs to use some P aint. The Building (B) service can be used to obtain some Construction, but it needs BuildingM aterials. Finally, two subclasses of Building are specialized in production of wooden constructions using the supplied boards and nails. The services W oodBuilding (W b) and W oodBuildingLux (W bx) are similar, but the latter also paints the product to the chosen colour using their own paint, however for a higher price.
Assume the user wants to get a wooden arbour painted in blue. He formulates the query as follows: in = inout = ; , pre = true, out = {Arbour a}, post = (a.colour = blue ^ a.owner = M e ^ a.location = M yAddress). The post formula is automatically translated to its abstract form, that is (isSet(a.colour) ^ isSet(a.owner) ^ isSet(a.location)). The shortest plans are [St + Sg] and [St + Sg + T ]. The former satisfies the user query only if the Selling service is located in a close proximity of the user’s address.
Assume that during the next planning steps (i.e., the offer collecting and the concrete planning) those plans turn out to have no realization acceptable by the user. Perhaps, there are no blue arbours in nearby shops or they are too expensive. Then, the alternative plan is to buy and transport an arbour in any colour, as well as some blue paint, and then use the P ainting service: [2St + 2Sg + 2T + P ], where one triple of services (St, Sg, T ) provides the arbour, and the other a blue paint.
However, it could be the case that, e.g., the transport price of such a big object like an arbour exceeds the budget. If so, the possible solution is to buy boards, nails, and paint, transport them to the destination address, then to assembly the components with an appropriate building service, and paint, finally. This scenario is covered, for example, by the following plan: [3St + 3Sg + 3T + W b + P ], where the triples of services (St, Sg, T ) provide and transport boards, nails, and the paint.
Although, there are over eight hundred abstract plans of length from 2 to 11 satisfying the above user query, including these with multiple transportations of the arbour, or painting it several times. In order to restrict the plans to more specific ones, the user can refine the query demanding of specific types of services to be present in the plan using stamps. Thus, for example, by adding the following set of stamps to out: {Stamp t1, Stamp t2, Stamp t3} and extending post by: Vi=1..3(ti.serviceClass instanceOf T ransport), the number of possible abstract plans (of length from 2 to 11) can be reduced below two hundred. Then, if instead of buying a final product the user wants to buy and transport the components, in order to build and paint the arbour, he can add two more stamps and conditions to the query. That is, by adding to out the set {Stamp b, Stamp p}, and by extending post by the expression (^ b.serviceClass instanceOf Building ^ t3.serviceClass instanceOf P ainting), one can reduce the number of resulting plans to 2 only: [3St + 3Sg + 3T + W b + P ] and [3St + 3Sg + 3T + W bx + P ].
However, even 2 abstract plans only can be realized in a number of different ways, due to possible many transformation contexts, and the number of different partial orders represented by a single abstract plan. If the user wants to further reduce the number of possible plan realizations by interfering with an order of services, he should specify some temporal restrictions. For example, if the user wants to ensure that all the transports are executed before the building starts, he can express it as a formula:
' 1 = F (b.level > t1.level) ^ (b.level > t2.level) ^ (b.level > t3.level)) Moreover, if the intention of the user is to proceed with some service directly after another one, for example, to start building just after the third transport, one can express such a constraint as:
' 2 = F(b.level = t3.level + 1)
Moreover, using a temporal query the user can prevent some services from occurring in the plan. For example, using the following formula: ' 3 = ¬pEx(a) U pNull(a.colour), which means that just after the arbour has been produced, its colour is not set, the user excludes the W oodBuildingLux service (which builds and paints the arbour).
The other possibility of extending the user query by a temporal component includes using the k-restricted versions of modal operators. For example, consider the following formula:
' 4 = F<10(pEx(t1) ^ pEx(t2) ^ pEx(t3)), which states that three transportations should be executed in the first nine steps of the plan. 6
In this section we sketch the implementation of the propositions and the level constraints, and then we evaluate the efficiency of our tool using several scalable benchmarks. 6.1
The implementation of the propositions and the level constraints exploits our symbolic representation of world sequences. The objects and the worlds are represented by sets of variables, which are first allocated in the memory of an SMT-solver, and then used to build formulas mentioned in Section 4. The representation of an object is called a symbolic object. It consists of an integer variable representing the type of an object, called a type variable, and a number of Boolean variables to represent the object attributes, called the attribute variables. In order to represent all types and identifiers as numbers, we introduce a function num : A [ P [ S [ O 7 ! N, which with every attribute, object type, service type, and object assigns a natural number.
A symbolic world consists of a number of symbolic objects. Each symbolic world is indexed by a natural number from 0 to n. Formally, the i-th symbolic object from the j-th symbolic world is a tuple: oi,j = (ti,j , ai,0,j , ..., ai,maxat 1,j ), where ti,j is the type variable, ai,x,j is the attribute variable for 0 x < maxat, where maxat is the maximal number of the attribute variables needed to represent the object.
Note that actually a symbolic world represents a set of worlds, and only a valuation of its variables makes it a single world. The j-th symbolic world is denoted by wj , while the number of the symbolic objects in wj - by |wj |. Note that the set of the initial worlds of the query q (Wiqnit) is represented by a symbolic world w0. Fig. 3 shows subsequent symbolic worlds of a transformation sequence.
One of the important features of our encoding is that for a given index of a symbolic object i we are able to determine the step of a solution, in which the object was produced. This is done by the function levq : N 7! N, such that for a levq(i) = (0 for i < |w0| b (mi|axwo0u|t) c + 1 for i |w0| (2) where maxout is the maximal number of the objects produced by a single service.
Another important feature of our encoding is that the objects of outq need to be identified among the objects of the symbolic world wn (of indices greater than |w0|). To this aim, we allocate a new symbolic world we (with e = n + 1), containing all the objects from outq. Note that the world we is not a part of a Final wn o0,n1 o1,n1 o2,n o3,n m0,e o4,n m1,e m2,e o5,n o6,n ox,n
Expected
we
o0,e
o1,e
o2,e
outq
world solution, but it provides a set of additional, helper variables. Finally, we
need a mapping between the objects from a final world wn produced during the
subsequent transformations and the objects from we. To this aim we allocate p
additional mapping variables in the symbolic world we, where p = |outq|. These
variables, denoted by m0,e, . . . , mp 1,e, are intended to store the indices of the
objects from a final world, which are compatible with the objects encoded over
we. Thus, we encode the state of the expected worlds of the query q (Weqxp),
imposed by postq, using two sets of symbolic objects. The objects of inq [ inoutq
are encoded directly over the (final) symbolic world wn. The state of the
objects from outq are encoded over we, and since their indices are not known, all
possible mappings between objects from we and wn are considered, by encoding
a disjunction of equalities between objects from we and wn. See [
The translation of the propositions defined over the objects and their attributes of a user query q in a symbolic world wm (0 m n) is as follows: 8> true, for o 2 inq [ inoutq, [pEx(o)]m = < f alse, for o 2 outq, m = 0,
>: levq(mnum(o),e) m, for o 2 outq, m > 0.
That is, the objects from the initial world exist in all the subsequent worlds, the objects from the out set do not exist in the world w0, and they appear in some subsequent world. Then, since the index of the object o is stored as the value of corresponding mapping variable mnum(o),e, we can determine if it exists in the world wm using the levq function.
The proposition pSet(o.a) is encoded over the symbolic world wm as: [pSet(o.a)]m = [pEx(o)]m ^ (aj,x,m, for o 2 inq [ outq,
W|iw=m|w|0|1(mj,e = i ^ ai,x,m), for o 2 outq where j = num(o) and x = num(a).
It follows from our symbolic representation that the indices of objects from an initial world are known, and we can get the value of the appropriate attribute variable directly. However, in the case of objects from outq we have to consider all possible mappings between objects from we and wm. Note that the encoding of the proposition pNull(o.a) over the symbolic world wm (i.e., [pNull(o.a)]m) is very similar. The only change is the negation of ai,x,m in the above formula.
In order to encode the level constraints, we introduce a set of the special level variables. That is, for every stamp s used in some level constraint we introduce to the world we an additional integer variable li,e, where i = num(s), intended to store the level value of the stamp s. The level value is assigned to li,e using the following formula [bind(i)] := (li,e = levq(mi,e)) for i = num(s), where q is a user query. Then, for every stamp s used in a level constraint we add the corresponding [bind(num(s))] formula as an SMT assertion. Thus, the encoding of the level constraints is as follows: (3) (4) 8> c for lexp = c < [lexp] = li,e, for lexp = s.level, i = num(s) >: [lexp0] [lexp00] for lexp = lexp0 lexp00 (5)
The encoding of arithmetic operators is straightforward, since they are supported by theories built in SMT-solvers, like, e.g., Linear Integer Arithmetic or Bitvector theory. In what follows, [' ]nm denotes the translation of the formula ' at the state wm of the world sequence of length n + 1.
LT Lk X formula, (w0, . . . , wn) be a sequence of symbolic worlds, and 0 m n. •• [[p¬]pnm]nm:=:=[p¬]m[p,] mfo,r fpor2pP2VP, V , • [lexp0 ⇠ lexp00]nm := [lexp0] ⇠ [lexp00] Vs2 st(lexp0)[pEx(s)]m
Vs2 st(lexp00)[pEx(s)]m, • [¬lc]nm := ¬[lc]nm, for lmc 2 LC, • [' ^ ]nm := [' ]nm ^ [ ]n , • [' _ ]nm := [' ]nm _ [ ]nm, • [' U<k ]nm := Wim=imn(m+k,n)([ ]in ^ Vij=1m[' ]jn), • [' R<k ]nm := Vim=imn(m+k,n)[ ]in _ Wim=imn(m+k,n)([' ]in ^ Vij=m[ ]jn), where st(lexp) returns the set of the stamps over which the expression lexp is built.
Theorem 1. The encoding of the temporal query is correct.
Proof. This can be shown by induction on the length of a formula. Omitted here because of lack of space3. 6.2
In order to evaluate the efficiency of our approach we performed several
experiments using standard PC with 2GHz CPU and 8GB RAM, and Z3 [
First, we ran our planner for each ontology and each query instance without a temporal query (column 1), in order to collect statistics concerning the time needed to find the first plan (P1), all 10 plans (P10), as well as the total time (column T) and the memory consumed (M) by the SMT-solver in order to find all the plans and checking that no more plans of length k exist. We imposed the time limit of 1000 seconds for the SMT-solver. Each time-out is reported in the table by T O. It is easy to observe that during these experiments as many as 9 instances ran out of time. The next experiments involve temporal queries using level constraints. To this aim we extended the out set of the generated queries by the appropriate stamp set. Moreover, the post formulas of the queries have been also extended k with the expression: Vib=21c(si.serviceClass instanceOf Ci), where si 2 ST, while Ci 2 S are service types occurring in the solutions generated by OG.
Our second group of experiments involved the temporal formula 2: k b 2 c 1 2 = F( ^ si.level < si+1.level),
i=1 which expresses that about a half of the stamps being effects of the solution execution, should be produced in the given order. We do not present detailed results, because they are in general comparable with the performance in the former experiments. Similarly, there are 9 time-outs, but the time and the memory consumption varies a bit - for some cases the results are slightly better, while for others are a little worse.
In the third group of the experiments we imposed stronger restrictions on the possible service orders of the solutions using the following formula: This formula still leaves a certain degree of freedom in a service ordering, however its encoding as an SMT-instance is more compact, since the constant values are introduced in place of some level variables. Thus, probably, it is also easier to solve. The results are summarized in the column 3 in Table 1. It is easy to observe that the time and the memory consumption is significantly lower. Moreover, the number of time-outs dropped to 6. Thus, this is an example showing an improvement in the planning efficiency using a temporal query.
Our next experiment involves the formula 4 specifying the strict ordering of several services in the solution using stamp-based level constraints: The analysis of the results (given in the column 4 of Table 1) indicates a dramatic improvement of our planner efficiency, in terms of time and memory consumption by the SMT-solver. Moreover, in this experiments group the planner has been able to terminate its computations in the given time limit for all but one instances.
Finally, we want to confront the planner behaviour with other kind of temporal formulae. Using the Until modality, we demand that one of the objects from outq has to be produced no later than in the middle of the plan. Moreover, knowing the structure of the generated queries, we impose that after the object appears one of its attributes should already be set. This is expressed by the following formula:
5 = ¬pEx(o) U<d k2 e pSet(o.a) where o 2 outq, a 2 attr(o), and the expression isSet(o.a) is not contradictory with postq. The results has been summarised in column 5 of Table 1. It is easy to observe that also this time the plans have been found faster and using less memory than in the case when no temporal formula is involved. 7
In this paper we have applied the logic LT Lk X to specifying temporal queries for temporal planning within our tool Planics. This is a quite natural extension of our web service composition system, in which the user gets an opportunity to specify more requirements on plans. These requirements are not only declarative any more. The overall conclusion is that the more restrictive temporal query, the more efficient planning, given the same ontology. Assuming that the more restrictive temporal queries, the longer formulas expressing them, the above conclusion shows a difference with model checking, where the complexity depends exponentially on the length of an LT Lk X formula.
Our temporal planner is the first step towards giving the user even more freedom by defining a so-called parametric approach. We aim at having a planner which in addition to the current capabilities, could also suggest what extensions to the ontology or services should be made in order to get better or unrealizable plans so far. This is going to be a subject of our next paper.