Joint achievement of services’ personal goals Matteo Baldoni, Cristina Baroglio, Elisa Marengo, Viviana Patti, Claudio Schifanella Dipartimento di Informatica — Università degli Studi di Torino c.so Svizzera, 185, I-10149 Torino, Italy Email: {baldoni, baroglio, emarengo, patti, schi}@di.unito.it Abstract—Web service specifications can be quite complex, none of them alone can accomplish. Semantic annotations including various operations and message exchange patterns. In alone are not sufficient in this case; it becomes useful to this work, we give a rule-based declarative representation of introduce a notion of goal [6], [7], [8], which can be used services, and in particular of WSDL operations, that enables the application of techniques for reasoning about actions and change, to guide both the selection and the composition of services. that are typical of agent systems. This makes it possible to reason The introduction of goals opens the way to the introduction on a rule-based specification of choreography roles and about the of another abstraction, that of agent. Agents include not only selection of possible role players on a goal-driven basis, and allows the ability of dealing with goals and of performing goal- us to attack the problem of the joint achievement of individual driven forms of reasoning, but they also show autonomy and goals for a set of services which animate a choreography. proactivity, which are characteristics that help when dealing I. I NTRODUCTION with open environments, allowing for instance a greater fault tolerance (see [9], [10], [11]). Declarative languages are becoming very important in the In this work, we take the perspective of a candidate role Semantic Web, since the focus started to shift from the player, willing to take part to an interaction, that is ruled ontology layer to the logic layer, with a consequent need of by a choreography. We see such an entity as an enhanced expressing rules and of applying various forms of reasoning1 , (proactive) service, made of a declarative description of its an interest also witnessed by the creation of a W3C working behavior, of the operations that it can execute, of its goals [7], group to define a Rule Interchange Format2 . Particularly and with the capability of reasoning (on its own behavior) so challenging applications concern web services. to build orchestations that allow the achievement of its goals One of the key ideas behind web services is that services (proactiveness). So, for instance, a service that wishes to play should be amenable to automatic retrieval, thus facilitating the role of the “Seller” of a ticket-purchase choreography may their re-use. Nevertheless, retrieval cannot yet be accomplished have the aim of “selling tickets”, guaranteed by playing the automatically as well and as precisely as desired because choreography role, and have the additional, private goal of the current web service representations (mainly WSDL [1] “loyalizing clients”. Notice that personal goals may vary along and BPEL [2]) and the discovery mechanisms are seman- time, hence, different participations (to the same choreography tically poor and lack of sufficient flexibility. As shown by of a same agent as player of the same role) may be character- the framework presented in this paper, rule-based declarative ized by different personal goals. For example, the flight ticket languages, and the reasoning techniques that they support, selling service may change at some point its personal goal, supply both an expressive formal semantics and flexibility in which becomes the “promotion of additional services” offered the accomplishment of the service selection task. by the same company. The presence of additional goals, which The need of adding a semantic layer to service descriptions may not be disclosed to the interacting parties, biases the is not new. Some approaches, e.g. OWL-S [3] and WSMO behavior and the choices of a service. A service will take [4], propose a richer annotation, aimed at representing inputs, on a role only after checking the possible achievement of this outputs, preconditions and effects of the service. Inputs and final condition. outputs are usually expressed by ontological terms, while Orchestrations compose the interactions of sets of services. preconditions and effects are often expressed by means of However, reasoning on the goals of the orchestrator alone is logic representations. Preconditions and effects are also used not sufficient. Indeed, in the context of choreographies that in design by contract, originally introduced by Meyer for the provide a pattern of interaction among services, each service EiffelT M language [5]. Here preconditions are the part of involved has its own goals, that it tries to pursue. The research the contract which is to be guaranteed by the client; if this question is: even though each service has proved that there condition is guaranteed in the execution context of a method, is a possible way of playing its role, which leads to the then the server commits to guaranteeing that the postcondition achievement of its personal goal, is it possible to guarantee holds in the state reached by the execution. the compatibility of these individual solutions? In other words, On the other hand, there is often the need of using services will the joint working plan, made of the identified individual not in an individual way but jointly, for executing tasks that solutions, allow the joint achievement of all the goals of the 1 REWERSE NoE, http://rewerse.net interacting parties? A ticket selling service that wants to do 2 http://www.w3.org/2005/rules/wiki/RIF_Working_Group some advertisement by sending a newsletter to its clients will not match the aims of a client which considers this kind of unknown fluents, we use an epistemic operator B, to represent information as spam. the beliefs an entity has about the world: Bf means that the In this paper we describe the first steps of a study about fluent f is known to be true, B¬f means that the fluent f is the joint achievement of goals of a set of services, whose known to be false. A fluent f is undefined when both ¬Bf interaction is ruled by a choreography. The approach relies and ¬B¬f hold (¬Bf ∧ ¬B¬f ). Thus each fluent in a state on a rule-based declarative representation of the choreography can have one of the three values: true, false or unknown. For roles and of the interacting services, which extends and the sake of readability, we will add as a superscript of B the refines the work in [8], [12], [13], exploiting the results about name of the service that has the belief. conservative matching defined in there. The framework enables Services exhibit interfaces, called port-types, which make a the application of techniques for reasoning on the effects of set of operations available to possible clients. In our proposal, playing a role in a choreography, thus checking whether the a service description is defined as a pair hO, Pi, where O desired personal goal can be accomplished. The representation is a set of basic operations, and P (policy) is a description is based on the logic programming language described in of the complex behavior of the service. Analogously to what [14], [15]. Behaviors, as roles and service policies, build upon happens for OWL-S composite processes, P is built upon basic WSDL-like basic operations, represented as atomic actions operations and tests, that control the flow of execution. with preconditions and effects. The paper is organized as follows. Section II sets the A. Basic operations representation of services and of choreographies that we adopt. Let us start with basic operations. According to the main Moreover, it explains how it is possible to reason on such languages for representing web services, like WSDL and a representation in order to allow each service to check OWL-S, there are four basic kinds of operations [17] (or the reachability of its goals locally, i.e. by using only the atomic processes, when using OWL-S terminology [3]): specification of the desired choreography role. Section III • one-way involves a single message exchange, a client tackles the joint achievement of personal goals. A running invokes an operation by sending a message to the service; example is distributed along the pages to better explain the • notify involves a single message exchange, the client proposed notions and mechanisms. Conclusions end the paper. receives a message from the service; • request-response involves the exchange of two messages, II. A THEORETICAL FRAMEWORK FOR REPRESENTING AND REASONING ABOUT SERVICES are initiated by the invoker of the operation, which sends a message to the service and, after that, waits for a In this section, we introduce the notation that we use to response; represent services and we discuss the problem of verifying • solicit-response involves the exchange of two messages, a personal goal. The notation, which is a refinement of the the order of the messages is inverted w.r.t. a request- proposal in [13], is based on a logical theory for reasoning response, first the invoker waits for a message from the about actions and change in a modal logic programming service and then it sends an answer. setting and on the language DYnamics in LOGic, described A basic operation is described in terms of its executability in details in [14]. This language is designed for specifying preconditions and effects, the former being a set of fluents agents behaviour and for modeling dynamic systems. It is (introduced by the keyword possible if) which must be con- fully set inside the logic programming paradigm by defining tained in the service state in order for the operation to be programs by sets of Horn-like rules and giving a SLD-style applicable, the latter being a set of fluents (introduced by the proof procedure. The capability of reasoning about interaction keyword causes) which will be added to the service state after protocols, supported by the language, has already been ex- the operation execution. Syntax for basic operations is: ploited for customizing web service selection and composition w.r.t. to the user’s constraints, based on a semantic description operation(content) causes Es (1) of the services [14]. The language is based on a modal theory operation(content) possible if Ps (2) of actions and mental attitudes where modalities are used for representing primitive and complex actions as well as the agent where Es and Ps , denote respectively the fluents, which are beliefs. Complex actions are defined by inclusion axioms [16] expected as effect of the execution of an operation and the and by making use of action operators from dynamic logic, precondition to its execution, while content denotes possible like sequence “;” and test “?”. additional data that is required by the operation. Notice that In this framework, the problem of reasoning amounts either such operations can also be implemented as invocations to to build or to traverse a sequence of transitions between states. other services. A state is a set of fluents, i.e., properties whose truth value can Operations, when executed, trigger a revision process on change over time, due to the application of actions. In general, the actor’s beliefs. Since we describe web services from a we cannot assume that the value of each fluent in a state is subjective point of view, we distinguish between the case when known: we want to have both the possibility of representing the service is either the initiator (the operation invoker) or unknown fluents and the ability of reasoning about the exe- the servant of an operation (the operation supplier) by further cution of actions on incomplete states. To explicitly represent decorating the operation name with a notation inspired by [18]. The two views are complementary, so if one view includes the act of sending a message, the other correspondingly includes a message reception. With reference to a specific service, operation≫ denotes the operation from the point of view of the invoker, while operation≪ denotes the operation from the point of view of the supplier. The view of operations that is used by invoker is given in terms of the operation inputs, outputs, preconditions, and effects as usual for semantic web services [3]. In the next part of this section, inputs and outputs are represented as single messages for simplicity but Fig. 1. The request-response basic operation. the representation can easily be extended to sets of exchanged data, as in Example (II-C). In this case, preconditions Ps in (2) and effects Es in (1) are respectively the conditions required current state (a). The execution of the invocation brings about by the operation in order to be invoked, and the expected the effects Es (c), and the invoker will know the received in- effects that result from the execution of the operation. For formation (b). Using OWL-S terminology, mout represents the what concerns the view of the supplier, also in this case output of the operation, while Ps and Es are its preconditions the operation is described in terms of its inputs and outputs. and effects. Notify operations have no input. The supplier must Moreover, we also represent a set of conditions that enable meet the requirements Rs (e). The execution of the operation the executability of the operation. In order to distinguish them simply causes the fact that the supplier will know the message from the above, in this case we use Rs instead of Ps in to send (f) and that it has sent some information to the invoker (2), calling them requirements. Finally, we represent a set of (g). As above, we allow the possibility of having some side conditions that constitute the side effects of the operation. In effects on the supplier’s state (h). this case we use Ss instead of Es in (1). For example, a buy 3) Request-response: In request-response operations (see operation of a selling service has as a precondition the fact Figure 1), the invoker requests an execution which involves that the invoker has a valid credit card, as inputs the credit sending an information min (the input, according to OWL- card number of the buyer and its expiration date, as output it S terminology) and then receiving an answer mout from the generates a receipt, and as effect the credit card is charged. supplier (the output in OWL-S). The invoker can execute From the point of view of the supplier, the requirement to the the operation only if the preconditions Ps are satisfied in execution is to have an active connection to the bank, and the its current state and if it owns the information to send (a) side effect is that the store availability is decreased while the (see Table I). The execution of the invocation brings about service bank account is increased of the perceived amount. the effects Es (d), and the fact that the invoker knows that Let us now introduce the formal representation of the four it has sent the input min to the supplier (b). One further kinds of basic operations (for each operation we report both effect of the execution is that the invoker knows the answer views) and of complex operations. returned by the operation (c). This representation abstracts 1) One-way: In one-way operations, the invoker requests away from the actual message exchange mechanism, which an execution which involves sending an information min to is implemented. Our aim is to reason on the effects of the the supplier; the invoker must obviously know the information execution on the mental state of the parties [15]. As for one- to send before the invocation (a) (see Table I). The invoker can way operations, the supplier has the requirements Rs to the execute the operation only if the preconditions are satisfied in operation execution (e). It receives an input min from the its current state (a). The execution of the invocation brings invoker (f). The execution produces an answer mout (g), which about the effects Es (c), and the invoker will know that it is sent to the invoker (h). As usual, it is possible to have has sent an information to the supplier (b). Using OWL- some side effects on the supplier’s state. On the supplier’s S terminology, min represents the input of the operation, side, we can notice more evidently the abstraction of the while Ps and Es are its preconditions and effects. One-way representation from the actual execution process. In fact, we operations have no output. On the other hand, the supplier, do not model how the answer is produced but only the fact which exhibits the one-way operation as one of the services that it is produced. that it can execute, has the requirements Rs (e). The execution 4) Solicit-response: With ref. to Table I, in solicit-response of the operation causes the supplier to know the information operations, the invoker requests an execution which involves sent by the invoker (f). We also allow the possibility of having receiving an information mout (the output, according to OWL- some side effects on the supplier’s state. These effects are not S terminology) and then sending a message min to the supplier to be confused with the operation effects described by IOPE, (the input in OWL-S). The invoker can execute the invocation and have been added for the sake of completeness. only if the preconditions Ps are satisfied in its current state 2) Notify: With ref. to Table I, in notify operations, the (a). The execution of the invocation brings about the effects invoker requests an execution which involves receiving an Es (e). The invoker receives a message mout from the supplier information mout from the supplier. The invoker can execute (b) then, it produces the input information min which is sent the operation only if the preconditions are satisfied in its to the supplier, see (c) and (d). As for notify operations, the Operation Invoker’s view Supplier’s view (a) operation≫ Invoker m (e) operation≪ One-Way ow (min ) possible if B in ∧ Ps ow (min ) possible if Rs (b) operation≫ (m ) Invoker sent(m ) (f) operation≪ Supplier m ow in causes B in ow (min ) causes B in (c) operation≫ ow (min ) causes Es (g) operation≪ ow (min ) causes Ss Notify (a) operation≫ n (mout ) possible if Ps (e) operation≪ n (mout ) possible if Rs (b) operation≫ Invoker m (f) operation≪ Supplier m n (mout ) causes B out n (mout ) causes B out (c) operation≫ (m ) (g) operation≪ (m ) Supplier sent(m n out causes E s n out causes B out ) (h) operation≪ n (mout ) causes Ss (a) operation≫ Invoker m (e) operation≪ Request- rr (min , mout ) possible if B in ∧ Ps rr (min , mout ) possible if Rs (b) operation≫ (m ) Invoker sent(m ) (f) operation≪ Supplier m response rr in , mout causes B in rr (min , mout ) causes B in (c) operation≫ Invoker m (g) operation≪ Supplier m rr (min , mout ) causes B out rr (min , mout ) causes B out (d) operation≫ (h) operation≪ Supplier sent(m rr (min , mout ) causes Es rr (min , mout ) causes B out ) ≪ (i) operationrr (min , mout ) causes Ss Solicit- (a) operation≫ sr (min , mout ) possible if Ps (f) operation≪ sr (min , mout ) possible if Rs (b) operation≫ Invoker m (g) operation≪ Supplier m response sr (min , mout ) causes B out sr (min , mout ) causes B out (c) operation≫ Invoker m (h) operation≪ Supplier sent(m sr (min , mout ) causes B in sr (min , mout ) causes B out ) (d) operation≫ Invoker sent(m ) (i) operation≪ Supplier m sr (min , mout ) causes B in sr (min , mout ) causes B in (e) operation≫ sr (min , mout ) causes Es (l) operation≪ sr (min , mout ) causes Ss TABLE I T HE REPRESENTATION OF THE FOUR KINDS OF BASIC OPERATIONS IN THE PROPOSED FRAMEWORK : EACH OPERATION IS GIVEN IN TERMS OF ITS PRECONDITIONS AND EFFECTS , FOR EACH OF THEM WE REPORT BOTH THE INVOKER ’ S VIEW AND THE SUPPLIER ’ S VIEW. supplier must fulfill the requirements Rs (f). The execution causes the supplier to know the information to send (g) and that it has sent such information to the invoker (h). Moreover, it produces also the knowledge of the information min received from the invoker (i). Side effects on the supplier’s state are allowed (l). B. Service policies and choreography roles The framework accounts also for complex behaviors that require the execution of many operations. A service policy P is a collection of clauses of the kind: p0 is p1 , . . . , pn (3) where p0 is the name of the procedure and pi , i = 1, . . . , n, is either an atomic action (operation), a test action (denoted by the symbol ?), or a procedure call. Procedures can be recursive Fig. 2. A simple choreography for reserving a flight, expressed as a UML and are executed in a goal-directed way, similarly to standard sequence diagram. logic programs, and their definitions can be non-deterministic as in Prolog. Complex behaviors are used also for represent- ing choreography roles. Generally speaking, we represent a choreography C as a tuple (R1 , . . . , Rn ) of interacting and complementary roles, each role Ri being a subjective view of the interaction that is encoded. operations are represented as normal basic operations, in Also a role R is represented by a pair hO, Pi. The dif- terms of their preconditions and effects. This is one of the ference with services is that it composes specifications of advantages of adopting a logic language: it allows handling operations and not implemented operations. The player of implementations and specifications in the same way. In our each role has to supply appropriate implementations. We call case, both operations and operation specifications are given in such specifications unbound operations. Formally, unbound terms of their preconditions and effects. C. Flight-purchase it waits for being asked about the preferred flight, chosen As an example, let’s consider searchFlight, an operation of among the flights list obtained by the previous operation a flight reservation service, which is offered by a seller and (askChosenFlight≪ n ). This evaluation can give either a negative can be invoked by a buyer to search information about flights outcome, hence the interaction is interrupted (noBusiness≫ ow ) with given departure (dep) and arrival locations (arr) plus the or the interaction continues with the selection of the payment date of departure (date). From the point of view of the buyer, method (choosePayment≪ rr ). Then, the buyer performs the the operation, which is of kind request-response, is: payment (doPayment≫ rr and, at the end, it is notified about ) the obtained miles (askForMiles≫ n ). (a) searchFlight≫rr ((dep, arr, date), f lightList) possible if Bbuyer dep ∧ Bbuyer arr ∧ Bbuyer date∧ D. Reasoning on goals Bbuyer ¬sellingStarted In the outlined framework, it is possible to reason about (b) searchFlight≫rr ((dep, arr, date), f lightList) causes personal goals by means of queries of the form Fs after p, Bbuyer sent(dep) ∧ Bbuyer sent(arr)∧ where Fs is the goal (represented as a conjunction of fluents), Bbuyer sent(date) that we wish to hold after the execution of a policy p. (c) searchFlight≫rr ((dep, arr, date), f lightList) causes Checking if a formula of this kind holds corresponds to Bbuyer f lightList answering the query: “Is it possible to execute p in such a (d) searchFlight≫rr ((dep, arr, date), f lightList) causes way that the condition Fs is true in the final state?”. When Bbuyer sellingStarted the answer is positive, the reasoning process returns a sequence of atomic actions that allows the achievement of the desired The inputs of the operation are dep, arr, and date, while the condition. This sequence corresponds to an execution trace of output is f lightList. In this case the set Ps contains only the the procedure and can be seen as a plan to bring about the goal belief Bbuyer ¬sellingStarted (in bold text above) while the Fs. This form of reasoning is known as temporal projection. set Es of effects contains the belief Bbuyer sellingStarted (in Temporal projection fits our needs because, as mentioned in bold text as well). the introduction, in order to perform the selection we need From the point of view of the supplier, instead, the operation a mechanism that verifies if a goal condition holds after the is represented as: interaction with the service has taken place. Fs is the set of (a) searchFlight≪ facts that we would like to hold “after” p. rr ((dep, arr, date), f lightList) possible if true Reasoning is done by exploiting a goal-directed proof (b) searchFlight≪ procedure (denoted by “⊢” in the following) designed for rr ((dep, arr, date), f lightList) causes Bseller dep ∧ Bseller arr ∧ Bseller date the language DYnamics in LOGic [15], [14], which supports (c) searchFlight≪ both temporal projection and planning and allows the proof of rr ((dep, arr, date), f lightList) causes Bseller f lightList existential queries of the kind reported above. The procedure (d) searchFlight≪ definition constrains the search space. In particular, for what rr ((dep, arr, date), f lightList) causes Bseller sent(f lightList) concerns planning, the proof procedure allows the automatic extraction of linear or conditional plans for achieving the goal In this case the sets Rs and Ss of requirements and side effects of interest from an incompletely specified initial state. are empty. The operation expects as input the departure and Let hO, Pi be a service description. The application of arrival locations and the date of the flight, and it produces temporal projection to P returns, if any, an execution trace a f lightList, which it sends to its customer, so after the (a linear plan), that makes a goal of interest become true. Let operation the belief Bseller sent(f lightList) will be in its us, then, consider a procedure p belonging to P and denoting belief state. its top level, and denote by Q the query Fs after p. Given buyTicket is, instead, an example of procedure implemented a state s0 , containing all the fluents that we know as being by a possible buyer service: true in the beginning, we denote the fact that the query Q is successful in the service description by (hO, Pi, s0 ) ⊢ Q. (a) buyTicket is The execution of the above query returns as a side-effect an searchFlight≫ rr ((dep, arr, date), f lightList); execution trace σ of p; the execution trace σ is a sequence askChosenFlight≪ n (f light); a1 , . . . , an of atomic actions. We denote this by: evaluateAndBuy. (b) evaluateAndBuy is (hO, Pi, s0 ) ⊢ Q w.a. σ (4) noBusiness≫ow (reason). where “w.a.” stands for with answer. (c) evaluateAndBuy is For example, suppose that the initial state of the choosePayment≪ rr (payM ethods, chosenM ethod); service b1 is s0 = {Bbuyer dep, Bbuyer arr, Bbuyer date, doPayment≫ rr ((credential, payInf o), resN um); Bbuyer def erredP aymentP os, Bbuyer ¬sellingStarted, askForMiles≫n (miles). Bbuyer credentials}, (all the other fluents truth value First, it invokes an operation for searching flights that cor- is “unknown”). This means that b1 assumes a date, a respond to a given specification (searchFlight≫ rr ). After that, departure location, an arrival location, the fact that it is possible to defer the payment to the departure (at a desk role choreographies. To this aim, let us introduce a few useful at the airport), and that no selling process has started yet. notions. The goal of b1 is to achieve the following condition: Q = Definition 1 (Compatible execution traces): Let {Bbuyer sellingComplete, Bbuyer resN um} after buyTicket σ = a0 ; . . . ; an and σ ′ = a′0 ; . . . ; a′n be two execution Intuitively, the buyer expects that, after the interaction, it will traces, we say that σ is compatible to σ ′ iff for each operation have a reservation number as a result. ai in σ the corresponding a′i in σ ′ is its complementary view. By reasoning on its policy and by using the definitions of the unbound operations that are given by the choreography, b1 Given an operation a, we denote by a its complementary ≫ can identify an execution trace, that leads to a state where Q operation. For instance, in Example II-C searchFlightrr is ≪ holds: complementary to searchFlightrr and vice versa. We extend the notion of complementarity to execution traces, so the σ = searchFlight≫ rr ((dep, arr, date), f lightList); complementary σ on an execution trace σ is the sequence askChosenFlight≪ n (f light); made of the operations that are respectively complementary choosePayment≪ rr (payM ethods, chosenM ethod); to those of σ. doPayment≫ rr ((credential, payInf o), resN um); When a service plays a choreography role, it must supply askForMiles≫ n (miles) a set of operations that will substitute the corresponding This is possible because in a declarative representation spec- specifications, thus producing ai service policy. Let hO, Pi be ifications are executable. Moreover notice that this execution a service description, and let Ou be a subset of O, containing does not influence the belief about the deferred payment, unbound operations that are to be supplied by a same role which persists from the initial through the final state and is player Si . Let OSi be the i set of such operations, that are bound not contradicted. to the operations in Ou In case Si is the player of hO, Pi, . they will be operations decorated by ≪, otherwise they will III. J OINT ACHIEVEMENT OF PERSONAL GOALS be ≫ operations. We represent the binding by the substitution θ = [OSi /Oui ] applied to hO, Pi. Notice that by [OSi /Oui ] So far, we have talked about goals, whose achievement we identify a set of substitutions [o/ou ] of single service motivates the participation of a service to a choreography. It operations to single unbound operations. The application of is, in fact, reasonable that a service may decide of taking on a the substitution is denoted by hOθ, Pθi, where every element role only if by doing so it will have the possibility of satisfying of Oui is substituted by/bound to an element of OSi . its purposes. In our proposal a service takes this decision When the matching process is applied for selecting a service based on knowledge that includes a public role representation that should play a role in a choreography, the desire is that and a representation, given in terms of preconditions and the substitution (of the service operations to the specifications effects, of its own operations, part of which will substitute contained in the choreography) preserves the properties of in- some specifications contained in the role description. More terest, i.e. the goals that could be entailed before by reasoning generally, a choreography is made of many roles, that are on each role description separately should be still achievable. played by different services, each of which has its own goal. Thus, we rely on the notion of Conservative substitution by The question we try to answer here is whether it is possible for Baldoni et al. in [13]. this team of enhanced proactive services to reach an agreement Let us, now, consider two-role choreography and see how about their possible executions so that in the team all of them the services S1 and S2 can identify a set of compatible traces, will achieve their personal goals. As observed in [19], [20] the whose execution allows the achievement of both their personal team can achieve a goal if there is a joint working plan that goals. The mechanism we are going to describe can be can achieve the goal. extended to more complicated choreographies. However, we For example, consider a choreography C = (R1 , R2 ) and do not discuss the case, due to the lack of space, concerning a two services, interested to play respectively R1 and R2 for number of roles more than two. Suppose that S1 has identified achieving the goals G1 and G2 . By applying the described an execution trace σ that allows the achievement of its goal reasoning technique, the two services might both find that Fs1 , and it has verified that the substitutions θR1 and θR2 they can achieve their personal goals, one by following the are conservative (the two substitutions involve disjoint sets of execution trace σ1 , the other σ2 . The problem is that σ1 and unbound operations by construction). Therefore, it now has σ2 might not be compatible, e.g. one invokes a operation≫ , an execution trace σθR1 θR2 that does not contain unbound when the other side does not include the corresponding exe- operations. Before executing it, its candidate partner S2 must cution of operation≪ . agree on executing the complementary trace σθR1 θR2 . Of In some cases, such compatible execution traces might not course, S2 might have its own goal Fs2 which should be exist. In others, each party may have a set of alternative σi achieved with the execution of the top level procedure of available, part of which are indeed compatible with executions the role R2 , that we here call p2 . Therefore, the following traces identified by the partner. The problem, then, becomes to conditions must be verified: converge to a common solution that allows for the achievement 1) σθR1 θR2 must be an execution trace of p2 ; of both goals. Let us discuss these issues, focusing on two- 2) after executing σθR1 θR2 the goal Fs2 must hold. An interesting issue is whether there is any guarantee that both partners will stick to execution traces that are in Σ′ . In game theory words [26] and considering a choreography as a set of game rules, is Σ′ an equilibrium? Generally, the answer is no. It might, in fact, be the case that S2 has some execution trace, that is not contained in Σ′ but allows anyway the achievement of its goal: at some point of the execution of an agreed trace, S2 might decide to continue with an unagreed action, because such action is particularly convenient for it. A related issue is whether a service has a dominant strategy, i.e. Fig. 3. Role R1 takes a decision about invoking operation a1 or a2 on R2 . an execution trace such that all of the alternative courses of In the former case, R2 will subsequently invoke b1 over R1 ; in the latter, it action, that its partner has, belong to Σ′ . For instance, with will take a decision and choose between the invocation of b2 or the invocation of b3 on R1 . reference to Figure 3, let us suppose that Σ′ contains the exe- cution traces a1 ; b1 and a2 ; b2 . In this case, the execution trace a1 ; b1 is dominant for S1 because the only possible answer of S2 is b1 and the overall trace allows the achievement of The first condition is guaranteed by the assumption that both goals. Instead, the execution trace a2 ; b2 is not dominant the choreography is well-defined, i.e. roles are interoperable, because S2 has the possibility of deciding to execute b3 in and that the services that will animate it are conform to alternative to b2 and the trace a2 ; b3 does not belong to Σ′ . the corresponding roles. The expectation that the roles of The existence of a dominant strategy depends on the goal a choreography are by construction interoperable and that that one wants to satisfy, on the choreography, and on the services are conform to them implies that, for any execution identified substitutions. The derivation that we have proposed trace that a party can execute, its partner has a complementary is not focussed on the identification of dominant strategies. In execution trace. Interoperability is a hot research issue. A general, and differently than what happens for equilibria, the discussion about it is out of the scope of this work but the decision whether an execution trace is a dominant strategy can interested reader can take a look at [21], [22], [23], [24]. be taken without knowing the goal of the interlocutor. Indeed, The second condition is to be verified by S2 by rea- a strategy is dominant if any action that the interlocutor can soning on its goal, i.e. by verifying that hR2 θR1 θR2 , s0 i ⊢ perform, lead to an execution trace which still belong to Σ′ . Fs2 after σθR1 θR2 , where s0 in this case is the initial state Thus a service which has a dominant strategy has the guarantee of S2 and θR1 θR2 represents the substitution obtained from to have a way to reach his goal. Therefore, it can be taken by θR1 θR2 by using the complementary views of the involved a service individually. operations. Notice that the above reasoning is much simpler Another interesting problem concerns preference criteria than the one executed on p1 because S2 only has to check if that services may apply in order to rank a set of strategies. the goal is satisfied after σ has been executed. The reasoning Supposing that the two services decide to behave well and applied to p1 , instead, was aimed at identifying such a trace. to execute a trace which is in the agreement, how can they To increase the probability of reaching an agreement, we converge to a best-compromise agreement? One criterion could can imagine that S1 produces a set of alternative execution be to select the trace which entails the minimum number traces Σ, each of which allows the achievement of F s1 , and of effects. For example, one can imagine that a buyer of a then propose them to S2 , that will restrict them to a set flight ticket prefers a trace at the end of which it has simply of alternatives Σ′ ⊆ Σ, satisfying both goals. It is worth bought the desired ticket w.r.t. one in which it has additionally noting that, in general, the set of alternative execution traces been registered in the advertisement mailing list of the flight might not be finite. Moreover, the derivation (⊢) is semi- company. This issue will be part of our future works. decidable unless the choreographies are properly restricted, As a final remark, negotiation, does not substitute the for instance by focussing onto regular sets [15]. Indeed, many execution of the choreography but it rather concerns checking choreographies are of this kind [25]. This interaction between the possibility of, in this case, achieving all of the goals. The the services, proposed so to allow the joint achievement of fact that the two services converged to a set of promising their goals, can be seen as a kind of negotiation [26], [27]. In execution traces does not imply that, after starting the real case no other preference criterion is introduced, it is indifferent execution, they will be able to stick to them. The reason is which of the execution traces in Σ′ will be followed, and that those traces were identified by making assumptions on it is not necessary to perform any further negotiation step the values returned by tests and conditions, which cannot be because the choreography is respected by both partners [24], known in advance. The actual results of such tests, obtained and Σ′ is known to both of them. Whatever the initiator of at execution time, could be different than the assumed ones. the interaction will be, they know how to behave to allow the The additional value of performing the negotiation is double: mutual achievement of their personal goals, although none of on the one hand, it is possible to avoid the interaction with them can make a commitment on a specific execution trace partners with which the agreement cannot be reached at all, on because both take choices that contribute to its definition. the other hand, each partner has the means to understand when the interaction takes an unagreed path and decide accordingly, Some correspondences with the technique “Planning as for instance concluding that it is better to stop the interaction. Model Checking” proposed in [30] can be investigate. In this approach, the planning domain is a semantic model, the IV. C ONCLUSIONS planning problem is represented through a set of global state and plan generation is done by checking whether suitable The coordination of a set of autonomous, cooperating agents formulas are true in a semantic model. However, deal with is well-known and crucial in multi-agent systems research web services that have to cooperate in order to reach their [27]. Solutions proposed in the literature are, for example, own goals seems to be more complicated. Indeed, planning coordination as a post-planning process [28], where constraints has to be performed by each service on its own, ignoring are checked after the plan has been found, and the use of con- which are the goals and which will be the substitutions used versation moderators [29], which guarantee that achievement by the interlocutors. At the end, the chosen plan must be of shared objectives. convenient for every service involved. Instead, by means of Along this line, this work tackles the problem of allowing the mechanism proposed in this paper planning is made only a set of independent services, which must cooperate in the by one service and the resulting set of compatible plans, at context of a given choreography, to reason about the joint the end of the negotiation, allows everyone to achieve its own achievement of their goals. The approach that we propose goal. implements a simple form of negotiation, inspired by [20], Some similarities can be found also with the proposal by [19]. There are, however, some important differences w.r.t the Son and Sakama [31], that concerns the process of creating work by Ghaderi et al. The first is that the behavior of our a joint plan in a MAS. They define a joint plan as one in services is ruled by a choreography, which specifies all the which there are some cooperative actions, i.e. actions that possible interactions that can occur. The assumption is that are mutually requested/offered by agents. Indeed, also the when services play choreography roles, they commit to keep actions involved in a protocol can be seen as cooperative their behavior adherent to the role specification. Ghaderi et actions, in the sense that a service is not able to achieve al., instead, do not use or represent choreographies or other its goal on its own, and needs the “cooperation” of other kinds of interaction protocols: the reasoning process considers services. The main difference between the two proposals is all the possible execution traces that can be composed out of a that a protocol defines not only which actions can be invoked set of atomic actions. Moreover, even when an execution trace, on other services, but also when this can occur. One of the that allows the joint achievement of goals, is identified there advantages of choreographies is that they limit the number is still the need of adding coordination mechanisms that allow of possible plans, restricting the search space of a joint plan. its actual execution. In our case, the necessary coordination Moreover, condition 1) in Section III is guaranteed by the fact that makes the cooperation of the services possible is supplied that whatever execution trace one of the partners focuses on, by the choreography. The other assumption that we make is the other surely has a compatible one, if all of the interacting that the roles that compose a choreography are interoperable. partners are conformant to the choreography and this is made Interoperability is a hot research topic that is orthogonal to the of a set of interoperable roles. problems faced in this work. Some analogies can be found also with the case in which Moreover, in the work by Ghaderi et al. each agent reasons protocols are defined by social commitments [32]. Indeed, also for the partner, because the two agents share a common a commitment is a “promise” of an agent to another on goal and a common state. The method, when successful, iden- performing some actions. A protocols defined by commitments tifies a set of joint plans, that correspond to preferred strategies does not specify when actions are to be taken. However, in this for the agents. These are obtained by the iterative elimination case there is a common knowledge (i.e. the commitments) that of dominated strategies. In our framework each partner does constrain somehow the behaviour of the involved parties. This not have knowledge about the goals of its interlocutor, as mechanism can guide the reasoning process in a better way. it is reasonable to suppose for web services; therefore, the Indeed the reasoning is not on the belief that one agent has on execution traces that we identify are not necessarily dominant. the others –e.g. I believe that if he has provide this actions he For example, a greedy partner may take an action (if the will do it–, but is on the obligation one agent has taken: I know protocol includes it) that is not in the agreement but that allows that he has taken the obligation of performing this action when the immediate achievement of its own goal. This behavior is, I will ask him. Of course, this does not mean that the action however, not convenient over the long run because the former will be executed when required. Indeed, actions are defined in partner knows the choreography and knows the agreed traces, terms of preconditions. Thus, its is possible that a condition therefore, it has a way of monitoring the on-going course of is not satisfied when the action should be executed. interaction. As soon as it realizes that the partners has deviated from the agreed traces, it can take appropriate action, e.g. R EFERENCES interrupt the interaction, enact compensation actions, publish a low reputation rate for the partner. In other words, there is [1] W3C, “Web services description language (WSDL) version 2.0 part 1: Core language.” [Online]. Available: http://www.w3.org/TR/wsdl20/ a correspondence to what is known in game theory as a game [2] OASIS, “Web services business process execution language version iterated forever [27]. 2.0, working draft.” [Online]. Available: http://www.oasis- open.org/committees/download.php/17355/wsbpel-specification- [25] Foundation for Intelligent Physical Agents, “http://www.fipa.org.” draft.doc [26] M. J. Osborne and A. Rubinstein, A Course in Game Theory. MIT [3] OWL-S Coalition. [Online]. Available: Press, July 1994. http://www.daml.org/services/owl-s/ [27] M. Wooldridge, An Introduction to Multiagent Systems. John Wiley & [4] D. Fensel, H. Lausen, J. de Bruijn, M. Stollberg, D. Roman, and Sons, March 2002. A. Polleres, Enabling Semantic Web Services : The Web Service Mod- [28] J. R. Steenhuisen, C. Witteveen, A. ter Mors, and J. Valk, “Framework eling Ontology. Springer. and Complexity Results for Coordinating Non-cooperative Planning [5] B. Meyer, “Applying ”design by contract”,” Computer, vol. 25, no. 10, Agents,” in MATES, ser. Lecture Notes in Computer Science, vol. 4196. pp. 40–51, 1992. Springer, 2006, pp. 98–109. [6] M. Pistore, L. Spalazzi, and P. Traverso, “A minimalist approach to [29] C. Sibertin-Blanc and N. Hameurlain, “Participation Components for semantic annotations for web processes compositions.” in ESWC, ser. Holding Roles in Multiagent Systems Protocols,” in Engineering Soci- LNCS, Y. Sure and J. Domingue, Eds., vol. 4011. Springer, 2006, pp. eties in the Agents World, ser. Lecture Notes in Computer Science, vol. 620–634. 3451, August 2005, pp. 60–73. [7] M. B. van Riemsdijk and M. Wirsing, “Goal-Oriented and Procedu- [30] F. Giunchiglia and P. Traverso, “Planning as Model Checking,” in Recent ral Service Orchestration. A Formal Comparison,” in AWESOME007, Advances in AI Planning, ser. LNCS. Springer, 2000, pp. 1–20. Durham, UK, September 2007. [31] T. C. Son and C. Sakama, “Reasoning and Planning with Cooperative [8] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella, “Rea- Actions for Multiagents Using Answer Set Programming,” in DALT: soning on choreographies and capability requirements,” International Declarative Agent Languages and Technologies, ser. LNAI. Budapest, Journal of Business Process Integration and Management, vol. 2, no. 4, Hungary: Springer, May 2009. pp. 247–261, 2007. [32] M. P. Singh, “Agent communication languages: Rethinking the princi- [9] G. Caire, D. Gotta, and M. Banzi, “WADE: A software platform to ples,” in Communication in Multiagent Systems, ser. Lecture Notes in develop mission critical applications exploting agents and workflows,” Computer Science, M.-P. Huget, Ed., vol. 2650. Springer, 2003, pp. in Proc. of 7th Int. Conf. on Autonomous Agents and Multiagent Systems 37–50. (AAMAS 2008), Estoril, Portugal, 12-16 May 2008, pp. 29–36. [10] M. Piunti, A. Ricci, and A. Santi, “SOA/WS Applications using Cogni- tive Agents working in CArtAgO Environments,” in Decimo Workshop Nazionale “Dagli Oggetti agli Agenti” (WOA 2009), Parma, 2009. [11] L. Bozzo, V. Mascardi, D. Ancona, and P. Busetta, “CooWS: Adaptive BDI agents meet service-oriented computing,” in Proceedings of the Int. Conference on WWW/Internet, 2005, pp. 205–209. [12] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella, “Service selection by choreography-driven matching,” in Emerging Web Services Technology, ser. Whitestein Series in Software Agent Technolo- gies and Autonomic Computing, T. Gschwind and C. Pautasso, Eds. Birkhäuser, September 2008, vol. II, ch. 1, pp. 5–22. [13] M. Baldoni, C. Baroglio, V. Patti, and C. Schifanella, “Conservative re- use ensuring matches for service selection,” in Proc. of the 6th European Workshop on Multi-Agent Systems (EUMAS), 2008. [14] M. Baldoni, C. Baroglio, A. Martelli, and V. Patti, “Reasoning about interaction protocols for customizing web service selection and com- position,” JLAP, special issue on Web Services and Formal Methods, vol. 70, no. 1, pp. 53–73, 2007. [15] M. Baldoni, L. Giordano, A. Martelli, and V. Patti, “Programming Rational Agents in a Modal Action Logic,” Annals of Mathematics and Artificial Intelligence, Special issue on Logic-Based Agent Implementation, vol. 41, no. 2-4, pp. 207–257, 2004. [Online]. Available: http://www.kluweronline.com/issn/1012-2443 [16] M. Baldoni, “Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension,” Ph.D. dissertation, Dipartimento di Informatica, Università degli Studi di Torino, Italy, 1998. [17] G. Alonso, F. Casati, H. Kuno, and V. Machiraju, Web Services. Springer, 2004. [18] D. Berardi, D. Calvanese, G. De Giacomo, M. Lenzerini, and M. Me- cella, “Synthesis of Underspecified Composite e-Service bases on Ato- mated Reasoning,” in Proc. of ICSOC04. ACM, 2004, pp. 105–114. [19] H. Ghaderi, H. Levesque, and Y. Lespérance, “Towards a logical theory of coordination and joint ability,” in Proc. of the 6th International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS07), 2007, pp. 532–534. [20] ——, “A logical theory of coordination and joint ability,” in Proc. of AAAI’07, 2007, pp. 421–426. [21] S. K. Rajamani and J. Rehof, “Conformance checking for models of asynchronous message passing software,” in CAV, ser. LNCS, vol. 2404. Springer, 2002, pp. 166–179. [22] L. Bordeaux, G. Salaün, D. Berardi, and M. Mecella, “When are two web services compatible?” in TES 2004, ser. LNCS, vol. 3324. Springer, 2005, pp. 15–28. [23] M. Bravetti and G. Zavattaro, “Contract based multi-party service composition,” in FSEN, ser. LNCS, vol. 4767. Springer, 2007, pp. 207–222. [24] M. Baldoni, C. Baroglio, A. Chopra, N. Desai, V. Patti, and M. Singh, “Choice, interoperability, and conformance in interaction protocols and service choreographies,” in Proc. of the 8th Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS), 2009.