# clouseau_generating_communication_protocols_from_commitments__f7b2ef8f.pdf

The Thirty-Fourth AAAI Conference on Artiﬁcial Intelligence (AAAI-20)

Clouseau: Generating Communication Protocols from Commitments

Munindar P. Singh North Carolina State University Raleigh, NC 27695-8206, USA singh@ncsu.edu

Amit K. Chopra Lancaster University Lancaster LA1 4WA, United Kingdom amit.chopra@lancaster.ac.uk

Engineering a decentralized multiagent system (MAS) requires realizing interactions modeled as a communication protocol between autonomous agents. We contribute Clouseau, an approach that takes a commitment-based speciﬁcation of an interaction and generates a communication protocol amenable to decentralized enactment. We show that the generated protocol is (1) correct realizes all and only the computations that satisfy the input speciﬁcation; (2) safe ensures the agents local views remain consistent; and (3) live ensures the agents can proceed to completion.

1 Introduction Any application where stakeholders collaborate or compete while retaining their autonomy, such as in ﬁnance, healthcare, and the Internet of Things, may be naturally understood as a decentralized multiagent system (MAS). Engineering a MAS presupposes a means to ensure that the agents interoperate even though their internal representations and decision making are hidden from each other. This paper uniﬁes two core aspects of interoperation. One, operational or how the agents realize their interactions. A communication protocol speciﬁes what messages an agent may send or receive, and when (Bauer, M uller, and Odell 2000). To reduce coupling, interactions must be asynchronous, i.e., no agent blocks for another except to receive essential information. Recent MAS platforms (Boissier et al. 2019) and protocol approaches (Ferrando et al. 2019; Singh 2011) support asynchrony. Two, meanings or the social import of an interaction. We must represent the meanings formally and independently of agent construction, such that the agents can reason about meanings of interactions and agree on the outcomes upon observing the same events. Social commitments (Singh 1991; 1999; Fornara and Colombetti 2003; Marengo et al. 2011; Chesani et al. 2013) provide high-level meanings to messages, providing an operations-independent standard of correctness. For example, Alice (a merchant), may commit to Bob (a customer) to send Bob some goods if he pays. Now if Bob pays, the commitment is discharged only if Alice sends the goods. Whereas a protocol offers a clear operational interface for agents, commitments capture the meanings of interactions.

Copyright 2020, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

Current MAS approaches separately specify meanings and protocols, which (1) creates a burden of maintaining the consistency of two speciﬁcations and (2) leads to inﬂexible protocols because manually operationalizing meanings under decentralization is nontrivial. Clouseau, our approach, provides a new way to operationalize commitments by compiling meanings into ﬂexible protocols that can be enacted by agents using asynchronous messaging over unordered channels. This is a signiﬁcant advance over existing approaches, which lack such a capability. In particular, Clouseau produces correct and ﬂexible protocols, thereby avoiding the above limitations.

Contribution: Operationalizing Commitments How can we automatically generate a communication protocol based on commitments, thereby bridging the gap between meanings and protocols that beneﬁt from asynchronous messaging? A desirable protocol would (1) enable computing commitment states; (2) ensure alignment of the agents with respect to the commitments; (3) be ﬂexible, i.e., allow as many interactions as possible given the commitments and the capabilities of the agents. Accordingly, we contribute a speciﬁcation comprising (1) a domain information model; (2) roles to be played by the interacting agents; (3) commitments between these roles in terms of the information model; (4) capabilities of the roles; and (5) description of satisfactory completion (an event expression). This input provides the essential knowledge for capturing meanings computationally. This language augments Cupid (Chopra and Singh 2015a) with agent capabilities, which help capture how an agent may enact a protocol. Crucially, we reformulate the semantics of Cupid to a decentralized model. We adopt as output information-based protocols (Singh 2011) that express causality and integrity properties in information. An output protocol captures all legitimate decentralized enactments, thereby offering ﬂexible agent interaction. Our overarching contribution is a method to generate a protocol from a commitment speciﬁcation. We show that a generated protocol is (1) correct, that is, it supports exactly the computations of the speciﬁcation, (2) safe, in the sense that local views of agents remain consistent despite decentralization and asynchronous enactment, and (3) live, ensuring that agents can proceed to completion.

BUYER, SELLER: rfq(item)

SELLER, BUYER: quote(item, price)

SELLER, BUYER: quote(price, item)

BUYER, SELLER: accept(price, item)

BUYER, SELLER: reject(price, item)

SELLER, BUYER: deliver(item)

BUYER, SELLER: pay(price)

SELLER, BUYER: deliver(item)

SELLER, BUYER: receipt(cipher)

BUYER, SELLER: pay(price)

SELLER, BUYER: receipt(cipher)

SELLER, BUYER: deliver(item)

Figure 1: Finite state machine representations of Net Bill. The solid lines describe the original Net Bill. The dashed lines show some possible generalizations that follow trivially from commitments.

2 Net Bill and Commitments

We adopt Net Bill (Sirbu 1997), a protocol for trading digital media, as a familiar running example (Yolum and Singh 2002a; Winikoff, Liu, and Harland 2005). Figure 1 shows Net Bill as a ﬁnite state machine (FSM) whose transitions are labeled with messages (SENDER, RECEIVER: content). Net Bill begins with an rfq (request for quotes) message from BUYER to SELLER for an item (transition from s0 to s1), who responds to BUYER with a quote including the price of item (transition from s1 to s2). If BUYER sends a reject in response (transition from s2 to s3), the protocol ends, indicated by the double circle on s3. Otherwise, if BUYER sends an accept (transition from s2 to s4), SELLER sends a deliver to BUYER, including item in an encrypted format (transition from s4 to s5). After receiving deliver, BUYER sends pay (i.e., an electronic cheque) to SELLER (transition from s5 to s6). After receiving pay, SELLER sends a receipt to BUYER including cipher to decrypt the item (transition from s6 to s7), and the protocol ends.

