=Paper=
{{Paper
|id=None
|storemode=property
|title=SMT-based Abstract Temporal Planning
|pdfUrl=https://ceur-ws.org/Vol-1160/paper4.pdf
|volume=Vol-1160
|dblpUrl=https://dblp.org/rec/conf/apn/NiewiadomskiP14
}}
==SMT-based Abstract Temporal Planning==
<pdf width="1500px">https://ceur-ws.org/Vol-1160/paper4.pdf</pdf>
<pre>
        SMT-based Abstract Temporal Planning?

                  Artur Niewiadomski1 and Wojciech Penczek1,2
             1
                ICS, Siedlce University, 3-Maja 54, 08-110 Siedlce, Poland
                           artur.niewiadomski@uph.edu.pl
    2
      ICS, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland
                               penczek@ipipan.waw.pl



        Abstract. An abstract planning is the first phase of the web service
        composition in the Planics framework. A user query specifies the initial
        and the expected state of a plan in request. The paper extends Planics
        with a module for temporal planning, by extending the user query with
        an LT Lk X formula specifying temporal aspects of world transformations
        in a plan. Our solution comes together with an example, an implemen-
        tation, and experimental results.


Keywords: Web Service Composition, SMT, Abstract Planning, Temporal Plan-
ning, LTL


1     Introduction
Web service composition within Service-Oriented Architecture (SOA) [2] is still
attracting a lot of interest, being a subject of many theoretical and practical
approaches. The main idea consists in dealing with independent (software) com-
ponents available via well-defined interfaces. As typically a simple web service
does not satisfy the user objective, a composition is investigated in order to
make the user fully satisfied. An automatic composition of Web services aims at
relieving the user of a manual preparation of detailed execution plans, matching
services to each other, and choosing optimal providers for all the components.
The problem of finding such a satisfactory composition is NP-hard and well
known in the literature as the Web Service Composition Problem (WSCP) [2, 1,
21]. There are many various approaches to solve WSCP [14, 16], some of them
we discuss in the next section.
    In this paper, we follow the approach of the system Planics [8, 9], which has
been inspired by [1]. The main assumption is that all the web services in the
domain of interest as well as the objects which are processed by the services, can
be strictly classified in a hierarchy of classes, organised in an ontology. Another
key idea consists in dividing planning into several stages. The first phase, called
the abstract planning, deals with classes of services, where each class represents
a set of real-world services. This phase has been implemented in Planics using
?
    This work has been supported by the National Science Centre under the grant No.
    2011/01/B/ST6/01477.
56      PNSE’14 – Petri Nets and Software Engineering



two approaches: one based on a translation to SMT-solvers [17] and another one
exploiting genetic algorithms [22]. The second phase, called concrete planning,
deals with concrete services. Thus, while the first phase produces an abstract
plan, it becomes a concrete plan in the second phase. Such an approach enables
to reduce dramatically the number of concrete services to be considered as they
are already eliminated in the abstract planning phase. This paper focuses on the
abstract planning problem, but extends it to so called temporal planning. This
extension together with the experimental results is the main contribution of the
paper. The main idea behind this approach consists in providing the user with a
possibility to specify not only the first and the expected state of a plan in request,
but also to specify temporal aspects of state transformations in a plan. To this
aim we introduce two general types of atomic properties for writing a temporal
formula, namely propositions and level constraints. The propositions are used to
describe (intermediate) states of a plan in terms of existence (or non-existence)
of objects and abstract values of object attributes. The level constraints, built
over a special set of objects, are used for influencing a service ordering within
solutions. However, in order to express such restrictions the user has to rely on
some knowledge about the planning domain. In order to get this knowledge, the
planner can be first run without temporal constraints and then these restrictions
can be added after a non-temporal planning results have been obtained.
    We propose a novel approach based on applying SMT-solvers. Contrary to
a number of other approaches, we focus not only on searching for a single plan,
but we attempt to find all significantly different plans. We start with defining
the abstract planning problem (APP, for short). Then, we present our original
approach to APP based on a compact representation of abstract plans by mul-
tisets of service types. We introduce the language of LT Lk X for specifying the
temporal aspects of the user query. This approach is combined with a reduction
to a task for an SMT-solver. The encoding of blocking formulas allows for prun-
ing the search space with many sequences which use the same multiset of service
types in some plan already generated. Moreover, we give details of our algo-
rithms and their implementations that are followed by experimental results. To
the best of our knowledge, the above approach is novel, and as our experiments
show it is also very promising.
    The rest of the paper is organized as follows. Related work is discussed in
Section 2. Section 3 deals with the abstract planning problem. In Section 4 the
temporal planning is presented. An example of an abstract temporal planning is
shown in Section 5. Section 6 discusses the implementation and the experimen-
tal results of our planning system. The last section summarizes this paper and
discusses a further work.


2    Related Work

A classification matrix aimed at the influence on the effort of Web service compo-
sition is presented in [14]. According to [14], situation calculus [6], Petri nets [11],
theorem proving [20], and model checking [23] among others belongs to AI plan-
      A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning         57



ning. A composition method closest to ours based on SMT is presented in [16],
where the authors reduce WSCP to a reachability problem of a state-transition
system. The problem is encoded by a propositional formula and tested for satis-
fiability using a SAT-solver. This approach makes use of an ontology describing
a hierarchy of types and deals with an inheritance relation. However, we consider
also the states of the objects, while [16] deals with their types only. Moreover,
among other differences, we use a multiset-based SMT encoding instead of SAT.
    Most of the applications of SMT in the domain of WSC is related to the
automatic verification and testing. For example, a message race detection prob-
lem is investigated in [10], the paper [4] takes advantage of symbolic testing and
execution techniques in order to check behavioural conformance of WS-BPEL
specifications, while [15] exploits SMT to verification of WS-BPEL specifications
against business rules.
    Recently, there have also appeared papers dealing with temporal logics in
the context of WSC. Bersani et al. in [5] present a formal verification technique
for an extension of LTL that allows the users to include constraints on integer
variables in formulas. This technique is applied to the substitutability problem
for conversational services. The paper [13] deals with the problem of automatic
service discovery and composition. The authors characterize the behaviour of a
service in terms of a finite state machine, specify the user’s requirement by an
LTL formula, and provide a translation of the problem defined to SAT. However,
the paper does not specify precisely experimental results and such important
details as, e.g., the number of services under consideration. An efficient appli-
cation of the authors method is reported for plans of length up to 10 only. The
authors of [3] address the issue of verifying whether a composite Web services
design meets some desirable properties in terms of deadlock freedom, safety, and
reachability. The authors report on automatic translation procedures from the
automata-based design models to the input language of the NuSMV verification
tool. The properties to be verified can be expressed as LTL or CTL formulae.
    Searching for plans meeting temporal restrictions is also a topic of interest of
