=Paper=
{{Paper
|id=None
|storemode=property
|title=Towards Automatic Composition of Web Services: A SAT-Based Phase
|pdfUrl=https://ceur-ws.org/Vol-827/34_WojciechPenczek_article.pdf
|volume=Vol-827
|dblpUrl=https://dblp.org/rec/conf/acsd/PenczekPZ10
}}
==Towards Automatic Composition of Web Services: A SAT-Based Phase==
https://ceur-ws.org/Vol-827/34_WojciechPenczek_article.pdf
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.