3 Specifying Interactions using Clouseau

Net Bill includes only two (i.e., accept and reject) branches. We could enhance its ﬂexibility by including, e.g., the dashed edges in Figure 1 whereby SELLER may send an unsolicited quote and BUYER may pay in advance. But how would we establish that any path, original or added, is legitimate? The idea behind using commitments (Yolum and Singh 2002b) is to express the meaning of an interaction formally and thereby to ensure that all and only the legitimate interactions are realized. Given commitments, paths where the commitments are not violated can be included in the protocol without fear of violating a business

Table 1: Syntax of Clouseau s input speciﬁcation.

Spec S {roles RR+ Base+ Commit+ Cap+ Comp} Base event B( A opt +) key A + Commit commitment C R to R create Ev detach Ev discharge Ev release Ev Cap capability R B with fresh A + Comp completion Ev Ev B [ Time, Time] | Life C [ Time, Time] | Ev and Ev | Ev or Ev | Ev except Ev Time T | B + T Life created | detached | discharged | released | expired | violated| done

requirement. A major beneﬁt is raising the level of abstraction from operations to meanings. (Clouseau supports event expressions as completion requirements.) Clouseau provides a way to generate a protocol that retains the ﬂexibility of a meaning-level speciﬁcation thus obviating the need for manual design of a protocol.

3.1 Syntax of Clouseau Speciﬁcations A Clouseau speciﬁcation comprises (1) a set of roles; (2) an information schema of base events over lists of attributes; (3) commitments between the roles over the events; (4) each role s capabilities, i.e., which events a role can bring about and attribute bindings it can set; and (5) a completion event expression. Cupid (Chopra and Singh 2015a) has (2) and (3); Clouseau adds (1), (4), and (5). Table 1 shows Clouseau s surface syntax. Here, indicates a production, and | indicates choice. A + indicates one or more repetitions. indicate optionality. A , B, C , R, and S are sets of (terminal) attributes, base events, commitments, roles, and speciﬁcation names. T = N is a set of time instances. ([ ] are terminals that identify time intervals.) We write , , and for and, or, and except, respectively. Listing 1 speciﬁes Net Bill based on Yolum and Singh (2002b). Lines 4 10 show base event schemas, each a relation over its attributes. Some attributes form a key. A timestamp attribute is implicit. For example, rfq has attributes n ID (its key) and item. Each instance of rfq is a tuple of values for its attributes that is unique for its value of n ID.

Listing 1: Speciﬁcation of Net Bill in Clouseau.

1 Net Bill F l e x i b l e { 2 roles Seller , Buyer 3 4 event r f q ( n ID , item ) key n ID 5 event quote ( n ID , item , price ) key n ID 6 event accept ( n ID , item , price , decision ) key n ID 7 event r e j e c t ( n ID , item , price , decision ) key n ID 8 event pay ( n ID , price , decision , cheque ) key n ID 9 event d e l i v e r ( n ID , decision , item ) key n ID 10 event receipt ( n ID , item , cheque , cipher ) key n ID 11 12 commitment Promise Goods Sel ler to Buyer 13 create quote 14 detach created Accept Quote 15 discharge d e l i v e r [ accept + 3] 16 release r e j e c t

17 18 commitment Promise Receipt Seller to Buyer 19 create quote 20 detach created Accept Quote and pay [ accept + 3] 21 discharge receipt [ pay + 1] 22 release r e j e c t 23 24 commitment Accept Quote Buyer to Seller 25 create accept [ quote + 5] 26 detach d e l i v e r [ accept + 3] 27 discharge pay [ accept + 5] 28 29 capability Seller quote with n ID , item , price 30 capability Seller d e l i v e r 31 capability Seller receipt with cipher 32 capability Buyer r f q with n ID , item 33 capability Buyer accept with fresh decision 34 capability Buyer r e j e c t with fresh decision 35 capability Buyer pay with cheque 36 37 completion done Promise Goods and done Promise Receipt and done Accept Goods 38 }

Only a role who has the capability to bring about a base event (along with any its attributes) can instantiate it. Line 29 states that SELLER can bring about quote and may produce bindings for n ID, item, and price indicated by with that respect quote s key. Lines 33 34 state that BUYER must bind a fresh value indicated by fresh for decision in accept and reject. Therefore, since accept and reject have the same key, n ID, at most one of them can occur for any n ID value. A commitment involves four event expressions: create and discharge are required but detach and release are optional. Accept Quote begins on Line 24: BUYER (its debtor) commits to SELLER (its creditor) upon accept (its create event) that if deliver occurs within three time units of accept (its detach event) then pay occurs within ﬁve time units of accept (its discharge event). A created commitment expires when its detach fails to occur; is violated if it is detached but fails to discharge; and released (frees the debtor) if its release event (shown for Promise Receipt) occurs. An event expression (Ev in Table 1) is either a base event or a lifecycle event restricted by time constraints, or a complex event built up from simpler events using and, or, except. Lifecycle events refer to a commitment s being created, detached, discharged, expired, violated, or released (the last four mean the commitment is terminated). A commitment s lifecycle events are derived entirely from its speciﬁcation. Here, done means if detached then terminated, i.e., (created except detached) or discharged or violated or released. Line 37 means that Net Bill completes when for each of its three commitments, any instance that is created terminates. Deﬁnition 1 states Clouseau s deep syntax.

Deﬁnition 1. A speciﬁcation S, is a tuple R, B, A, C, Q , where R is a set of two or more roles; B is a nonempty set of base events; A is a set of capabilities over R and B; C is a set of commitments over R and B; Q is a completion event. A base event, e or e( a, κ, q), associates an event named e with sets of attributes a A, key attributes κ a, and optional attributes q ( a \ κ).

