-Web service specifications can be quite complex, including various operations and message exchange patterns. In this work, we give a rule-based declarative representation of services, and in particular of WSDL operations, that enables the application of techniques for reasoning about actions and change, that are typical of agent systems. This makes it possible to reason on a rule-based specification of choreography roles and about the selection of possible role players on a goal-driven basis, and allows us to attack the problem of the joint achievement of individual goals for a set of services which animate a choreography.
Declarative languages are becoming very important in the Semantic Web, since the focus started to shift from the ontology layer to the logic layer, with a consequent need of expressing rules and of applying various forms of reasoning1, an interest also witnessed by the creation of a W3C working group to define a Rule Interchange Format2. Particularly challenging applications concern web services.
One of the key ideas behind web services is that services
should be amenable to automatic retrieval, thus facilitating
their re-use. Nevertheless, retrieval cannot yet be accomplished
automatically as well and as precisely as desired because
the current web service representations (mainly WSDL [
The need of adding a semantic layer to service descriptions is not new. Some approaches, e.g. OWL-S [3] and WSMO [4], propose a richer annotation, aimed at representing inputs, outputs, preconditions and effects of the service. Inputs and outputs are usually expressed by ontological terms, while preconditions and effects are often expressed by means of logic representations. Preconditions and effects are also used in design by contract, originally introduced by Meyer for the EiffelT M language [5]. Here preconditions are the part of the contract which is to be guaranteed by the client; if this condition is guaranteed in the execution context of a method, then the server commits to guaranteeing that the postcondition holds in the state reached by the execution.
On the other hand, there is often the need of using services not in an individual way but jointly, for executing tasks that none of them alone can accomplish. Semantic annotations alone are not sufficient in this case; it becomes useful to introduce a notion of goal [6], [7], [8], which can be used to guide both the selection and the composition of services.
The introduction of goals opens the way to the introduction of another abstraction, that of agent. Agents include not only the ability of dealing with goals and of performing goaldriven forms of reasoning, but they also show autonomy and proactivity, which are characteristics that help when dealing I. INTRODUCTION with open environments, allowing for instance a greater fault tolerance (see [9], [10], [11]).
In this work, we take the perspective of a candidate role player, willing to take part to an interaction, that is ruled by a choreography. We see such an entity as an enhanced (proactive) service, made of a declarative description of its behavior, of the operations that it can execute, of its goals [7], and with the capability of reasoning (on its own behavior) so to build orchestations that allow the achievement of its goals (proactiveness). So, for instance, a service that wishes to play the role of the “Seller” of a ticket-purchase choreography may have the aim of “selling tickets”, guaranteed by playing the choreography role, and have the additional, private goal of “loyalizing clients”. Notice that personal goals may vary along time, hence, different participations (to the same choreography of a same agent as player of the same role) may be characterized by different personal goals. For example, the flight ticket selling service may change at some point its personal goal, which becomes the “promotion of additional services” offered by the same company. The presence of additional goals, which may not be disclosed to the interacting parties, biases the behavior and the choices of a service. A service will take on a role only after checking the possible achievement of this final condition.
Orchestrations compose the interactions of sets of services.
However, reasoning on the goals of the orchestrator alone is not sufficient. Indeed, in the context of choreographies that provide a pattern of interaction among services, each service involved has its own goals, that it tries to pursue. The research question is: even though each service has proved that there is a possible way of playing its role, which leads to the achievement of its personal goal, is it possible to guarantee the compatibility of these individual solutions? In other words, will the joint working plan, made of the identified individual solutions, allow the joint achievement of all the goals of the 1REWERSE NoE, http://rewerse.net interacting parties? A ticket selling service that wants to do 2http://www.w3.org/2005/rules/wiki/RIF_Working_Group some advertisement by sending a newsletter to its clients will unknown fluents, we use an epistemic operator B, to represent the beliefs an entity has about the world: Bf means that the fluent f is known to be true, B¬f means that the fluent f is known to be false. A fluent f is undefined when both ¬Bf and ¬B¬f hold (¬Bf ∧ ¬B¬f ). Thus each fluent in a state can have one of the three values: true, false or unknown. For the sake of readability, we will add as a superscript of B the name of the service that has the belief.
Services exhibit interfaces, called port-types, which make a set of operations available to possible clients. In our proposal, a service description is defined as a pair hO, Pi, where O is a set of basic operations, and P (policy) is a description of the complex behavior of the service. Analogously to what happens for OWL-S composite processes, P is built upon basic operations and tests, that control the flow of execution.
not match the aims of a client which considers this kind of information as spam.
In this paper we describe the first steps of a study about the joint achievement of goals of a set of services, whose interaction is ruled by a choreography. The approach relies on a rule-based declarative representation of the choreography roles and of the interacting services, which extends and refines the work in [8], [12], [13], exploiting the results about conservative matching defined in there. The framework enables the application of techniques for reasoning on the effects of playing a role in a choreography, thus checking whether the desired personal goal can be accomplished. The representation is based on the logic programming language described in [14], [15]. Behaviors, as roles and service policies, build upon WSDL-like basic operations, represented as atomic actions with preconditions and effects.
The paper is organized as follows. Section II sets the representation of services and of choreographies that we adopt. Moreover, it explains how it is possible to reason on such a representation in order to allow each service to check the reachability of its goals locally, i.e. by using only the specification of the desired choreography role. Section III tackles the joint achievement of personal goals. A running example is distributed along the pages to better explain the proposed notions and mechanisms. Conclusions end the paper.
AND REASONING ABOUT SERVICES
Let us start with basic operations. According to the main languages for representing web services, like WSDL and OWL-S, there are four basic kinds of operations [17] (or atomic processes, when using OWL-S terminology [3]): • one-way involves a single message exchange, a client
invokes an operation by sending a message to the service; • notify involves a single message exchange, the client
receives a message from the service; • request-response involves the exchange of two messages, are initiated by the invoker of the operation, which sends a message to the service and, after that, waits for a response; • solicit-response involves the exchange of two messages, the order of the messages is inverted w.r.t. a requestresponse, first the invoker waits for a message from the service and then it sends an answer.
A basic operation is described in terms of its executability preconditions and effects, the former being a set of fluents (introduced by the keyword possible if) which must be contained in the service state in order for the operation to be applicable, the latter being a set of fluents (introduced by the keyword causes) which will be added to the service state after the operation execution. Syntax for basic operations is:
In this section, we introduce the notation that we use to represent services and we discuss the problem of verifying a personal goal. The notation, which is a refinement of the proposal in [13], is based on a logical theory for reasoning about actions and change in a modal logic programming setting and on the language DYnamics in LOGic, described in details in [14]. This language is designed for specifying agents behaviour and for modeling dynamic systems. It is fully set inside the logic programming paradigm by defining programs by sets of Horn-like rules and giving a SLD-style proof procedure. The capability of reasoning about interaction protocols, supported by the language, has already been exploited 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 ineffects 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 OWLcard 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 oneto 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 OWLsome 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 (a) operationr≫r(min, mout) possible if BInvokermin ∧ Ps (b) operationr≫r(min, mout) causes BInvokersent(min) (c) operationr≫r(min, mout) causes BInvokermout (d) operationr≫r(min, mout) causes Es (a) operations≫r(min, mout) possible if Ps (b) operations≫r(min, mout) causes BInvokermout (c) operations≫r(min, mout) causes BInvokermin (d) operations≫r(min, mout) causes BInvokersent(min) (e) operations≫r(min, mout) causes Es (e) operationn≪(mout) possible if Rs (f) operationn≪(mout) causes BSuppliermout (g) operationn≪(mout) causes BSuppliersent(mout) (h) operationn≪(mout) causes Ss (e) operationr≪r(min, mout) possible if Rs (f) operationr≪r(min, mout) causes BSuppliermin (g) operationr≪r(min, mout) causes BSuppliermout (h) operationr≪r(min, mout) causes BSuppliersent(mout) (i) operationr≪r(min, mout) causes Ss (f) operations≪r(min, mout) possible if Rs (g) operations≪r(min, mout) causes BSuppliermout (h) operations≪r(min, mout) causes BSuppliersent(mout) (i) operations≪r(min, mout) causes BSuppliermin (l) operations≪r(min, mout) causes Ss 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).
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 and are executed in a goal-directed way, similarly to standard logic programs, and their definitions can be non-deterministic as in Prolog. Complex behaviors are used also for representing 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.
Also a role R is represented by a pair hO, Pi. The difference with services is that it composes specifications of operations and not implemented operations. The player of each role has to supply appropriate implementations. We call such specifications unbound operations. Formally, unbound operations are represented as normal basic operations, in terms of their preconditions and effects. This is one of the advantages of adopting a logic language: it allows handling implementations and specifications in the same way. In our case, both operations and operation specifications are given in terms of their preconditions and effects.
As an example, let’s consider searchFlight, an operation of a flight reservation service, which is offered by a seller and can be invoked by a buyer to search information about flights with given departure (dep) and arrival locations (arr) plus the date of departure (date). From the point of view of the buyer, the operation, which is of kind request-response, is: (a) searchFlightr≫r((dep, arr, date), f lightList) possible if Bbuyerdep ∧ Bbuyerarr ∧ Bbuyerdate∧
Bbuyer¬sellingStarted (b) searchFlightr≫r((dep, arr, date), f lightList) causes Bbuyersent(dep) ∧ Bbuyersent(arr)∧
Bbuyersent(date) (c) searchFlightr≫r((dep, arr, date), f lightList) causes
Bbuyerf lightList (d) searchFlightr≫r((dep, arr, date), f lightList) causes
BbuyersellingStarted The inputs of the operation are dep, arr, and date, while the output is f lightList. In this case the set Ps contains only the belief Bbuyer¬sellingStarted (in bold text above) while the set Es of effects contains the belief BbuyersellingStarted (in bold text as well).
From the point of view of the supplier, instead, the operation is represented as: (a) searchFlightr≪r((dep, arr, date), f lightList) possible if true (b) searchFlightr≪r((dep, arr, date), f lightList) causes
Bsellerdep ∧ Bsellerarr ∧ Bsellerdate (c) searchFlightr≪r((dep, arr, date), f lightList) causes
Bsellerf lightList (d) searchFlightr≪r((dep, arr, date), f lightList) causes
Bsellersent(f lightList) In this case the sets Rs and Ss of requirements and side effects are empty. The operation expects as input the departure and arrival locations and the date of the flight, and it produces a f lightList, which it sends to its customer, so after the operation the belief Bsellersent(f lightList) will be in its belief state.
buyTicket is, instead, an example of procedure implemented by a possible buyer service: (a) buyTicket is searchFlightr≫r((dep, arr, date), f lightList); askChosenFlightn≪(f light); evaluateAndBuy. (b) evaluateAndBuy is
noBusinesso≫w(reason). (c) evaluateAndBuy is choosePaymentr≪r(payM ethods, chosenM ethod); doPaymentr≫r((credential, payInf o), resN um); ≫ askForMilesn (miles).
First, it invokes an operation for searching flights that correspond to a given specification (searchFlightr≫r). After that, it waits for being asked about the preferred flight, chosen among the flights list obtained by the previous operation (askChosenFlightn≪). This evaluation can give either a negative outcome, hence the interaction is interrupted (noBusinesso≫w) or the interaction continues with the selection of the payment method (choosePaymentr≪r). Then, the buyer performs the payment (doPaymentr≫r) and, at the end, it is notified about the obtained miles (askForMilesn≫).
In the outlined framework, it is possible to reason about personal goals by means of queries of the form Fs after p, where Fs is the goal (represented as a conjunction of fluents), that we wish to hold after the execution of a policy p.
Checking if a formula of this kind holds corresponds to answering the query: “Is it possible to execute p in such a way that the condition Fs is true in the final state?”. When the answer is positive, the reasoning process returns a sequence of atomic actions that allows the achievement of the desired condition. This sequence corresponds to an execution trace of the procedure and can be seen as a plan to bring about the goal Fs. This form of reasoning is known as temporal projection.
Temporal projection fits our needs because, as mentioned in the introduction, in order to perform the selection we need a mechanism that verifies if a goal condition holds after the interaction with the service has taken place. Fs is the set of facts that we would like to hold “after” p.
Reasoning is done by exploiting a goal-directed proof procedure (denoted by “⊢” in the following) designed for the language DYnamics in LOGic [15], [14], which supports both temporal projection and planning and allows the proof of existential queries of the kind reported above. The procedure definition constrains the search space. In particular, for what concerns planning, the proof procedure allows the automatic extraction of linear or conditional plans for achieving the goal of interest from an incompletely specified initial state.
Let hO, Pi be a service description. The application of temporal projection to P returns, if any, an execution trace (a linear plan), that makes a goal of interest become true. Let us, then, consider a procedure p belonging to P and denoting its top level, and denote by Q the query Fs after p. Given a state s0, containing all the fluents that we know as being true in the beginning, we denote the fact that the query Q is successful in the service description by (hO, Pi, s0) ⊢ Q.
The execution of the above query returns as a side-effect an execution trace σ of p; the execution trace σ is a sequence a1, . . . , an of atomic actions. We denote this by: (hO, Pi, s0) ⊢ Q w.a. σ
(4) where “w.a.” stands for with answer.
For example, suppose that the initial state of the service b1 is s0 = {Bbuyerdep, Bbuyerarr, Bbuyerdate, Bbuyerdef erredP aymentP os, Bbuyer¬sellingStarted, Bbuyercredentials}, (all the other fluents truth value is “unknown”). This means that b1 assumes a date, a 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. {TBhebugyoerasleollfinb1gCiso mtoplaecthei,eBvebutyheerrfeoslNlowuming} caofntdeirtiobnu: yQTic=ket σ D=efinai0ti;o.n. .1; a(Cnomanpdatiσb′le =exeacu′0t;i.o.n. ;traa′ncebs)e: tLweot 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 can identify an execution trace, that leads to a state where Q holds: σ = searchFlightr≫r((dep, arr, date), f lightList); askChosenFlightn≪(f light); choosePaymentr≪r(payM ethods, chosenM ethod); doPaymentr≫r((credential, payInf o), resN um);
≫ askForMilesn (miles) This is possible because in a declarative representation specifications are executable. Moreover notice that this execution does not influence the belief about the deferred payment, which persists from the initial through the final state and is not contradicted.
So far, we have talked about goals, whose achievement motivates the participation of a service to a choreography. It is, in fact, reasonable that a service may decide of taking on a role only if by doing so it will have the possibility of satisfying its purposes. In our proposal a service takes this decision based on knowledge that includes a public role representation and a representation, given in terms of preconditions and effects, of its own operations, part of which will substitute some specifications contained in the role description. More generally, a choreography is made of many roles, that are played by different services, each of which has its own goal. The question we try to answer here is whether it is possible for this team of enhanced proactive services to reach an agreement about their possible executions so that in the team all of them will achieve their personal goals. As observed in [19], [20] the team can achieve a goal if there is a joint working plan that can achieve the goal.
For example, consider a choreography C = (R1, R2) and two services, interested to play respectively R1 and R2 for achieving the goals G1 and G2. By applying the described reasoning technique, the two services might both find that they can achieve their personal goals, one by following the execution trace σ1, the other σ2. The problem is that σ1 and σ2 might not be compatible, e.g. one invokes a operation≫, when the other side does not include the corresponding execution of operation≪.
In some cases, such compatible execution traces might not exist. In others, each party may have a set of alternative σi available, part of which are indeed compatible with executions traces identified by the partner. The problem, then, becomes to converge to a common solution that allows for the achievement of both goals. Let us discuss these issues, focusing on twoGiven an operation a, we denote by a its complementary operation. For instance, in Example II-C searchFlightr≫r is complementary to searchFlightr≪r and vice versa. We extend the notion of complementarity to execution traces, so the complementary σ on an execution trace σ is the sequence made of the operations that are respectively complementary to those of σ.
When a service plays a choreography role, it must supply a set of operations that will substitute the corresponding specifications, thus producing a service policy. Let hO, Pi be a service description, and let Oui be a subset of O, containing unbound operations that are to be supplied by a same role player Si. Let OSi be the set of such operations, that are bound to the operations in Oui. In case Si is the player of hO, Pi, they will be operations decorated by ≪, otherwise they will be ≫ operations. We represent the binding by the substitution θ = [OSi /Oui] applied to hO, Pi. Notice that by [OSi /Oui] we identify a set of substitutions [o/ou] of single service operations to single unbound operations. The application of the substitution is denoted by hOθ, Pθi, where every element of Oui is substituted by/bound to an element of OSi .
When the matching process is applied for selecting a service that should play a role in a choreography, the desire is that the substitution (of the service operations to the specifications contained in the choreography) preserves the properties of interest, i.e. the goals that could be entailed before by reasoning on each role description separately should be still achievable. Thus, we rely on the notion of Conservative substitution by Baldoni et al. in [13].
Let us, now, consider two-role choreography and see how the services S1 and S2 can identify a set of compatible traces, whose execution allows the achievement of both their personal goals. The mechanism we are going to describe can be extended to more complicated choreographies. However, we do not discuss the case, due to the lack of space, concerning a number of roles more than two. Suppose that S1 has identified an execution trace σ that allows the achievement of its goal Fs1, and it has verified that the substitutions θR1 and θR2 are conservative (the two substitutions involve disjoint sets of unbound operations by construction). Therefore, it now has an execution trace σθR1 θR2 that does not contain unbound operations. Before executing it, its candidate partner S2 must agree on executing the complementary trace σθR1 θR2 . Of course, S2 might have its own goal Fs2 which should be achieved with the execution of the top level procedure of the role R2, that we here call p2. Therefore, the following conditions must be verified: 1) σθR1 θR2 must be an execution trace of p2; 2) after executing σθR1 θR2 the goal Fs2 must hold. Fig. 3. Role R1 takes a decision about invoking operation a1 or a2 on R2. In the former case, R2 will subsequently invoke b1 over R1; in the latter, it will take a decision and choose between the invocation of b2 or the invocation of b3 on R1.
The first condition is guaranteed by the assumption that the choreography is well-defined, i.e. roles are interoperable, and that the services that will animate it are conform to the corresponding roles. The expectation that the roles of a choreography are by construction interoperable and that services are conform to them implies that, for any execution trace that a party can execute, its partner has a complementary execution trace. Interoperability is a hot research issue. A discussion about it is out of the scope of this work but the interested reader can take a look at [21], [22], [23], [24].
The second condition is to be verified by S2 by reasoning on its goal, i.e. by verifying that hR2θR1 θR2 , s0i ⊢ Fs2 after σθR1 θR2 , where s0 in this case is the initial state of S2 and θR1 θR2 represents the substitution obtained from θR1 θR2 by using the complementary views of the involved operations. Notice that the above reasoning is much simpler than the one executed on p1 because S2 only has to check if the goal is satisfied after σ has been executed. The reasoning applied to p1, instead, was aimed at identifying such a trace.
To increase the probability of reaching an agreement, we
can imagine that S1 produces a set of alternative execution
traces Σ, each of which allows the achievement of F s1, and
then propose them to S2, that will restrict them to a set
of alternatives Σ′ ⊆ Σ, satisfying both goals. It is worth
noting that, in general, the set of alternative execution traces
might not be finite. Moreover, the derivation (⊢) is
semidecidable unless the choreographies are properly restricted,
for instance by focussing onto regular sets [15]. Indeed, many
choreographies are of this kind [
Another interesting problem concerns preference criteria that services may apply in order to rank a set of strategies. Supposing that the two services decide to behave well and to execute a trace which is in the agreement, how can they converge to a best-compromise agreement? One criterion could be to select the trace which entails the minimum number of effects. For example, one can imagine that a buyer of a flight ticket prefers a trace at the end of which it has simply bought the desired ticket w.r.t. one in which it has additionally been registered in the advertisement mailing list of the flight company. This issue will be part of our future works.
As a final remark, negotiation, does not substitute the execution of the choreography but it rather concerns checking the possibility of, in this case, achieving all of the goals. The fact that the two services converged to a set of promising execution traces does not imply that, after starting the real execution, they will be able to stick to them. The reason is that those traces were identified by making assumptions on the values returned by tests and conditions, which cannot be known in advance. The actual results of such tests, obtained at execution time, could be different than the assumed ones. The additional value of performing the negotiation is double: on the one hand, it is possible to avoid the interaction with partners with which the agreement cannot be reached at all, on the other hand, each partner has the means to understand when the interaction takes an unagreed path and decide accordingly, for instance concluding that it is better to stop the interaction.
The coordination of a set of autonomous, cooperating agents
is well-known and crucial in multi-agent systems research
[
Along this line, this work tackles the problem of allowing a set of independent services, which must cooperate in the context of a given choreography, to reason about the joint achievement of their goals. The approach that we propose implements a simple form of negotiation, inspired by [20], [19]. There are, however, some important differences w.r.t the work by Ghaderi et al. The first is that the behavior of our services is ruled by a choreography, which specifies all the possible interactions that can occur. The assumption is that when services play choreography roles, they commit to keep their behavior adherent to the role specification. Ghaderi et al., instead, do not use or represent choreographies or other kinds of interaction protocols: the reasoning process considers all the possible execution traces that can be composed out of a set of atomic actions. Moreover, even when an execution trace, that allows the joint achievement of goals, is identified there is still the need of adding coordination mechanisms that allow its actual execution. In our case, the necessary coordination that makes the cooperation of the services possible is supplied by the choreography. The other assumption that we make is that the roles that compose a choreography are interoperable. Interoperability is a hot research topic that is orthogonal to the problems faced in this work.
Moreover, in the work by Ghaderi et al. each agent reasons
also for the partner, because the two agents share a common
goal and a common state. The method, when successful,
identifies a set of joint plans, that correspond to preferred strategies
for the agents. These are obtained by the iterative elimination
of dominated strategies. In our framework each partner does
not have knowledge about the goals of its interlocutor, as
it is reasonable to suppose for web services; therefore, the
execution traces that we identify are not necessarily dominant.
For example, a greedy partner may take an action (if the
protocol includes it) that is not in the agreement but that allows
the immediate achievement of its own goal. This behavior is,
however, not convenient over the long run because the former
partner knows the choreography and knows the agreed traces,
therefore, it has a way of monitoring the on-going course of
interaction. As soon as it realizes that the partners has deviated
from the agreed traces, it can take appropriate action, e.g.
interrupt the interaction, enact compensation actions, publish
a low reputation rate for the partner. In other words, there is
a correspondence to what is known in game theory as a game
iterated forever [
Some correspondences with the technique “Planning as
Model Checking” proposed in [
Some similarities can be found also with the proposal by
Son and Sakama [
Some analogies can be found also with the case in which
protocols are defined by social commitments [
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 Technologies and Autonomic Computing, T. Gschwind and C. Pautasso, Eds.
Birkha¨user, September 2008, vol. II, ch. 1, pp. 5–22. [13] M. Baldoni, C. Baroglio, V. Patti, and C. Schifanella, “Conservative reuse 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 composition,” 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, Universita` 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. Mecella, “Synthesis of Underspecified Composite e-Service bases on Atomated Reasoning,” in Proc. of ICSOC04. ACM, 2004, pp. 105–114. [19] H. Ghaderi, H. Levesque, and Y. Lespe´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. Salau¨ 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.