In practical contexts where protocols model business interactions (e.g. trading, banking), designers need tools allowing them to analyse the impact on the possible interactions of regulations, preferences, conventions and the like. This work faces the issue of how to equip commitment protocols with formal and practical instruments aimed at supporting such an analysis by identifying the possible risks of violation and, thus, enabling the de nition of operational strategies aimed at reducing risks of violation. Speci cally, we present an operational semantics for the commitment protocol language 2CL as well as a tool for visualizing as a graph the possible interactions, labelling the states of the interaction so as to highlight legal situations and violations.
Agent interaction is generally speci ed by de ning interaction protocols [
In many practical contexts where protocols model business interactions (e.g.
trading, banking), designers must be able to regulate and constrain the
possible interactions as speci ed by conventions, regulations [
The work presented in this paper aims at lling this gap. To this purpose,
we started from the commitment protocol language 2CL described in [
The chief characteristic of our solution is that it performs a state evaluation of
protocol constraints, rather than performing path evaluation (as, instead, done
by model checking techniques). State evaluation allows considering each state
only once, labelling it as a state of violation if some constraint is violated in it
or as a legal state when no constraint is violated. This is a great di erence with
respect to path evaluation, where a state belonging to di erent paths can be
classi ed as a state of violation or not depending on the path that is considered.
The advantage is practical: state evaluation allows to easily supply the user an
overall view of the possible alternatives of action, highlighting those which will
bring to a violation and those that will not. State evaluation, however, is possible
only by making some restriction on the proposal in [
The paper is organized as follows. Section 2 brie y summarizes 2CL interaction protocol speci cation. Section 3 describes the formalization of 2CL-GCM. Section 4 presents a Prolog implementation of 2CL-GCM. Section 5 describes the 2CL Tools that supply features for supporting the protocol design and analysis. Related Work and Conclusions end the paper. Along the paper we use as a running example the well-known NetBill interaction protocol. 2
Let us brie y recall the chief characteristics of commitment protocols, as de ned
in [
De nition 1 (Interaction protocol). An interaction protocol P is a tuple hRo; F; s0; A; Ci, where Ro is a set of roles, identifying the interacting parties, F is a set of facts and commitments that can occur in the social state, s0 is the set of facts and commitments in the initial state of the interaction, A is a set of actions, and C is a set of constraints.
The set of social actions A, de ned on F and on Ro, forms the constitutive
speci cation of the protocol. The social e ects are introduced by the construct
means, and their achievement can depend on a precondition (conditional
effects). Both preconditions and e ects are given in terms of the set F speci ed
in the protocol, which contains commitments and facts (i.e. the conditions that
are brought about). The means construct amounts to a counts-as relation [
The regulative speci cation of the protocol is made of the set of 2CL
constraints C, de ned on F and on Ro as well. 2CL is a declarative language,
which allows expressing what is mandatory and what is forbidden without the
need of listing the possible executions extensionally. Constraints have the form
\dnf1 op dnf2", where dnf1 and dnf2 are disjunctive normal forms of facts and
Action De nitions
(a1) sendRequest means request if :quote ^ :goods
(a2) sendQuote means quote ^ create(C(m; c; C(c; m; goods; pay); goods))
^ create(C(m; c; pay; receipt))
(a3) sendAccept means create(C(c; m; goods; pay)) if :pay
(a4) sendGoods means goods ^ create(C(m; c; pay; receipt))
(a5) sendEP O means pay
(a6) sendReceipt means receipt if pay
Constraints
(c1) quote . C(c; m; goods; pay) _ C(c; m; pay)
(c2) C(m; c; pay; receipt) ^ goods . pay
(c2) pay . receipt
commitments, and op is one of the 2CL operators, reported in Table 1 together
with their Linear-time Temporal Logic [
Among the possible interactions, derivable from the action speci cation, those that respect the constraints are said to be legal. Violations amounting to the fact that a constraint is not respected can be detected during the execution. The following section provides the operational semantics 2CL lacked of. 3
In order to provide the semantics of commitment protocols as speci ed in [
According to [
Example 1. Considering NetBill, the expression goods ^ C(c; m; pay) represents one possible con guration of the social state. This expression means that goods were shipped and that there is a commitment from c (customer) to m (merchant) to pay for them.
Particularly relevant is the subset of S, whose elements are named good states: they are the desired nal states of the interaction. The characterization of good states depends on the particular application. For instance, they may be only those that do not contain unsatis ed active commitments, or they could be the ones which satisfy a condition of interest (e.g. payment done and goods shipped).
In GCM, transitions between the states are logically inferred on the basis of
an action theory , that contains a set of axioms of the kind p ,!a q, meaning
that q is a consequence of performing action a in a state where p holds. When q
is false the meaning is that a is impossible if p holds. In general, contains all
the axioms deriving from the speci cation of the protocol actions. Additionally,
also contains an axiom for each action a and for each couple of states s and
s0 such that the execution of a in s causes a transition to s0: for instance, if the
precondition p of a is satis ed in s and its e ect q is satis ed in s0, then s ,!a s0
is in . The way in which these axioms are obtained is explained in [
In GCM paths must be in nite. All the nite paths are transformed into
in nite ones by adding a transition from the last state of the nite path towards
an arti cial new state with a self loop [
De nition 2 (2CL Generalized Commitment Machine). Let ` and be, respectively, the logical consequence and the logical equivalence of propositional logic. A 2CL-GCM is a tuple P = hS; A; s0; ; G; Ci, where: - S is a nite set of states; - A is a nite set of actions; - s0 2 S is the initial state; - is an action theory; - G S is a set of good states; - C is a set of 2CL constraints. (i) Members of S are logically distinct, that is: 8s; s0 2 S; s 6 s0; (ii) false 62 S; and (iii) 8s 2 G; s0 2 S : (s0 ` s) ) (s0 2 G), i.e. any state that logically derives a good state is also good.
A sequence of states is a path of a 2CL-GCM if it satis es all of the constraints in C. Since 2CL constraints are de ned in terms of LTL formulas, to perform the veri cation one can consider the transition system corresponding to the path. Given a sequence of states interleaved by actions, the corresponding transition system can be derived quite straightforwardly. Intuitively, the set of states and transitions of the system is the same set of states and transitions in the sequence. A requirement on transition systems is that each state has at least one outgoing transition (i.e. runs are in nite).
De nition 3 (Transition System). Let = h( 0; a0; 1); ( 1; a1; 2); : : : i be an in nite and ordered sequence of triples, where i is the state at position i in and ai is the action that causes the transition from state i to state i+1. The transition system T ( ) corresponding to is a triple hS ; ; L i where: - S = f ij i 2 g is a set of states; - : S ! S is a transition function where: ( j ) = k i ( j ; a; k) 2 ; - L : S ! 2F is a labelling function, where: F is a set of facts and commitments and given l 2 F , then l 2 L( i) i i ` l.
To de ne a 2CL-GCM path, we adapt the de nition of GCM path by adding
the requirement that the sequence of states satis es all the constraints of the
2CL-GCM. This condition is checked on the transition system corresponding to
the path, by means of the LTL satisfaction relation [
Given a protocol speci cation it is possible to build the corresponding
2CLGCM:
De nition 5 (2CL-GCM of a protocol). Let P = hRo; F; s0; A; Ci be a
protocol, S be a set of states and G S be a set of good states. P = hS; LA; s0; ; G; Ci
is a 2CL-GCM of P when (i) LA is the set of action labels in A; and (ii) is
the action theory of A, i.e.:
a
{ for each (a means e if p) belonging to A, then p ,! e belongs to
{ is closed under inference rules in [
This section describes a Prolog implementation for the 2CL-GCM, formalized above. It allows exploring all the possible executions of an interaction protocol, showing the regulative violations | i.e. both those states in which some constraint is violated and those that contain unsatis ed commitments. We prove that if a path is legal according to the implementation, then it is a path of the corresponding 2CL-GCM.
The implementation is realized in tuProlog 1 and it builds upon the enhanced
commitment machine realized by Winiko et al. [
In order to provide a compact but global view of the possible interactions, the evaluation of constraints is performed on one state at a time rather than on paths (as, instead, usually done in LTL model checking). Speci cally, the
Correlation Co-existence Response Before Cause
State Condition (A B) = A ^ B (A 6 (A (A 6 (A
B) = :(A ^ B) B) = (A B) ^ (B
B) = (A 6 . B) = A ^ B
B) ^ (B 6
A)
A)
(A 6 . B) = :(A ^ B)
(A . B) = :(B ^ :A)
(A 6 . B) = :(A ^ B)
(A . B) = (A . B) ^ (A . B)
state content is given in terms of positive facts and commitments. A fact that
is not true in a state has not been achieved yet, so we use negation as failure
in the conditions of the action de nitions to verify whether a fact is present or
not in the social state. In this setting, the evaluation of 2CL constraints can
be made on single states. For instance, if in a state b holds but a does not, we
can infer that the constraint `a before b' is violated. This kind of veri cation,
however, can be performed only on a subset of 2CL formulas, speci cally, only
on constraints corresponding to conditions that persist (i.e. that involve DNFs
of facts without negation). Since commitments do not persist because they can
be cancelled, discharged, etc., another requirement is to associate a fact to each
operation that is performed on commitments (along the line of [
Given a constraint c, we denote by (c) the corresponding condition to be veri ed one state at a time (state condition). The above assumptions allow the simpli cation of the LTL formulas, corresponding to the 2CL operators, in the way that is reported in Table 3. Consider, for instance, the before operator ( . ): it requires that A is met before or in the same state of B. So, given a run , if in there is a state j such that B holds while A does not, that is a state where a violation occurred. In formulas: i j=LT L A . B , :9j i s:t: j j=LT L (B ^ :A) (when a formula does not contain temporal operators, the relation j=LT L checks the condition in the rst state of a path).
The other 2CL operators can be divided in two groups. Correlation ( ) and response ( .) are part of the same group. A B requires that if A is achieved in a run, then also B is achieved in the same run (before or after A is not relevant). If B is achieved before A it will remain true also after. Therefore, in those cases in which the constraint is satis ed, from a certain time onwards both conditions will hold. In formulas: i j=LT L A B , :9j i s:t: j j=LT L A and 8j0 j; j0 j=LT L (A ^ :B). The same equivalence holds for i j=LT L A . B. In 2CL A . B requires that when A is met, B is achieved at least once later (even if it already occurred in the past) but under our assumptions it can be checked in the same way of correlation. The state condition amounts to verifying whether a state satis es A but does not satisfy B. Notice that states that satisfy the test cannot be marked as states of violation because the constraint does not require B to hold whenever A holds. A state of violation is signalled when the interaction does not continue after it: we say that there is a pending condition.
Negated correlation, response and before correspond to the same formula: i j=LT L A op B , :9j i s:t: j j=LT L (A ^ B) where op 2 f 6 ; 6 .; 6 . g. Intuitively, a constraint of the kind A 6 B (negative correlation) requires that if A holds, B is not achieved. Since facts persist, this amounts to check that the two conditions do not hold in the same state, otherwise a violation occurs. Negative response (negative before) adds a temporal aspect to not-correlation: if A holds, B cannot hold later (before, respectively). Since facts persist, the rst achieved condition will remain true also after the other becomes true. Also in this case we only need to check that the two conditions do not hold together.
Derived operators are decomposed and the reasoning made for the operators, from which they derive, is applied. For instance, cause ( . ) derives from before and response. If a state does not satisfy the response part of the cause, it is marked as \pending"; if it violates the before part, it is marked as a \violation". Both labels are applied when the state does not satisfy any of the two.
Summarizing, given a constraint formula and a state in which to verify it, we have three possible cases: (i) the state satis es the formula; (ii) the state does not satisfy the formula and this leads to a violation; and (iii) the state does not satisfy the formula but the violation is potential, depending on future evolution. Considering all the constraints of a protocol, a state can both violate some constraint and have pending conditions. Moreover, states are also evaluated based on the presence of unsatis ed active commitments.
These considerations enable the generation and the labelling of all the states that can be reached by applying the protocol actions. The result is a labelled graph, as de ned in De nition 6, where each state is associated a set of labels. De nition 6 (Labelled Graph). Let P = hRo; F; s0; A; Ci be a protocol, the corresponding labelled graph G(P) is a triple (S; ; L) where: { S is a set of states reachable from s0, such that 8s; s0 2 S; s 6 s0; { S A S is a transition relation such that 8(s; a; s0) 2 then s; s0 2 S and 9a 2 A s.t. when a is executed in s it determines s0; { L S fpending,violation, nal,non- nalg is a labelling relation such that given s 2 S: violation 2 L(s) i 9c 2 C s.t. s 2LT L (c) and c is not a response or a correlation; pending 2 L(s) i 9c 2 C s.t. s 2LT L (c) and c is a response or a correlation;
nal 2 L(s) i there are no unsatis ed active commitments in s;
Listing 1.1. Prolog clauses that generate the labelled graph: consequence(A,State) is a clause that determines if the fact (or the DNF formula) A can be derived in State; response and before are constraints. The complete program is downloadable at the URL http://di.unito.it/2cl.
not- nal 2 L(s) i s contains unsatis ed active commitments.
Following De nition 6, our implementation starts from the initial state and
determines all the reachable states, by applying a depth- rst search, as in [
Given a labelled graph we are now able to de ne when a path is legal. De nition 7 (Legal path). Let G(P) = (S; ; L) be a labelled graph, = h( 0; a0; 1); : : : ; ( n 1; an 1; n)i be a path of at least one state. is a legal path of G(P) when: (i) 8i 0; i is a state of the graph and ( i; ai; i+1) 2 . (ii) @i 0 such that i 2 and violation 2 L( i); (iii) pending 62 L( n) and f inal 2 L( n).
Condition (i) requires that the transitions in the path nd correspondence in the graph; (ii) requires that none of the states of the path violates a constraint; (iii) requires that the last state of the path does not contain pending conditions or unsatis ed commitments.
Given a legal path , of a labelled graph produced by Listing 1.1, we can prove its correctness w.r.t. the 2CL-GCM built on the same protocol speci cation. This actually corresponds to prove that is a path of the 2CL-GCM. Theorem 1 (Soundness). Let P = hRo; F; s0; A; Ci be a protocol; let G(P) be the corresponding labelled graph; let = h( 0; a0; 1); : : : ; ( n 1; an 1; n)i be a path; and let P = hS ; A; s0; ; G; Ci be the 2CL-GCM of P, where S is the set of states in and G is the set of states in that do not contains unsatis ed commitments. If is a legal path of G then is a path of P.
The proof is by contradiction. It is omitted for lack of space. 5
Let us now present the tool that we developed based on the technical framework, described in the previous sections. The tool supports the user in two di erent ways: (i) it features two graphical editors for specifying the protocol actions and the constraints; (ii) it generates di erent kinds of graphs for supporting the user in the analysis of the possible interactions and in understanding which of them are legal. The system is realized as an Eclipse plug-in, available at the URL http://di.unito.it/2cl.
The functionalities that the system supports can be grouped into three components: design, reasoning and visualization.
Design Component. The design component provides the tools that are
necessary for de ning the protocol. It supplies two editors: one for the de nition of
the actions and one for the de nition of constraints. The action de nition editor
is basically a text editor, where actions can be speci ed following the grammar
in [
Reasoning Component. The reasoning component consists of a Java Parser
and of the Prolog implementation of the commitment machine described in
Section 4. The former generates di erent kinds of graphs as well as the Prolog
program corresponding to the protocol speci cation. The latter is the input of
the Prolog implementation of the commitment machine for the generation of the
labelled graph. As explained, the labelled graph represents all the possible
interactions where each state is labelled according to the evaluation of the protocol
constraints. The graphical conventions is: (i) a state of violation is represented as
a red diamond, with an incoming red arrow (e.g. states 54, 57, 108 in Figure 1);
(ii) a state in which there is a pending condition is yellow (e.g. states 45, 53,
108); (iii) a state with a single outline, independently from the shape (e.g. 49,
57, 60), is a state that contains unsatis ed commitments; (iv) a state with a
double outline, independently from the shape, does not contain active commitments
(e.g. 41, 108). Graphical notations can be combined, e.g. a yellow diamond with
single outline is a state where there are unsatis ed active commitments, where a
constraint is violated and where there is a pending condition (e.g. 53, 57, 114).
Visualization Component. All the graphs produced by the reasoning
component can be visualized as images. Labelled graph, however, can be explored
by means of the tool Graph Explorer, which is realized in Java and relies on
iDot (Incremental Dot Viewer) { an open source project that uses the prefuse2
visualization framework for Dot graph display. The Graph Explorer supplies
different functionalities, like the visualization of the shortest path given a source
and a target state, and the visualisation of legal (or illegal) paths only. The user
can add or delete a node in a path; search a state starting from its label; and
search all the states that contain a certain fact or commitment. Moreover, the
tool allows the exploration of the graph one state at a time, by choosing which
node to expand. Figure 1 reports part of the labelled graph for NetBill.
Protocol Analysis. The tool can be used as a support in protocol analysis [
when specifying a protocol, to individuate which constraints to introduce but, with the help of the tool, it becomes easy to identify misbehaviours and revise the constraints so as to avoid them. Moreover, a designer can decide, by analysing the graph, to modify the speci cation so as to regiment some of the patterns expressed as constraints, or to remove some of them. For instance, considering the running example, from Figure 1 it is possible to infer that the protocol does not allow the customer to pay (sendEP O) before the merchant sends the goods. This is due to the constraint created(C(m; c; pay; receipt)) ^ goods . pay. If this behaviour was not in the intention of the designer, he/she can discover it and, e.g., relax the before constraint ( . ) transforming it into a co-existence ( ). If, instead, that is exactly the desired behaviour, one may decide to regiment sendEP O so as to enable the payment only after the goods have been sent.
The complete NetBill protocol encoding and the corresponding labelled graph
together with further examples (like CNet, OECD guidelines and MiFID [
This work provides an operational semantics of 2CL protocols [
Other approaches, are based on expectations and abductive logic
programming. Chesani et al. [
Concerning model checking, El-Menshawy et al. [
For what concerns the semantics of commitment protocols, the literature
proposes di erent formalizations. Some approaches present an operational
semantics that relies on commitment machines to specify and execute protocols
[