C(x, y, c, r, u, l) is a commitment from debtor x R to creditor y R with create, detach, discharge, and release events c, r, u, and l, respectively. A(x, e, w, n) denotes a capability of role x R for base event e( a, κ, q) B. It means that role x can bring about instances of e by supplying values for e s nonoptional attributes. The attributes w are those for which x may generate a value if not already known. The attributes n ( n w) are those for which x must produce a fresh value (meaning those attributes cannot be already known).

3.2 Semantics of Clouseau Speciﬁcations

Although we adopt Cupid s syntax, we reformulate its semantics based on roles. This section provides a synchronous model of observations by roles. Section 4 provides an asynchronous model based on messages. Section 5 shows how to generate a asynchronous model (embodied in a protocol) from the synchronous model. (Below, V is the domain of values for all attributes.) Deﬁnition 2 states that a base event s instance provides bindings for its attributes and a timestamp. An observation associates an instance with observers, including one doer.

Deﬁnition 2. An instance, (e, b, t), of event e( a, κ, q) associates a partial function b: a V with a \ q dom(b) (binds all nonoptional attributes of e), and a timestamp t. An observation, O(x, y, e, b, t), associates an instance (e, b, t) with observer roles y, where | y| 2, and a distinguished doer x y who brings about the instance.

Below, b(a) is the result of evaluating b on a and b( κ) is a vector mapping b over each element of κ. For brevity, we omit the obvious components of O(x, y, e, b, t) and abbreviate it as o, oi, and so on. Deﬁnition 3 states that in a run for role r, (1) r makes each observation and (2) the sequence respects timestamp order.

Deﬁnition 3. A run for r, τ r, is a sequence of observations o1o2 . . ., where oi, oj : (1) r yi and (2) i < j iff ti < tj.

At most one instance occurs at a time: if O(xi, yi, ei, bi, t) and O(xj, yj, ej, bj, t), then and xi = xj, yi = yj, ei = ej, and bi = bj. Deﬁnition 4 captures synchrony: if a role makes an observation in a run vector, all roles mentioned in that observation also make that observation.

Deﬁnition 4. A run vector, Γ = [τ 1 . . . τ |R|], is one where r R, (1) τ r is a run, and (2) oi τ r, y yi : oi τ y. An observation o Γ iff it appears in some run in Γ.

Deﬁnition 5 states that a run for role r is viable iff for any observation of which r is the doer: (1) r has the capability for the observed event; (2) r previously observes each attribute that is not part of the capability; and (3) r does not previously observe any of e s fresh attributes.

Deﬁnition 5. A run of role r, τ r, is viable iff O(r, y, e, b, t) τ r: (1) A(r, e, w, n) A; (2) a a \ w: ( oi : ti < t, a ai, κi κ, b( κi) = bi( κi), and b(a) = bi(a)); (3) n n: oi : ti < t, n ai, and κi κ. A run vector is viable iff each of its runs is viable. [ S ] denotes the set of viable runs in S.

Seller Buyer

rfq(1, cot)

quote(2, bed, 10)

Seller Buyer

rfq(1, cot)

quote(1, bed, 10)

(b) Unviable.

Seller Buyer

quote(1, cot, 10)

accept(1, cot, 10, OK)

(c) Viable.

Seller Buyer

quote(1, bed, 10)

accept(1, cot, 10, OK)

reject(1, cot, 10, OK)

(d) Unviable.

Figure 2: Some run vectors for Listing 1. Each vertical line shows a role s run comprising a sequence of its observations. Each horizontal line is an observation of an event linking its observer roles with the doer shown with a solid circle.

Figures 2a 2d show example run vectors based on Listing 1. Figure 2a is viable because BUYER has the capability to bring about an rfq by generating values for n ID and item (bound to 1 and cot, respectively), and SELLER has the capability to bring about a quote by generating values for n ID, item, and price (bound to 2, bed, and 10 respectively). Figure 2b is unviable because it violates clause (2) of Deﬁnition 5; speciﬁcally, rfq and quote supply different values for item for the same value of n ID. Figure 2c is viable as SELLER has the capability to bring about a quote by generating values for n ID, item, and price, and BUYER has the capability to bring about an accept by supplying known values for n ID, item, and price and generating a value for decision. Figure 2d is unviable because clause (3) of Deﬁnition 5; speciﬁcally, reject requires generating a value for decision; however a prior accept has already generated the value for decision.

Consistency A run vector is consistent iff any two observations in it respect key integrity, i.e., if they agree on their common key attributes, they agree on all common attributes.

Deﬁnition 6. Let oi and oj be observations. Let κ = κi κj and a = ai aj. Then, oi and oj are consistent iff bi( κ) = bj( κ) bi( a) = bj( a). A run vector Γ is consistent iff for any roles i, j, any oi τ i and oj τ j are consistent. Speciﬁcation S is consistent iff every run vector in [ S ] is consistent.

Inconsistency may occur only if the agents have overlapping capabilities. Listing 2 modiﬁes Net Bill-Flexible: deliver includes cheque and SELLER can do deliver with cheque. Upon accept, SELLER and BUYER can bring about deliver and pay, respectively. Since both SELLER and BUYER control cheque, they can set different bindings for it for the same n ID, producing an inconsistency.

Listing 2: An inconsistent variant of Net Bill (Listing 1).

1 Net Bill Inconsistent { / / Modifying Net Bill F l e x i b l e 2 / / Showing only the elements that are modified

3 event accept ( n ID , item , price , decision ) 4 event pay ( n ID , decision , item , price , cheque ) 5 event d e l i v e r ( n ID , decision , item , cheque ) key n ID 6 7 capability Seller d e l i v e r with cheque 8 capability Buyer pay with cheque 9 }

Overlapping capabilities need not cause inconsistency. As Listing 1 shows, SELLER and BUYER can bind item but at most one of them can do so for any binding of n ID. In the rest of this paper, all speciﬁcations are consistent.

