Verifying Compliance with Commitment Protocols.
Interaction protocols are specific, often standard, constraints on the behaviors of autonomous agents in a multiagent system. Protocols are essential to the functioning of open systems, such as those that arise in most interesting web applications. A variety of common protocols in negotiation and electronic commerce are best treated as commitment protocols, which are defined, or at least analyzed, in terms of the creation, satisfaction, or manipulation of the commitments among the participating agents.When protocols are employed in open environments, such as the Internet, they must be executed by agents that behave more or less autonomously and whose internal designs are not known. In such settings, therefore, there is a risk that the participating agents may fail to comply with the given protocol. Without a rigorous means to verify compliance, the very idea of protocols for interoperation is subverted. We develop an approach for testing whether the behavior of an agent complies with a commitment protocol. Our approach requires the specification of commitment protocols in temporal logic, and involves a novel way of synthesizing and applying ideas from distributed computing and logics of program.
Introduction
Interaction among agents is the distinguishing property of multiagent sys-
tems. However, ensuring that only the desirable interactions occur is one of
the most challenging aspects of multiagent system analysis and design. This
is especially so when the given multiagent system is meant to be used as an
open system, for example, in web-based applications.
Because of its ubiquity and ease of use, the web is rapidly becoming the
platform of choice for a number of important applications, such as trading,
supply-chain management, and in general electronic commerce. However, the
web can enforce few constraints on the agents' behavior. Current approaches
to security on the web emphasize how the different parties to a transaction
may be authenticated or how their data may be encrypted to prevent unauthorized
access. Even with authentication and controlled access, the parties
would have support beyond conventional protocol techniques (such as finite
state machine models) neither to specify the desired interactions nor to detect
any violation. However, authentication and access control are conceptually
orthogonal to ensuring that the parties behave and interact correctly. Even
when the parties are authenticated, they may act undesirably through error or
Venkatraman & Singh
malice. Conversely, the parties involved may resist going through authentica-
tion, but may be willing to be governed by the applicable constraints.
The web provides an excellent infrastructure through which agents can
communicate with one another. But the above problems are exacerbated when
agents are employed in the web. In contrast with traditional programs and in-
terfaces, neither their behaviors and interactions nor their construction is fixed
or under the control of a single authority. In general, in an open system, the
member agents are contributed by several sources and serve different inter-
ests. Thus, these agents must be treated as
autonomous-with few constraints on behavior, reflecting the independence
of their users, and
heterogeneous-with few constraints on construction, reflecting the independence
of their designers.
Effectively, the multiagent system is specified as a kind of standard that its
member agents must respect. In other words, the multiagent system can be
thought of as specifying a protocol that governs how its member agents must
act. For our purposes, the standard may be de jure as created by a standards
body, or de facto as may emerge from practice or even because of the arbitrary
decisions of a major vendor or user organization. All that matters for us is that
a standard imposes some restrictions on the agents. Consider the fish-market
protocol as an example of such a standard protocol [14].
Example 1. In the fish-market protocol, we are given agents of two roles: a
single auctioneer and one or more potential bidders. The fish-market protocol
is designed to sell fish. The seller or auctioneer announces the availability of
a bucket of fish at a certain price. The bidders gathered around the auctioneer
can scream back Yes if they are interested and No if they are not; they may
also stay quiet, which is interpreted as a lack of interest or No. If exactly one
bidder says Yes, the auctioneer will sell him the fish; if no one says Yes, the
auctioneer lowers the price; if more than one bidder says Yes, the auctioneer
raises the price. In either case, if the price changes, the auctioneer announces
the revised price and the process iterates.
Because of its relationship to protocols in electronic commerce and because it
is more general than the popular English and Dutch auctions, the fish-market
protocol has become an important one in the recent multiagent systems liter-
ature. Accordingly, we use it as our main example in this paper.
Because of the autonomy and heterogeneity requirements of open sys-
tems, compliance testing can be based neither on the internal designs of the
agents nor on concepts such as beliefs, desires, and intentions that map to internal
representations [16]. The only way in which compliance can be tested
aamas.tex; 20/02/1999; 16:40; no v.
Compliance with Commitment Protocols 3
is based on the behavior of the participating agents. The testing may be performed
by a central authority or by any of the participating agents. However,
the requirements for behavior in multiagent systems can be quite subtle. Thus,
along with languages for specifying such requirements, we need corresponding
techniques to test compliance.
1.1. COMMITMENTS IN AN OPEN ARCHITECTURE
There are three levels of architectural concern in a multiagent system. One
deals with individual agents; another deals with the systemic aspects of how
different services and brokers are arranged. Both of these have received much
attention in the literature. In the middle is the multiagent execution architec-
ture, which has not been as intensively studied within the community. An execution
architecture must ultimately be based on distributed computing ideas
albeit with an open flavor, e.g., [1, 5, 11]. A well-defined execution functionality
can be given a principled design, and thus facilitate the construction of
robust and reusable systems. Some recent work within multiagent systems,
e.g., Ciancarini et al. [8, 9] and Singh [18], has begun to address this level.
Much of the work on this broad theme, however, focuses primarily on co-
ordination, which we think of as the lowest level of interaction. Coordination
deals with how autonomous agents may align their activities in terms of what
they do and when they do it. However, there is more to interaction in gen-
eral, and compliance in particular. Specifically, interaction must include some
consideration of the commitments that the agents enter into with each other.
The commitments of the agents are not only base-level commitments dealing
with what actions they must or must not perform, but also metacommitments
dealing with how they will adjust their base-level commitments [20]. Commitments
provide a layer of coherence to the agents' interactions with each
other. They are especially important in environments where we need to model
any kind of contractual relationships among the agents.
Such environments are crucial wherever open multiagent systems must be
composed on the fly, e.g., in electronic commerce of various kinds on the
Internet. The addition of commitments as an explicit first-class object results
in considerable flexibility of how the protocols can be realized in changing
situations. We term such augmented protocols commitment protocols.
Example 2. We informally describe the protocol of Example 1 in terms of
commitments. When a bidder says Yes, he commits to buying the bucket of
fish at the advertised price. When the auctioneer advertises a price, he commits
that he will sell fish at that price if he gets a unique Yes. Neither commitment
is irrevocable. For example, if the fish are spoiled, the auctioneer
releases the bidder from paying for them. Specifying all possibilities in terms
of irrevocable commitments would complicate each commitment, but would
still fail to capture the practical meanings of such a protocol. For instance,
the auctioneer may not honor his offering price if a sudden change in weather
indicates that fishing will be harder for the next few days.
1.2. COMPLIANCE IN OPEN SYSTEMS
The existence of standardized protocols is necessary but not sufficient for the
correct functioning of open multiagent systems. We must also ensure that the
agents behave according to the protocols. This is the challenge of compliance.
However, unlike in traditional closed systems, verifying compliance in open
systems is practically and even conceptually nontrivial.
Preserving the autonomy and heterogeneity of agents is crucial in an open
environment. Otherwise, many applications would become infeasible. Con-
sequently, protocols must be specified as flexibly as possible without making
untoward requirements on the participating agents. Similarly, an approach for
testing compliance must not require that the agents are homogeneous or impose
stringent demands on how they are constructed.
Consequently, in open systems, compliance can be meaningfully expressed
only in terms of observable behavior. This leads to two subtle consid-
erations. One, although we talk in terms of behavior, we must still consider
the high-level abstractions that differentiate agents from other active objects.
The focus on behavior renders approaches based on mental concepts ineffective
[16]. However, well-framed social constructs can be used. Two, we must
clearly delineate the role of the observer who assesses compliance.
1.3. CONTRIBUTIONS
The approach developed here treats multiagent systems as distributed sys-
tems. There is an underlying messaging layer, which delivers messages asynchronously
and, for now, reliably. However, the approach assumes for simplicity
that the agents are not malicious and do not forge the timestamps on
the messages that they send or receive.
The compliance testing is performed by any observer of the system-
typically, a participating agent. Our approach is to evaluate temporal logic
specifications with respect to locally constructed models for the given ob-
server. The model construction proposed here employs a combination of the
notion of potential causality and operations on social commitments (both described
below). Our contributions are in
incorporating potential causality in the construction of local models
identifying patterns of messages corresponding to different operations on
commitments
showing how to verify compliance based on local information.
Compliance with Commitment Protocols 5
Our approach also has important ramifications on agent communication in
general, which we discuss in Section 4.
Organization. The rest of this paper is organized as follows. Section 2
presents our technical framework, which combines commitments, potential
causality, and temporal logic. Section 3 presents our approach for testing
(non-)compliance of agents with respect to a commitment protocol. Section 4
concludes with a discussion of our major themes, the literature, and the important
issues that remain outstanding.
2. Technical Framework
Commitment protocols as defined here are a multiagent concept. They are
far more flexible and general than commitment protocols in distributed computing
and databases, such as two-phase commit [12, pp. 562-573]. This is
because our underlying notion of commitment is flexible, whereas traditional
commitments are rigid and irrevocable. However, because multiagent systems
are distributed systems and commitment protocols are protocols, it is natural
that techniques developed in classical computer science will apply here.
Accordingly, our technical framework integrates approaches from distributed
computing, logics of program, and distributed artificial intelligence.
2.1. POTENTIAL CAUSALITY
The key idea behind potential causality is that the ordering of events in a
distributed system can be determined only with respect to an observer [13]. If
event e precedes event f with respect to an observer, then e may potentially
cause f . The observed precedence suggests the possibility of an information
flow from e to f , but without additional knowledge of the internals of the
agents, we cannot be sure that true causation was involved. It is customary
to define the local time of an agent as the number of steps it has executed. A
vector clock is a vector, each of whose elements corresponds to the local time
of each communicating agent. A vector v is considered later than a vector u
if v is later on some, and not sooner on any, element.
Definition 1. A clock over n agents is an n-ary vector
natural numbers. The starting clock is ~ 0 4
Notice that the vector representation is just a convenience. We could just as
well use pairs of the form hagent-id, local-timei, which would allow
us to model systems of varying membership more easily.
Definition 2. Given n-ary vectors u and v, u OE v if and only if
6 Venkatraman & Singh
Each agent starts at ~ 0. It increments its entry in that vector whenever it performs
a local event [15]. It attaches the entire vector as a timestamp to any
message it sends out. When an agent receives a message, it updates its vector
clock to be the element-wise maximum of its previous vector and the vector
timestamp of the message it received. Intuitively, the message brings news of
how far the system has progressed; for some agents, the recipient may have
better news already. However, any message it sends after this receive event
will have a later timestamp than the message just received.000000000111111111000000000000000000000000000111111111111111111111111111000000000000000000111111111111111111000000000000000000111111111111111111000000000111111111000000000111111111111111111
Auctioneer A Bidder B1 Bidder B2
[1,1,0]
[3,2,0]
money
fish