a broad planning community. The PDDL language [12] has been also extended
with LTL-like modal operators, but for planning automata-based methods are
used instead of SMT-based symbolic ones.


3     Abstract Planning

This section introduces APP as the first stage of WSCP in the Planics frame-
work. First, the Planics ontology is presented. Next, we provide some basic
definitions and explain the main goals of APP.


3.1    Planics Ontology

The OWL language [19] is used as the Planics ontology format. The concepts
are organized in an inheritance tree of classes, all derived from the base class -
Thing. There are 3 children of Thing: Artifact, Stamp, and Service (Fig. 1).
58     PNSE’14 – Petri Nets and Software Engineering




                                       Thing


                          Artifact     Stamp        Service


                    Fig. 1. The base classes in Planics ontology


     The branch of classes rooted at Artifact is composed of the types of the
objects, which the services operate on. Each object consists of a number of
attributes, whereas an attribute consists of a name and a type. Note that the
types of the attributes are irrelevant in the abstract planning phase as they are
not used by the planner. The values of the attributes of an object determine
its state, but in the abstract planning it is enough to know only whether an
attribute does have some value (i.e., is set), or it does not (i.e., it is null). The
Stamp class and its descendants define special-purpose objects, often useful in
constructing a user query, and in the planning process. A stamp is a specific type
aimed at a confirmation of the service execution. The specialized descendants
of the Service class can produce the stamp being an instance of any subtype
of Stamp and describing additional execution features. Note that each service
produces exactly one confirmation object. The classes derived from Artifact and
Stamp are called the object types.
     Each class derived from Service, called a service type, stands for a description
of a set of real-world services. It contains a formalized information about their
activities. A service type affects a set of objects and transforms them into a new
set of objects. The detailed information about this transformation is contained
in the attributes of a service type: the sets in, inout, and out, and the Boolean
formulas pre and post (pre and post, for short). These sets enumerate the objects,
which are processed by the service. The objects of the in set are read-only,
i.e., they are passed unchanged to the next world. Each object of inout can be
modified - the service can change some values of its attributes. The objects of
out are produced by the service.


3.2   Basic definitions

Let I denote the set of all identifiers used as the type names, the objects, and the
attributes. In APP we deal with abstract values only, the types of the attributes
are irrelevant, and we identify the attributes with their names. Moreover, we
denote the set of all attributes by A, where A ⇢ I. An object type is a pair
(t, Attr), where t 2 I, and Attr ✓ A. That is, an object type consists of the type
name and a set of the attributes. By P we mean a set of all object types.

Example 1. Consider the following exemplary ontology containing in addition to
Thing also the class Artifact and Stamp. The class Artifact corresponds to the
object type (Artif act, {id}) (the only attribute is an identifier) while the class
     A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning             59



Stamp corresponds to the object type (Stamp, {serviceClass, serviceId, level}),
introducing the attributes describing the service generating the stamp, and the
position of this service in an execution sequence we consider.

We define also a transitive, irreflexive, and antisymmetric inheritance relation
Ext ✓ P ⇥ P, such that (t1 , A1 ), (t2 , A2 ) 2 Ext iff t1 6= t2 and A1 ✓ A2 . That
is, a subtype contains all the attributes of a base type and optionally introduces
more attributes. An object o is a pair o = (id, type), where id 2 I and type 2 P.
By type(o) we denote the type of o. The set of all objects is denoted by O.
Amongst all the objects we distinguish between the artifacts (the instances of
the Artifact type) and the stamps (the instances of the Stamp type). The set of
all the stamps is denoted by ST, where ST ✓ O. Moreover, we define the function
attr : O 7 ! 2A returning the set of all attributes for each object of O.

Service types and user queries. The service types available for composition are
defined in the ontology by service type specifications. The user goal is provided
in a form of a user query specification, which is then extended by a temporal
formula. Before APP, all the specifications are reduced to sets of objects and
abstract formulas over them. An abstract formula over a set of objects O
and their attributes is a DNF formula without negations, i.e., the disjunction of
clauses, referred to as abstract clauses. Every abstract clause is the conjunction
of literals, specifying abstract values of object attributes using the functions
isSet and isN ull. In the abstract formulas used in APP, we assume that no
abstract clause contains both isSet(o.a) and isN ull(o.a), for the same o 2 O
and a 2 attr(o). For example (isSet(o.a) ^ isSet(o.b)) _ isN ull(o.a) is a correct
abstract formula. The syntax of the specifications of the user queries and of the
service types is the same and it is defined below.