Intensions The intension of an event gives all the run vectors in which instances of the event, including commitment events, occur. We develop this idea below. Two instances cohere iff they bind their common key attributes to the same values.

Deﬁnition 7. Two instances, ei, bi, ti and ej, bj, tj , cohere iff bi( κ) = bj( κ), where κ = κi κj. Two sets of instances cohere iff each pair of their members coheres.

A chain is a set (ordered by time) of instances drawn from one consistent run vector that are (pairwise) coherent and implicitly ordered by timestamp. The mix of two chains ignores coherence so the result is not a chain. The merge of two chains is their mix restricted by coherence.

Deﬁnition 8. A chain in a run vector Γ is a set of instances { (e0, b0, t0)(e1, b1, t1) . . . } iff i, j : (ei, bi, ti) Γ and ei, bi, ti and ej, bj, tj are coherent. The mix of two sets of chains is their element-wise union: σ1 σ2 = {u1 u2|u1 σ1, u2 σ2} The merge of two sets of chains is their mix restricted by coherence: σ1 σ2 = {u|u σ1 σ2 and u is coherent}.

The certiﬁcate for an event expression is a chain that makes the expression true. Let Γ [ S ] for speciﬁcation S. In Deﬁnitions D1 D17, e is a base event, E, F, and G are base or lifecycle events, and X and Y are event expressions. last and ts give the last instance of a chain and the timestamp of an instance respectively.

D1 e Γ = { (e, b, t) | O(x, y, e, b, t) Γ}

D2 E[c, d] Γ = {σ|σ E Γ and c ts(last(σ)) < d}

D3 E[F + c, d] Γ = {σ|σ E Γ F Γ and ts(last(F, σ)) + c ts(last(E, σ)) < d}

D4 E[c, G + d] Γ = {σ|σ E Γ G Γ and c ts(last(E, σ)) < ts(last(G, σ)) + d}

D5 E[F + c, G + d] Γ = {σ|σ E[F + c, ] Γ E[0, G + d] Γ}

D6 X Y Γ = X Γ Y Γ

D7 X Y Γ = X Γ Y Γ

D8 X (Y Z) Γ = (X Y ) (X Z) Γ

D9 X (Y Z) Γ = (X Y ) (X Z) Γ

D10 X (Y Z) Γ = (X Y ) (X Z) Γ

D11 X ET Γ = ( X Γ ET Γ) \ ( X Γ ET Γ) (T is a time expression)

Table 2: Syntax of protocols generated by Clouseau.

Prot S {roles R+ parameters Param key + + Msg+} Msg R R+ : M [Param+] Param in X | out X | nil X

For brevity, let k = C(x, y, c, r, u, l) be a commitment.

D12 created(k) Γ = c Γ

D13 detached(k) Γ = created(k) r Γ

D14 expired(k) Γ = created(k) r Γ

D15 discharged(k) Γ = created(k) u Γ

D16 violated(k) Γ = detached(k) (u l) Γ

D17 released(k) Γ = created(k) l Γ

The intension of an event X is {Γ|Γ [ S ] and X Γ = }. The intension of an speciﬁcation is the intension of its completion event (Q), computed via the above semantics. Deﬁnition 9. The intension of speciﬁcation S, S = Q .

4 Communication Protocols We express protocols in a variant of BSPL (Singh 2011), which speciﬁes protocols via causality and integrity constraints. Our variant includes (1) multicast messages and (2) multiple protocol parameter lines, each a list of parameters needed for one alternative completion. Table 2 shows the syntax using M , R, S , and X as sets of (terminal) messages, roles, protocols, and parameter names, respectively. Listing 3 shows a protocol generated from Listing 1. Section 5 shows how to do so automatically.

Listing 3: Protocol generated by Clouseau for Net Bill. Clouseau adorns all protocol parameters out omitted here for readability.

1 Net Bill Flexible Protocol { 2 roles Seller , Buyer 3 parameters n ID key , item , price , quote P 4 parameters n ID key , item , price , rfq P , quote P 5 parameters n ID key , item , price , decision , rfq P , quote P , reject P 6 parameters n ID key , item , price , decision , rfq P , quote P , accept P 7 parameters n ID key , item , price , decision , cheque , rfq P , quote P , accept P , pay P 8 parameters n ID key , item , price , decision , rfq P , quote P , accept P , deliver P 9 parameters n ID key , item , price , decision , cheque , rfq P , quote P , accept P , pay P , deliver P 10 parameters n ID key , item , price , decision , cheque , rfq P , cipher , quote P , accept P , pay P , receipt P 11 parameters n ID key , item , price , decision , cheque , rfq P , cipher , quote P , accept P , pay P , deliver P , receipt P 12 13 Buyer Seller : rfq M [ out n ID , out item , out rfq P ] 14 Seller Buyer : quote M [ in n ID , in item , out price , out quote P ] 15 Seller Buyer : quote M [ out n ID , out item , out price , out quote P ]

16 Buyer Seller : accept M [ in n ID , in item , in price , out decision , out accept P ] 17 Buyer Seller : reject M [ in n ID , in item , in price , out decision , out reject P ] 18 Buyer Seller : pay M [ in n ID , in price , in decision , out

cheque , out pay P ] 19 Seller Buyer : deliver M [ in n ID , in item , in decision , out deliver P ] 20 Seller Buyer : receipt M [ in n ID , in item , in cheque , out cipher , out receipt P ] 21 }