Figure

1. Vector clocks in the fish-market protocol.
Example 3. Figure 1 illustrates the evolution of vector timestamps for one
possible run of the fish-market protocol. In the run described here, the auctioneer
(A) announces a price of 50 for a certain bucket of fish. Bidders B1
and B2 both decline. A lowers the price to 40 and announces it. This time
leading A to transfer the fish to B1 and B1 to send money to A.
For uniformity, the last two steps are also modeled as communications. The
messages are labeled m i to facilitate reference from the text.
2.2. TEMPORAL LOGIC
The progression of events, which is inherent in the execution of any protocol,
suggests the need for representing and reasoning about time. Temporal logics
aamas.tex; 20/02/1999; 16:40; no v.
Compliance with Commitment Protocols 7
provide a well-understood means of doing so, and have been applied in various
subareas of computer science. Because of their naturalness in expressing
properties of systems that may evolve in more than one possible way and for
the efficiency of reasoning that they support, the branching-time logics have
been especially popular in this regard [10]. Of these, the best known is Computation
Tree Logic (CTL), which we adapt here in our formal language L.
Conventionally, a model of CTL is expressed as a tree. Each node in the tree
is associated with a state of the system being considered; the branches of the
tree or paths thus indicate the possible courses of events or ways in which the
system's state may evolve. CTL provides a natural means by which to specify
acceptable behaviors of the system.
The following Backus-Naur Form (BNF) grammar with a distinguished
start symbol L gives the syntax of L. L is based on a set \Phi of atomic propo-
sitions. Below, slant typeface indicates nonterminals; \Gamma! and j are meta-
symbols of BNF specification; - and AE delimit comments; the remaining
symbols are terminals. As is customary in formal semantics, we are only concerned
with abstract syntax.
L1. L \Gamma! Prop -atomic propositions: members of \Phi AE
L2.
L3. L \Gamma! L - L -conjunctionAE
L4. L \Gamma! A P -universal quantification over pathsAE
L5. L \Gamma! E P -existential quantification over pathsAE
L6. P \Gamma! L U L -until: operator over a single pathAE
The meanings of formulas generated from L are given relative to a model and
a state in the model. The meanings of formulas generated from P are given
relative to a path and a state on the path. The boolean operators are standard.
Useful abbreviations include false j (p -:p), for any p 2 \Phi, true j :false,
q. The temporal operators A and E
are quantifiers over paths. Informally, pUq means that on a given path from
the given state, q will eventually hold and p will hold until q holds. Fq means
"eventually q" and abbreviates trueUq. Gq means "always q" and abbreviates
:F:q. Therefore, EpUq means that on some future path from the given state,
q will eventually hold and p will hold until q holds.
is a formal model for L. S is a set of states;
S \Theta S is a partial order indicating branching time, and I : S 7! P (\Phi) is
an interpretation, which tells us which atomic propositions are true in a given
state. For t 2 S, P t is the set of paths emanating from t.
at t" and M
p at t along path P ."
M1. M
M2. M
M3. M
M4. M
M5. M
q and
The above is an abstract semantics. In Section 3.3, we specify the concrete
form of \Phi, S, !, and I, so the semantics can be exercised in our computations.
3. Approach
In their generic forms, both causality and temporal logic are well-known.
However, applying them in combination and in the particular manner suggested
here is novel to this paper.
Temporal logic model checking is usually applied for design-time reasoning
[10, pp. 1042-1046]. We are given a specification and an implementation,
i.e., program, that is supposed to meet it. A model is generated from the pro-
gram. A model checking algorithm determines whether the specification is
true in the generated model. However, in an open, heterogeneous environ-
ment, a design may not be available at all. For example, the vendors who
supply the agents may consider their designs to be trade secrets.
By contrast, ours is a run-time approach, and can meaningfully apply
model checking even in open settings. This is because it uses a model generated
from the joint executions of the agents involved. Model checking in this
setting simply determines whether the present execution satisfies the specifi-
cation. If an execution respects the given protocol, that does not entail that all
executions will, because an agent act inappropriately in other circumstances.
However, if an execution is inappropriate, that does entail that the system
does not satisfy the protocol. Consequently, although we are verifying specific
executions of the multiagent system, we can only falsify (but not verify)
the correctness of the construction of the agents in the system.
Model checking of the form introduced above may be applied by any observer
in the multiagent system. A useful case is when the observer is one
of the participating agents. Another useful case is when the observer is some
aamas.tex; 20/02/1999; 16:40; no v.
Compliance with Commitment Protocols 9
agent dedicated to the task of managing or auditing the interactions of some
of the agents in the multiagent system.
Potential causality is most often applied in distributed systems to ensure
that the messages being sent in a system satisfy causal ordering [3]. Causality
motivates vector clocks and vector timestamps on messages, which help
ensure correct ordering by having the messaging subsystem reorder and re-transmit
messages as needed. This application of causality can be important,
but is controversial [4, 6], because its overhead may not always be justifiable.
In our approach, the delivery of messages may be noncausal. However,
causality serves the important purpose of yielding accurate models of the observations
of each agent. These are needed, because in a distributed system,
the global model is not appropriate. Creating a monolithic model of the execution
of the entire system requires imposing a central authority through
which all messages are routed. Adding such an authority would take away
many of the advantages that make distributed systems attractive in the first
place. Consequently, our method of constructing and reasoning with models
should
not require a centralized message router
\Gamma work from a single vantage of observation, but be able to handle situations
where some agents pool their evidence.
Such a method turns out to naturally employ the notion of potential causality.
3.1. MODELS FROM OBSERVATIONS
The observations made by each agent are essentially a record of the messages
it has sent or received. Since each message is given a vector timestamp, the
observations can be partially ordered. In general, this order is not total, because
messages received from different agents may be mutually unordered.
Example 4. Figure 2 shows the models constructed locally from the observations
of the auctioneer and a bidder in the run of Example 3.
Although a straightforward application of causality, the above example shows
how local models may be constructed. Some subtleties are discussed next.
As remarked above, commitments give the core meaning of a protocol.
Our approach builds on a flexible and powerful variety of social commit-
ments, which are the commitments of one agent to another [20]. These commitments
are defined relative to a context, which is typically the multiagent
system itself. The debtor refers to the agent that makes a commitment, and
the creditor to the agent who receives the commitment. Thus we have the
following logical form.
[1,0,0]
[3,2,0]
[1,0,0]
[1,2,0]
Auctioneer A Bidder B1
start
start