Definition 1. A specification is a 5-tuple (in, inout, out, pre, post), where in,
inout, out are pairwise disjoint sets of objects, and pre is an abstract formula
defined over objects from in [ inout, while post is an abstract formula defined
over objects from in [ inout [ out.

A user query specification q or a service type specification s is denoted by
specx = (inx , inoutx , outx , prex , postx ), where x 2 {q, s}, resp. In order to for-
mally define the user queries and the service types, which are interpretations
of their specifications, we need to define the notions of valuation functions and
worlds.
                       W
Definition 2. Let ' = i=1..n ↵i be an abstract formula.
                                                    S     A valuation of
the attributes over ↵i is the partial function v↵i : o2O {o} ⇥ attr(o) 7 !
{true, f alse}, where:

• v↵i(o, a)= true if isSet(o.a) is a literal of ↵i , and
• v↵i(o, a)= f alse if isN ull(o.a) is a literal of ↵i , and
• v↵i(o, a) is undefined, otherwise.
60      PNSE’14 – Petri Nets and Software Engineering



We define the restriction of a valuation function v↵i to a set of objects O ⇢ O
as v↵i (O) = v↵i S {o}⇥attr(o) . The undefined values appear when the inter-
                    o2O
preted abstract formula does not specify abstract values of some attributes,
which is a typical case in the WSC domain. The undefined values are used also
for representing families of total valuation functions. Next, for a partial valua-
tion function f , by total(f ) we denote the family of the total valuation functions
on the same domain, which are consistent with f , i.e., agree on the values de-
fined of f . Moreover, we define a family of the valuation functions V' over the
abstract formula ' as the union of the sets Snof the consistent valuation functions
over every abstract clause ↵i , i.e., V' = i=1 total(v↵i ). The restriction of the
family of Sfunctions V' to a set of objects O and their attributes is defined as
             n
V' (O) = i=1 total(v↵i (O)).

Definition 3. A world w is a pair (Ow , vw ), where Ow ✓ O and vw = v(Ow )
is a total valuation function equal to some valuation function v restricted to Ow .
The size of w, denoted by |w| is equal to |Ow |.

That is, a world represents a state of a set of objects, where each attribute is
either set or null. By a sub-world of w we mean a world built from a subset of
Ow and vw restricted to the objects from the chosen subset. Moreover, a pair
consisting of a set of objects and a family of total valuation functions defines a set
of worlds. That is, if V = {v1 , . . . , vn } is a family of total valuation functions and
O ✓ O is a set of objects, then O, V(O) means the set { O, vi (O) | 1  i  n},
for n 2 N. Finally, the set of all worlds is denoted by W.
    Now, we are in a position to define a service type and a (basic) user query
as an interpretation of its specification. In the next section the user query is
extended to a temporal version.

Definition 4. Let specx = (inx , inoutx , outx , prex , postx ) be a user query or a
service type specification, where x 2 {q, s}, resp. An interpretation of specx is a
pair of world sets x = (Wprex     x
                              , Wpost ), where:

 – Wpre
      x
         = inx [ inoutx , Vpre
                           x
                               , where Vpre
                                         x
                                            is the family of the valuation func-
   tions over prex ,
 – Wpost
      x
          = inx [inoutx [outx , Vpost
                                  x
                                      , where Vpost
                                                x
                                                    is the family of the valuation
   functions over postx .
An interpretation of a user query (service type) specification is called simply a
user query (service type, resp.).

For a service type (Wpre
                       s     s
                          , Wpost      s
                                  ), Wpre  is called the input world set, while Wpost
                                                                                    s

- the output world set. The set of all the service types defined in the ontology is
                                             q
denoted by S. For a user query (Wpre q
                                        , Wpost      q
                                                ), Wpre is called the initial world set,
         q                                                 q
while Wpost - the expected world set, and denoted by Winit     and Wexp
                                                                      q
                                                                         , respectively.
Abstract Planning Overview. The main goal of APP is to find a composition
of service types satisfying a user query, which specifies some initial and some
expected worlds as well as some temporal aspects of world transformations.
     A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning                    61



    Intuitively, an initial world contains the objects owned by the user, whereas
an expected world consists of the objects required to be the result of the service
composition. To formalize it, we need several auxiliary concepts.
    Let o, o0 2 O and v and v 0 be valuation functions. We say that v 0 (o0 ) is
compatible with v(o), denoted by v 0 (o0 ) obj v(o), iff the types of both objects
are the same, or the type of o0 is a subtype of type of o, i.e., type(o) = type(o0 )
or (type(o0 ), type(o)) 2 Ext, and for all attributes of o, we have that v 0 agrees
with v, i.e., 8a2attr(o) v 0 (o0 , a) = v(o, a). Intuitively, an object of a richer type (o0 )
is compatible with the one of the base type (o), provided that the valuations of
all common attributes are equal.
    Let w = (O, v), w0 = (O0 , v 0 ) be worlds. We say that the world w0 is compati-
ble with the world w, denoted by w0 wrl w, iff there exists a one-to-one mapping
map : O 7 ! O0 such that 8o2O v 0 (map(o)) obj v(o). Intuitively, w0 is compat-
ible with w if both of them contain the same number of objects and for each
object from w there exists a compatible object in w0 . The world w0 is called sub-
compatible with the world w, denoted by w0 swrl w iff there exists a sub-world
of w0 compatible with w.
World transformations. One of the fundamental concepts in our approach con-
cerns a world transformation. A world w, called a world before, can be trans-
formed by a service type s, having specification specs , if w is sub-compatible
with some input world of s. The result of such a transformation is a world w0 ,
called a world after, in which the objects of outs appear, and, as well as the
objects of inouts , they are in the states consistent with some output world of s.
The other objects of w do not change their states. In a general case, there may
exist a number of worlds possible to obtain after a transformation of a given
world by a given service type, because more than one sub-world of w can be
compatible with an input world of s. Therefore, we introduce a context function,
which provides a strict mapping between objects from the worlds before and
after, and the objects from the input and output worlds of a service type s.
Definition 5. A context function ctxsO : ins [ inouts [ outs 7 ! O is an
injection, which for a given service type s and a set of objects O assigns an
object from O to each object from ins , inouts , and outs .
Now, we can define a world transformation.
Definition 6. Let w, w0 2 W be worlds, called a world before and a world after,
respectively, and s = (Wpre  s      s
                               , Wpost  ) be a service type. Assume that w = (O, v),
w = (O , v ), where O ✓ O ✓ O, and v, v 0 are valuation functions. Let ctxsO0
  0      0 0                    0

be a context function, and the sets IN , IO, OU be the ctxsO0 images of the sets
ins , inouts , and outs , respect., i.e., IN = ctxsO0 ins , IO = ctxsO0 inouts , and
OU = ctxsO0 outs . Moreover, let IN, IO ✓ (O \ O0 ) and OU = (O0 \ O).
    We say that a service type s transforms the world w into w0 in the context
                        s,ctxs 0
ctxsO0 , denoted by w !O w0 , if for some vpre
                                           s      s
                                               2 Vpre and vpost
                                                           s       s
                                                                2 Vpost , all the
following conditions hold:
 1. IN, v(IN )       wrl          s
                           ins , vpre (ins ) ,
62     PNSE’14 – Petri Nets and Software Engineering



2. (IO, v(IO)) wrl inouts , vpres
                                   (inouts ) ,
3. (IO, v (IO))
         0        wrl            s
                      inouts , vpost (inouts ) ,
4. (OU, v 0 (OU )) wrl outs , vpost
                               s
                                    (outs ) ,
5. 8o2(O\IO) 8a2attr(o) v(o, a) = v 0 (o, a).

Intuitively, (1) the world before contains a sub-world built over IN , which is
compatible with a sub-world of some input world of the service type s, built
over the objects from ins . (2) The world before contains a sub-world built over
IO, which is compatible with a sub-world of the input world of the service type
s, built over the objects from inouts . (3) After the transformation the state of
objects from IO is consistent with posts . (4) The objects produced during the
transformation (OU ) are in a state consistent with posts . (5) The objects from
IN and the objects not involved in the transformation do not change their states.
    In the standard way we extend a world transformation to a sequence of world
transformations seq. We say that a world w0 is transformed by the sequence seq
                                   seq
into a world wn , denoted by w0         wn , iff there exists a sequence of worlds
                                                         s
                                                   si ,ctxOi
⇢ = (w0 , w1 , . . . , wn ) such that 81in wi 1 ! i wi = (Oi , vi ) for some vi .
Then, the sequence seq = (s1 , . . . , sn ) is called a transformation sequence and ⇢
is called a world sequence.
    Having the transformation sequences defined, we introduce the concept of
user query solutions or simply solutions, in order to define a plan.
                                                                   q
Definition 7. Let seq be a transformation sequence, q = (Winit             q
                                                                       , Wexp ) be a
                                                              q
user query. We say that seq is a solution of q, if for w 2 Winit and some world
                seq
w0 such that w      w0 , we have w0 swrl wexp
                                           q
                                              , for some wexp
                                                           q
                                                               2 Wexpq
                                                                        . The world
sequence corresponding to seq is called a world solution. The set of all the (world)
solutions of the user query q is denoted by QS(q) (W S(q), resp.).

Intuitively, by a solution of q we mean any transformation sequence transforming
some initial world of q to a world sub-compatible to some expected world of q.
Plans. Basing on the definition of a solution to the user query q, we can now
define the concept of an (abstract) plan, by which we mean a non-empty set of
solutions of q. We define a plan as an equivalence class of the solutions, which
do not differ in the service types used. The idea is that we do not want to distin-
guish between solutions composed of the same service types, which differ only in
the ordering of their occurrences or in their contexts. So we group them into the
same class. There are clearly two motivations behind that. Firstly, the user is
typically not interested in obtaining many very similar solutions. Secondly, from
the efficiency point of view, the number of equivalence classes can be exponen-
tially smaller than the number of the solutions. Thus, two user query solutions
are equivalent if they consist of the same number of the same service types,
regardless of the contexts.

Definition 8. Let seq 2 QS(q) be a solution of some user query q. An abstract
plan is a set of all the solutions equivalent to seq, denoted by [seq]⇠ .
      A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning           63



It is important to notice that all the solutions within an abstract plan are built
over the same multiset of service types, so a plan is denoted using a multiset
notation, e.g., the plan [2S + 4T + 3R] consists of 2 services S, 4 services T , and
3 services R.
    In order to give the user a possibility to specify not only the initial and
expected states of a solution, we extend the user query with an LT Lk X formula
' specifying temporal aspects of world transformations in a solution. Then, the
temporal solutions are these solutions for which the world sequences satisfy '.
This is formally introduced in the next section.


4     Temporal Abstract Planning

In this section we extend the user query by an LT Lk X temporal formula and a
solution to a temporal solution by requiring the temporal formula to be satisfied.
The choice of linear time temporal logic is quite natural since our user query
solutions are defined as sequences of worlds. The reason for disallowing a direct
use of the operator X (by removing it from the syntax) is twofold. Firstly, we
still aim at not distinguishing sequences which differ only in the ordering of
independent service types. Secondly, if the user wants to introduce the order on
two consequtive service types he can use formulas involving level constraints. On
the other hand our language and the temporal planning method can be easily
extended with the operator X.
     We start with defining the set of propositional variables, the level constraints,
and then the syntax and the semantics of LT Lk X .


4.1    Propositional variables

Let o 2 O be an object, a 2 attr(o). The set of propositional variables P V =
{pEx(o), pSet(o.a), pNull(o.a) | o 2 O, a 2 attr(o)}. Intuitively, pEx(o) holds
in each world, where the object o exists, pSet(o.a) holds in each world, where
the object o exists and the attribute a is set, and pNull(o.a) holds in each world,
where the object o exists and the attribute a is null.
    In addition to P V we use also the set of level constraints LC over the stamps
ST, defined by the following grammar:

                           lc ::= lexp ⇠ lexp                                     (1)
                         lexp ::= c | s.level | lexp   lexp

where s 2 ST, c 2 Z,       2 {+, , ·, /, %}, ⇠ 2 {, <, =, >, }, and /, % stand
for integer division and modulus, respectively.
    Intuitively, s.level < c holds in each world, where the stamp s exists and the
value of its level is smaller than c.
64      PNSE’14 – Petri Nets and Software Engineering



4.2   Syntax of LT Lk X

The LT Lk X formulae are defined by the following grammar:
             ' ::= p | ¬p | lc | ¬lc | ' ^ ' | ' _ ' | 'U<k ' | 'R<k '.
where p 2 P V , lc 2 LC, and k 2 N.
    Observe that we assume that the LT Lk X formulae are given in the negation
normal form (NNF), in which the negation can be only applied to the propo-
sitional variables and the level constraints. The temporal modalities U<k and
R<k are named as usual k-restricted until and release, respectively. Intuitively,
'U<k means that eventually, but in less than k steps, holds and always ear-
lier ' holds. The formula 'R<k expresses that either for the next k 1 states
   holds or in less than k steps, ' holds and always earlier holds.
                                                                    def
The derived basic temporal modalities are defined as follows: F<k ' = trueU<k '
           def
and G<k ' = f alseR<k '.

4.3   Semantics of LT Lk X
We start with defining models over the world solutions, which are finite sequences
of worlds.

Definition 9. A model is a pair M = (⇢, V⇢ ), where ⇢ = (w Sn0 , w1 , . . . , wn ) is a
world solution with wi = (Oi , vi ) for 0  i  n, and V⇢ : i=0 {wi } ⇥ ST !
N [ {1} is the function over the worlds of ⇢ valuating the expressions of the
form stamp.level, defined as follows:
 – V⇢ (wi , s.level) = 1 if s 62 Oi ,
 – V⇢ (wi , s.level) = 0 if s 2 O0 ,
 – V⇢ (wi , s.level) = j if s 2 Oj and s 62 Oj 1 , for some 1  j  i.

The intuition behind the definition of V⇢ is as follows. If a stamp s is not an
element of a world w, then the value of s.level in w does not exist, and this is
denoted by 1. If a stamp s is an element of the world w0 , then the value of
s.level is 0 in all the worlds. If wj is the world, where s appears for the first
time, then the value of s.level is equal to j in wj as well as in all further worlds.
    Before defining the semantics of LT Lk X we extend the stamp.level valuation
function V⇢ from ST to the level expressions as follows:

 – V⇢ (wi , c) = c,
 – V⇢ (wi , lexp lexp0 ) = V⇢ (wi , lexp) V⇢ (wi , lexp0 ) if V⇢ (wi , lexp) 6= 1 =
                                                                                  6
   V⇢ (wi , lexp0 ),
 – V⇢ (wi , lexp lexp0 ) = 1 if V⇢ (wi , lexp) = 1 or V⇢ (wi , lexp0 ) = 1,

We say that an LT Lk X formula ' is true in M = (⇢, V⇢ ) (in symbols M |= ')
iff w0 |= ', where for m  n we have:
 – wm |= pEx(o) iff o 2 Om .
        A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning                                                            65



 – wm |= pSet(o.a) iff o 2 Om and vm (o, a) = true,
 – wm |= pNull(o.a) iff o 2 Om and vm (o, a) = f alse,
 – wm |= ¬p iff wm 6|= p, for p 2 P V ,
 – wm |= (lexp ⇠ lexp0 ) iff V⇢ (w(m), lexp) ⇠ V⇢ (wm , lexp0 ) and
           V⇢ (wm , lexp) 6= 1 =6 V⇢ (wm , lexp0 ),
 – wm |= ¬lc iff wm 6|= lc, for lc 2 LC,
 – wm |= ' ^ iff wm |= ' and wm |= ,
 – wm |= ' _ iff wm |= ' or wm |= ,
 – wm |= 'U<k iff (9min(m+k,n)>l m )(wl |= and (8mj<l )wj |= '),
 – wm |= 'R<k iff (8min(m+k,n)>l m ) wl |= ) or
         (9min(m+k,n)>l m )(wl |= ' and (8mjl )wj |= ).
The semantics of the propositions follows their definitions, for the level con-
straints the semantics is based on the valuation function V⇢ , whereas for the
temporal operators the semantics is quite standard. Note that we interpret our
language over finite sequences as the solutions we are dealing with are finite.
    Now, by a temporal query we mean a query (as defined in the former section)
extended with an LT Lk X formula '. The temporal solutions are these solutions
for which the world sequences satisfy '. A temporal plan is an equivalence class
of the temporal solutions, defined over the same multiset of services.


5       Example of Temporal Abstract Planning
This section contains an example showing how the abstract temporal planning
can be used in practice for a given ontology and user (temporal) queries.


                                                               


                                                                                      


                                                      


                                                 


                          



                                                   Fig. 2. Example ontology


    Consider the ontology depicted in Fig. 2. In the Artif act branch one can see
several types of objects, like, e.g., Arbour (the main point of interest of this ex-
ample), which is a subclass of W are, P aintableArtif act, and Construction. At
the left hand side the Service branch and its subclasses are located. The service
Select (St) is able to search any W are, Selling (Sg) allows to purchase it, while
T ransport (T ) can be used to change its location. The P ainting (P ) service
is able to change colour of any P aintableArtif act, but it needs to use some
P aint. The Building (B) service can be used to obtain some Construction, but
66     PNSE’14 – Petri Nets and Software Engineering



it needs BuildingM aterials. Finally, two subclasses of Building are specialized
in production of wooden constructions using the supplied boards and nails. The
services W oodBuilding (W b) and W oodBuildingLux (W bx) are similar, but
the latter also paints the product to the chosen colour using their own paint,
however for a higher price.
     Assume the user wants to get a wooden arbour painted in blue. He formulates
the query as follows: in = inout = ;, pre = true, out = {Arbour a}, post =
(a.colour = blue ^ a.owner = M e ^ a.location = M yAddress). The post
formula is automatically translated to its abstract form, that is (isSet(a.colour)
^ isSet(a.owner) ^ isSet(a.location)). The shortest plans are [St + Sg] and
[St + Sg + T ]. The former satisfies the user query only if the Selling service is
located in a close proximity of the user’s address.
     Assume that during the next planning steps (i.e., the offer collecting and
the concrete planning) those plans turn out to have no realization acceptable
by the user. Perhaps, there are no blue arbours in nearby shops or they are
too expensive. Then, the alternative plan is to buy and transport an arbour
in any colour, as well as some blue paint, and then use the P ainting service:
[2St+2Sg +2T +P ], where one triple of services (St, Sg, T ) provides the arbour,
and the other a blue paint.
     However, it could be the case that, e.g., the transport price of such a big
object like an arbour exceeds the budget. If so, the possible solution is to buy
boards, nails, and paint, transport them to the destination address, then to
assembly the components with an appropriate building service, and paint, finally.
This scenario is covered, for example, by the following plan: [3St + 3Sg + 3T +
W b + P ], where the triples of services (St, Sg, T ) provide and transport boards,
nails, and the paint.
     Although, there are over eight hundred abstract plans of length from 2 to 11
satisfying the above user query, including these with multiple transportations of
the arbour, or painting it several times. In order to restrict the plans to more
specific ones, the user can refine the query demanding of specific types of ser-
vices to be present in the plan using stamps. Thus, for example, by adding the
followingVset of stamps to out: {Stamp t1 , Stamp t2 , Stamp t3 } and extending
post by: i=1..3 (ti .serviceClass instanceOf T ransport), the number of possible
abstract plans (of length from 2 to 11) can be reduced below two hundred. Then,
if instead of buying a final product the user wants to buy and transport the com-
ponents, in order to build and paint the arbour, he can add two more stamps and
conditions to the query. That is, by adding to out the set {Stamp b, Stamp p},
and by extending post by the expression (^ b.serviceClass instanceOf Building
^ t3 .serviceClass instanceOf P ainting), one can reduce the number of result-
ing plans to 2 only: [3St + 3Sg + 3T + W b + P ] and [3St + 3Sg + 3T + W bx + P ].
     However, even 2 abstract plans only can be realized in a number of different
ways, due to possible many transformation contexts, and the number of different
partial orders represented by a single abstract plan. If the user wants to further
reduce the number of possible plan realizations by interfering with an order of
services, he should specify some temporal restrictions. For example, if the user
      A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning              67



wants to ensure that all the transports are executed before the building starts,
he can express it as a formula:

      '1 = F (b.level > t1 .level) ^ (b.level > t2 .level) ^ (b.level > t3 .level))

    Moreover, if the intention of the user is to proceed with some service directly
after another one, for example, to start building just after the third transport,
one can express such a constraint as:

                            '2 = F(b.level = t3 .level + 1)

   Moreover, using a temporal query the user can prevent some services from
occurring in the plan. For example, using the following formula:

                         '3 = ¬pEx(a) U pNull(a.colour),

which means that just after the arbour has been produced, its colour is not set,
the user excludes the W oodBuildingLux service (which builds and paints the
arbour).
    The other possibility of extending the user query by a temporal component
includes using the k-restricted versions of modal operators. For example, consider
the following formula:

                    '4 = F<10 (pEx(t1 ) ^ pEx(t2 ) ^ pEx(t3 )),

which states that three transportations should be executed in the first nine steps
of the plan.


6     Implementation, Experiments, and Conclusions

In this section we sketch the implementation of the propositions and the level
constraints, and then we evaluate the efficiency of our tool using several scalable
benchmarks.


6.1    Implementation

The implementation of the propositions and the level constraints exploits our
symbolic representation of world sequences. The objects and the worlds are rep-
resented by sets of variables, which are first allocated in the memory of an
SMT-solver, and then used to build formulas mentioned in Section 4. The rep-
resentation of an object is called a symbolic object. It consists of an integer
variable representing the type of an object, called a type variable, and a number
of Boolean variables to represent the object attributes, called the attribute vari-
ables. In order to represent all types and identifiers as numbers, we introduce a
function num : A [ P [ S [ O 7 ! N, which with every attribute, object type,
service type, and object assigns a natural number.
68      PNSE’14 – Petri Nets and Software Engineering



   A symbolic world consists of a number of symbolic objects. Each symbolic
world is indexed by a natural number from 0 to n. Formally, the i-th symbolic
object from the j-th symbolic world is a tuple: oi,j = (ti,j , ai,0,j , ..., ai,maxat 1,j ),
where ti,j is the type variable, ai,x,j is the attribute variable for 0  x < maxat ,
where maxat is the maximal number of the attribute variables needed to repre-
sent the object.


                    Initial                                                       Final            Expected
                     w0                  w1                w2                      wn                we
                     o0,0                o0,1              o0,2
                                                            0,1
                                                                                  o0,n
                                                                                   0,1
                                                                                                     o0,e
              inq
                     o1,0                o1,1              o1,2                   o1,n               o1,e     outq
                                s1               s2         1,1 ... s              1,1
                                                                     n
                                                                                                     o2,e
                     o2,0                o2,1              o2,2                   o2,n
           inoutq    o3,0                o3,1              o3,2                   o3,n      m0,e
                     o4,0                o4,1              o4,2                   o4,n
                                                                                            m1,e
                                         o5,1              o5,2                   o5,n
                               outs
                                     1
                                         o6,1              o6,2                   o6,n
                                                           o7,2                   o7,n      m2,e
                                                outs
                                                       2
                                                           o8,2                   o8,n
                                                                                    ...
                                                                  outs ...s
                                                                       1      n
                                                                                  ox-1,n
                                                                                  ox,n


                    Fig. 3. Symbolic worlds of a transformation sequence


    Note that actually a symbolic world represents a set of worlds, and only
a valuation of its variables makes it a single world. The j-th symbolic world
is denoted by wj , while the number of the symbolic objects in wj - by |wj |.
                                                         q
Note that the set of the initial worlds of the query q (Winit ) is represented by a
symbolic world w0 . Fig. 3 shows subsequent symbolic worlds of a transformation
sequence.
    One of the important features of our encoding is that for a given index of a
symbolic object i we are able to determine the step of a solution, in which the
object was produced. This is done by the function levq : N 7! N, such that for a
given query q:                 (
                                                0 for i < |w0 |
                              levq (i) =              |w0 |)                                                         (2)
                                                b (imax out
                                                             c + 1 for i                   |w0 |

where maxout is the maximal number of the objects produced by a single service.
   Another important feature of our encoding is that the objects of outq need
to be identified among the objects of the symbolic world wn (of indices greater
than |w0 |). To this aim, we allocate a new symbolic world we (with e = n + 1),
containing all the objects from outq . Note that the world we is not a part of a
     A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning             69



world solution, but it provides a set of additional, helper variables. Finally, we
need a mapping between the objects from a final world wn produced during the
subsequent transformations and the objects from we . To this aim we allocate p
additional mapping variables in the symbolic world we , where p = |outq |. These
variables, denoted by m0,e , . . . , mp 1,e , are intended to store the indices of the
objects from a final world, which are compatible with the objects encoded over
we . Thus, we encode the state of the expected worlds of the query q (Wexp        q
                                                                                     ),
imposed by postq , using two sets of symbolic objects. The objects of inq [ inoutq
are encoded directly over the (final) symbolic world wn . The state of the ob-
jects from outq are encoded over we , and since their indices are not known, all
possible mappings between objects from we and wn are considered, by encoding
a disjunction of equalities between objects from we and wn . See [18] for more
details.
    The translation of the propositions defined over the objects and their at-
tributes of a user query q in a symbolic world wm (0  m  n) is as follows:
                     8
                     <true, for o 2 inq [ inoutq ,
                     >
                   m
           [pEx(o)] = f alse, for o 2 outq , m = 0,                                (3)
                     >
                     :
                       levq (mnum(o),e )  m, for o 2 outq , m > 0.

That is, the objects from the initial world exist in all the subsequent worlds, the
objects from the out set do not exist in the world w0 , and they appear in some
subsequent world. Then, since the index of the object o is stored as the value of
corresponding mapping variable mnum(o),e , we can determine if it exists in the
world wm using the levq function.
    The proposition pSet(o.a) is encoded over the symbolic world wm as:
                                (
              m            m      aj,x,m , for o 2 inq [ outq ,
  [pSet(o.a)] = [pEx(o)] ^ W|wm | 1                                             (4)
                                    i=|w0 | (mj,e = i ^ ai,x,m ), for o 2 outq


where j = num(o) and x = num(a).
    It follows from our symbolic representation that the indices of objects from
an initial world are known, and we can get the value of the appropriate attribute
variable directly. However, in the case of objects from outq we have to consider
all possible mappings between objects from we and wm . Note that the encoding
of the proposition pNull(o.a) over the symbolic world wm (i.e., [pNull(o.a)]m )
is very similar. The only change is the negation of ai,x,m in the above formula.
    In order to encode the level constraints, we introduce a set of the special level
variables. That is, for every stamp s used in some level constraint we introduce
to the world we an additional integer variable li,e , where i = num(s), intended
to store the level value of the stamp s. The level value is assigned to li,e using
the following formula [bind(i)] := (li,e = levq (mi,e )) for i = num(s), where q
is a user query. Then, for every stamp s used in a level constraint we add the
corresponding [bind(num(s))] formula as an SMT assertion. Thus, the encoding
of the level constraints is as follows:
70        PNSE’14 – Petri Nets and Software Engineering




                       8
                       <c for lexp = c
                       >
               [lexp] = li,e , for lexp = s.level, i = num(s)                            (5)
                       >
                       :
                         [lexp0 ] [lexp00 ] for lexp = lexp0          lexp   00


    The encoding of arithmetic operators is straightforward, since they are sup-
ported by theories built in SMT-solvers, like, e.g., Linear Integer Arithmetic or
Bitvector theory. In what follows, [']m
                                      n denotes the translation of the formula '
at the state wm of the world sequence of length n + 1.

Definition 10 (Translation of the LT Lk X formulae to SMT). Let ' be an
LT Lk X formula, (w0 , . . . , wn ) be a sequence of symbolic worlds, and 0  m  n.
         m
    • [p]n := [p]m , for p 2 P V ,
          m
    • [¬p]n := ¬[p]m , for p 2 P V ,             V
    • [lexp0 ⇠ lexp00 ]m     [lexp0 ] ⇠ [lexp00 ] s2st(lexp0 ) [pEx(s)]m
                        n := V
                               s2st(lexp00 ) [pEx(s)] ,
                                                     m
           m
    • [¬lc]n := ¬[lc]n , for lc 2 LC,
                       m
             m         m       m
    • [' ^ ]n := [']n ^ [ ]n ,
             m         m       m
    • [' _ ]n := [']n _ [ ]n ,
               m      W min(m+k,n)            Vi 1
    • ['U<k ]n := i=m              ([ ]in ^ j=m [']jn ),
               m      Vmin(m+k,n) i Wmin(m+k,n)                   Vi
    • ['R<k ]n := i=m              [ ]n _ i=m            ([']in ^ j=m [ ]jn ),

where st(lexp) returns the set of the stamps over which the expression lexp is
built.

Theorem 1. The encoding of the temporal query is correct.

Proof. This can be shown by induction on the length of a formula. Omitted here
because of lack of space3 .

6.2      Experimental Results
In order to evaluate the efficiency of our approach we performed several exper-
iments using standard PC with 2GHz CPU and 8GB RAM, and Z3 [7] ver-
sion 4.3 as an SMT-solver. The results are summarized in Table 1. Using our
Ontology Generator (OG) we generated 15 ontologies, each of them consist-
ing of 150 object types and from 64 to 256 service types (the column named
n of Tab. 1). For each ontology a query has been generated in such a way
that it is satisfied by exactly 10 plans of length from 6 to 18 (the parameter
k). The queries demand at least two objects to be produced, and impose re-
strictions on (abstract) values of some of their attributes. A generated query
example is as follows: in = {Rjlbp rjlbp1}, inout = {Bozwd bozwd1}, out =
{Opuf o opuf o1, Ehxjb ehxjb2}, pre = isSet(bozwd1.avg) ^ isSet(rjlbp1.ppw),
3
     The full version of this paper is available at http://artur.ii.uph.edu.pl/pnse14ltl.pdf.
     A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning                                              71



post = isSet(opuf o1.epv) ^ isN ull(bozwd1.dyn) ^ isSet(ehxjb2.zdv) ^
isN ull(ehxjb2.rxz) ^ isSet(bozwd1.f sl).
    First, we ran our planner for each ontology and each query instance without
a temporal query (column 1 ), in order to collect statistics concerning the time
needed to find the first plan (P1 ), all 10 plans (P10 ), as well as the total time
(column T) and the memory consumed (M) by the SMT-solver in order to find
all the plans and checking that no more plans of length k exist. We imposed the
time limit of 1000 seconds for the SMT-solver. Each time-out is reported in the
table by T O. It is easy to observe that during these experiments as many as 9
instances ran out of time.

                                  Table 1. Experimental results


          1 = true                              3                            4                            5
 n   k P1 P10 T M                  P1 P10 T               M      P1 P10 T              M      P1 P10 T              M
         [s]   [s]   [s]   [MB]    [s]    [s]       [s]   [MB]   [s]   [s]       [s]   [MB]   [s]   [s]       [s]   [MB]

     6 7.23 9.73 19.5 19.7 2.34 7.17 8.49 14.1 2.19 4.14 4.21 11.6 3.51 4.7 6.48 10.8
     9 23.5 53.1 177 173 20.1 34.5 47.0 38.3 15.9 18.8 19.2 22.3 14.8 40.1 44.7 36.0
 64 12 165 479 TO        - 101 216 354 117 60.5 85.2 87.6 59.3 95.1 122 127 68.1
    15 305 TO TO         - 329 762 TO        - 119 216 241 105 195 345 351 129
    18 TO TO TO          - TO TO TO          - 461 TO TO         - 604 TO TO -
     6 16.0 28.1 55.7 42.7 9.75 19.8 22.6 21.3 7.68 10.1 10.2 16.8 10.9 12.7 15.1 16.3
     9 53.1 94.9 270 250 55.5 98.2 104 44.7 21.8 34.0 34.2 31.0 38.1 54.7 62.6 44.9
128 12 136 677 TO        - 134 428 474 96.3 76.8 99.9 102 61.9 93.1 114 117 47.9
    15 TO TO TO          - 456 780 TO        - 116 199 202 86 183 258 263 79.8
    18 TO TO TO          - TO TO TO          - 381 556 573 143 383 708 714 130
     6 16.1 30.6 41.5 35.4 20.3 25.7 30.0 26.1 11.1 13.9 14.1 21.7 14.9 18.3 21 21.6
     9 84.4 137 374 466 63.7 99.3 131 53.4 26.2 38.4 39.1 37.5 88.5 119 156 74.9
256 12 267 TO TO         - 242 584 692 112 114 181 183 80.6 250 315 321 73.4
    15 685 TO TO         - 562 TO TO         - 198 304 309 86.8 472 582 592 120
    18 TO TO TO          - TO TO TO          - 574 919 937 137 942 TO TO -




    The next experiments involve temporal queries using level constraints. To
this aim we extended the out set of the generated queries by the appropriate
stamp set. Moreover, the post formulas of the queries have been also extended
                     Vb k2 c
with the expression: i=1     (si .serviceClass instanceOf Ci ), where si 2 ST, while
Ci 2 S are service types occurring in the solutions generated by OG.
    Our second group of experiments involved the temporal formula 2 :
                                         bk
                                          2c 1
                                          ^
                             2 = F(                 si .level < si+1 .level),
                                          i=1

which expresses that about a half of the stamps being effects of the solution
execution, should be produced in the given order. We do not present detailed
72     PNSE’14 – Petri Nets and Software Engineering



results, because they are in general comparable with the performance in the for-
mer experiments. Similarly, there are 9 time-outs, but the time and the memory
consumption varies a bit - for some cases the results are slightly better, while
for others are a little worse.
    In the third group of the experiments we imposed stronger restrictions on
the possible service orders of the solutions using the following formula:
                                     bk
                                      2c
                                     ^
                            3 = F(         si .level < i + 2).
                                     i=1

This formula still leaves a certain degree of freedom in a service ordering, how-
ever its encoding as an SMT-instance is more compact, since the constant values
are introduced in place of some level variables. Thus, probably, it is also easier
to solve. The results are summarized in the column 3 in Table 1. It is easy to
observe that the time and the memory consumption is significantly lower. More-
over, the number of time-outs dropped to 6. Thus, this is an example showing
an improvement in the planning efficiency using a temporal query.
    Our next experiment involves the formula 4 specifying the strict ordering
of several services in the solution using stamp-based level constraints:
                                       bk
                                        2c
                                       ^
                              4 = F(         si .level = i).
                                       i=1

The analysis of the results (given in the column 4 of Table 1) indicates a
dramatic improvement of our planner efficiency, in terms of time and memory
consumption by the SMT-solver. Moreover, in this experiments group the plan-
ner has been able to terminate its computations in the given time limit for all
but one instances.
    Finally, we want to confront the planner behaviour with other kind of tem-
poral formulae. Using the Until modality, we demand that one of the objects
from outq has to be produced no later than in the middle of the plan. Moreover,
knowing the structure of the generated queries, we impose that after the object
appears one of its attributes should already be set. This is expressed by the
following formula:
                         5 = ¬pEx(o) U<d k e pSet(o.a)
                                                 2

where o 2 outq , a 2 attr(o), and the expression isSet(o.a) is not contradictory
with postq . The results has been summarised in column 5 of Table 1. It is easy
to observe that also this time the plans have been found faster and using less
memory than in the case when no temporal formula is involved.


7    Conclusions
In this paper we have applied the logic LT Lk X to specifying temporal queries
for temporal planning within our tool Planics. This is a quite natural extension
     A. Niewiadomski, W. Penczek.: SMT-based Abstract Temporal Planning             73



of our web service composition system, in which the user gets an opportunity to
specify more requirements on plans. These requirements are not only declarative
any more. The overall conclusion is that the more restrictive temporal query,
the more efficient planning, given the same ontology. Assuming that the more
restrictive temporal queries, the longer formulas expressing them, the above
conclusion shows a difference with model checking, where the complexity depends
exponentially on the length of an LT Lk X formula.
    Our temporal planner is the first step towards giving the user even more
freedom by defining a so-called parametric approach. We aim at having a planner
which in addition to the current capabilities, could also suggest what extensions
to the ontology or services should be made in order to get better or unrealizable
plans so far. This is going to be a subject of our next paper.


References
 1. S. Ambroszkiewicz. Entish: A language for describing data processing in open
    distributed systems. Fundam. Inform., 60(1-4):41–66, 2004.
 2. M. Bell. Introduction to Service-Oriented Modeling. John Wiley & Sons, 2008.
 3. J. Bentahar, H. Yahyaoui, M. Kova, and Z. Maamar. Symbolic model checking
    composite web services using operational and control behaviors. Expert Systems
    with Applications, 40(2):508 – 522, 2013.
 4. L. Bentakouk, P. Poizat, and F. Zaidi. Checking the behavioral conformance of
    web services with symbolic testing and an SMT solver. In Tests and Proofs, volume
    6706 of LNCS, pages 33–50. Springer, 2011.
 5. M. M. Bersani, L. Cavallaro, A. Frigeri, M. Pradella, and M. Rossi. SMT-based
    verification of LTL specification with integer constraints and its application to
    runtime checking of service substitutability. In SEFM, pages 244–254, 2010.
 6. V. Chifu, I. Salomie, and E. St. Chifu. Fluent calculus-based web service composi-
    tion - from OWL-S to fluent calculus. In Proc. of the 4th Int. Conf. on Intelligent
    Computer Communication and Processing, pages 161 –168, 2008.
 7. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. of TACAS’08,
    volume 4963 of LNCS, pages 337–340. Springer-Verlag, 2008.
 8. D. Doliwa, W. Horzelski, M. Jarocki, A. Niewiadomski, W. Penczek, A. Półrola,
    and J. Skaruz. HarmonICS - a tool for composing medical services. In ZEUS,
    pages 25–33, 2012.
 9. D. Doliwa, W. Horzelski, M. Jarocki, A. Niewiadomski, W. Penczek, A. Półrola,
    M. Szreter, and A. Zbrzezny. PlanICS - a web service compositon toolset. Fundam.
    Inform., 112(1):47–71, 2011.
10. M. Elwakil, Z. Yang, L. Wang, and Q. Chen. Message race detection for web ser-
    vices by an SMT-based analysis. In Proc. of the 7th Int. Conference on Autonomic
    and Trusted Computing, ATC’10, pages 182–194. Springer, 2010.
11. V. Gehlot and K. Edupuganti. Use of colored Petri nets to model, analyze, and
    evaluate service composition and orchestration. In System Sciences, 2009. HICSS
    ’09., pages 1 –8, jan. 2009.
12. A. E. Gerevini, P. Haslum, D. Long, A. Saetti, and Y. Dimopoulos. Deterministic
    planning in the fifth international planning competition: PDDL3 and experimen-
    tal evaluation of the planners. Artificial Intelligence, 173(5–6):619 – 668, 2009.
    Advances in Automated Plan Generation.
74      PNSE’14 – Petri Nets and Software Engineering



13. S. Hao and L. Zhang. Dynamic web services composition based on linear tem-
    poral logic. In Information Science and Management Engineering (ISME), 2010
    International Conference of, volume 1, pages 362–365, Aug 2010.
14. Z. Li, L. O’Brien, J. Keung, and X. Xu. Effort-oriented classification matrix of web
    service composition. In Proc. of the Fifth International Conference on Internet and
    Web Applications and Services, pages 357–362, 2010.
15. G. Monakova, O. Kopp, F. Leymann, S. Moser, and K. Schäfers. Verifying business
    rules using an SMT solver for BPEL processes. In BPSC, pages 81–94, 2009.
16. W. Nam, H. Kil, and D. Lee. Type-aware web service composition using boolean
    satisfiability solver. In Proc. of the CEC’08 and EEE’08, pages 331–334, 2008.
17. A. Niewiadomski and W. Penczek. Towards SMT-based Abstract Planning in Plan-
    ICS Ontology. In Proc. of KEOD 2013 – International Conference on Knowledge
    Engineering and Ontology Development, pages 123–131, September 2013.
18. A. Niewiadomski, W. Penczek, and A. Półrola. Abstract Planning in PlanICS
    Ontology. An SMT-based Approach. Technical Report 1027, ICS PAS, 2012.
19. OWL 2 web ontology language document overview. http://www.w3.org/TR/owl2-
    overwiew/, 2009.
20. J. Rao, P. Küngas, and M. Matskin. Composition of semantic web services using
    linear logic theorem proving. Inf. Syst., 31(4):340–360, June 2006.
21. J. Rao and X. Su. A survey of automated web service composition methods. In
    Proc. of SWSWPC’04, volume 3387 of LNCS, pages 43–54. Springer, 2004.
22. J. Skaruz, A. Niewiadomski, and W. Penczek. Automated abstract planning with
    use of genetic algorithms. In GECCO (Companion), pages 129–130, 2013.
23. P. Traverso and M. Pistore. Automated composition of semantic web services into
    executable processes. In The Semantic Web – ISWC 2004, volume 3298 of LNCS,
    pages 380–394. 2004.

</pre>