Each message morph has a sender, a receiver, a name, and a set of parameters (subset of the protocol s parameters), some of which form a key. Each parameter has an adornment, which captures the sender s knowledge of a binding of that parameter: in means the sender knows it prior to sending; out means the sender doesn t know it prior but produces it when sending; nil means the sender doesn t know it prior and doesn t produce it. For example, Line 14 shows quote M with sender SELLER and receiver BUYER; n ID is the key (inherited from the protocol); SELLER must have observed n ID and item (for the speciﬁed key) before sending; must not know price before; but produce price when sending. The adornments capture causal dependencies. For example, rfq M of Line 13, which produces n ID and item, must precede quote M of Line 14, which uses those parameters. Capturing causality explicitly offers ﬂexibility: the constraints are causally essential; every compatible order is correct. Thus, deliver M and pay M may be sent in any mutual order. Message morphs encode alternative enactments. Morphs of the same name have the same sender and receiver but their parameters and parameter adornments can differ. For example, quote M has two morphs: Line 14 adorns n ID and item in ; and Line 15 has only out parameters. We assume the message name, λ, includes an identiﬁer to distinguish different morphs of the same name. Below, W = { in , out , nil } is the set of adornments. Deﬁnition 10. A message (morph), M(λ, x, y, p, α, κ), comprises a name λ, a sender role x, a set of receiver roles y, a function α: p W assigning an adornment to each parameter, and a list of key parameters κ p. A protocol consists of a set of roles, a set of protocol parameter lines each with the same key (subset of parameters), and a set of messages (morphs). A protocol completes if all parameters on any parameter line are bound. We extend BSPL with multiple parameter lines because each line captures one alternative completion of the protocol while avoiding the need for giving a null binding to any parameter. Deﬁnition 11. A protocol, λ, x, p, π, κ, F , comprises a name λ, a list of roles x, a list of parameters p, a set π of parameter lines (each a pair [ q, α], where q p and α: q W), a set of key parameters κ p, and a set of message morphs F. An instance of a message binds its parameters. A role s history is a sequence of message instances that a role views. We overload b from attribute to parameter bindings. Deﬁnition 12. N(λ, b) is an instance of a message M(λ, x, y, p, α, κ) iff p = dom(b). The history of role x, hx,

is a sequence of message instances m0m1 . . ., emitted or received by x. N(λ, b) appears in hx when emitted by x and, for all y y, in hy when received by y.

A message instance m is viable for emission by role x at its history hx iff (1) the bindings of m s in parameters are set earlier in the history and the bindings of m s out or nil parameters are not set earlier in the history.

Deﬁnition 13. For integer i, let N(λi, bi) be an instance of message M(λi, x, yi, pi, αi, κi) that occurs at index i in history hx. Then, N(λj, bj) is viable in hx iff it is a reception, or (1) p p, α(p) = in : i < j : κi κj, p dom(αi), and bj(p) = bi(p); and (2) p p, α(p) { out , nil }: i < j : κi κj and p dom(αi).

A history vector H progresses to H , H H , based on a message emission or reception, capturing asynchrony.

Deﬁnition 14. H = [h1 . . . h|R|] is viable iff (1) all its histories are empty, or (2) it progresses a viable history vector through the emission or reception of a viable message. P is the set of viable history vectors for protocol P.

A safe protocol guarantees integrity of information, i.e., no parameter may obtain conﬂicting bindings.

Deﬁnition 15. Messages N(λi, bi) and N(λj, bj) are consistent iff, for κ = κi κj and a = ai aj, bi( κ) = bj( κ) bi( a) = bj( a). A history vector is safe iff all pairs of messages in it are consistent. A protocol P is safe if and only if each vector in P is safe.

Deﬁnition 16. A history vector H is complete for parameters p iff ( p p: N(λ, b) H and p dom(b)). A protocol P is live iff H P : H : H H where H P and H is complete for a parameter line p of P.

5 Generating a Communication Protocol The correctness of a generated protocol requires that its set of history vectors matches the intension (i.e., the set of run vectors) of the speciﬁcation. Clouseau uses commitments and capabilities for determining senders and receivers of messages, and capabilities for determining the operational constraints expressed via adornments. We demonstrate this method by generating Listing 3 from Listing 1. Information integrity requires that (1) if two messages share a parameter, their keys must overlap and (2) instances determined by the same key bindings must be equal. Deﬁnition 17 captures the intuition that when a parameter is in , its binding in an instance with respect to its key must be known before the instance is produced. That is, the parameter must be accompanied by sufﬁcient key parameters to be meaningful. The determinant of a parameter p, Δp, is the intersection of keys of all message morphs in which p appears. A message is well-determined iff when a parameter is in so is each parameter in its determinant.

Deﬁnition 17. M(λ, x, y, p, α, κ) is well-determined iff ( p p: α(p) = in p Δp α(p ) = in ).

Generating Message Parameters and Adornments Clouseau generates message morphs to capture alternatives. Listing 3 captures two paths in Figure 1 via two morphs

Table 3: The adornments for a parameter based on attribute a depend on whether a is optional (a q), whether the sender can produce a (a w), and whether it must produce a (a n). Rows 2 and 6 are ill-formed because a must be produced by the sender, but it cannot be; row 8 because a must be produced but is optional.

# a q a w a n α(a) (Possible adornments)

1 No No No in 2 No No Yes Ill-formed: no output 3 No Yes No in , out 4 No Yes Yes out 5 Yes No No in , nil 6 Yes No Yes Ill-formed: no output 7 Yes Yes No in , out , nil 8 Yes Yes Yes Ill-formed: no output

of quote M (Lines 14 15). Line 14 adorns n ID and item in to capture the interaction in which SELLER receives an rfq M, which binds n ID and item, before sending a quote. Conversely, Line 15 adorns n ID and item out to capture that SELLER can send quote without receiving rfq M. Table 3 captures the possible adornments for each parameter in a message.

Generating Message Senders and Receivers Senders are those roles with a capability for bringing about an event from which a morph is generated. In Listing 1, SELLER can bring about quote, so it would be a sender for quote M. For receivers, we have some choices. The simplest is to multicast the message to everyone: those to whom it matters will read it. However, we can avoid generating superﬂuous messages through the following criteria. First, include receivers to ensure commitment alignment (Chopra and Singh 2015b). In Listing 1, quote features in the creates of Promise Goods and Promise Receipt, of which SELLER is debtor and BUYER is creditor. Thus, make SELLER the sender and BUYER the receiver of quote M. Second, include receivers to enable a stated capability, i.e., if a role needs an attribute binding to exercise a capability. If so, we make that role a receiver of any message arising from an event that includes that attribute.