Figure

2. Observations for auctioneer and a bidder in the fish-market protocol.
Definition 4. A commitment is an expression C(x; G; p), where x is the
debtor, y the creditor, G the context, and p the condition committed to.
The expression c is considered true in states where the corresponding commitment
exists.
Definition 5. A commitment G; p) is base-level if p does not refer
to any other commitments; c is a metacommitment if p refers to a base-level
commitment (we do not consider higher-order commitments here).
Intuitively, a protocol definition is a set of metacommitments for the different
roles (along with a mapping of the message tokens to operations on commit-
ments). In combination with what the agents communicate, these lead to base-level
commitments being created or manipulated, which is primarily how a
commitment may be referred to within a protocol. The violation of a base-level
commitment can give us proof or the "smoking gun" that an agent is
noncompliant.
The following operations on commitments define how they may be created
or manipulated. When we view commitments as an abstract data type,
the operations are methods of that data type.
Each operation is realized through a simple message pattern, which states
what messages must be communicated among which of the participants and
in what order. For the operations on commitments we consider, the patterns
aamas.tex; 20/02/1999; 16:40; no v.
Compliance with Commitment Protocols 11
are simple. As described below, most patterns require only a single message,
but some require three messages. Obeying the specified patterns ensures that
the local models have the information necessary for testing compliance. That
the given operation can be performed at all depends on whether the proto-
col, through its metacommitments, allows that operation. However, when an
operation is allowed, it affects the agents' commitments. For simplicity, we
assume that the operations on commitments are given a deterministic inter-
pretation. Here z is an agent and G; p) is a commitment.
O1. Create(x; c) instantiates a commitment c. Create is typically performed
as a consequence of the commitment's debtor promising something contractually
or by the creditor exercising a metacommitment previously
made by the debtor. Create usually requires a message from the debtor
to the creditor.
O2. Discharge(x; c) satisfies the commitment c. It is performed by the debtor
concurrently with the actions that lead to the given condition being sat-
isfied, e.g., the delivery of promised goods or funds. For simplicity, we
treat the discharge actions as performed only when the proposition p is
true. Thus the discharge actions are detached, meaning that p can be
treated as true in the given moment. We model the discharge as a single
message from the debtor to the creditor.
O3. Cancel(x; c) revokes the commitment c. It can be performed by the
debtor as a single message. At the end of this action, :c usually holds.
However, depending on the existing metacommitments, the cancel of one
commitment may lead to the create of other commitments.
O4. Release(G; c) or release(y; c) essentially eliminates the commitment c.
This is distinguished from both discharge and cancel, because release
does not mean success or failure, although it lets the debtor off the hook.
At the end of this action, :c usually holds. The release action may be
performed by the context or the creditor of the given commitment, also
as a single message. Because release is not performed by the debtor,
different metacommitments apply than for cancel.
O5. Delegate(x; z; c) shifts the role of debtor to another agent within the
same context, and can be performed by the (old) debtor (or the context).
G; p). At the end of the delegate action, c 0 - :c holds.
To prevent the risk of miscommunication, we require the creditor to also
be involved in the message pattern. Figure 3(l) shows the associated pat-
tern. The first message sets up the commitment c from x to y and is not
part of the pattern. When x delegates the commitment c to z, x tells both
y and z that the commitment is delegated. z is now committed to y. Later
aamas.tex; 20/02/1999; 16:40; no v.
delegate(x,z,c)
y z x y z
assign(y,z,c)
create(x,c)
assign(y,z,c)
delegate(x,z,c)
discharge(x,c)
discharge(x,c)
x
create(x,c)

