=Paper= {{Paper |id=Vol-201/paper-31 |storemode=property |title=Policy-based Reasoning for Smart Web Service Interaction |pdfUrl=https://ceur-ws.org/Vol-201/22.pdf |volume=Vol-201 |dblpUrl=https://dblp.org/rec/conf/swap/AlbertiCGLM06 }} ==Policy-based Reasoning for Smart Web Service Interaction== https://ceur-ws.org/Vol-201/22.pdf

Policy-based reasoning for
smart web service interaction
Marco Alberti Federico Chesani
Marco Gavanelli Paola Mello
Evelina Lamma Marco Montali
ENDIF, Università di Ferrara Paolo Torroni
{marco.alberti|marco.gavanelli|evelina.lamma}@unife.it DEIS, Università di Bologna
{fchesani|pmello|mmontali|ptorroni}@deis.unibo.it

Abstract— We present a vision of smart, goal-oriented web and exploit them. This solves part of the problem: as through
services that reason about other services’ policies and evaluate discovery we only know that there are some services, which
the possibility of future interactions. We assume web services possibly follow some standards, but understanding whether
whose interface behaviour is specified in terms of reactive rules.
Such rules can be made public, in order for other web services interacting with them will be profitable or detrimental, is far
to answer the following question: “is it possible to inter-operate from being a trivial question. For one, it is not possible to think
with a given web service and achieve a given goal?” In this article to try and invoke all newly discovered services and analyze the
we focus on the underlying reasoning process, and we propose a results. Beside being highly error-prone, such a method would
declarative and operational abductive logic programming-based require expensive rollbacks that are often unaffordable at run-
framework, called WAVe .
time. Thus, alternative approaches have to be developed. This
N OTE is what we intend to address in this article.
This article is a modified version of [5]. The focus of this article is the following problem: how
to dynamically understand if two web services can inter-
I. I NTRODUCTION operate, without them having a-priori knowledge of each
Service Oriented Computing (SOC) is rapidly emerging as other’s capabilities, but by reasoning about policies exchanged
a new programming paradigm, propelled by the wide avail- at run-time.
ability of network infrastructures, such as the Internet, and by We present a vision of smart, goal-oriented web services
the success of its predecessor, Object Oriented programming that reason about other services’ specifications, with the aim to
paradigm. Web service-based technologies are an implementa- separate out those that can lead to a fruitful interaction, without
tion of SOC, aimed at overcoming the intrinsic difficulties of resorting to trial and error. We envisage a two-phase discovery
integrating different platforms, operating systems, languages, activity on the side of web services. First, web services collect
etc., into new applications. It is then in the spirit of SOC to information about other web services, and try and understand
take off-the-shelf solutions, like web services, and compose by reasoning which ones can lead to a fruitful interaction.
them into new applications. Service composition is very at- This activity is carried out off-line, beforehand. Then they use
tractive for its support to rapid prototyping and possibility the available information to interact with each other. It is the
to create complex applications from simple elements. It is same philosophy of search engines: before, collect information
the philosophy followed, e.g., by BPEL [11]: composing new through web spiders, then use it when requested by the user.
applications through existing web services. In this article we focus on the reasoning involved in the off-
If we adopt the SOC programming paradigm, how to exploit line phase, assuming that a new web service has been found,
the potential of a growing base of web services becomes and we must decide about the possibility to interact with it.
one of our strategic issue. In a domain in which being more We assume that each web service publishes, alongside with its
competitive means knowing more and using all available WSDL, its interface behaviour specifications. By reasoning on
information at best, how shall we cope with the proliferation the information available about other web services’ interface
of new services? How shall we decide to use a web service behaviour, each web service can verify which goals can be
rather than another one? when new ones become available, reached by interaction.
shall we go for them? are there new opportunities that were To achieve our vision, we propose a proof theoretic ap-
not there before? It is a necessary, never-ending, heavy and proach, based on computational logic – in fact, on abductive
thus potentially very costly decision process, but it could also logic programming. In particular, we formalise policies for
be very rewarding, if we had the proper tools. web services in a declarative language which is a modification
A partial answer to these questions is given by service dis- of the SCIFF language originally defined in the context of the
covery. As new services become available, they are published, EU IST-2001-32530 project, to specify and verify social-level
for instance by registration on some yellow-pages server; agent interaction.
existing services can then become aware of the new ones In this new language, policies can be defined by way
of social integrity constraints (ICs): a sort of reactive rules C C
used to generate and reason about expectations about possible
evolutions of a given interaction setting.
As claimed in [14], a rule-based approach to reactivity on WAV e WAV e Reasoning
the Web provides the following benefits over the conventional
approach: policies policies

• Rules are easy to understand for humans. Requirements Knowledge
specifications often already comes in the for of rules Gws KBws ICws Gws' KBws' ICws'

expressed in a natural or formal language;
Rules
• Rule-based specifications are flexible and easy to adapt; RIF RIF
Interchange
decoder/encoder decoder/encoder
• Rules are well-suited for processing and analyzing by Format
machines (verification, transformation);
• Rules can be managed in a single knowledge base or
in several knowledge bases possibly distributed over the network

Web.
Fig. 1. The architecture of WAVe
Moreover, we believe that, as advocated by Alferes et al.
[10], an approach based on logic programming allows to
express knowledge in form of rules, and to make inference vice versa), a Rule Interchange Format (RIF) is adopted. One
with those rules. Like the authors, we follow Tim Berners- possibility for such a RIF could be RuleML [3]. Finally, as
Lee et al. [12] in considering logic a natural conceptual and a result of the reasoning activity, ws produces an answer C
computational tool for the Semantic Web (“Adding logic to to the question: “is it possible to inter-operate with ws0 and
the Web - the means to use rules to make inferences, choose achieve goal Gws ?”
courses of action and answer questions - is the task before the Fig. 1 does not show control elements, but only information
Semantic Web community at the moment”) flows. We assume that suitable interaction protocols are de-
Based on the SCIFF framework we propose a new declar- fined to control the flow of information (e.g. policies) between
ative semantics and a new proof-procedure that combines for- the web services. In particular, in a more comprehensive
ward, reactive reasoning with backward, goal-oriented reason- setting, ws and ws0 could negotiate the exchange of policies
ing, and is tailored to the discovery activity’s off-line phase’s in an incremental way, or could use the result C of this
verification problem. We have called this new framework reasoning activity to perform the second, on-line phase of
WAVe (Web-service Abductive Verification). service interaction we mentioned in the introduction. All this
In order to support the exchange of rules between web is outside of this picture, and of this article’s scope.
services in a standard format, we also propose a RuleML
encoding for our language. III. T HE alice & eShop S CENARIO
We start by showing the abstract architecture of WAVe . In
This scenario is inspired to the one described by the
Sect. III we introduce a running on-line shopping scenario.
Working Group on Rule Interchange Format [25]. A similar
In Sect. IV, we briefly introduce the language used in the
scenario is also in [14]. We consider two entities, which we
framework, and in Sect. V we show how the scenario can
call alice and eShop.1 eShop is a web service which sells
be modeled in WAVe in terms of ICs. Sect. VI presents the
devices. alice is another web service which instead needs
declarative and operational semantics of WAVe , and Sect. VII
to obtain a device, and which is considering buying it from
proposes the application of WAVe to the verification problem
eShop. alice and eShop describe their behaviour concerning
in the reference scenario. Sect. VIII discusses the encoding of
sales/payment/... of items through policies, specified as rules,
WAVe rules in RuleML. A brief discussion, also with respect
which they publish using some RIF.
to related work, follows.
Before alice buys an item from eShop, alice checks
II. T HE A RCHITECTURE OF WAVe whether her policies and eShop’s policies are compatible, i.e.,
Fig. 1 depicts our general reference architecture. Arrows if they allow a successful transaction. During this process, it
indicate the flow of policies between web services. The layered turns out that eShop accepts credit card payments, besides
architecture of a web service, e.g. ws, has WAVe at the top of other payment methods, and that alice can only pay by credit
the stack, performing reasoning based on its own knowledge card; in this case, in order to proceed with the payment, she
and on the policies obtained from other web services, e.g. ws0 . requires evidence of the shop’s membership to some trusted
The functionalities of the various elements of the knowledge “Better Business Bureau” (BBB) association. We assume that
will be explained in Sect. IV. For the moment, we say the shop is able and ready to provide such a piece of evidence.
that policies are identified with the IC ws component. The We can thus define eShop’s and alice’s policies as follows:
architecture is symmetric. We represented with thick borders 1 In this simplified scenario, we identify alice and eShop with their
the modules involved in the operations carried out by ws, representative software counterparts which will carry out transactions on their
and its output. In order for ws0 to pass IC ws0 on to ws (and behalf.
(shop1) if a customer wishes to buy an item, then (s)he should involved in (3) is the subject of this article.
pay it either by credit card, or by cash, or by cheque;
(shop2) if a customer wishes to buy an item, and (s)he has
IV. T HE WAVe F RAMEWORK
paid it either by credit card, or by cash, or by cheque,
then eShop will deliver the item; In WAVe , the observable behaviour of the web services is
(shop3) if a customer wishes to receive a certificate about represented by events. Since we focus on (explicit) interaction
eShop’s membership to the BBB, then the shop will between web services, events always represent exchanged
send it; messages.
(alice1) if a shop requires that alice pays by credit card,
WAVe considers two types of events: those that one can con-
alice expects that the shop provides evidence of its trol and those that one cannot. Typically, from the standpoint
membership to the BBB; of a web service ws, an event such as a message generated
(alice2) if a shop requires that alice pays by credit card, and
by ws himself will fall into the first category, a message
the shop has provided evidence of its membership to that ws is expecting from another fellow web service ws0
the BBB, then alice will pay by credit card; will fall instead into the second one. We use two different
In this example, we can identify two kinds of policy rules. functors to keep these two categories of messages distinct
shop1 and alice1 express requirements, i.e., what is needed from each other. Atoms denoted by functor H will stand for
in order to proceed with accomplishing some request. shop2, events that a web service expects to be producing itself; atoms
shop3 and alice2 represent the effect of requests, i.e., they denoted by functor E will stand for events that a web service
tell what has to be expected if some conditions hold and some is expecting, and over which it does not have any control.
request is received. Since WAVe is about reasoning on possible future courses of
Using this scenario, we want to demonstrate the possibility events, both kinds of events represent hypotheses that a web
of reaching an agreement through rules exchange. Besides, we service can make on possibly happening events. The notation
want to show how policies support backward and forward rea- is: H(ws, ws0 , M, T ), for messages (M ) that a web service ws
soning, in the following way. Backward, pro-active reasoning is expecting to send to ws0 at time T , and E(ws0 , ws, M, T )
starts from goals to produce (expectations about) actions or for messages (M ) expected by ws from ws0 for time T .
events that should be generated in order to achieve the goals. Web service specifications in WAVe are relations among
Forward, reactive reasoning starts from events and is used to expected events, expressed by an Abductive Logic Program
generate (expectations about) actions that represent reactions (ALP). In general, an ALP [21] is a triplet hP, A, ICi,
to such events. where P is a logic program, A is a set of predicates named
In this scenario, the goal of alice interacting with eShop is abducibles, and IC is a set of integrity constraints. Roughly
to obtain an item from eShop. Actions are all the messages speaking, the role of P is to define predicates, the role of A
exchanged between the two web services. is to fill-in the parts of P which are unknown, and the role of
The steps that we envisage are as follows: IC is to constrain the ways elements of A are hypothesised,
1) alice wants to obtain a device. She knows that she can or “abduced”. Reasoning in abductive logic programming is
have it if eShop delivers it to her. Thus, she sends eShop usually goal-directed (being G a goal), and it accounts to
a request, by which she wants to know eShop’s policies finding a set of abduced hypotheses ∆ built from predicates
regarding the delivery of that device; in A such that P ∪ ∆ |= G and P ∪ ∆ |= IC. In the past,
2) eShop considers alice’s request, and composes a set a number of proof-procedures have been proposed to compute
of rules related to alice’s request (its policies), possibly ∆ (see Kakas and Mancarella [22], Fung and Kowalski [17],
deriving/filtering them from a larger set. In this example, Denecker and De Schreye [15], etc.).
the set contains shop1, shop2, and shop3. Once such Definition 4.1 (Web service interface behaviour specification):
a set is put together, eShop communicates it to alice; Given a web service ws, its web service interface behaviour
3) alice reasons on (1) her goal, (2) her own policies specification Pws is an ALP, represented by the triplet
(alice1 and alice2), and (3) eShop’s policies. Two are
the possible outcomes: Pws ≡ hKBws , Ews , IC ws i
• either alice infers that she and eShop can have
a successful transaction that satisfies each other’s where:
policies and that achieves her goal, • KB ws is ws’s Knowledge Base,
• or alice infers that there is no such a possibility. • Ews is ws’s set of abducible predicates, and
4) possibly, at a later point, alice and eShop may engage • IC ws is ws’s set of Integrity Constraints.
in a transaction which (hopefully) makes alice achieve KB ws is a set of clauses which declaratively specifies pieces
her goal. of knowledge of the web service. Note that the body of KB ws ’s
Points (1) through (3) represent the off-line phase of service clauses may contain E expectations about the behaviour of the
discovery/interaction, whereas point (4) represent the actual web services, as defined above. KB ws ’s syntax is summarised
transaction occurring between alice and eShop. The reasoning in Eq. (1).
IC shop2 says that, if alice expects eShop to deliver the Item,
KB ws ::= [ Clause ]? and alice has paid for it, then eShop will actually deliver it
to alice. In that case, the abducible in the head is an event,
Clause ::= Atom ← Cond because it represents an action that eShop should perform,
Cond ::= ExtLiteral [ ∧ ExtLiteral ]? (1) and therefore it assumes that it will indeed happen (since it is
ExtLiteral ::= Atom | true | Expect | Constr its own responsibility).
Expect ::= E(Atom, Atom, Atom, Atom)
E(eShop, alice, give guarantee, Tg )
Ews includes E expectations, H events, and predicates not (shop3)
→H(eShop, alice, give guarantee, Tg ).
defined in KB ws .
IC shop3 says that if alice expects to receive a guarantee,
IC ws [ IC ]?
::= then eShop will send it. The following two rules represent
alice’s policies.
IC Body → Head
::=
Body (Event | Expect) [∧BodyLit]?
::= E(alice, eShop, pay(Item, cc), Tp )
(alice1)
BodyLit Event | Expect | Atom | Constr
::= →E(eShop, alice, give guarantee, Tg ) ∧ Tg < Tp .
Head Disjunct [ ∨ Disjunct ]? | false
::= (2)
Disjunct (Expect | Event | Constr)
::= IC alice1 says that, if eShop expects alice to pay for an
Item by credit card, then alice expects that eShop will have
[ ∧ (Expect | Event | Constr)]? provided a guarantee by the time she pays.
Expect ::= E(Atom, Atom, Atom, Atom)
Event ::= H(Atom, Atom, Atom, Atom) E(alice, eShop, pay(Item, cc), Tp )
∧ H(eShop, alice, give guarantee, Tg ) ∧ Tg < T(alice2)
p
Integrity Constraints (ICs) are forward rules, of the form
Body → Head (Eq. (2)). The Body of ICs is a conjunction →H(alice, eShop, pay(Item, cc), Tp ).
of literals and expected events; the Head instead is a disjunc- IC alice2 says that, if eShop expects alice to pay for an
tion of conjunctions of expectations, events and literals, or Item by credit card, and eShop has provided alice with a
false. The syntax of IC ws is a modification of the integrity guarantee, then alice will pay the Item by credit card. Finally,
constraints in the SCIFF language [6]. In particular, unlike the following clause is part of KB alice
SCIFF, WAVe treats H events as abducible predicates, and have(alice, Item, T ) ←
as such it allows them to occur in the Head of integrity (alice3)
E(eShop, alice, deliver(Item), Td ) ∧ Td ≤ T.
constraints; however, this initial version of WAVe does not
yet accommodate negative expectations nor negation (¬). We Clause alice3 says that, in order for alice to have an Item at
intend to consider these two features in future extensions of time T , then alice expects eShop to deliver the Item by time
WAVe . T.
Intuitively, the operational behaviour of integrity constraints
is similar to forward rules: whenever the body becomes true, VI. D ECLARATIVE AND O PERATIONAL S EMANTICS
the head is also made true. We have assumed that all web services have their own
V. M ODELING IN WAV e interface behaviour specified in the language of ICs. This
In this section, we demonstrate web service policy mod- interface behaviour could be thought of as an extension of
elling in WAVe by showing the specification of alice and WSDL, that could be used by other fellow web services to
eShop. The first three rules represent eShop’s policies. reason about the specifications, or to check if inter-operability
E(eShop, alice, deliver(Item), Ts ) is possible.
→E(alice, eShop, pay(Item, cc), Tcc ) ∧ Tcc < Ts Another approach would be to obtain web services’ in-
(shop1) terface behaviour through an appropriate request protocol,
∨E(alice, eShop, pay(Item, cash), Tca ) ∧ Tca < Ts
∨E(alice, eShop, pay(Item, cheque), Tch ) ∧ Tch < Ts in which ICs are (interactively) exchanged so that each
web service may disclose ad hoc, customised information on
IC shop1 says that, if alice expects eShop to deliver an demand.
Item, then eShop expects alice to pay by credit card, cash, or
cheque, and that payment must be made before delivery.2 In In this work, we make the simplifying assumption that all
that case, the abducibles in the head are expectations, because information regarding the interface behaviour is provided at
they represent actions that should be performed by alice: from once. The web service will then try and prove that a fruitful
eShop’s viewpoint, they can only be expected. interaction is possible based on what it receives.
E(eShop, alice, deliver(Item), Ts ) The web service initiating the interaction has a goal G,
∧ H(alice, eShop, pay(Item, How), Tp ) ∧ Tp < Ts which is a given state of affairs. A typical goal could be
(shop2)
∧ How::[cc, cash, cheque]) to access a resource, to retrieve some information, or to
→H(eShop, alice, deliver(Item), Ts ). obtain a service from another web service. G will often be an
expectation (of obtaining a service, accessing a resource, or
2 The alternative in the head could alternatively be expressed via
gathering information), but in general it can be any conjunction
a variable with domain: E(alice, eShop, pay(Item, How), T ) ∧
How::[cc, cash, cheque] ∧ T < Ts , where “::” represents a domain of expectations, CLP constraints, and any other literals, in the
constraint. syntax of IC ws Head Disjuncts (Eq. 2).
The verification of a web service ws about the possibility to Definition 6.2 (Possible interaction achieving G): Given
achieve a goal G by interacting with another fellow web ser- two web services, ws and ws0 , and a goal G, a possible
vice ws0 makes use of KB ws , IC ws , G, and of the information interaction achieving G is a possible interaction about G
obtained about ws0 ’s policies, IC ws0 (see Fig. 1). The idea is satisfying Eq. 5.
to obtain, through abductive reasoning, a set of expectations Intuitively, the “→” implication in Eq. 5 avoids situations in
about a possible course of events that together with KB ws which a web service waits forever for an event that the other
entails IC ws ∪ IC ws0 and G. web service will never produce. The “←” implication avoids
Note that we do not assume that ws knows KB ws0 , as the that one web service sends unexpected messages, which in the
KB is not part of the interface. However, in general integrity best case may not be understood (and in the worst scenarios
constraints can involve predicates defined in the knowledge it may lead to faulty, unpredictable behaviour of the parties
base. For example, they can contain predicates defining pa- involved).
rameters, deadlines, coefficients, etc., or other knowledge only
available to ws0 . If the interface behaviour provided by ws0 A. Operational Semantics
involves predicates defined in KB ws0 , unknown to ws, we have The operational semantics is a modification of the SCIFF
two alternatives: proof-procedure [9]. SCIFF is a transition system, whose state
0
• either ws provides ws with the necessary information, is given by the following tuple:
e.g. with (part of) its KB ws0 ;
• or ws will have to make assumptions about such unknown T ≡ hR, CS, P SIC, ∆A, PEND, HAP, FULF, VIOLi
predicates.
We take the second option, and consider unknowns that The set of expectations EXP is partitioned into the fulfilled
are neither H events nor E expectations as literals that can (FULF), violating (VIOL), and pending (PEND) expecta-
be abduced, and we keep them in a set ∆. We then have tions. The other elements are: the resolvent (R), the abduced
the following two equations that define the set of abductive literals that are not expectations (∆A), the constraint store
answers representing possible interaction between ws and ws0 (CS), a set of implications, inherited from the IFF [17], called
achieving G: partially solved integrity constraints (P SIC), and the history
of happened events (HAP).
KB ws ∪ HAP ∪ EXP ∪ ∆ |= G (3) A classical application of SCIFF is on-line checking of
KB ws ∪ HAP ∪ EXP ∪ ∆ |= IC ws ∪ IC ws0 (4) compliance of agent interaction to protocols. In fact, SCIFF
was initially developed to specify and verify agent interaction
where HAP is a conjunction of H atoms, EXP is a conjunc- protocols on-the-fly, under the assumption of open agent
tion of E atoms, and ∆ a conjunction of abducible atoms. environments adopted by other noteworthy agent research
We can now proceed with defining what kind of interaction work [27]. SCIFF processes events drawing from HAP
is possible/fruitful, given two web services and a goal. and generates (abduces) expectations; then it checks that all
Definition 6.1 (Possible interaction about G): A possible expectation are fulfilled by at least one happened event. The
interaction about a goal G between two web services ws and declarative semantics of SCIFF contains in fact a requirement
ws0 is an A-minimal set HAP ∪ EXP ∪ ∆ such that Eq. 3 E(X) → H(X) – differently from WAVe , which has a double
and 4 hold. implication (Eq. 5). In SCIFF, as soon as new H events are
Among all possible interactions about G, some of them
processed, a transition fulfilment labels the relevant matching
are fruitful, and some are not. An interaction only based
expectations as fulfilled and moves them to the set FULF. At
on expectations which will not be matched by corresponding
the end of the derivation, if some expectation remains in the
events is not a fruitful one: for example, the goal of ws might
set PEND, a failure node is generated, and other alternative
not have a corresponding event, thus the goal is not actually
branches will be explored in backtracking, if there exist any.
reached, but only expected. Or, one of the web services could
WAVe extends SCIFF and abduces H events as well as
be waiting for a message from the other fellow, which will
expectations. The events history is not taken as input, but
never arrive, thus undermining the inter-operability.
all possible interactions are hypothesised. Moreover, in WAVe
We select, among the possible interactions, those whose
events not matched by an expectation (which are perfectly
history satisfies all the expectations of both the web services.
acceptable in the multi-agent scenario addressed by SCIFF)
After the abductive phase, we have a verification phase in
cannot be part of a possible interaction achieving the goal.
which there are no abducibles, and in which the previously
The two phases in the declarative semantics (generation
abduced predicates H and E are now considered as defined
of possible interactions and their test for conformance) are
by atoms in HAP and EXP, and they have to match. If
condensed into one single derivation process, thanks to a new
among the possible interactions there exists one satisfying
transition adopted in WAVe . The expected transition, symmet-
HAP ∪ EXP |= E(X, Y, Action, T ) ↔ H(X, Y, Action, T ) rical to fulfilment, labels each H events with an expected flag
(5) as soon as an expectation matching it is abduced. At the end
then ws has found a sequence of actions that obtains the goal of the derivation, H with expected status = false will cause
G. failure.
Otherwise, if the WAVe derivation in a program P for a Given the guarantee, alice will pay by credit card (rule
goal G succeeds with set of expectation EXP ∪ HAP ∪ ∆, (alice2) fires):
we write P `EXP∪HAP∪∆ G.
Soundness and completeness results. WAVe is a conser- EXP4a ={E(eShop, alice, deliver(device), Ts ) ∧ Ts < 50
vative modification of the SCIFF proof-procedure, which ∧E(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts
is sound and complete under reasonable assumptions [7]. ∧E(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc
Therefore, soundness and completeness results also hold for HAP4a ={H(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc
WAVe . A detailed discussion of this issue can be found in [5].
∧H(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts }
We will next demonstrate the operational functioning of
(by (alice2))
verification in WAVe in the alice & eShop scenario. (10)
VII. V ERIFICATION IN WAVe
Having received the payment, eShop’s policy would be to
In the following, the sets EXPN N
a and HAPa represent
the evolution of alice’s expectations and events as WAVe ’s deliver the device:
derivation progresses; N is an incremental index. Let g be the
following goal of alice’s: EXP5a ={E(eShop, alice, deliver(device), Ts ) ∧ Ts < 50
g ← have(alice, device, 50). ∧E(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts
(goal)
∧E(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc }
Then, by unfolding of clause alice3, HAP5a ={H(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc
∧H(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts
EXP0a ={E(eShop, alice, deliver(device), Ts ) ∧ Ts < 50} ∧H(eShop, alice, deliver(device), Ts ) ∧ Ts < 50}
(6)
(by (alice3)) (by (shop2))
(11)
To this expectation, eShop will react by expecting a pay-
ment: Summarising, alice devised the following set of events,
which should let her achieve her goal (have the desired device)
EXP1a ={E(eShop, alice, deliver(device), Ts ) ∧ Ts < 50 while respecting both of alice’s and eShop’s policies.
∧(E(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts
Ca ={H(eShop, alice, give guarantee, Tg ) ∧ Tg < Tp
∨E(alice, eShop, pay(device, cash), Tca ) ∧ Tca < Ts
∧H(alice, eShop, pay(device, cc), Tp ) ∧ Tp < Ts (12)
∨E(alice, eShop, pay(device, cheque), Tch ) ∧ Tch < Ts )
∧H(eShop, alice, deliver(device), Ts ) ∧ Ts < 50)}
(by (shop1))
(7)
VIII. RULE M ARK -U P
Since the expectation containing the payment by cc is the e
In WAV , the ICs can be exchanged between web services,
only one which generates an expectation matching a rule of as well as advertised together with their WSDL. For this
alice ((alice1)), the first expectation among the three payment reason, a mark-up language is necessary for the rules in ICs.
alternatives is selected (the other branches eventually fail RuleML [3] is the perfect mark-up language for exchanging
by Eq. 5, because no matching H is abduced). This choice rules on the web, so our choice has been easy. RuleML 0.9
triggers (alice1): contains mark-ups for expressing important concepts of the
SCIFF proof-procedure. In particular, SCIFF is a rule engine
EXP2a ={E(eShop, alice, deliver(device), Ts ) ∧ Ts < 50 able to distinguish and use both backward and forward rules.
∧E(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts Backward rules are used to plan, reason upon events, perform
(8)
∧E(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc } proactive reasoning. Forward rules are used for reactive rea-
(by (alice1)) soning, to quickly perform actions in response to occurred
events. Both are seamlessly integrated in SCIFF. RuleML 0.9
Then (shop3) fires, and abduces the happening of contains a direction attribute that can be attached to rules.
give guarantee event. We then have: Being based on abduction, SCIFF can deal both with negation
as failure and negation by default, that have an appropriate
EXP3a ={E(eShop, alice, deliver(device), Ts ) ∧ Ts < 50 tagging in RuleML. In this work, we only used standard
∧E(alice, eShop, pay(device, cc), Tcc ) ∧ Tcc < Ts RuleML syntax; in future work we might be interested in
∧E(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc } distinguishing between defined and abducible predicates, or
(by (alice1)) between expectations and events.
HAP3a ={H(eShop, alice, give guarantee, Tg ) ∧ Tg < Tcc } SCIFF was implemented in SICStus Prolog: SICStus con-
(by (shop3)) tains an implementation of the PiLLoW library [19], which
(9) makes it easy to perform http requests, as well as implement-
ing services on the web. Finally, SICStus contains an XML
parser, which allowed us to easily implement the RuleML certain course of events in an acceptable option, possibly after
parser. The RuleML parser is freely available on the SCIFF another mutual verification phase. This is subject of ongoing
web site [26]. work. Finally, we are currently investigating the exchange of
policies between web services, for which a suitable interaction
IX. D ISCUSSION AND RELATED WORK protocol needs to be devised. We are thinking of specifying
WAVe is a framework intended for describing declaratively such a protocol for exchanging the policies in the same
the behavioural interface of web services, and for testing language WAVe uses to specify policies.
operationally the possibility of fruitful interaction between In this work, we do not address the problem of reasoning
them. WAVe answers the question “does there exist a viable about ontologies: rather, we focus on the reasoning process,
interaction, between two given web services, which achieves given the policies of both the peers involved in the interaction.
a given goal G?” In case of success, WAVe produces a set of Many other approaches instead focus on the former issue:
expectations about events. WAVe is particularly suitable for hence our proposal could be seen as a complementary func-
highly dynamic environments, in which interoperability is an tionality, that could further improve the discovery process. For
unknown that has to be checked. instance, in [24] an ontology language to define web services is
WAVe uses and extends a technology initially developed for proposed. In [1], [2], besides proposing a general language for
online compliance verification of agent interaction to protocols representing semantic web service specifications using logic, a
[6]. SCIFF and the protocol specification language based on discovery scenario is depicted and an architectural solution is
social integrity constraints were motivated and inspired by proposed (we draw inspiration for our scenario from the Dis-
conspicuous work done in the context of agent interaction in covery Engine example). A notion of mediator is introduced to
open societies, notably work by Singh [27] and colleagues. overcome differences between different ontologies, and then
The extension of such a work to the context of web services, a reasoning process is performed over the user inputs and the
centering around the concept of policies, as proposed in this hypothetical effects caused by the service execution. To some
work, seems to be very promising. The idea of policies for extent, our work can be related to [23], where the authors
web services and policy-based reasoning is one that many present a framework for automated web service discovery that
other authors also adopt. We will cite work by Finin and uses the Web Service Modeling Ontology (WSMO) as the
colleagues [20], and by Bradshaw and colleagues [28], the first conceptual model for describing web services, requester goals
one with an emphasis on representation of actions, the latter and related aspects. This conceptual framework distinguishes
on the deontic semantic aspects of web service interaction. We two main stages. During the discovery stage, the requester
acknowledge the importance of action modelling and we point states only the things that are desired, thus seeks for all the
that the idea of expected behaviour of web services can have services that can potentially satisfy a request of such a kind.
a deontic reading. In fact, previous work on SCIFF has been During the contracting stage, instead, the requester provides in
devoted to investigating and clarifying the interesting links input specific information for an already requested service. The
between deontic operators and expectation-based reasoning purpose of this second stage is to verify that the input provided
[8]. The distinguishing features of WAVe , compare to most will lead to a desired state that satisfies the requester goal.
work of literature, are its logical underpinning and its sound In our work, we are concerned mainly with the contracting
and complete operational characterisation. It is in our agenda stage. While in [23] the authors use F-logic and transaction
to carry out an extensive empiric evaluation of WAVe based logic as the underlying formalisms, we rely on extended logic
on interesting cases and scenarios such as those proposed in programming. In both the approaches, however, hypothetical
related work, and on the existing implementation of the SCIFF reasoning is used for service contracting.
framework.3 In [23], [1], [2], only the clients goal is considered, while in
Another direction of current work relates to the actual use our framework the client can specify its policies (its intended
of the answers of WAVe by web services after they manage behavioural interface); in this way, the client could be consid-
a successful derivation. In principle, the sequence of events ered a web service as well. Therefore, our framerwork can be
produced by WAVe could be instantiated into a concrete exploited without major changes to deal with the problem of
sequence of messages, which will guarantee the achievement interoperability between web services behavioural interfaces
of G, under ideal external conditions. But this is true only [4].
if the policies disclosed by both web services are a faithful Foster et al. [16] propose a model-based approach to ver-
representation of their actual behaviour. This may not be the ify a given service composition can successfully execute a
case, as for example policies may depend on sensible data, and choreography, in particular with respect to the obligations
web services may be not allowed to disclose full information imposed on the services by a choreography. The web service
to the outside. In that case nothing warrants that the course specifications and the choreography are translated to FSP
of action produced by WAVe will be satisfactory for either algebra and checked by model checking techniques. The main
web service. We might then have to resort to further steps. difference with respect to our work is that Foster et al.
For example both web services could “formally” agree that a check a web service composition against a choreography for
conformance, while we check a set of web services for their
3 See http://lia.deis.unibo.it/research/sciff. capability to achieve a goal. Another notable difference is in
the adopted formal approaches (abduction in our case, model Revised Selected Papers, volume 3267 of Lecture Notes in Artificial
checking in theirs). Intelligence, pages 324–339. Springer-Verlag, 2005.
[7] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma,
The outcome of the reasoning process performed by WAVe Paola Mello, and Paolo Torroni. Verifiable agent interaction in abductive
could be intended as a sort of “contract agreement” between logic programming: the SCIFF proof-procedure. Technical Report
the client and the discovered service, provided that each peer DEIS-LIA-06-001, University of Bologna (Italy), March 2006. LIA
Series no. 75.
is tightly bounded to the policies/knowledge bases he/she has [8] Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, Giovanni
previously published. For example, the dynamical agreement Sartor, and Paolo Torroni. Mapping deontic operators to abductive
about contracts (e-contracting) is addressed in [13], where expectations. Computational and Mathematical Organization Theory,
12(2–3):205 – 225, October 2006.
Situated Courteous Logic is adopted for reasoning about rules [9] Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and
that defines business provisions policies. The used formal- Paolo Torroni. The SCIFF abductive proof-procedure. In Proceedings
ism supports contradicting rules (by imposing a priorization of the 9th National Congress on Artificial Intelligence, AI*IA 2005,
volume 3673 of Lecture Notes in Artificial Intelligence, pages 135–147.
and mutual exclusion between rules), different ontologies, Springer-Verlag, 2005.
and effectors as procedures with side effects. However, their [10] José Júlio Alferes, Carlos Viegas Damásio, and Luı́s Moniz Pereira.
work is more focussed on establishing the characteristics of Semantic web logic programming tools. In François Bry, Nicola Henze,
and Jan Maluszynski, editors, PPSWR, volume 2901 of Lecture Notes
a business deal, while our approach address the problem in Computer Science, pages 16–32. Springer, 2003.
of evaluating the feasibility of an interaction. To this end, [11] Tony Andrews, Francisco Curbera, Hitesh Dholakia, Yaron Goland,
we perform hypothetical reasoning on the possible actions Johannes Klein, Frank Leymann, Kevin Liu, Dieter Roller, Doug Smith,
Satish Thatte, Ivana Trickovic, and Sanjiva Weerawarana. Business
and consequences; moreover, we hypothesised also which process execution language for web services version 1.1, May 2003.
condition must hold, in order to interoperate. Other works http://www.ibm.com/developerworks/library/ws-bpel/.
use rules to reason about established contracts: in [18], for [12] Tim Berners-Lee, James Hendler, and Ora Lassila. The semantic web.
Scientific American, May 2001.
example, Defeasible Deontic Logic of Violation is used to [13] S. Bhansali and N. Grosof. Extending the sweetdeal approach for e-
monitor the execution of a previously agreed contract. We procurement using sweetrules and ruleml. In Adi et al. [3].
have addressed such issue in a companion paper [8], where [14] Franois Bry and Michael Eckert. Twelve theses on reactive rules for the
web. In Proceedings of the Workshop on Reactivity on the Web, Munich,
integrity constraints have been exploited and conciliated with Germany, March 2006.
the deontic concepts. [15] M. Denecker and D. De Schreye. SLDNFA: an abductive procedure for
abductive logic programs. Journal of Logic Programming, 34(2):111–
ACKNOWLEDGEMENTS 167, 1998.
[16] Howard Foster, Sebastian Uchitel, Jeff Magee, and Jeff Kramer. Model-
This work has been partially supported by the MIUR PRIN based analysis of obligations in web service choreography. In Proceed-
2005 projects Specification and verification of agent inter- ings of the International Conference on Internet and Web Applications
and Services (ICIW 2006), Guadeloupe French Caribbean, 2006. IEEE
action protocols and Vincoli e preferenze come formalismo Computer Society Press.
unificante per l’analisi di sistemi informatici e la soluzione di [17] T. H. Fung and R. A. Kowalski. The IFF proof procedure for abductive
problemi reali, and by the MIUR FIRB project Tecnologie logic programming. Journal of Logic Programming, 33(2):151–165,
November 1997.
Orientate alla Conoscenza per Aggregazioni di Imprese in [18] G. Governatori and D. P. Hoang. A semantic web based architecture for
Internet. e-contracts in defeasible logic. In Adi et al. [3].
[19] Daniel Cabeza Gras and Manuel V. Hermenegildo. Distributed WWW
R EFERENCES programming using (Ciao-)Prolog and the PiLLoW library. Theory and
Practice of Logic Progr., 1(3):251–282, 2001.
[1] http://www.w3.org/Submission/SWSF-SWSL/. [20] Lalana Kagal, Timothy W. Finin, and Anupam Joshi. A policy based
[2] http://www.w3.org/Submission/2005/SUBM-SWSF-Applications- approach to security for the semantic web. In Dieter Fensel, Katia P.
20050909/. Sycara, and John Mylopoulos, editors, International Semantic Web
[3] Asaf Adi, Suzette Stoutenburg, and Said Tabet, editors. Rules and Conference, volume 2870 of Lecture Notes in Computer Science, pages
Rule Markup Languages for the Semantic Web, First International 402–418. Springer, 2003.
Conference, RuleML 2005, Galway, Ireland, November 10-12, 2005, [21] A. C. Kakas, R. A. Kowalski, and Francesca Toni. Abductive Logic
Proceedings, volume 3791 of Lecture Notes in Computer Science. Programming. Journal of Logic and Computation, 2(6):719–770, 1993.
Springer Verlag, 2005. [22] A. C. Kakas and Paolo Mancarella. On the relation between Truth
[4] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Maintenance and Abduction. In T. Fukumura, editor, Proceedings of
Paola Mello, and Marco Montali. An abductive framework for a-priori the 1st Pacific Rim International Conference on Artificial Intelligence,
verification of web services. In Michael Maher, editor, Proceedings PRICAI-90, Nagoya, Japan, pages 438–443. Ohmsha Ltd., 1990.
of the Eighth Symposium on Principles and Practice of Declarative [23] Michael Kifer, Ruben Lara, Axel Polleres, Chang Zhao, Uwe Keller,
Programming, July 10-12, 2006, Venice, Italy, pages 39–50, New York, Holger Lausen, and Dieter Fensel. A logical framework for web service
USA, July 2006. Association for Computing Machinery (ACM), Special discovery. In Semantic Web Services: Preparing to Meet the World
Interest Group on Programming Languages (SIGPLAN), ACM Press. of Business Applications, ISWC Worshop, Hiroshima, Japan, November
[5] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, 2004.
Paola Mello, Marco Montali, and Paolo Torroni. Policy-based reasoning [24] D. et al. Martin. http://www.daml.org/services/owl-s/1.0/.
for smart web service interaction. In Proceedings of the 1st International [25] Working Group on Rule Interchange Format. Use cases and
Workshop on Applications of Logic Programming in the Semantic Web requirements. http://www.w3.org/2005/rules/wg/ucr/
and Semantic Web Services (ALPSWS 2006), volume 196 of CEUR draft-20060323.html, March 2006.
Workshop Proceedings, pages 87–102, Seattle, WA, USA, August 2006. [26] The SCIFF abductive proof procedure, 2005. http://lia.deis.
[6] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, unibo.it/research/sciff/.
Paola Mello, and Paolo Torroni. The SOCS computational logic [27] M. Singh. Agent communication language: rethinking the principles.
approach for the specification and verification of agent societies. In IEEE Computer, pages 40–47, December 1998.
Corrado Priami and Paola Quaglia, editors, Global Computing: IST/FET [28] Andrzej Uszok, Jeffrey M. Bradshaw, Renia Jeffers, Austin Tate, and
International Workshop, GC 2004 Rovereto, Italy, March 9-12, 2004 Jeff Dalton. Applying kaos services to ensure policy compliance
for semantic web services workflow composition and enactment. In
Sheila A. McIlraith, Dimitris Plexousakis, and Frank van Harmelen,
editors, International Semantic Web Conference, volume 3298 of Lecture
Notes in Computer Science, pages 425–440. Springer, 2004.