Generating Autonomy Parameters Each generated message includes an out autonomy parameter to make the sender s exercising of its autonomy explicit in the information model. Doing so is essential to reﬂect the social meaning of communications. A sufﬁx P indicates such a parameter, e.g., quote P for quote M. This representation makes the performative nature (Austin 1962) of each communication explicit. Speciﬁcally, even if a role sends a message that merely relays information from other sources, the sending of that message is its autonomous action and no one else s.

Generating Protocol Parameters Clouseau generates parameter lines. The connection with events is enforced through the inclusion of relevant autonomy parameters in a parameter line. In Listing 3, Line 4 includes rfq P and quote P and omits accept P: thus, it is one of the complete

vectors when Promise Goods and Promise Receipt expire because Accept Quote is not created. To select the appropriate parameter lines, we begin from the completion event in the speciﬁcation. We convert it to a quasi disjunctive normal form (DNF) by applying the semantics of Section 3.2 to eliminate the commitment lifecycle events and to remove any from within the scope of or . Then, we produce one parameter line for each disjunct, including the parameters of messages derived from events that appear positively in the disjunct and excluding the autonomy parameter of any message derived from an event that appears as the second argument of .

Generating a Protocol Deﬁnition 18 consolidates the foregoing intuitions to identify (the, in general, multiple) message morphs with distinct parameter adornments that each capability yields, and thus the messages that a speciﬁcation yields. This deﬁnition adopts the simple approach of setting the receivers to all roles other than the sender. For convenience, we use the same name for each message morph that a capability for an event yields, speciﬁcally, appending M to the event name.

Deﬁnition 18. Let S = R, B, A, C, Q be a speciﬁcation. Let e( a, κ, q) B and χ = A(x, e, w, n) A. Then, χ yields message M(λ, x, y, p, α, κ) iff y = R \ x, p = a {e P} and a a: α(a) α(a) as speciﬁed in the column of Table 3 in the matching row, and α(e P) = out . Let Mχ be the set of messages that χ yields. The set of messages that S yields, MS =

Algorithm 1: Protocol Generation

input : Speciﬁcation S = R, B, A, C, Q output: Protocol G(S) generated from S

1 The name of the protocol is the name of the speciﬁcation;

2 The roles of the protocol are the roles of the speciﬁcation;

3 Let Completion = DNF of Q;

4 for each disjunct D in Completion

5 output parameter line for D;

6 Output MS, the set of messages that S yields (Deﬁnition 18);

6 Correctness of Protocol Generation To establish correctness of a protocol generated via Algorithm 1, we ﬁrst deﬁne how the run vectors of a speciﬁcation yield the history vectors of a protocol. We give a series of deﬁnitions, including (1) of an observation of an event instance yielding a message instance; (2) a run yielding a history; (3) a run vector yielding a history vector; and (4) a speciﬁcation yielding a protocol.

Deﬁnition 19. Let O(x, y, e, b, t) be an observation and μ = N(λ, bμ) be a well-determined instance of a morph M(λ, xμ, yμ, pμ, αμ, κμ). Then, e yields λ, e λ, iff λ = e M, x = xμ, y = yμ, and b = bμ.

Run vectors progress in a lockstep manner in their global timestamp order whereas history vectors progress in asynchrony. The message emissions in a role s history anchor the desired correspondence with the events brought about. Write a role r s run τ as μ1β1μ2 . . . where each μi is a possibly empty list of observations O(x, y, e, b, t), r = x, and each βi is an observation O(r, y, e, b, t) whose doer is r. Write a role r s history h as ν0δ0ν1 . . . where each νi is a possibly empty set of message receptions and each δi is a single message emission. Then, h is canonical for τ iff (1) |τ| = |h|; (2) μi : μi νi; and (3) βi : βi δi. Let h = μ0δ0μ1 . . .. Then, h causally permutes h iff the δi are unmoved and each μi is a permutation of νi.

Deﬁnition 20. A run τ yields a history h, τ h, iff h where h causally permutes h, and h is canonical for τ. A run vector Γ yields a history vector H, Γ H, iff their respective members correspond: r R: τ r hr.

Deﬁnition 21. Let S and P be a speciﬁcation and protocol, respectively. S yields P, S P, iff Γ [ S ] H P : Γ H and H P Γ [ S ]: Γ H.

Theorem 1 establishes correctness of protocol generation.

Theorem 1. S G(S).

Proof sketch. First, show by induction on run vectors that for every Γ [ S ]: H G(S) such that Γ H. For the base case, consider a run vector Γ with a single observation O(x, y, e, b, t). This means that A(x, e, w, n) A for base event e( a, κ, q) B such that a = w (all values must be generated in this observation). According to Deﬁnition 18 m = M(e M, x, y, a, α, κ) where a a: α(a) = out is in G(S). Therefore, there exists a history vector H in which the only message instance sent instantiates m as deﬁned above. Therefore, Γ H. For the inductive step, assume for each Γi that is a run vector over i observations, Γi Hi. Let O(x, y, e, b, t) be the (i + 1)st observation. This means that A(x, e, w, n) A for e( a, κ, q) B. Let a a be known from Γi. This means that a n = and w \ a are the bindings produced in the observation. Let m = M(e M, x, y, p, α, κ) where a p and a a : α(a ) = in and w w \ a : α(w) = out . From clause (2) of Deﬁnition 5, if some attribute is new for x (not previously observed), then x cannot previously have observed any of its nonkey attributes whose determinant includes the new key attribute. Thus m is well-determined, as in Deﬁnition 17. According to Deﬁnition 18, m is in G(S). Therefore, there exists Γi+1 such that Γi+1 Hi+1. Now we show the converse, that is, H G(S) : Γ [ S ]. The argument is by induction on history vectors. The empty run vector yields the empty history vector. Let H be a history vector such that for all strictly shorter H , there exists Γ such that Γ H . Going from H to H may have either involved a reception or emission by r of an instance of M(e M, x, y, p, α, κ). In either case, there exists capability A(x, e, w, n) A for base event e( a, κ, q) B, which would guarantee that there exists Γ such that Γ H. Theorem 2 relates the consistency of a speciﬁcation and the safety of a generated protocol.