Figure

3. Message pattern for delegate (l) and assign (r).
z may discharge the commitment. The two delegate messages constitute
the pattern.
O6. Assign(y; z; c) transfers a commitment to another creditor within the
same context, and can be performed by the present creditor or the con-
text. Let c G; p). At the end of the assign action, c 0 -:c holds.
Here we require that the new creditor and the debtor are also involved as
shown in Figure 3(r). The figure shows only the general pattern. Here x
is committed to y. When y assigns the commitment to z, y tells both x
and z (so z knows it is the new creditor). Eventually, x should discharge
the commitment to z. A potentially tricky situation is if x discharges the
commitment c even as y is assigning c to z (i.e., the messages cross).
In this case, we require y to discharge the commitment to z-essentially
by forwarding the contents of the message from x. Thus the worst case
requires three messages.
We write the operations as propositions indicating successful execution.
Based on the applicable metacommitments, each operation may entail additional
operations that take place implicitly.
Definition 6. A commitment c is resolved through a release, discharge, can-
cel, delegate, or assign performed on c. c ceases to exist when resolved. How-
ever, a new commitment is created for delegate or assign.
(New commitments created because of some existing metacommitment are
not included in the definition of resolution. Theorem 1 states that the creditor
knows the disposition of any commitments due to it. This result helps establish
that the creditor can always determine compliance of others relative to
what was committed to it.
Compliance with Commitment Protocols 13
Theorem 1. If message m i creates commitment c and message m j resolves
c, then the creditor of c sees both m i and m j .
Proof. By inspection of the message patterns constructed for the various operations
on commitments.
Definition 7. A commitment c is ultimately resolved through a release, dis-
charge, or cancel performed on c, or through the ultimate resolution of any
commitments created by the delegate or assign of c.
Theorem 2 essentially states that the creation and ultimate resolution of a
commitment occur along the same causal path. This is important, because
it legitimizes a significant optimization below. Indeed, we defined the above
message patterns so we would obtain Theorem 2.
Theorem 2. If message m i creates commitment c and message m j ultimately
resolves
Proof. By inspection of the message patterns constructed for the various operations
on commitments.
3.2. SPECIFYING PROTOCOLS
We first consider the coordination and then the commitment aspects of com-
pliance. A skeleton is a coarse description of how an agent may behave [18].
A skeleton is associated with each role in the given multiagent system to
specify how an agent playing that role may behave in order to coordinate
with others. Coordination includes the simpler aspects of interaction, e.g.,
turn-taking. Coordination is required so that the agents' commitments make
sense. For instance, a bidder should not make a bid prior to the advertise-
ment; otherwise, the commitment content of the bid would not even be fully
defined.
The skeletons may be constructed by introspection or through the use of
a suitable methodology [19]. No matter how they are created, the skeletons
are the first line of compliance testing, because an agent that does not comply
with the skeleton for its role is automatically in violation. So as to concentrate
on commitments in this paper, we postulate that a "proxy" object is interposed
between an agent and the rest of the system and ensures that the agent follows
the dictates of the skeleton of its role.
We now define the syntax of the specification language through the following
whose start symbol is Protocol. The braces f and g indicate
that the enclosed item is repeated 0 or more times.
L7. Protocol \Gamma! fMetag fMessageg
aamas.tex; 20/02/1999; 16:40; no v.
14 Venkatraman & Singh
L8. Message \Gamma! Token: Commitment -messages correspond to
L9. Meta \Gamma! C(Debtor, Creditor, Context, MetaProp)
L11. Bool \Gamma! -Boolean combinations ofAE Act j Commitment j Dom
L12. Act \Gamma! Operation(Agent, Commitment)
L13. Operation \Gamma! -the six operations of Section 3.1AE
L14. Commitment \Gamma! Meta j C(Debtor, Creditor, Context, AFDom)
L15. Dom \Gamma! -domain-specific conceptsAE
The above language embeds a subset of L. Our approach is to detach the outer
actions and commitments, so we can process the inner L part as a temporal
logic. By using commitments and actions on them, instead of simple domain
propositions, we can capture a variety of subtle situations, e.g., to distinguish
between release and cancel both of which result in the given commitment
being removed.
Example 5 applies the above language on the fish-market protocol.
Example 5. The messages in Figure 1 can be given a content based on the
following definitions. Here FM is the fish-market context.
proposition meaning the fish is delivered
proposition meaning that the appropriate money is
paid (subscripted to allow different prices)
an abbreviation for
))])-meaning the bidder
promises to pay money i if given the fish
an abbreviation for
AFfish))])-meaning the auctioneer offers
to deliver the fish if he gets a bid for money i
an abbreviation for
))-meaning that at least two bidders have bid for the fish
at price i
proposition meaning the fish is spoiled
Armed with the above, we can now state the commitments associated with
the different messages in the fish market protocol.
Compliance with Commitment Protocols 15
Payment of i from
Delivering fish to
\Gamma Yes from B j (for price i): create(B
\Gamma No from B j (for price i): true
Further, the protocol includes metacommitments that are not associated with
any single message. In the present protocol, these metacommitments are of
the context itself to release a committing party under certain circumstances.
For practical purposes, we could treat these as metacommitments of the creditor

Bad
In addition, in a monotonic framework, we would also need to state the completion
requirements to ensure that only the above actions are performed.
The auctioneer does not commit to a price if no bid is received. If more
than one bid is received, the auctioneer is released from the commitment. Notice
that the auctioneer can exit the market or adjust the price in any direction
if a unique Yes is not received for the current price money i . It would neither
be rational for the auctioneer to raise the price if there are no takers at
the present price, nor to lower the price if takers are available. However, the
protocol per se does not legislate against either behavior.
The No messages have no significance on commitments. They serve only to
assist in the coordination so the context can determine if enough bids are
received. The lower-level aspects of coordination are not being studied in this
paper. Now we can see how the reasoning takes place in a successful run of
the protocol.
Example 6. The auctioneer sends out an advertisement, which commits
the auctioneer to supplying the fish if he receives a suitable
bid. This commitment will be discharged if AG[Bid i (B
holds. When Bid i (B j ) is sent by B j ,
the bidder is committed to the bid, which is discharged if AG[fish !
holds. To discharge the adver-
tisement, the auctioneer must eventually create a commitment to eventually
supply the fish. If he does not create this commitment, he is in violation. If he
aamas.tex; 20/02/1999; 16:40; no v.
Venkatraman & Singh
creates it, but does not supply the fish, he is still in violation. If he supplies
the fish, the bidder is then committed to eventually forming a commitment to
supply the money. If the bidder does so, the protocol is executed successfully.
3.3. REASONING WITH THE CONCRETE MODEL
Now we explain the main reasoning steps in our approach and show that they
are sound. The main reasoning with models applies the CTL model-checking
algorithm on a model and a formula denoting the conjunction of the specifi-
cations. The algorithm evaluates whether the formula holds in the initial state
of the model. Thus a concrete version of the model M (see Section 2.2) is es-
sential. For the purposes of the semantics, we must define a global model with
respect to which commitment protocols may be specified. Intuitively, a protocol
specification tells us which behaviors of the entire system are correct.
Thus, it corresponds naturally to a global model in which those behaviors can
be defined.
Our specific concrete model identifies states with messages. Recall that
the timestamp of a message is the clock vector attached to it. The states are
ordered according to the timestamps of the messages. The proposition true
in a state is the one corresponding to the operation that is performed by the
message.
Definition 8.
Definition 9. For s;
Definition 10. For s 2 Q, operations executed by message sg
The structure is a quasimodel. (Here and below, we assume
that ! and I are appropriately projected to the available states.) MQ is structurally
a model, because it matches the requirements of Definition 3. How-
ever, MQ is not a model of the computations that may take place, because the
branches in MQ are concurrent events and do not individually correspond to a
single path. A quasimodel can be mapped to a model, M with an
initial state ~ 0, by including all possible interleavings of the transitions. That
is, S would include a distinct state for every message in each possible ordering
of the messages in Q that is consistent with the temporal order ! of MQ .
The relation ! can be suitably defined for M S . However, there is potentially
an exponential blowup in that the size of S may be exponentially greater than
the size of Q.
Theorem 3 shows that naively treating a quasimodel as if it were a model is
correct. Thus, the above blowup can be eliminated entirely. Our construction
aamas.tex; 20/02/1999; 16:40; no v.
Compliance with Commitment Protocols 17
ensures that all the events relevant to another event are totally ordered with
respect to each other. Notice that, as showing in Figure 3, the construction
may appear to require one more message than necessary for the assign and
delegate operations. This linear amount of extra work (for the entire set of
messages), however, pays off in reducing the complexity of our reasoning
algorithm. In the following, p refers to the proposition (of the form AG[q !
AFr]) of a metacommitment, which becomes true when the metacommitment
is discharged.
Definition 11. For a proposition p, p T is the proposition obtained by substituting
EF for AF in p.
Theorem 3. MQ
p.
Proof. From Theorem 2 and the restricted structure of MQ .
The above results show that compliance can be tested and without blowing
up the model unnecessarily. However, we would like to test for compliance
based on local information-so that any agent can decide for itself whether
it has been wronged by another. For this reason, we would like to be able to
project the global model onto local models for each agent, while ensuring that
the local models carry enough information that they are indeed usable in isolation
from other local models. Accordingly, we can define the construction
of local models corresponding to an agent's observations. This is simply by
defining a subset of S for a given agent a.
Definition 12. S a is a message from or to ag. M a = hS a ; !; Ii.
Theorem 4 shows that if we restrict attention to commitments that the given
agent can observe, then the projected quasimodel yields all and only the correct
conclusions relative to the global quasimodel. Thus, if the interested party
is vigilant, it can check if anyone else violated the protocol.
Theorem 4. M a
only if MQ
that a sees all
the commitments mentioned in p.
Proof. From Theorem 2 and the construction of M a .
Example 7. If one of the bidders backs down from a successful bid, the auctioneer
immediately can establish that he is cheating, because the auctioneer
is the creditor for the bidder's commitment. However, a bidder cannot ordinarily
decide whether the auctioneer is noncompliant, because the bidder
does not see all relevant commitments based on which the auctioneer may be
released from a commitment to the bidder.
Theorem 5 lifts the above results to sets of agents. Thus, a set of agents may
pool their evidence in order to establish whether a third party is noncompliant.
Venkatraman & Singh
Thus, in a setting with two bidders, a model that includes all their evidence
can be used to determine whether the auctioneer is noncompliant. Ordinarily,
the bidders would have to explicitly pool their information to do so. However,
in a broadcast-based or outcry protocol (like a traditional fish market in which
everyone is screaming), the larger model can be built by anyone who hears
all the messages. Let A be a set of agents.
Definition 13.
a2A S a .
Theorem 5. Let the commitments observed by agents in A include all the
commitments in p. Then MA
Proof. From Theorem 2 and the construction of MA .
Information about commitments that have been resolved, i.e., are not
pending, is not needed in the algorithm, and can be safely deleted from each
observer's model. This is accomplished by searching backward in time whenever
something is added to the model. Pruning extraneous messages from
each observer's model reduces the size of the model and facilitates reasoning
about it. This simplification is sound, because the CTL specifications do not
include nested commitments.
Mapping from an event-based to a state-based representation, we should
consider every event as potentially corresponding to a state change. This approach
would lead to a large model, which accommodates not only the occurrence
of public events such as message transmissions, but also local events.
Such an approach would thus capture the evolution of the agent's knowledge
about the progress of the system, which would help in accommodating unreliable
messaging. Our approach, as described above, loses some of the agents'
knowledge by not separating events and states, but has all the details we need
to assess compliance assuming reliable messaging.
4. Discussion
Given the autonomy and heterogeneity of agents, the most natural way to treat
interactions is as communications. A communication protocol involves the
exchange of messages with a streamlined set of tokens. Traditionally, these
tokens are not given any meaning except through reference to the beliefs or
intentions of the communicating agents. By contrast, our approach assigns
public, i.e., observable, meanings in terms of social commitments. Viewed in
this light, every communication protocol is a commitment protocol.
Formulating and testing compliance of autonomous and heterogeneous
agents is a key prerequisite for the effective application of multiagent systems
in open environments. As asserted by Chiariglione, minimal specifications
based on external behavior will maximize interoperability [7]. The research
Compliance with Commitment Protocols 19
community has not paid sufficient attention to this important requirement. A
glaring shortcoming of most existing semantics for agent communication languages
is their fundamental inability to allow testing for the compliance of an
agent [16, 22]. The present approach shows how that might be carried out.
While the purpose of the protocols is to specify legal behavior, they should
not specify rational behavior. Rational behavior may result as an indirect consequence
of obeying the protocols. However, not adding rationality requirements
leads to more succinct specifications and also allows agents to participate
even if their rationality cannot be established by their designers.
The compliance checking procedure can be used by any agent who participates
in, or observes, a commitment protocol. There are two obvious uses.
One, the agent can track which of the commitments made by others are pending
or have been violated. Two, it might track which of its own commitments
are pending or whose satisfaction has not been acknowledged by others. The
agent can thus use the compliance checking procedure as an input to its normal
processes of deliberation to guide its interactions with other agents.
We have so far discussed how to detect violations. Once an agent detects
a violation, as far as the above method is concerned, it may proceed in any
way. However, some likely candidates are the following. The wronged agent
may
inform the agents who appeared to have violated their commitments and
ask them to respect the applicable metacommitments
inform the context, who might penalize the guilty parties, if any; the context
may require additional information, e.g., certified logs of the messages
sent by the different agents, to establish that some agents are in
violation.
agents in an attempt to spoil the reputation of the guilty
parties.
4.1. LITERATURE
Some of the important strands of research of relevance to commitment protocols
have been carried out before. However, the synthesis, enhancement,
and application of these techniques on multiagent commitment protocols is a
novel contribution of this paper. Interaction (rightly) continues to draw much
attention from researchers. Still, most current approaches do not consider an
explicit execution architecture (however, there are some notable exceptions,
e.g., [8, 9, 18]). Other approaches lack a formal underpinning; still others
focus primarily on monolithic finite-state machine representations for proto-
cols. Such representations can capture only the lowest levels of a multiagent
Venkatraman & Singh
interaction, and their monolithicity does not accord well with distributed execution
and compliance testing. Model checking has recently drawn much attention
in the multiagent community, e.g., [2, 17]. However, these approaches
consider knowledge and related concepts and are thus not directly applicable
for behavior-based compliance.
4.2. FUTURE DIRECTIONS
The present approach highlights the synergies between distributed computing
and multiagent systems. Since both fields have advanced in different direc-
tions, a number of important technical problems can be addressed by their
proper synthesis. One aspect relates to situations where the agents may suffer
a Byzantine failure or act maliciously. Such agents may fake messages or
deny receiving them. How can they be detected by the other agents? Another
aspect is to capture additional structural properties of the interactions so that
noncompliant agents can be more readily detected. Alternatively, we might
offer an assistance to designers by synthesizing skeletons of agents who participate
properly in commitment protocols. Lastly, it is well-known that there
can be far more potential causes than real causes [15]. Can we analyze conversations
or place additional, but reasonable, restrictions on the agents that
would help focus their interactions on the true relationships between their
respective computations? We defer these topics to future research.

Acknowledgements

This work is supported by the National Science Foundation under grants IIS-
9529179 and IIS-9624425, and IBM corporation. We are indebted to Feng
Wan and Sudhir Rustogi for useful discussions and to the anonymous reviewers
for helpful comments.



--R

Concurrent programming for distributed artificial intelligence.
Model checking multi-agent systems
The process group approach to reliable distributed computing.
A response to Cheriton and Skeen's criticism of causal and totally ordered communication.
Coordination languages and their significance.
Understanding the limitations of causally and totally ordered communication.
Foundation for intelligent physical agents
PageSpace: An architecture to coordinate distributed applications on the web.
Coordinating multiagent applications on the WWW: A reference architecture.
Temporal and modal logic.
Interacting Processes: A Multiparty Approach to Coordinated Distributed Programming.
Transaction Processing: Concepts and Techniques.


Detecting causal relationships in distributed computations: In search of the holy grail.
Agent communication languages: Rethinking the principles.
Applying the mu-calculus in planning and reasoning about action
A customizable coordination service for autonomous agents.
Developing formal specifications to coordinate heterogeneous autonomous agents.
An ontology for commitments in multiagent systems: Toward a unification of normative concepts.
Gerhard Wei-
Verifiable semantics for agent communication languages.
--TR

--CTR
Manfred A. Jeusfeld , Paul W. P. J. Grefen, Detection tests for identifying violators of multi-party contracts, ACM SIGecom Exchanges, v.5 n.3, p.19-28, April 2005
Ashok U. Mallya , Michael N. Huhns, Commitments Among Agents, IEEE Internet Computing, v.7 n.4, p.90-93, July
Amit K. Chopra , Munindar P. Singh, Contextualizing commitment protocol, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Jeremy Pitt , Frank Guerin , Chris Stergiou, Protocols and intentional specifications of multi-party agent conversions for brokerage and auctions, Proceedings of the fourth international conference on Autonomous agents, p.269-276, June 03-07, 2000, Barcelona, Spain
Feng Wan , Munindar P. Singh, Formalizing and achieving multiparty agreements via commitments, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Nicoletta Fornara , Marco Colombetti, Operational specification of a commitment-based agent communication language, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy
Feng Wan , Munindar P. Singh, Enabling Persistent Web Services via Commitments, Information Technology and Management, v.6 n.1, p.41-60, January   2005
Pinar Yolum , Munindar P. Singh, Flexible protocol specification and execution: applying event calculus planning using commitments, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy
Ashok U. Mallya , Munindar P. Singh, Modeling exceptions via commitment protocols, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Lai Xu, A multi-party contract model, ACM SIGecom Exchanges, v.5 n.1, p.13-23, July, 2004
Pinar Yolum, Towards design tools for protocol development, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Jeremy Pitt , Lloyd Kamara , Marek Sergot , Alexander Artikis, Formalization of a voting protocol for virtual organizations, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
Pnar Yolum, Design time analysis of multiagent protocols, Data & Knowledge Engineering, v.63 n.1, p.137-154, October, 2007
Chrysanthos Dellarocas , Mark Klein , Juan Antonio Rodriguez-Aguilar, An exception-handling architecture for open electronic marketplaces of contract net software agents, Proceedings of the 2nd ACM conference on Electronic commerce, p.225-232, October 17-20, 2000, Minneapolis, Minnesota, United States
Frank Guerin, Applying game theory mechanisms in open agent systems with complete information, Autonomous Agents and Multi-Agent Systems, v.15 n.2, p.109-146, October   2007
Peter McBurney , Simon Parsons, Posit spaces: a performative model of e-commerce, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
Lalana Kagal , Tim Finin, Modeling conversation policies using permissions and obligations, Autonomous Agents and Multi-Agent Systems, v.14 n.2, p.187-206, April     2007
Pnar Yolum , Munindar P. Singh, Reasoning about Commitments in the Event Calculus: An Approach for Specifying and Executing Protocols, Annals of Mathematics and Artificial Intelligence, v.42 n.1-3, p.227-253, September 2004
Munindar P. Singh, Synthesizing Coordination Requirements for Heterogeneous Autonomous Agents, Autonomous Agents and Multi-Agent Systems, v.3 n.2, p.107-132, June 2000
Phillipa Oaks , Arthur Hofstede, Guided interaction: A mechanism to enable ad hoc service interaction, Information Systems Frontiers, v.9 n.1, p.29-51, March     2007
Chihab Hanachi , Christophe Sibertin-Blanc, Protocol Moderators as Active Middle-Agents in Multi-Agent Systems, Autonomous Agents and Multi-Agent Systems, v.8 n.2, p.131-164, March 2004
protocols;formal methods;commitments;causality;temporal logic