Towards Automatic Composition of Web Services: A SAT-Based Phase ? Wojciech Penczek1,2 , Agata Półrola3 , and Andrzej Zbrzezny4 1 Polish Academy of Sciences, ICS, Ordona 21, 01-237 Warsaw, Poland 2 University of Podlasie, ICS, Sienkiewicza 51, 08-110 Siedlce, Poland penczek@ipipan.waw.pl 3 University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland polrola@wmi.uni.lodz.pl 4 Jan Długosz University, IMCS, Armii Krajowej 13/15, 42-200 Czȩstochowa, Poland a.zbrzezny@ajd.czest.pl Abstract. Automating the composition of web services is an object of a growing interest nowadays. In our former paper [3] we proposed a method for converting the problem of the composition to the problem of building a graph of worlds consisting of formally defined objects, and presented the first phase of this com- position resulting in building a graph of types of services (an abstract graph). In this work we propose a method of replacing abstract flows of this graph by sequences of concrete services able to satisfy the user’s request. The method is based on SAT-based reachability checking for (timed) automata with discrete data and parametric assignments. 1 Introduction In recent years there has been a growing interest in automating the composition of web services. The number of more and more complex Internet services is still growing nowa- days; several standards describe how services can be invoked (WSDL [17]), how they exchange information (SOAP [13]), how they synchronise the executions in complex flows (BPEL [16]), and finally how they can be discovered (UDDI [15]). However, still there is a lack of automatic methods for arranging and executing their flows. One of the problems to deal with is the size of the environment - most existing composition methods work with concrete instances of web services, so even a simple query requires taking all the instances of all the types of services into account. Another problem fol- lows from incompatibilities in inputs/outputs of services, and difficulties in comparing their capabilities and qualities - two services can offer the same functionality, but this fact cannot be detected automatically without unification of their interfaces made by the providers. In our work [3] we proposed an approach to automatic composition of services which can potentially solve the above problems. The problem of automatic composition of web services is converted to the problem of building a graph of worlds consisting of ? Supported by the Polish National Science Center under the decision DEC- 2011/01/B/ST6/01477 Recent Advances in Petri Nets and Concurrency, S. Donatelli, J. Kleijn, R.J. Machado, J.M. Fernandes (eds.), CEUR Workshop Proceedings, ISSN 1613-0073, Jan/2012, pp. 453–473. 454 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny formally defined objects, which are transformed by services. We introduce a uniform semantic description of service types. In order to adapt a possibly wide class of existing services, specific interfaces of concrete services are to be translated to the common one by adapters (called proxies), built in the process of service registration. The process is to be based on descriptions of interfaces of services, specified both in WSDL and in the languages containing a semantic information (like OWL-S or Entish [1]). The client’s goal is expressed in a fully declarative intention language. The user describes two worlds: the initial and the final one, using the notions coming from an ontology, and not knowing any relations between them or between the services. The task of the composition system consists in finding a way of transforming the initial world into the final one. The composition is three-phase. In the first phase, called abstract planning or planning in types, we create an abstract plan, which shows sequences of service types whose executions possibly allow to accomplish the goal. The second phase makes these scenarios “concrete”, which means replacing the types of services by their concrete instances. This can also involve choosing a plan which is optimal from the user’s point of view. Finally, the last phase consists in supervising the execution of the optimal run, with a possibility of correcting it in the case of a service failure. Our previous paper [3] described a method of generating an abstract graph of ser- vices. In the current work we deal with the second phase of composition: concretising abstract flows, i.e., with searching for sequences of concrete services which can lead to satisfying user’s request. We apply model checking techniques to this aim. The sub- stage aimed at choosing an optimal scenario is not considered in this version of the approach. The rest of the paper is organised as follows. In Sec. 2 we present the related work. Sec. 3 introduces worlds and services transforming them. Sec. 4 describes briefly the abstract planning phase and its result. Next, in Sec. 5 we present our approach to SAT- based concretising abstract scenarios. Sec. 6 show experimental results and concluding remarks. 2 Related Work There are many papers dealing with the topic of web services composition [4, 7–10, 14]. Some of these works consider static approaches, where flows are given as a part of the input, while the others deal with dynamically created flows. One of the most active research areas is a group of methods referred to as AI Planning [4]. Several approaches use Planning Domain Definition Language (PDDL [5]). Another group of methods is built around the so-called rule-based planning, where composite services are generated from high-level declarative descriptions, and compositionality rules describe the conditions under which two services are composable. The information obtained is then processed by some designated tools. The project SWORD [6] uses an entity- relation formalism to specify web services. The services are specified using pre- and postconditions; a service is represented as a Horn rule denoting that the postcondition is achieved when the preconditions are true. A rule-based expert system generates a plan. Another methodology is the logic-based program synthesis [8]. Definitions of web services and user requirements, specified in DAML-S [2], are translated to formulas of Automatic composition of web services Petri Nets & Concurrency – 455 Linear Logic (LL): the descriptions of web services are encoded as LL axioms, while a requirement is specified as a sequent to be proven by the axioms. Then, a theorem prover determines if such a proof exists. Besides the automatic approaches mentioned above, there exist also half-automatic methods assuming human assistance at certain stages [12]. Some approaches are based on specifying a general plan of composition manually; the plan is then refined and updated in an automatic way. Inspired by the Entish project [1], our approach enables to model automated com- position based on matching input and output types of services. We adapt also the idea of three-phase composition, but introduce original definitions of services and composition techniques. 3 Worlds and Services In our approach we introduce a unified semantics for functionalities offered by services, which is done by defining a dictionary of notions/types describing their inputs and out- puts. A service is then understood as a function which transforms a set of data into another set of data (or as a transition between them). The sets of data are called worlds. The worlds can be described by the use of an ontology, i.e., a formal representation of a knowledge about them. Definition 1 (World and objects). The universum is the set of all the objects. The objects have the following features: – each object is either a concrete object or an abstract object, – each object contains named attributes whose values are either other objects or: • values of simple types (numbers, strings, boolean values; called simple at- tributes) or NULL (empty value) for concrete objects, • values from the set {NULL, SET, ANY} for abstract objects. If an attribute A of the object O is an object itself, then O is extended by all the attributes of A (of the names obtained by adding A’s name as a prefix). Moreover, when an object having an object attribute is created, its subobject is created as well, with all the attributes set to NULL. – each simple attribute has a boolean-valued flag const. A world is a set of objects chosen from the universum. Each object in a world is identi- fied by a unique name. By default each const flag is set to false. If the flag of an attribute is true, then performing on the object any operation (service) which sets this attribute (including services initialising it) is not allowed (the value of the attribute is considered to be final). The attributes are referred to by ObjectName.AttributeName. Definition 2 (Object state, world state). A state of an object O is a function Vo as- signing values to all the attributes of O (i.e., is the set of pairs (AttributeName, AttributeValue), where AttributeName ranges over all the attributes of O). A state of a world is defined as the state of all the objects of this world. 456 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny In order to reason about worlds and their states we define the following two-argument functions (the second default argument of these functions is the world we are reasoning about): – Exists - a function whose first argument is an object, and which says whether the object exists in the world, – isSet - a function whose first argument is an attribute of an object, and which says whether the attribute is set (has a nonempty value), – isConst - a function whose first argument can be either an attribute or an object. When called for an attribute, the function returns the value of its const flag; when called for an object it returns the conjunction of the const flags of all the attributes of this object. The ontologies collect the knowledge not only about the structure of worlds, but also about the ways they can be transformed, i.e., about services. The services are organised in a hierarchy of classes, and described both on the level of classes (by specifying what all the services of a given class do - such a pattern of behaviour is referred to as an abstract service or a metaservice), and on the level of objects (concrete services). The description of a service includes, besides specifying input and output data types, also declaration of introducing certain changes to a world, i.e., of creating, removing and modifying objects. The definition of a service is as follows: Definition 3 (Service). A service is an object of a non-abstract subclass1 of the ab- stract class Service. A service contains (initialised) attributes, inherited from the base class Service. The attributes can be grouped into – processing lists (the attributes produces, consumes, requires), – modification lists (the attributes mustSet, maySet, mustSetConst, maySetConst), and – validation formulas (the attributes preCondition and postCondition). Moreover, a service can contain a set of quality attributes. A service modifies (transforms) a world, as well as the world’s state. The world to be transformed by a service is called its pre-world (input world), while the result of the execution is called a post-world (output world). Modifying a world consists in modifying a subset of its objects. The objects being transformed by one service cannot be modified by another one at the same time (i.e., transforming objects is an atomic activity). A world consisting of a number of objects can be transformed into a new state in two ways2 : by a service which operates on a subset of its elements, or by many services which operate concurrently on disjoint subsets of its elements. The groups of attributes are presented in the definitions below. 1 We use the standard terminology of object-oriented programming. The term “subclass” is re- lated to inheritance. A class is called abstract if instantiating it (i.e., creating objects following the class definition) is useless, in the sense that the objects obtained this way do not correspond to any real-world entity. 2 Services which create new objects are not taken into account. Automatic composition of web services Petri Nets & Concurrency – 457 Definition 4 (Processing lists). The processing lists are as follows: – produces - a list of named objects of classes whose instances are created by the service in the post-world, – consumes - a list of named objects of classes whose objects are taken from the input world, and do not exist in the world resulting from the service execution (the service removes them from the world), – requires - a list of named objects of classes whose instances are required to exist in the current world to invoke the service and are still present in the output world. The formal parameters from the above lists define an alphabet for modification lists and validation formulas. Definition 5 (Modification lists). The modification lists are as follows: – mustSet - a list of attributes of objects occurring in the lists produces and re- quires of a service, which are obligatorily set (assigned a nonempty value) by this service, – maySet - a list of attributes of objects occurring in the lists produces and requires of a service, which may (but not must) be set by this service, – mustSetConst - a list of attributes of the objects which occur in the lists produces and requires of a service, which are obligatorily set as being constant in the worlds after executing this service, – maySetConst - a list as above, but of the attributes which may be set as constant. A grammar for the above lists can be found in [3]. The attributes of the objects appearing in processing lists which do not belong to the union of lists mustSet and maySet are not changed when the service is called. Definition 6 (Validation formulas). The validation formulas are as follows: – preCondition - a formula which describes the condition under which the ser- vice can be invoked. It consists of atomic predicates over the names of objects from the lists consumes and requires of the service and over their attributes, and is written in the language of the first order calculus without quantification (atomic predicates with conjunction, disjunction and negation connectives). The language of atomic predicates contains comparisons of expressions over attributes with con- stants, and functions calls with object names and attributes as arguments. In par- ticular, it contains calls of the functions isSet, isConst and Exists3 . – postCondition - a formula which specifies conditions satisfied by the world re- sulting from invoking the service. The formula consists of atomic predicates over the names of objects from the lists consumes, produces and requires of the service and over their attributes. To the objects and attributes one can apply pseud- ofunctions pre and post which refer to the state of an object or an attribute in the 3 Using Exists in preCondition is redundant w.r.t. using an appropriate object in the list consumes or requires. However, the future directions of developing the service descrip- tion language mentioned in the final part of the paper, include moving modification lists to validation formulas. 458 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny input and the output world of this service, respectively. By default, the attributes of objects listed in consumes refer to the state of the pre-world, whereas these in produces and requires - to the state of the post-world. Definition 7. A service U is enabled (executable) in the current state of a world S if: – each object O from the lists consumes and requires of U can be mapped onto an object in S, of the class of O or of its subclass; the mapping is such that each object in S corresponds to at most one object from the above lists; – for the objects in S which, according to the above mapping, are actual values of the parameters in consumes and requires the formula preCondition of U holds, – the list mustSet of U contains no attributes for which, in objects which are actual values of the parameters, the flag const is set. Definition 8. A service U executable at the current world S produces a new world S ’ in which: – there are all the objects from S, besides these which in the mapping done for exe- cuting U were actual values for the parameters in consumes, – there is a one-to-one mapping between all the other objects in S ’ and the objects in the list produces of U, such that each object O from the list produces corresponds to an object in S ’ which is of a (sub)class of O; – for the objects which, according to the above mappings, are actual values of the parameters in the processing lists the formula postCondition holds, – in the objects which are actual values of the appropriate parameters the flags const of the attributes listed in mustSetConst of U are set, and the attributes listed in mustSet of U have nonempty values, – assuming the actual values of the parameters as above, all the attributes of all the objects existing both in S and in S ’ which do not occur neither in mustSet nor in maySet have the same values as in the world S; the same holds for the flags const of the attributes which do not occur neither in mustsetConst nor in maySetConst. Moreover, all the attributes listed in mustSet or maySet which are of nonempty values in S, in S ’ are of nonempty values as well. 3.1 Concrete Services We assume here that concrete services present their offers in their pre- and postcondi- tions. and that their maySetConst and maySet lists are empty (i.e., setting an attribute or the Const flag optionally is not allowed in this case). A grammar for validation formulas is as follows: ::= | pre() | post(objectName from requires>) | ::= . | . ::= "integer value" | "real value" | Automatic composition of web services Petri Nets & Concurrency – 459 "of a numeric type" ::= + | - | * | / ::= | ::= = | < | <= | > | >= ::= Exists() | isSet() | isConst() | not | | "value" ::= | and ::= | or It should be noticed that pre() and post() are allowed in postCondition only. Moreover, in this paper we assume that the expressions involve only attributes which refer either to names of objects from consumes, or to the names of objects which are of the form pre(objectName from requires) (i.e., that the expressions involve only values of attributes in the input world of a service). We assume also that all the elements of an expression are of the same type, the result is of this type as well, and so is the attribute this result is compared with. The expressions involve attributes of numeric types only, while the atomic predicates allow comparing an attribute of an arbitrary type with a value of the same type4 . The values of the attributes and the values occurring in comparisons in the atomic predicates above are as follows: – boolean values, – integer values of a certain range5 , – characters, – real values of a certain range, with the precision limited to a number of decimal places (usually two), – values of certain enumeration types. Enumeration types are used instead of strings. In fact, such an approach seems sufficient to represent the values necessary: in most cases the names of items offered or processed by services come from a certain set of known names (e.g. names of countries, cities, names of washing machines types etc), or can be derived from the repository (e.g. names of shops which registered their offers). Similarly, restricting the precision of real values seems reasonable (usually two decimal places are sufficient to express the amount of a ware we buy, a price, a capacity etc). Consequently, all the values considered can be treated as discrete. It should be noticed also that we assume an ordering on the elements of enumeration types and the boolean values6 . 4 The grammar for validation formulas is given in a semi-formal way. The “quoted” items should be understood as notions from the natural language. By "value" we mean a value of an arbitrary (also non-numeric) type. 5 A natural restriction when using programming languages. 6 Similarly as in the Ada programming language. 460 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny 4 Abstract Planning The aim of the composition process is to find a sequence of services whose execution can satisfy a user’s goal. The user describes its goal in a declarative language defined by the ontology. He specifies (possibly partially) an initial and a final (desired) world, possibly giving also some evaluation criteria. The query is defined in the following way: Definition 9 (Query). A query consists of the following elements: – an initial domain - a list of named objects which are elements of the initial world. The form of the list is analogous to the form of the list produces in the description of a service; – an initial clause specifying a condition which is to be satisfied by the initial world. The clause is a formula over the names of objects and their attributes, taken from the initial domain. The grammar of the clause is analogous to the grammar of the preCondition; – an effect domain - a list of named objects which have to be present in a final world (i.e., a subset the final world must contain); – an effect clause specifying a condition which is to be satisfied by the final world. The clause is a formula over the names of objects and their attributes from both the domains defined above; references to the initial state of an object, if ambiguous, are specified using the notations pre(objectName) and post(objectName), anal- ogously as in the language used in the formulas postCondition of services. The grammar of the effect clause is analogous to the grammar of the postCondition; – an execution condition - a formula built over services (unknown to the user when specifying the query) from a potential run performing the required transformation of the initial world into a target world. While construction of this formula simple methods of quantification and aggregation are used; – a quality function - a real-valued function over the initial world, the final world and services in a run, which specifies a user’s criterion of valuating the quality of runs. The run of the smallest value of this function is considered to be the best one. The last two parts of a query are used after finishing both the abstract planning phase and the first part of concrete planning, which adjusts types and analyses pre- and post- conditions of concrete services. The aim of a composition process is to find a path in the graph of all the possible transitions between worlds which leads from a given initial world to a given final world, specified (possibly partially) in a user’s query, using no other knowledge than that con- tained in the ontology. The composition is three-phase; the first phase (described in [3]) consists in finding all the sequences of service types (abstract services) which can po- tentially lead to satisfying the user’s goal. The result of the abstract planning phase is an abstract graph. The abstract graph is a directed multigraph. The nodes of the graph are worlds in certain states, while its edges are labelled by services. Notice that such a labelling carries an information which part of a input world (node) is transformed by a given service (that is specified by actual values of the parameters in consumes and requires of the service), and which part of the output world (node) it affects (the lists produces Automatic composition of web services Petri Nets & Concurrency – 461 and requires of this service). We distinguish some nodes of the graph - these which have no input edges represent alternative initial worlds, while these with no output edges are alternative final worlds. A formal definition of the abstract graph is as follows: Definition 10. An abstract graph is a tuple GA = (V, Vp , Vk , E, L), where V is a subset of the set S of all the worlds, Vp ⊆ V is a set of initial nodes, Vk ⊆ V is a set of final nodes, and E ⊆ V × V is a transition relation s.t. e = (v, v 0 ) ∈ E iff L(e) transforms the world v into v 0 , where L : E −→ U is a function labelling the edges with services. 5 Main Idea From the phase of abstract composition [3] we get a graph showing the sequences of ser- vice types which can potentially lead to satisfying user’s request. The next step towards obtaining a flow to be run is to find concrete services of the appropriate types whose offers enable satisfying the query. We use SAT-based bounded model checking to this aim. In the paper [19] we have shown how to test reachability for timed automata with discrete data using BMC and the model checker VerICS. We adapt the above approach. The main idea of our solution consists in translating each path of the abstract graph to a timed automaton with discrete data and parametric assignments (TADDPA). The automaton represents concrete services of appropriate types (corresponding to the types of services in the scenario we are working on) which can potentially be executed to reach the goal. The variables of the automaton store the values of the attributes of the objects occurring along the path, while the parameters are assigned to variables when the exact value assigned by a service is unknown. Next, we test reachability of a state satisfying the user’s query. If such a state is reachable, we get a reachability witness, containing both an information about a sequence of concrete services to be executed to reach the goal and the values of parameters for which this sequence is executable. In spite of using timed automata we currently do not make use of the timing part of this formalism, but the reason for using them is twofold. Firstly, doing this allowed us to adapt the existing implementation for timed automata with discrete data (modified to handle their extension - TADDPA). Secondly, in the future we are going to use the clocks to represent the declared times of services executions, which should enable us searching for scenarios of an appropriate timed length. Below, we introduce all the elements of our approach. 5.1 Timed Automata with Discrete Data and Parametric Assignments S Given a set of discrete types T = i=1,...,n Ti (n ∈ IN), including an integer type, a character type, user-defined enumeration types, a real type of a precision given etc., such that for any Ti ∈ T there is an ordering7 on the values of Ti . By TN ⊂ T we denote the subset of T containing all the numeric types T ∈ T . Let DV be a finite set of variables whose types belong to T , and let DP be a finite set of parameters whose 7 Similarly as in some programming languages, e.g. the Ada language. 462 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny types belong to T . Let type(a), for a ∈ DV ∪ DP , denote the type of a. The sets of arithmetic expressions over T for T ∈ TN , denoted Expr(T ), are defined by expr ::= c | v | expr ⊗ expr, where c ∈ T , v ∈ DV with type(v) = T , and ⊗ ∈ {+, −, ∗, /}. By type(expr) we denote the type of all the components of S the expression and therefore the type of the result8 . Moreover, we define Expr(T ) = T ∈TN Expr(T ). The set of boolean expressions over DV , denoted BoE(DV ), is defined by β ::= true | v ∼ c | v ∼ v 0 | expr ∼ expr0 | β ∧ β | β ∨ β | ¬β, where v , v 0 ∈ DV , c ∈ type(v), type(v 0 ) = type(v), expr, expr0 ∈ Expr(T ), type(expr) = type(expr0 ), and ∼∈ {=, 6=, <, ≤, ≥, >}. The set of instructions over DV and DP , denoted Ins(DV , DP ), is given by α ::=  | v := c | v := p | v := v 0 | v := expr | αα, where  denotes the empty sequence, v , v 0 ∈ DV , c ∈ type(v ), p ∈ DP and type(p) = type(v), type(v 0 ) = type(v), expr ∈ Expr(T ), and type(expr) = type(v)9 . Thus, an instruction over DV is either an atomic instruction over DV which can be either non-parametric (v := c, v := v 0 , v := expr) or parametric (v := p), or a (possibly empty) sequence of atomic instructions. Moreover, by Ins3 (DV , DP ) we denote the set consisting of all these α ∈ Ins(DV , DP ) in which any v ∈ DV appears on the left-hand side of “:=” (i.e. is assigned a new value, possibly taken from a parameter) at most once. By a variables valuation we mean a total mapping v : DV −→ T satisfying v(v ) ∈ type(v ) for each v ∈ DV . We extend this mapping to expressions of Expr(T ) in the usual way. Similarly, by a parameters valuation we mean a total mapping p : DP → T satisfying p(p) ∈ type(p) for each p ∈ DP . Moreover, we assume that the domain of values for each variable and each parameter is finite. The satisfaction relation (|=) for a boolean expression β ∈ BoE(DV ) and a valu- ation v is defined as: v |= true, v |= β1 ∧ β2 iff v |= β1 and v |= β2 , v |= β1 ∨ β2 iff v |= β1 or v |= β2 , v |= ¬β iff v 6|= β, v |= v ∼ c iff v(v ) ∼ c, v |= v ∼ v 0 iff v(v ) ∼ v(v 0 ), and v |= expr ∼ expr0 iff v(expr) ∼ v(expr0 ). Given a variables valuation v, a parameter valuation p and an instruction α ∈ Ins(DV , DP ), we denote by v(α, p) a valuation v0 such that – if α =  then v0 = v, – if α = (v := c) then for all v 0 ∈ DV it holds v0 (v 0 ) = c if v 0 = v , and v0 (v 0 ) = v(v 0 ) otherwise, – if α = (v := v1 ) then for all v 0 ∈ DV it holds v0 (v 0 ) = v1 if v 0 = v , and v0 (v 0 ) = v(v 0 ) otherwise, 8 Using different numeric types in the same expression is not allowed. The “/” operator denotes either the integer division or the “ordinary” division, depending on the context. 9 Distinguishing between assigning an arithmetic expression, and separately assigning a param- eter, a constant or a variable follows from the fact that arithmetic expressions are defined for numeric types only. The same applies to the definition of boolean expressions. Automatic composition of web services Petri Nets & Concurrency – 463 – if α = (v := expr) then for all v 0 ∈ DV it holds v0 (v 0 ) = expr if v 0 = v , and v0 (v 0 ) = v(v 0 ) otherwise, – if α = (v := p) then for all v 0 ∈ DV it holds v0 (v 0 ) = p(p), and v0 (v 0 ) = v(v 0 ) otherwise, – if α = α1 α2 then v0 = (v(α1 , p))(α2 , p). Let X = {x1 , . . . , xnX } be a finite set of real-valued variables, called clocks. The set of clock constraints over X , denoted CX (X ), is defined by the grammar: cc ::= true | xi ∼ c | xi − xj ∼ c | cc ∧ cc, where xi , xj ∈ X , c ∈ IN, and ∼ ∈ {≤, <, =, >, ≥}. Let X + denote the set X ∪ {x0 }, where x0 6∈ X is a fictitious clock representing the constant 0. An assignment over X is a function a : X −→ X + . Asg(X ) denotes the set of all the assignments over X . By a clock valuation we mean a total mapping c : X −→ IR+ . The satisfaction relation (|=) for a clock constraint cc ∈ CX (X ) and a clock valuation c is defined as c |= true, c |= (xi ∼ c) iff c(xi ) ∼ c, c |= (xi − xj ∼ c) iff c(xi ) − c(xj ) ∼ c, and c |= cc1 ∧ cc2 iff c |= cc1 and c |= cc2 . In what follows, the set of all the clock valuations satisfying a clock constraint cc is denoted by [[cc]]. Given a clock valuation c and δ ∈ IR+ , by c + δ we denote a clock valuation c0 such that c0 (x) = c(x) + δ for all x ∈ X . Moreover, for a clock valuation c and an assignment a ∈ Asg(X ), by c(a) we denote a clock valuation c0 such that for all x ∈ X it holds c0 (x) = c(a(x)) if a(x) ∈ X , and c0 (x) = 0 otherwise (i.e., if a(x) = x0 ). Finally, by c0 we denote the initial clock valuation, i.e., the valuation such that c0 (x) = 0 for all x ∈ X . Definition 11. A timed automaton with discrete data and parametric assignments (TAD- DPA) is a tuple A = (L, L, l0 , DV , DP , X , E, Ic , Iv , v0 ), where L is a finite set of la- bels (actions), L is a finite set of locations, l0 ∈ L is the initial location, DV is a finite set of variables (of the types in T ), DP is a finite set of parameters (of the types in T ), X is a finite set of clocks, E ⊆ L×L×BoE(DV )×CX (X )×Ins3 (DV , DP )×Asg(X )×L is a transition relation, Ic : L −→ CX (X ) and Iv : L −→ BoE(DV ) are, respectively a clocks’ and a variables’ invariant functions, and v0 : DV −→ T s.t. v0 |= Iv (l0 ) is an initial variables valuation. The invariant functions assign to each location a clock constraint and a boolean expression specifying the conditions under which A can stay in this location. Each element t = (l, l, β, cc, α, a, l0 ) ∈ E denotes a transition from the location l to the location l0 , where l is the label of the transition t, β and cc define the enabling conditions for t, α is the instruction to be performed, and a is the clock assignment. Moreover, for a transition t = (l, l, β, cc, α, a, l0 ) ∈ E we write source(t), label(t), vguard(t), cguard(t), instr(t), asgn(t) and target(t) for l, l, β, cc, α, a and l0 respectively. Semantics of the above automata is given as follows: Definition 12. Semantics of a TADDPA A = (L, L, l0 , DV , DP , X , E, Ic , Iv , v0 ) for a parameter valuation p : DP −→ T is a labelled transition system10 S(A, p) = (Q, q 0 , LS , →), where: 10 By a labelled transition system we mean a tuple S = (S, s0 , Λ, →), where S is a set of states, s0 ∈ S is the initial state, Λ is a set of labels, and →⊆ S × Λ × S is a (labelled) transition relation. 464 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny |X | – Q = {(l, v, c) | l ∈ L ∧ ∀v∈DV v(v) ∈ type(v) ∧ c ∈ IR+ ∧ c |= Ic (l) ∧ v |= Iv (l)} is the set of states, – q 0 = (l0 , v0 , c0 ) is the initial state, – LS = L ∪ IR+ is the set of labels, – → ⊆ Q × LS × Q is the smallest transition relation defined by the rules: l • for l ∈ L, (l, v, c)→(l0 , v0 , c0 ) iff there exists a transition t = (l, l, β, cc, α, a, l0 ) ∈ E such that v |= Iv (l), c |= Ic (l), v |= β, c |= cc, v0 = v(α, p) |= Iv (l0 ), and c0 = c(a) |= Ic (l0 ) (action transition), δ • for δ ∈ IR+ , (l, v, c)→(l, v, c + δ) iff c, c + δ |= Ic (l) (time transition). A transition t ∈ E is enabled at a state (l, v, c) for a given parameter valuation p if v |= vguard(t), c |= cguard(t), c(asgn(t)) |= Ic (target(t)), and v(instr(t), p) |= Iv (target(t)). Intuitively, in the initial state all the variables are set to their initial val- ues, and all the clocks are set to zero. Then, being in a state q = (l, v, c) the system can either execute an enabled transition t and move to the state q 0 = (l0 , v0 , c0 ) where l0 = target(t), the valuation of variables is changed according to instr(t) and the pa- rameter valuation p, and the clock valuation is changed according to asgn(t), or move to the state q 0 = (l, v, c + δ) which results from passing some time δ ∈ IR+ such that c + δ |= inv(l). We say that a location l (a variables valuation v, respectively) is reachable if some state (l, ·, ·) ((·, v, ·), respectively) is reachable in S(A, p). Given D ⊆ DV , a partial variables valuation vD : D −→ T is reachable if some state (·, v, ·) s.t. v | D = vD is reachable in S(A, p). 5.2 SAT-Based Reachability Checking In the paper [19] we showed how to test reachability for timed automata with discrete data (TADD) using SAT-based bounded model checking to this aim. The main idea con- sisted in discretising the set of clock valuation of the automaton considered, in order to obtain a countable state space. Next, the transition relation of the transition system obtained was unfolded up to some depth k, and the unfolding was encoded as a propo- sitional formula. The property to be tested was encoded as a propositional formula as well, and satisfiablity of the conjunction of these two formulas was checked using a SAT-solver. Satisfiability of the conjunction allowed to conclude that a path from the initial state to a state satisfying the property was found. Comparing with the automata considered in [19], the automata used in this paper are extended in the following way: – values of discrete variables are not only integers, but are of several discrete types, – arithmetic expressions used can be of a more involved form, – the invariant function involves not only clock comparisons, but also boolean ex- pression over values of discrete variables, – the definition of the automaton contains additionally a set of parameters, and the instructions can be assignments of the form a variable := a parameter. Automatic composition of web services Petri Nets & Concurrency – 465 As it is easy to see, discretisation of the set of clock valuations for TADDPA can be done analogously as in [19]. The way of extending arithmetic operations on integers was described in [18]. New data types can be handled by conversions to integers; intro- ducing extended invariants is straightforward. The only problem whose solution cannot be easily adapted from the previous approach is that SAT-based reachability testing for TADDPA involves also searching for a parameter valuation for which a state satisfying a given property can be reached. However, the idea of doing this can be derived from the idea of SAT-solvers: a SAT-solver searches for a valuation of propositional vari- ables for which a formula holds. Thus, we represent the values of parameters by sets of propositional variables; finding a valuation for which a formula γ which encodes that a state satisfying a given property is reachable along a path of a length k implies also finding an appropriate valuation of parameters occurring along the path considered. 5.3 SAT-Based Service Composition In order to apply the above verification method to automatic searching for sequences of concrete services able to satisfy the user’s request we translate paths of the abstract graph to timed automata with discrete data and parametric assignments. The translation uses the descriptions of concrete services, as well as the user’s query. Consider a path π = w0 → w1 → . . . wn (n ∈ IN) in the abstract graph, such that w0 ∈ Vp (i.e., is an initial world) and wn ∈ Vk (i.e., is a final world) - i.e., a sequence of worlds and abstract services which transform them. Let Oπ be the set of all the objects which occur in all the worlds along this path (i.e., Oπ = {o ∈ wi | i = 0, . . . , n}). Then, we define V (π) = {objectN ame.attributeN ame | objectN ame ∈ Oπ }, Vpre (π) = {objectN ame.attributeN ame.pre | objectN ame ∈ Oπ ∧ ∃i∈{0,...,n−1} objectN ame ∈ wi ∩wi+1 } and V 0 (π) = V (π)∪{v.isConst | v ∈ V (π)}∪{v.isSet | v ∈ V (π)} ∪ {v.isAny | v ∈ V (π)} ∪ Vpre (π). The set of discrete variables of the au- tomaton A(π) corresponding to π is equal to V 0 (π). The intuition behind this construc- tion is that for each attribute of each objects occuring along the path we define a variable aimed at storing the value of the attribute (objectN ame.attributeN ame). Moreover, for each such variable we introduce three new boolean variables: the one saying whether the flag isConst for the attribute has been set (objectN ame.attributeN ame.isConst), the second one to express that the attribute has been set (has a nonempty value; object- N ame.attributeN ame.isSet, and the third one to specify that the value of the at- tribute is nonempty but its exact value is not given (objectN ame.attributeN ame.is- Any). The variables in Vpre (π) (of the form objectN ame.attributeN ame.pre) are aimed at storing values of attributes from a pre-world of a service. The initial values of variables are taken from the initial world w0 resulting from the user’s query: – for each attribute x.y which according to the query has a concrete value γ in w0 , we set x.y := γ, x.y.isAny := f alse and x.y.isSet := true; concerning x.y.isConst we set it true if such a condition occurs in the query, otherwise it is set to f alse, – for each attribute x.y which according to the query is set, but its value is not given directly, we set x.y.isSet := true, and x.y.isAny = true; x.y.isConst is set 466 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny according to the query as above; x.y can obtain any value of the appropriate type (we can assume it gets a “zero” value of type(x.y)), – for each attribute x.y which does not occur in the query or is specified there as hav- ing the empty value we set x.y.isSet = f alse, x.y.isAny = true, x.y.isConst = f alse, the value of x.y is set to an arbitrary value as above, – each variable of the form x.y.pre is assumed to have a “zero” value of type(x, y). Define for each wi , i = 0, . . . , n, a new location of A(π), denoted for simplicity wi as well, and consider an edge wi → wi+1 of π (i ∈ {0, . . . , n − 1}), corresponding to an abstract service sai . For each concrete service s of the type of sai we introduce a s ε new location wis and the transitions wi → wis and wis → wi+1 (where ε is an “empty” label)11 . Then, we make use of the description of s as follows: s – the precondition of s becomes the guard of the transition wi → wis (notice that a disjunctive form is here allowed); s – the list requires of s is used to construct the instruction α “decorating” wi → wis : initially α is set to , then, for each attribute y of an object x occurring in requires for which it holds x.y.isSet = true, α is extended by concatenating x.y.pre := x.y, – the lists mustSet and mustSetConst of s are used to construct the instruction α as well: for each attribute x.y occuring in the list mustSet α is extended by concatenating x.y.isSet := true, and for each attribute x.y occuring in the list mustSetConst of s α is extended by concatenating x.y.isConst := true, – the postcondition is used as follows (x.y denotes an attribute): • the predicates Exists are ignored, • the (possibly negated) predicates of the form isSet(x.y) or isConst(x.y) s result in extending the instruction α “decorating” wi → wis by concatenating respectively x.y.isSet := true or x.y.isConst := true if such an instruc- tion has not been added to α before (or respectively x.y.isSet := f alse or x.y.isConst := f alse if the predicates are negated)12 , • each predicate of the form x.y = z or post(x.y)=z (where z can be either a concrete value or an expression13 ) results in extending the instruction α by concatenating x.y := z, x.y.isSet := true (if it has not been added before) and x.y.isAny := f alse, • for each predicate of the form x.y # z or post(x.y) # z with # ∈ {< , >, ≤, ≥} (where z is either a concrete value or an expression) we introduce a new parameter p, extend α by concatenating x.y := p, x.y.isSet := true (if it has not been added before) and x.y.isAny := f alse, and conjunct the invariant of wis (initially true) with the above predicate. 11 We assume here that the postcondition of s contains no disjunctions; otherwise we treat s a number of concrete services each of which has the postcondition corresponding to one part of the DNF in the original postcondition of s. 12 Possible inconsistencies, i.e. an occurence of x.y in mustSet and the predicate not isSet(x.y) in postCondition, are treated as ontology errors. 13 Recall that the expressions can refer only to values the variables have in the pre-world of a service. Automatic composition of web services Petri Nets & Concurrency – 467 – moreover, for each attribute x.y which occurs either in mustSet or in the post- conidition in a predicate isSet(x.y), but does not have in the postCondtion any “corresponding” predicate which allows to set its value, we introduce a new parameter psx.y , and extend α by adding x.y := psx.y and x.y.isAny := f alse. The invariants of wi and wi+1 , as well as the guard of the transition labelled with ε are set to true. The set of instructions of the latter transition is empty. The set of clocks of A(π) is empty as well. The intuition behind the above construction is as follows: initially, only the variables of the form x.y corresponding to attributes specified by the user’s query as having concrete values are set, while the rest stores random values (which is expressed by x.y.isAny = true). Next, concrete services modify values of the variables. If the description of a service specifies that an attribute is set and specifies the exact value assigned, then the transition corresponding to execution of this service sets the corresponding variable in an appropriate way. If the exact value of the attribute set is not given, a parameter for the value assigned is introduced, and possible conditions on this parameter (specified in the postcondition) are assigned to the target location as a part of its invariant. Moreover, before introducing any changes to the values of the variables corresponding to the attributes of the objects in requires their previous values are stored. The above construction can be optimised in several ways. Firstly, one can add a new “intermediate” location wis only in the case when no location, corresponding to a service of the same type as s and having the appropriate invariant, has been added before; otherwise, the transition outgoing wi can be redirected to the existing location. Secondly, the variables of the form x.y.pre can be introduced only for these attributes for which there is a postcondition of a service which refers both to pre(x).y and post(x).y. Finally, if we have several concrete services of a given type t occuring as the i-th service along the abstract path, and - according to the above construction - need to introduce for each of them a parameter to be assigned to a variable x.y, then we can reduce the number of parameters: instead of introducing a new parameter for each concrete service we can introduce one parameter pt,i x.y . This follows from the fact that only one concrete service of this type is exectuted as the i-th, and therefore only one assignment a new value to x.y is performed. 6 Experimental Results and Concluding Remarks The method described above has been implemented. The preliminary implementation was tested on a Getting Juice example considered in [3], by running it to generate a sequence of concrete services corresponding to the abstract path SelectWare, then FruitSelling and then MakingJuice. The sequence has been found; a detailed de- scription of the example together with the result can be found in the appendix. Currently, the automaton is generated by hand, since a repository of concrete ser- vices is still under construction. In the future we are going to automate the method completely, including dynamic translation of a service, dynamic creation of enumera- tion types based on the query and on the contents of the repository, and building the automaton step by step. This will enable us to test efficiency of the approach. 468 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny References 1. S. Ambroszkiewicz. enTish: An Approach to service Description and Composition. ICS PAS, Ordona 21, 01-237 Warsaw, 2003. 2. DAML-S (and OWL-S) 0.9 draft release. http://www.daml.org/services/daml-s/0.9/, 2003. 3. M. Jarocki, A. Niewiadomski, W. Penczek, A. Półrola, and M. Szreter. Towards automatic composition of web services: Abstract planning phase. Technical Report 1017, ICS PAS, Ordona 21, 01-237 Warsaw, February 2010. 4. M. Klusch, A. Geber, and M. Schmidt. Semantic web service composition planning with OWLS-XPlan. In Proc. of the 1st Int. AAAI Fall Symposium on Agents and the Semantic Web. AAAI Press, 2005. 5. D. McDermott, M. Ghallab, A. Howe, C. Knoblock, A. Ram, M. Veloso, D. Weld, and D. Wilkins. PDDL - the Planning Domain Definition Language - version 1.2. Technical Report TR-98-003, Yale Center for Computational Vision and Control, 1998. 6. S. R. Ponnekanti and A. Fox. SWORD: A developer toolkit for web service composition. In Proc. of the 11st Int. World Wide Web Conference (WWW’02), 2002. 7. J. Rao. Semantic Web Service Composition via Logic-Based Program Synthesis. PhD thesis, Dept. of Comp. and Inf. Sci., Norwegian University of Science and Technology, 2004. 8. J. Rao, P. Küngas, and M. Matskin. Logic-based web services composition: From service description to process model. In Proc. of the IEEE Int. Conf. on Web Services (ICWS’04). IEEE Computer Society, 2004. 9. J. Rao and X. Su. A survey of automated web service composition methods. In Proc. of the 1st Int. Workshop on Semantic Web Services and Web Process Composition (SWSWPC 2004), pages 43–54, 2004. 10. D. Redavid, L. Iannone, and T. Payne. OWL-S atomic services composition with SWRL rules. In Proc. of the 4th Italian Semantic Web Workshop: Semantic Web Applications and Perspectives (SWAP 2007), 2007. 11. RSat. http://reasoning.cs.ucla.edu/rsat, 2006. 12. E. Sirin, J. Hendler, and B. Parsia. Semi-automatic compositions of web services using semantic description. In Proc. of the Int. Workshop ’Web Services: Modeling, Architecture and Infrastructure’ (at ICEIS 2003), 2003. 13. SOAP version 1.2. http://www.w3.org/TR/soap, 2007. 14. B. Srivastava and J. Koehler. Web service composition - current solutions and open problems. In Proc. of Int. Workshop on Planning for Web Services (at ICAPS 2003), 2003. 15. Universal Description, Discovery and Integration v3.0.2 (UDDI). http://www.oasis- open.org/committees/uddi-spec /doc/spec/v3/uddi-v3.0.2-20041019.htm, 2005. 16. Web Services Business Process Execution Language v2.0. http://docs.oasis-open.org/ wsbpel/2.0/OS/wsbpel-v2.0-OS.html, 2007. 17. Web Services Description Language (WSDL) 1.1. http://www.w3.org/TR/2001/NOTE- wsdl-20010315, 2001. 18. A. Zbrzezny. A boolean encoding of arithmetic operations. Technical Report 999, ICS PAS, 2007. 19. A. Zbrzezny and A. Półrola. SAT-based reachability checking for timed automata with dis- crete data. Fundamenta Informaticae, 70(1-2):579–593, 2007. A Experimental Results - A Detailed Description Below we present the Getting Juice example considered in [3]. Assume we have the following classes: Automatic composition of web services Petri Nets & Concurrency – 469 Ware id integer Ware name string Ware owner string Measurable capacity float Juice extends Ware, Measurable Fruits extends Ware, Measurable and the following types of services: SelectWare produces w:Ware SelectWare consumes null SelectWare requires null SelectWare mustSet w.name; w.owner Selling produces null Selling consumes null Selling requires w:Ware Selling mustSet w.id; w.owner Selling preCondition not isSet(w.id) and isSet(w.name) and isSet(w.owner) Selling postCondition w.owner!=pre(w).owner FruitSelling extends Selling FruitSelling requires w:Fruits FruitSelling mustSet w.capacity FruitSelling postCondition w.capacity>0 JuiceSelling extends Selling JuiceSelling requires w:Juice JuiceSelling mustSet w.capacity JuiceSelling postCondition w.capacity>0 MakingJuice produces j:Juice MakingJuice consumes f:Fruits MakingJuice mustSet j.id; j.name; j.capacity MakingJuice preCondition isSet(f.id) and isSet(f.name) and isSet(f.owner) and f.capacity>0 MakingJuice postCondition isSet(j.id) and isSet(j.name) and j.capacity>0 The user’s query is specified as follows: InitWorld null InitClause true EffectWorld j:Juice EffectClause j.id>0 and j.capacity=10 and j.owner="Me" One of the sequences of services which possibly can lead to satisfying the query is SelectWare, then FruitSelling and then MakingJuice [3]. Below we consider concretising the above path of the abstract graph. Assume the concrete instances of the SelectWare specify the following offers14 : 14 The current version of our implementation does not deal with inheritance of classes. 470 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny FruitNetMarket mustSet w.name, w.owner FruitNetMarket preCondition - FruitNetMarket postCondition (w.name=strawberry and w.owner=shop1) or (w.name=blueberry and w.owner=shop1) FruitNetOffers mustSet w.name, w.owner FruitNetOffers preCondition - FruitNetOffers postCondition (w.name=plum and w.owner=shop2) or (w.name=apple and w.owner=shop2) or (w.name=apple and w.owner=shop3) Next, the fruitselling services specify: Shop1 mustSet w.id, w.owner, w.capacity Shop1 precondition not isSet(w.id) and isSet(w.name) and isSet(w.owner) and w.owner=shop1 Shop1 postcondition w.owner!=pre(w).owner and w.id>0 and w.capacity>0 and w.capacity<=10 Shop2 mustSet w.id, w.owner, w.capacity Shop2 precondition not isSet(w.id) and isSet(w.name) and isSet(w.owner) and w.owner=shop2 Shop2 postcondition w.owner!=pre(w).owner and w.id>0 and w.capacity>0 Shop3 mustSet w.id, w.owner, w.capacity Shop3 precondition not isSet(w.id) and isSet(w.name) and isSet(w.owner) and w.owner=shop3 Shop3 postcondition w.owner!=pre(w).owner and w.id>0 and w.capacity>=100 which means that Shop1 is able to sell at most 10 units of fruits, Shop2 - at least 100 units, while Shop3 is able to sell any amount. Finally, we have the following services which make juice: HomeJuiceMaking mustSet j.id, j.name, j.capacity HomeJuiceMaking preCondition isSet(f.id) and isSet(f.name) and isSet(f.capacity) and isSet(f.owner) and f.capacity>0 and f.capacity<=10 and f.name!=plum and f.name!=apple HomeJuiceMaking postCondition isSet(j.id) and isSet(j.name) and j.capacity>0 and j.name=f.name and j.capacity=f.capacity and j.owner=f.owner GrandmaKitchen mustSet j.id, j.name, j.capacity GrandmaKitchen preCondition isSet(f.id) and isSet(f.name) and isSet(f.capacity) and isSet(f.owner) and f.capacity>0 and f.capacity<=5 Automatic composition of web services Petri Nets & Concurrency – 471 GrandmaKitchen postCondition isSet(j.id) and isSet(j.name) and j.capacity>0 and j.name=f.name and j.capacity=f.capacity and j.owner=f.owner JuiceTex mustSet j.id, j.name, j.capacity JuiceTex preCondition isSet(f.id) and isSet(f.name) and isSet(f.capacity) and isSet(f.owner) and f.capacity>0 JuiceTex postCondition isSet(j.id) and isSet(j.name) and j.capacity>0 and j.name=f.name and j.capacity=2*f.capacity and j.owner=f.owner Thus, assume that we have the following types: integer, float (we can assume that the precision is up to two decimal places), FruitTypes = (strawberry, blueberry, apple, plum), and OwnerNames = (Me, Shop1, Shop2, Shop3, Shop4) (the ranges of enumeration types can be deduced from the offers and from the user’s query). The variables and their types are: f.id : integer, f.name : F ruitT ypes, f.owner : OwnerN ames, f.capacity : f loat, j.id : integer, j.name : F ruitT ypes, j.owner : OwnerN ames, j.capacity : f loat plus the corresponding boolean variables of the form x.y.isSet, x.y.isAny and x.y.isConst. Moreover, we introduce one additional variable f.owner.pre : OwnerN ames to store the previous value of f.owner15 . All the variables of the form x, y are initialised to zero values of the appropriate types, each x.y.isSet and x.y.isConst is initialised with f alse, and each x.y.isAny is initialised with true. – The FruitNetMarket generates two transitions )together with the intermediate locations and the “ε-transitions” outgoing them). The first one is decorated with f.name.isSet := true; f.owner.isSet := true; f.name := strawberry; f.ow- ner := shop1; f.owner.isAny := f alse; f.name.isAny := f alse, the second one is decorated in a similar way, but with f.name := blueberry, the edges for the three offers of FruitNetOffers look similarily, – the fruitselling services correspond to the following edges and intermediate loca- tions: • for Shop1: ∗ the guard of the first edge is f.id.isSet = f alse∧f.name.isSet = true∧ f.owner.isSet = true ∧ f.owner = shop1, ∗ the instruction is f.id.isSet := true; f.owner.isSet := true; f.capaci- ty.isSet := true; f.id.isAny := f alse; f.owner.isAny := f alse; f.ca- pacity.isAny := f alse; f.owner.pre := f.owner; f.owner := pF S f.own ; f.id := pFf.id ; f.capacity := pf.cap (where p· are parameters), S FS FS ∗ the invariant of the intermediate location is ¬(f.owner.pre = f.owner) ∧ f.id > 0 ∧ f.capacity > 0 ∧ f.capacity ≤ 10; 15 We apply the optimisation allowing to add one variable of the form x.y.pre only, as well as the one consisting in reducing the number of parameters. 472 Petri Nets & Concurrency Penczek, Pólrola, and Zbrzezny • for Shop2: ∗ the guard of the first edge is f.id.isSet = f alse∧f.name.isSet = true∧ f.owner.isSet = true ∧ f.owner = shop2, ∗ the instruction is f.id.isSet := true; f.owner.isSet := true; f.capaci- ty.isSet := true; f.id.isAny := f alse; f.owner.isAny := f alse; f.ca- pacity.isAny := f alse; f.owner.pre := f.owner; f.owner := pF S f.own ; f.id ; f.capacity := pf.cap , f.id := pF S FS ∗ the invariant of the intermediate location is ¬(f.owner.pre = f.owner) ∧ f.id > 0 ∧ f.capacity > 0, • for Shop3: ∗ the guard of the first edge is f.id.isSet = f alse∧f.name.isSet = true∧ f.owner.isSet = true ∧ f.owner = shop3, ∗ the instruction is f.id.isSet := true; f.owner.isSet := true; f.capaci- ty.isSet := true; f.id.isAny := f alse; f.owner.isAny := f alse; f.ca- pacity.isAny := f alse; f.owner.pre := f.owner; f.owner := pF S f.own ; f.id := pf.id ; f.capacity := pf.cap , FS FS ∗ the invariant of the intermediate location is ¬(f.owner.pre = f.owner) ∧ f.id > 0 ∧ f.capacity ≥ 0, – for the services making juice from fruits: • for HomeJuiceMaking: ∗ the guard of the first edge is f.id.isSet = true ∧ f.name.isSet = true ∧ f.owner.isSet = true ∧ f.capacity.isSet = true ∧ f.capacity > 0 ∧ f.capacity ≤ 10 ∧ ¬(f.name = plum) ∧ ¬(f.name = apple) ∗ the instruction is j.id.isSet := true; j.id.isAny := f alse; j.name.is- Set := true; j.name.isAny := f alse; j.capacity.isSet := true; j.capa- city.isAny := f alse; j.owner.isSet := true; j.owner.isAny := f alse; j.id := pM J j.id ; j.capacity := f.capacity; j.name := f.name, j.owner := f.owner ∗ the invariant of the intermediate location is j.capacity > 0 • for GrandmaKitchen ∗ the guard of the first edge is f.id.isSet = true ∧ f.name.isSet = true ∧ f.owner.isSet = true ∧ f.capacity.isSet = true ∧ f.capacity > 0 ∧ f.capacity ≤ 5, ∗ the instruction is j.id.isSet := true; j.id.isAny := f alse; j.name.is- Set := true; j.name.isAny := f alse; j.capacity.isSet := true; j.capa- city.isAny := f alse; j.owner.isSet := true; j.owner.isAny := f alse; j.id := pM J j.id ; j.capacity := f.capacity; j.name := f.name, j.owner := f.owner ∗ the invariant of the intermediate location is j.capacity > 0 • for JuiceTex ∗ the guard of the first edge is f.id.isSet = true ∧ f.name.isSet = true ∧ f.owner.isSet = true ∧ f.capacity.isSet = true ∧ f.capacity > 0 ∗ the instruction is j.id.isSet := true; j.id.isAny := f alse; j.name.is- Set := true; j.name.isAny := f alse; j.capacity.isSet := true; j.capa- city.isAny := f alse; j.owner.isSet := true; j.owner.isAny := f alse; j.id := pM J j.id ; j.capacity := 2 ∗ f.capacity; j.name := f.name, j.ow- ner := f.owner Automatic composition of web services Petri Nets & Concurrency – 473 ∗ the invariant of the intermediate location is j.capacity > 0 The condition to be tested is j.id.isSet ∧ ¬j.id.isAny ∧ j.capacity.isSet ∧ ¬j.capa- city.isAny ∧ j.owner.isSet ∧ ¬j.owner.isAny ∧ j.id > 0 ∧ j.capacity = 10 ∧ j.owner = me. In practice, we extend it by adding an additional proposition which is true in the locations w0 , . . . , w3 to avoid obtaining paths which finish before both the transitions corresponding to a concrete service are executed. After running our preliminary implementation, we have obtained the path corre- sponding to selling 10 units of blueberries by Shop1 and processing them by Home- JuiceMaking. A screenshot displaying the witness is presented in Fig. 1. To find the Fig. 1. A witness for concretisation of an abstract path for the Getting Juice example witness, we checked satisfaction of the boolean formula encoding the translation of the tested condition. The formula in question consisted of 20152 variables and 52885 clauses; our implementation needed 0.65 second and 6.2 MB memory to produce it. Its satisfiability was checked by RSAT[11], a mainstream SAT solver; to checking it 0.1 seconds and 5.6 MB of memory were needed.