Theorem 2. If S is consistent, then protocol G(S) is safe. Proof sketch. The empty run vector is in [ S ] and is consistent. The empty run vector yields the empty history vector in G(S), which is safe. Assume S is consistent. Let Γ, Γ [ S ] such that that Γ extends Γ by one observation O(x, y, e, b, t) of instance (e, b, t), of event e( a, κ, q). Further, let the observation be effected by x exercising its capability A(x, e, w, n). By Theorem 1, H, H P such that Γ H and Γ H . Therefore, H differs from H in having one extra emission of a message instance m yielded by observation O. Assume that H is safe. Let v w such that each v v is not bound in Γ but bound in Γ , meaning that O produces the bindings for v. From Γ H, we see that no v v is bound in H. By Deﬁnition 18, we know that m is an instance of morph M for A where exactly the v are out . Hence, H is safe. Theorem 3. If S is consistent, then protocol G(S) is live. Proof sketch. Let Γ [ S ] be a run vector. Then Γ satisﬁes S s completion event Q. Viewing Q in DNF, therefore, Γ must satisfy at least one disjunct of Q. By construction of protocol G(S), each parameter line of G(S) yields one disjunct of Q as well. Let H G(S) such that Γ H. Since Γ would have bound each attribute in one disjunct of Q, H would bind the corresponding parameter as well as the autonomy parameter for each message, thereby completing the relevant parameter line.

7 Discussion Our contribution bridges the gap between meaning-based and operational speciﬁcations via a method for generating a protocol given a Clouseau speciﬁcation. Clouseau is higher level than operational languages since it works from meaning abstractions, especially commitments, events, and capabilities. But whereas events in Clouseau are synchronous (occurring simultaneously for all observers), messaging in BSPL is asynchronous (the emission of a message is decoupled from its reception). What makes Clouseau signiﬁcant is that a ﬂexible protocol supporting asynchrony is in general difﬁcult to construct and maintain by hand. By modeling the meanings precisely using Clouseau, a designer can avoid that overhead. Winikoff (2007) and Desai and Singh (2008) highlight the challenges of computing commitments in asynchronous settings. Although our focus here is on commitments, Clouseau could be extended to cover other kinds of norms (Chopra and Singh 2016). Further, although our approach generates BSPL protocols, it could be adapted to generate protocols in other languages, e.g., trace expressions (Ferrando et al. 2019) or HAPN (Winikoff, Yadav, and Padgham 2018). A general and major value proposition of multiagent systems is to enable sound and secure collaboration between autonomous, heterogeneous parties. The interactions of agents reﬂect the autonomy of the principals they represent without divulging the implementation details of the agents and, importantly, keeping the decision making of the principals conﬁdential, except as it is revealed through the communications. Clouseau in this way advances the view of sociotechnical systems, e.g., as Chopra and Singh (2016) describe.

Speciﬁcally, Clouseau could be applied to model and enact meaning-based interactions in virtually any sociotechnical setting, especially when extended to additional norm types (Chopra and Singh 2016). Important problem domains within its reach include foreign exchange trades based on commitments (Desai et al. 2007) and health information governance based on norms (Chopra and Singh 2016). Notably, Clouseau could naturally support an alternative to smart contracts for the purposes of specifying business contracts on blockchain (Singh and Chopra 2019). Yolum and Singh (2002a) introduced the idea of computing directly with commitments, leading to enhanced languages and tooling (Winikoff, Liu, and Harland 2005; Chopra and Singh 2006; Baldoni et al. 2014), and work on reasoning patterns (Yolum and Singh 2002b; Fornara and Colombetti 2003; Chopra and Singh 2015a). This body of work formalizes commitment reasoning in the context of a conceptually unitary machine and does not tackle asynchrony. Our contribution builds upon the core idea of these approaches, namely, that messages carry meanings, by supporting decentralized enactments. Recent work on monitoring commitments (Chesani et al. 2013; Kafalı and Torroni 2018) or norms (Alechina, Dastani, and Logan 2014; Dastani, Torroni, and Yorke-Smith 2018) assumes a unitary model with synchronous state changes. Conceptually, these works are closer to Cupid, which too is based on a unitary model, and which our contribution extends to decentralized settings. El-Menshawy et al. (2018) address the problem of model checking commitments with real-time constraints. Baldoni et al. (2018) give an approach for verifying agents against commitments. Such techniques would be valuable for Clouseau speciﬁcations. MAS programming frameworks, e.g., Ja Ca Mo (Boissier et al. 2019), address complementary concerns to ours. Ja Ca Mo supports asynchronous messaging, and can support agents that enact protocols generated by Clouseau. Boissier et al. (2019) point out that interaction between agents in Ja Ca Mo could be based on direct messaging between them or via shared artifacts. Indeed, Baldoni et al. (2014) show how to program agents using a shared Ja Ca Mo artifact to coordinate commitment-based interactions. In brief, Clouseau is unique in that it uniﬁes the meaningbased and operational aspects of interaction with respect to asynchronous communication. Clouseau is motivated with the expectation that the use of a high-level speciﬁcation can enhance productivity and quality in producing and maintaining a protocol that is maximally ﬂexible given a meaning speciﬁcation and correct. Previous empirical studies, e.g., (Telang, Kalia, and Singh 2015), lend credence to that expectation. We defer an empirical study of Clouseau s beneﬁts in a practical setting to future work.

Acknowledgments

Singh was supported by U.S. Department of Defense under the Science of Security Lablet grant and Chopra by EPSRC grant EP/N027965/1 (Turtles). We thank Akın G unay for valuable discussions. Thanks to the anonymous reviewers for their helpful comments.

References Alechina, N.; Dastani, M.; and Logan, B. 2014. Norm approximation for imperfect monitors. In Proc. 13th International Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 117 124. Austin, J. L. 1962. How to Do Things with Words. Oxford: Clarendon Press. Baldoni, M.; Baroglio, C.; Marengo, E.; Patti, V.; and Capuzzimati, F. 2014. Engineering commitment-based business protocols with the 2CL methodology. Autonomous Agents and Multi-Agent Systems (JAAMAS) 28(4):519 557. Baldoni, M.; Baroglio, C.; Capuzzimati, F.; and Micalizio, R. 2018. Type checking for protocol role enactments via commitments. Autonomous Agents and Multi-Agent Systems (JAAMAS) 32(3):349 386. Bauer, B.; M uller, J. P.; and Odell, J. 2000. An extension of UML by protocols for multiagent interaction an existing multi-agent planning system. In Proc. 4th International Conference on Multiagent Systems (ICMAS), 207 214. Boissier, O.; Bordini, R. H.; H ubner, J. F.; and Ricci, A. 2019. Dimensions in programming multi-agent systems. Knowledge Engineering Review 34:e2. Chesani, F.; Mello, P.; Montali, M.; and Torroni, P. 2013. Representing and monitoring social commitments using the event calculus. Autonomous Agents and Multi-Agent Systems (JAAMAS) 27(1):85 130. Chopra, A. K., and Singh, M. P. 2006. Contextualizing commitment protocols. In Proc. 5th International Joint Conference on Autonomous Agents and Multiagent Systems, 1345 1352. Chopra, A. K., and Singh, M. P. 2015a. Cupid: Commitments in relational algebra. In Proc. 29th Conference on Artiﬁcial Intelligence (AAAI), 2052 2059. Chopra, A. K., and Singh, M. P. 2015b. Generalized commitment alignment. In Proc. 14th International Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 453 461. Chopra, A. K., and Singh, M. P. 2016. Custard: Computing norm states over information stores. In Proc. 15th International Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 1096 1105. Dastani, M.; Torroni, P.; and Yorke-Smith, N. 2018. Monitoring norms: A multi-disciplinary perspective. Knowledge Engineering Review 33:e25. Desai, N., and Singh, M. P. 2008. On the enactability of business protocols. In Proc. 23rd Conference on Artiﬁcial Intelligence (AAAI), 1126 1131. Desai, N.; Chopra, A. K.; Arrott, M.; Specht, B.; and Singh, M. P. 2007. Engineering foreign exchange processes via commitment protocols. In Proc. 4th IEEE International Conference on Services Computing, 514 521. El-Menshawy, M.; Bentahar, J.; Kholy, W. E.; and Laarej, A. 2018. Model checking real-time conditional commitment logic using transformation. Journal of Systems and Software 138:189 205.

Ferrando, A.; Winikoff, M.; Craneﬁeld, S.; Dignum, F.; and Mascardi, V. 2019. On the enactability of agent interaction protocols. Co RR abs/1902.01131v4:1 13. Fornara, N., and Colombetti, M. 2003. Deﬁning interaction protocols using a commitment-based agent communication language. In Proc. 2nd International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 520 527. Kafalı, O., and Torroni, P. 2018. COMODO: Collaborative monitoring of commitment delegations. Expert Systems with Applications 105:144 158. Marengo, E.; Baldoni, M.; Chopra, A. K.; Baroglio, C.; Patti, V.; and Singh, M. P. 2011. Commitments with regulations: Reasoning about safety and control in REGULA. In Proc. 10th International Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 467 474. Singh, M. P., and Chopra, A. K. 2019. Computational governance and violable contracts for blockchain applications. IEEE Computer. In press. Singh, M. P. 1991. Social and psychological commitments in multiagent systems. In AAAI Fall Symposium on Knowledge and Action at Social and Organizational Levels, 104 106. Singh, M. P. 1999. An ontology for commitments in multiagent systems: Toward a uniﬁcation of normative concepts. Artiﬁcial Intelligence and Law 7(1):97 113. Singh, M. P. 2011. Information-driven interaction-oriented programming: BSPL, the Blindingly Simple Protocol Language. In Proc. 10th International Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 491 498. Sirbu, M. A. 1997. Credits and debits on the Internet. IEEE Spectrum 34(2):23 29. Telang, P. R.; Kalia, A. K.; and Singh, M. P. 2015. Modeling healthcare processes using commitments: An empirical evaluation. PLo S ONE 10(11):e0141202. Winikoff, M.; Liu, W.; and Harland, J. 2005. Enhancing commitment machines. In Proc. 2nd International Workshop on Declarative Agent Languages and Technologies (DALT), volume 3476 of LNAI, 198 220. Springer. Winikoff, M.; Yadav, N.; and Padgham, L. 2018. A new Hierarchical Agent Protocol Notation. Autonomous Agents and Multi-Agent Systems (JAAMAS) 32(1):59 133. Winikoff, M. 2007. Implementing commitment-based interactions. In Proc. 6th International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 868 875. Yolum, P., and Singh, M. P. 2002a. Commitment machines. In Proc. 8th International Workshop on Agent Theories, Architectures, and Languages (ATAL 2001), volume 2333 of LNAI, 235 247. Springer. Yolum, P., and Singh, M. P. 2002b. Flexible protocol speciﬁcation and execution: Applying event calculus planning using commitments. In Proc. 1st International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS), 527 534.