Requirement Patterns for Engineering Multiagent Interaction Protocols

1 Introduction

Interaction has been recognized as a crucial construct in multiagent systems since the field's inception [Boissier et al., 2023]. Practical approaches address various aspects of interaction [Casadei et al., 2021]. A protocol captures the interactions between the agents in a multiagent system (MAS). Specifically, it guides the development of a system whose member agents communicate via messaging based on protocols. Thus, the quality of a multiaent system and its effectiveness in meeting stakeholder requirements depend on the quality of the protocol on which it is based. It is crucial the protocol be flexible: ideally, it should constrain the agents just enough (so they coordinate properly) but no more than necessary (so they can exercise their autonomy), both aspects essential to achieving what stakeholders require.

As an example, consider a protocol Sale (formalized shortly) that involves the roles of buyer, seller, bank, and shipper and supports exchanging payment for goods. What makes Sale-or any protocol-correct? Safety means that no enactment of Sale violates integrity. Liveness means that any enactment can complete, i.e., if the agents want it to. In addition, Sale should satisfy stakeholder requirements. For example, the stakeholders may require that if payment happens but items are not delivered, then a refund is issued. Or, if payment happens, it precedes delivery.

The kind of multiagent system we have in mind is decentralized, meaning there is no reliance on a central decision maker or store of global state. Its member agents may be instantiated on the same or different machines-we don't require or forbid either-and its correctness should not be affected by such variations. Ideally, an agent waits for another only if it relies on information to be obtained from the other or if it is beneficial for it to wait. Thus, to achieve decentralization, we cannot rely on synchronous or order-preserving communication channels.

Information protocols avoid the limitations of traditional protocol representations [Chopra et al., 2020] by not demanding shared state or order-preserving communication. Combining a flexible semantics over asynchrony leads to a protocol having a large number of enactments: potentially, exponential in its size. For example, Sale has 639 enactments, which are too many to verify manually.

We introduce Mambo, an approach for verifying information protocols against requirements specified as path queries. We (i) introduce a language to encode requirements; although the language is simple, we highlight its effectiveness in capturing interesting requirements patterns for protocols; (ii) show how to verify these requirements in a semantic tableau generated from a protocol, and (iii) for purposes of efficiency, show how to generate a small model (tableau) that maintains coverage for verifying a given requirement.

Mambo's novelty lies in that it is the first general-purpose verification approach for information protocols. Its significance lies in that information protocols is a paradigm of growing importance [Chopra and Christie, 2023] in engineering multiagent systems using programming models geared to different approaches for implementing agents [Christie et al., 2023; Christie et al., 2022; Baldoni et al., 2025; Chopra et al., 2025]. More fundamentally, Mambo's significance lies in the fact that it helps modularize the engineering of multiagent systems by simplifying the engineering of member agents given a correct protocol.

Organization. Section 2 describes the related work on protocols. Section 3 introduces information protocols and our language for expressing protocol requirements. Section 4 presents a variety of requirement patterns. Section 5 shows how to construct a tableau for a protocol and how to verify requirements with it. Section 6 shows how to construct an equivalent smaller tableau by exploiting the structure of the requirement being verified. Section 7 describes our implementation and presents performance results. Section 8 makes some methodological observations and discusses future work.

2 RelatedWork: Interaction Protocols

Commitments capture the meaning of an interaction [Yolum, 2007] and thus express multiagent requirements [Chopra et al., 2014]. Fornara and Colombetti [2003] define interaction protocols via UML sequence diagrams but give soundness conditions that depend on the meanings of speech acts; Yolum [2007] formalizes properties related to liveness, consistency, and robustness of commitment protocols; G¨unay et al. [2015] dynamically generate protocols given commitments and goals; Kalia and Singh [2015] generate commitment protocols from interaction scenarios; Chopra et al. [2014] give rules for refining requirements into commitments. These works address requirements, but not operational challenges, such as those due to decentralization (distributed knowledge and asynchronous communication). Winikoff [2007] describes some difficulties in implementing commitment-based interactions in asynchronous settings, especially those involving more than two agents.

Tooling for operational protocols is valuable. Rooney et al. [2004] propose a graphical editor for protocols expressed as sequence diagrams in Agent UML (AUML) [Huget and Odell, 2004]. Winikoff et al. [2018] defines a hierarchical state-machine notation and model for information protocols that captures state transitions graphically. These works offer no support for verification. MAS engineering methodologies, e.g., Prometheus [Padgham and Winikoff, 2005] and Bliss [Singh, 2014], offer informal guidance for engineering protocols. Ferrando et al. [2019] provide a valuable analysis of protocol enactability in decentralized settings under increasingly strong message ordering assumptions. Information protocols are enactable under the weakest possible assumption, no message ordering, thus making verification nontrivial.

Mazouzi et al.'s [2002] approach to protocol verification brings forth key themes, including the use of formal methods and evaluation of various correctness properties. Though this work is strong for its era, Mambo differs from it in important respects: (1) Mambo provides a formal specification language for the requirements to be verified. (2) Mambo works on fully declarative information protocols, whose semantics is natively asynchronous, whereas they assume the restrictive sequence diagram notation of AUML. They support asynchronous messages but not order-free channels, as we do. (3) Mambo incorporates heuristics based on the structure underlying an information protocol to carry out heavy partial order reduction whereas they do not support such reductions, which would make their work intractable.

Singh [2012] and Singh and Christie [2021] are formal approaches for verifying information protocols based on satisfiability (SAT) solvers and semantic tableaux, respectively. The latter, Tango, is much faster than the former on account of its partial order reduction. Both approaches are limited to Boolean properties of a protocol, especially safety and liveness. Mambo is closer in spirit to Tango in adopting semantic tableaux. However, it goes beyond previous approaches by supporting a temporal specification language and heuristics to enable incremental tableau construction while progressing a query representation.

3 Background

We now introduce information protocols and our language for expressing stakeholder requirements.

3.1 Information Protocols

The Blindingly Simple Protocol Language (BSPL) [Singh, 2011a] is a language for specifying information protocols, i.e., protocols based on causality and integrity constraints based on the information exchanged. BSPL captures asynchrony and flexibility better than traditional approaches [Chopra et al., 2020]. An information protocol is a bag of messages, each of which specifies a sender, a receiver, a message name, and parameters. Listing 1 gives a protocol Sale in BSPL. Message offer's sender and receiver are SELLER and BUYER, respectively, and its parameters are ID, item, and price. A protocol enactment (a set of correlated messages) is identified by the bindings of the specified ⌜key⌝ parameters. Parameter ID constitutes Sale's key.

The parameter adornments ⌜in⌝ , ⌜out⌝ , and ⌜nil⌝ capture information causality (dependencies) and determine the messages that are enabled for emission by an agent relative to an enactment. Specifically, a message is enabled if each ⌜in⌝ parameter (its binding) is known from (exists in) the agent's local state (set of sent and received messages), and no ⌜out⌝ or ⌜nil⌝ parameter is known. Because all of offer's parameters are ⌜out⌝ , it is enabled for SELLER at the start of the enactment. Message rescind (pulling back the offer) is enabled for SELLER provided it has already sent or received messages that make the parameters ID, item, and price known and leave bail, payinfo, and instruction unknown.

To send an enabled message, the agent fleshes out the message by generating bindings for only its ⌜out⌝ parameters via its internal logic. For example, to send offer, SELLER must generate bindings for all its parameters; to send rescind, it must generate a binding for bail but not for payinfo or instruction. The internal logic may differ across agents and not be revealed to others. The emission of a message records it in the local state, making the bindings of its ⌜out⌝ parameters known. An agent may receive a message whenever it arrives. The received message is recorded in the local state, making the bindings of its parameters known to the agent.

Information protocols support multiple agents sending or receiving messages concurrently. Given the causal semantics, any concurrent enactment is equivalent to a sequential one in which the send ('!') and receive ('?') events at different agents are interleaved, the only restriction being that the reception of a message follows its emission. A possible enactment of Sale is ⟨Seller!offer, Buyer?offer, Buyer!reject, Seller?reject⟩, ignoring message parameters.

3.2 Query Language

We express protocol requirements in Precedence, a propositional logic with one temporal operator indicating occurs (sometime) before. We adopt Singh's [2012] formalization.

The atoms of Precedence are events. Below, e and f are events. If e is an event, its complement e is also an event. Precedence treats e and e on par. The term e · f means that e occurs prior to f. The Boolean operators: '∨' and '∧' have

Listing 1 A BSPL protocol for conducting ebusiness.

1: Sa l e { 2: r o l e s Buyer , Se l l e r , Bank , Shippe r 3: parame t er s ou t ID key , ou t i tem , ou t pr i ce , ou t outcome 4: p r i v a t e address , dec i s i on , payinfo , i n s t r u c t i o n , authcode , choice , acc , b a i l 5: 6: S e l l e r ↦→ Buyer : o f f e r [ ou t ID key , ou t i tem , ou t p r i c e ] 7: Buyer ↦→ S e l l e r : accep t [ i n ID key , i n i tem , i n pr i ce , ou t address , ou t acc , ou t de c i s i on ] 8: Buyer ↦→ S e l l e r : r e j e c t [ i n ID key , i n i tem , i n pr i ce , ou t dec i s i on , ou t outcome ] 9: 10: S e l l e r ↦→ Buyer : r e s c i nd [ i n ID key , i n i tem , i n pr i ce , ou t ba i l , n i l payinfo , n i l i n s t r u c t i o n ] 11: 12: Buyer ↦→ S e l l e r : resc indAck [ i n ID key , i n i tem , i n pr i ce , i n ba i l , n i l authcode , ou t outcome ] 13: 14: / / Buyer au t ho r i z e s Bank i f not r e s c i n d e d 15: Buyer ↦→ Bank : pay [ i n ID key , i n pr i ce , n i l ba i l , i n acc , ou t authcode ] 16: Bank ↦→ S e l l e r : t r a n s f e r [ i n ID key , i n pr i ce , i n authcode , ou t pay i nfo ] 17: 18: / / S e l l e r e i t h e r i n s t r u c t s Shipper t o sh i p or bank t o re f und 19: S e l l e r ↦→ Shippe r : sh i p [ i n ID key , i n i tem , i n address , i n payinfo , ou t i n s t r u c t i o n , ou t cho i ce ] 20: 21: S e l l e r ↦→ Bank : r e fund [ i n ID key , i n i tem , i n payinfo , ou t choice , ou t outcome ] 22: Shippe r ↦→ Buyer : d e l i v e r [ i n ID key , i n i tem , i n address , ou t outcome ] 23: }

the usual meanings. The syntax (Figure 1) follows the conjunctive normal form.

I -→ clause | clause ∧ I clause -→ term | term ∨ clause term -→ event | event · event

The semantics of Precedence is given by runs of events

(instances). Let Γ be a set of events where e ∈ Γ if and only if e ∈ Γ. A run is a function from the natural numbers to the power set of Γ, i.e., τ : N ↦→ 2Γ . The ith index of τ, τi = τ(i). The length of τ is the first index i at which τ(i) = ∅ (after which all indices are empty sets). We say τ is empty if |τ| = 0. The subrun from i to j of τ is notated τ[i,j]. Its first j - i + 1 values are extracted from τ and the rest are empty, i.e., τ[i,j] = ⟨τi, τi+1 . . . τj-i+1 . . . ∅ . . .⟩. On any run, e or e may not both occur. Events are nonrepeating.

Here, τ |=i E means that τ satisfies E at i or later and τ is a model of query E if and only if τ |=0 E. E is satisfiable if and only if it has a model. Below, r and u are formulas.

S1 τ |=i e if and only if (∃j ≥ i : e ∈ τj) S2 τ |=i r ∨ u if and only if τ |=i r or τ |=i u S3 τ |=i r ∧ u if and only if τ |=i r and τ |=i u S4 τ |=i e · f if and only if (∃j ≥ i : τ[i,j] |=0 e and τ[j+1,|τ|] |=0 f)

The semantics justifies applying De Morgan's laws and treating complementation as negation. That is, we can complement a query since it can be reduced to one where only atoms are complemented: (1) e ≡ e; (2) r ∨ u ≡ r ∧ u; (3) r ∧ u ≡ r ∨ u; and (4) e · f ≡ e ∨ f ∨ (f · e).

In surface syntax, we accept 'and' for '∧'; 'or' for '∨'; 'before' for '·'; and '-' and 'no' for overline (complementation). (The binding order is complementation > · > ∧ > ∨.)

4 Requirement Patterns

Sale, the protocol in Listing 1, is complex; the purpose of the present paper is to facilitate verifying whether an information protocol meets stakeholder requirements. We distinguish two kinds of requirements. Structural requirements apply to any protocol. Stakeholder requirements are protocol-specific.

The requirements are expressed using events such as the occurrence of a message, e.g., offer; a parameter being bound, e.g., item, and the observation of a message or parameter binding by an agent, e.g., Seller:offer and Bank:authcode.

4.1 Structural Properties

These protocol-agnostic requirements establish the wellformedness of a protocol. Failing these patterns often indicates other problems in the conception of a protocol.

Pattern 1 (Liveness). Liveness captures the idea that all enactments can progress to completion, i.e., all parameters in a protocol (except those declared private) (Line 3: in Sale) must be known. A protocol is live if and only if in every enactment, all its completion parameters are known. Desired: ID ∧ item ∧ price ∧ outcome is true for all enactments.

Pattern 2 (Safety). Safety captures the lack of integrity violations in a protocol's enactments. A protocol is safe if and only if in every enactment, a parameter is bound at most once. To determine safety, for every pair of messages in which a common parameter is ⌜out⌝ , we check that at most one of the messages in the pair occurs in any enactment. Desired: (refund ∧ deliver) ∨ (rescindAck ∧ refund) ∨ (rescindAck ∧ deliver) ∨ (reject ∧ refund) ∨ (reject ∧ deliver) is false on all enactments.

Mambo automatically generates queries for Liveness and Safety from a protocol.

4.2 Stakeholder Requirements

In general, even if a protocol were structurally acceptable, it could fail to serve its stakeholders' needs.

Pattern 3 (Desired End). Any Sale enactment must end in one of the following states: (i) offer is rescinded by SELLER; (ii) offer is rejected by BUYER; (iii) BUYER and SELLER exchange payment for goods; and (iv) BUYER pays but SELLER refunds. Desired: rescindAck ∨ reject ∨ transfer ∧ (refund ∨ deliver) is true for all enactments.

Pattern 4 (Complementary). Some pairs of semantically "opposite" messages, e.g., deliver and reject, must be mutually exclusive. Desired: deliver∧reject is false on all enactments. Pattern 5 (Concede). Sale illustrates an interesting design involving semantically "opposite" messages: SELLER's rescind (end) and BUYER's pay (proceed). Since they can occur concurrently, a conflict between them would be unsafe. Therefore, they are expressed such that if BUYER sends pay, the transaction proceeds (pay is on a path to completion), but BUYER cannot send pay once it has received rescind. To ensure liveness, BUYER can send rescindAck once it has received rescind to allow completion on the non-pay path. Desired: pay · Buyer:rescind ∨ (no rescind ∧ no rescindAck) ∨ rescind · rescindAck is true on all enactments.

Pattern 6 (Late Action). Here, rescind disables accept; that is, accept cannot occur after rescind. Desired: no accept ∨ no rescind ∨ accept · Buyer:rescind is true on all enactments. Pattern 7 (Flexibility). Suppose accept means a commitment from BUYER to SELLER that if deliver occurs, then transfer will occur. In conjunction with Pattern 9, this pattern ensures a flexible exchange of payment and goods. Desired: accept · deliver ∧ deliver · transfer is true on some enactments.

Pattern 8 (Compensation). There may be a compensation commitment to refund BUYER in case SELLER violates its offer commitment. Informally, if transfer has occurred, then either deliver or refund occurs; refund implies transfer; and refund and deliver are mutually exclusive. Desired: (no transfer ∨ deliver ∨ refund) ∧ (no refund ∨ transfer) ∧ (no refund ∨ no deliver) is true on all enactments.

Pattern 9 (Create-Detach-Discharge). Suppose offer creates a commitment from SELLER to BUYER that if accept and transfer both occur (the detach condition), then deliver will occur (the discharge condition). Given this commitment, at the operational level, a simple happy path is that the commitment is created, detached, and discharged in that order. Desired: offer · accept ∧ offer · transfer ∧ accept · deliver ∧ transfer · deliver is true for some enactment.

Pattern 10 (Delegation Guarantee). BUYER relies upon BANK to pay SELLER via a transfer, i.e., a delegation [Singh, 1999]. Stakeholders may require that pay ensures transfer and must precede it. Desired: no pay ∧ no transfer ∨ pay · transfer is true on all enactments.

4.3 Toward a Catalog of Requirement Patterns

Table 1 shows how our patterns capture various design needs. It shows how our patterns could form the basis for a catalog of patterns that a protocol designer could draw upon in eliciting requirements from stakeholders.

5 Formalization Background

We adopt Singh and Christie's [2021] tableau framework. A configuration corresponds to a state during the enactment of a protocol. Each protocol enactment goes through a series of configurations where the transition respects causality and no role emits a message that would locally cause integrity violation. Initially, no observations have occurred and each role knows all and only the ⌜in⌝ parameters of the protocol.

A semantic tableau [D'Agostino et al., 1999; Fitting, 1999] is a proof tree. Here, the nodes of the tree are configurations. The inference rules determine how one node leads to another node. Thus, each path-sequence of nodes beginning from the root-of a tableau is a protocol enactment. We adopt propositional logic with its usual rules. Below, m is a message schema x ↦→ y : m[⃗ pI , ⃗ pO, ⃗ pN], where ⃗ pI , ⃗ pO, ⃗ pN are sets of its parameters respectively adorned ⌜in⌝ , ⌜out⌝ , and ⌜nil⌝ . The modalities Kx and Ux capture that role x knows or does not know parameter bindings, and Lx that x observes the emission or reception of a message.

5.1 Knowledge and Observations

What is known to each role grows monotonically because parameter bindings are immutable, and the emission and reception of each message add to a role's knowledge.

Lxm means role x has observed message m. In BSPL, the only observations are local, i.e., emissions or receptions. Chaining back a role's observations to the root gives us its history in reverse. This is crucial in relating nodes to history vectors and tableaux to sets of history vectors [Singh, 2012]. The Kxp assertions in a tableau node together characterize a protocol configuration. Ux expresses which bindings are (so far) unknown to x. Each transition involves an observation and the associated increase in the knowledge of the observing role. The BSPL treatment of ⌜out⌝ and ⌜nil⌝ parameters at emission relies upon their bindings being unknown. To capture this increase in knowledge, we delete Uxp assertions simultaneously with when we infer Kxp assertions.

Figure 2 summarizes the core BSPL semantics [Singh and Christie, 2021]. SND says that an instance of x ↦→ y : m[⃗ pI , ⃗ pO, ⃗ pN] is enabled for emission by x if and only if x knows ⃗ pI but does not know ⃗ pO or ⃗ pN. Concomitantly, the sender produces and comes to know the bindings for ⃗ pO, and the message enters the communication channel from its

Figure 2: Message emission and reception in BSPL [Singh and Christie, 2021].

sender to its receiver. RCV states that a message from x to y is enabled for reception by y if and only if x has observed sending that message. Concomitantly, y comes to know the bindings for ⃗ pI and ⃗ pO.

5.2 Verifying Correctness Properties

The properties of interest concern paths unfolding as specified and reaching a specified configuration. We assert a property at the root of the tableau. A path ends when no more observations are enabled. A consistent path that ends provides an example of the property at the root. A path that hits a contradiction is closed; a tableau closes if all its paths close, which indicates the property is inconsistent and thus its negation is proved. The foregoing argument works because each path of a tableau, as generated from the SEND and RECEIVE rules above, respects the causal structure of BSPL and local consistency when a role sends a message.

5.3 HowMessages Relate in a Protocol

Table 2 summarizes direct enablement and disablement relationships between observations based on what parameters occur in them [Singh and Christie, 2021]. It is possible syntactically to have a protocol with two messages that both enable and disable each other.

6 Mambo Formalization

A naively generated tableau faces a combinatorial explosion because it encodes each possible interleaving of events separately. We generate a small tableau that covers all possibilities implicitly via heuristics that reflect the causality and integrity constraints of a protocol and our query language.

Specifically, we combine interleavings that are equivalent in that they exhibit the same causal relationships and provide the same options for integrity preservation and violation. (1) If one message is a necessary enabler of another, the tableau would unfold in the correct order and the wrong interleaving is impossible. (2) If two messages may interfere (e.g., one message may disable another), we must include both possibilities in the tableau. We need to recognize such interleavings even if one of the messages is not presently enabled and make sure we do not prematurely eliminate viable paths from the tableau. (3) If the truth of a query depends on the interleavings, we must include a representative for each interleaving in the tableau. (4) If two messages are causally independent and don't interfere, we can retain one of the interleavings and generate a path for it.

We refine Singh and Christie's [2021] tangles with construct. Observation a tangles with observation c, if and only if (1) a directly disables c or (2) a directly disables a message b where b enables c. Two observations are incompatible if and only if at least one is an emission and tangles with the other. Like Tango, the rest of the construction builds an undirected graph of incompatible observations and computes an approximate vertex cover to find sets of compatible observations. Each such set corresponds to a logically distinct path that effectively stands in for each permutation of these observations. A key difference from Tango is that this graph is computed at each tableau node in light of the current reduced query, which is also reduced at each step as events occur.

7 Implementation and Results

Our implementation is an extension of Tango, and proceeds as follows: (1) Create a tree representation of the requirement query. (2) Use the parameters of each clause in the query to construct a conflict graph of parameters whose order of occurrence in an enactment matters. (3) Construct an incompatibility graph from the protocol, reflecting conflicts due to parameter adornments as well as the query. (4) Expand a tableau, with incompatible events placed on different paths. (5) Filter the paths based on the query: paths where the query resolves to true or false terminate and the remaining paths are retained for further expansion (in the previous step).

Tango doesn't support flexible queries. And, for the properties that it handles-safety and liveness-Tango doesn't close paths early if the property is satisfied. By contrast, Mambo incorporates the query in each step of the tableau expansion, especially in the incompatibility graph generation (significant for queries that contain 'before' relationships). And, it applies query-specific optimizations and returns paths as soon as a query resolves to true or false-termed "shortcircuiting" below.

7.1 Incremental Query Reduction

We model a property based on when it first becomes true on a path, as follows: (1) None: the property is indeterminate; (2) False: the property is violated; (3) ∞: the event occurs eventually; and (4) n ∈ N+: the property is true upon the nth event. We evaluate a query tree as described next.

Occurs The leaf nodes of a query, checking when an event occurs. These nodes return the event's index in the enactment if it has occurred, otherwise None.

Or Returns the minimum of two integers, or otherwise prefers ∞ over None over False.

• And Prefers False over None over the maximum of its arguments (including∞).
• Not Returns ∞ if its argument is False or None, and False if its argument is ∞ or an int.
• Before Returns the first argument that is not an int, the second argument if they are ordered, else False.

7.2 Optimizations and Heuristics

We implement three important optimization heuristics:

Pruning Stop extending a path once the query resolves to a definite int or False, since further simulation would not change the result.

Residuation Save the results of a query subtree as soon as they resolve to a definite int or False, avoiding reevaluation on that path of the tableau. Other paths are not affected.

Incremental Occurs nodes don't scan the entire path, but look at the newest event for relevant information and save the results using residuation.

7.3 Experimental Setup

We evaluated Mambo's performance using a framework that generates every combination of the setup parameters, including protocol, query, method, and iteration ID (so the experiment runs a specific number of times).

We use Tango as a baseline since it is the best prior method for verifying information protocols. We used the latest version (taken from its public repository) of the Tango implementation and protocol specifications, so that all of the methods are run on the same hardware over the same protocols.

We created a second baseline, dubbed Tango+, as a hybrid of Tango and Mambo. Tango+ generates all maximal enactments, minus partial order reduction, using the traditional Tango method, then filters them using the Mambo query system without any of the optimizations enabled. Thus, Tango+ is expected to have a nearly worst-case performance, since it does not do any short-circuiting. The exceptions are cases where the protocol is trivially safe. Mambo constructs a query for potential conflicts, and a lack thereof proves safety before checking any enactments. Since Tango+ uses Mambo's queries, it also short-circuits on trivially safe protocols.

Our experiments were performed on an AMD Ryzen 7 6800U with 16GB of RAM.

7.4 Results

To compare against prior results, we performed one experiment verifying only safety and liveness for those protocols analyzed by Tango [Singh and Christie, 2021]. This evaluation is limited to liveness and safety verification since the baselines are limited to these properties.

In addition, we computed Cohen's [1988] d statistic for effect size, which is defined as the difference of means divided by the sum of standard deviations. We obtained strong effect sizes relative to Tango, with the worst case being 1.4 and the best being 29.5. The results are more varied with Tango+, which mostly performs worse than Tango, except where the protocol is trivially safe, and beats Mambo in one case. Details are in the appendix.

Next, we evaluate Mambo's efficiency with respect to the requirement patterns described in this paper. For practical purposes, it helps to include a semantic check for the brevity or minimality of a protocol. A deadwood message in a protocol is one that is not observed on any enactment. That is, message m is deadwood if and only if the corresponding event m is unsatisfiable. Deadwood is not implemented as a query. Instead, Mambo generates the possible enactments and subtracts their events from the set of messages in the protocol; any messages remaining are deadwood.

Table 4 shows that Mambo is able to verify each requirement in under 40ms. As Table 4 shows, Sale does not meet some of the requirements. Flexibility is not met because the protocol entertains no enactment in which deliver happens before transfer. For Concede, the Mambo tooling produces a counterexample; specifically, the enactment ⟨Seller!offer, Buyer?offer, Buyer!reject, Seller?reject, Seller!rescind, Buyer?rescind⟩. We could regiment the protocol further to try to prevent the Concede counterexample. Specifically, we could introduce ⌜in⌝ outcome in rescind so that the reception of reject disables the emission of rescind. Doing so, however, will not prevent the enactment where these messages are sent concurrently. In this particular case, one could take the alternative view that the counterexample represents a harmless case because the "outcome" of the interaction (rejection of offer) is not in doubt. Trying to avoid such cases makes the protocol overly complex for no gain in the quality of the multiagent system produced.

If stakeholders consider Flexibility important and want to ensure that transfer can happen after deliver (but must happen if deliver does), ship can be modified so that it does not depend on payinfo, and instead has a ⌜nil⌝ bail to prevent shipping and rescinding in the same enactment.

8 Discussion

It is important to support the engineering of protocols to produce decentralized multiagent systems. Information protocols offer a fine-grained view of coordination between agent and enable flexible, asynchronous operationalization. This flexibility is the reason it can be hard to imagine all the operational possibilities afforded by a protocol.

Traditionally, protocols are presented as finished work based on their designers' intuitions. Instead, we advocate the systematic engineering of protocols as crucial software artifacts in the sense of Osterweil [2008]. That is, protocol design would take place hand-in-hand with the iterative process of acquiring and refining stakeholder requirements [Telang and Singh, 2012]. Unlike in traditional agentoriented software engineering [Cernuzzi and Zambonelli, 2004; Bresciani et al., 2004] that produce sequence diagrams, in our conception, designers would craft information protocols to achieve flexibility and rigor [Winikoff et al., 2018; Singh, 2014].

Requirements in Mambo capture the constraints on the information (messages or parameters) exchanged and are thus more abstract and simpler than protocols. That is, the requirements are easier to formulate and provide a conceptual basis for evaluating protocols. Like in traditional systems, safety and liveness are prerequisites to proper implementation and have analogs in traditional approaches. Some requirements take a stakeholder's perspective. For example, a seller who doesn't trust a buyer may wish to ensure its agents will be able to delay delivery until payment or rescind an offer. Some requirements go beyond traditional systems. For example, specifying protocols that satisfy the Concede pattern is impossible in alternative protocol specification approaches [Chopra et al., 2020]. The flexible nature of information protocols is key to supporting novel requirement patterns. A useful direction would be to build a catalog of such patterns.

For brevity, we elide the discussion of syntactic checks, which despite being simple to understand and efficient to apply, can help avert design flaws. For example, a protocol that has an ⌜out⌝ parameter but no message with that parameter as ⌜out⌝ cannot be live. A private parameter that is ⌜in⌝ on some messages but never ⌜out⌝ indicates a redundant protocol in that those messages are clearly deadwood. And, one that is ⌜out⌝ but not ⌜nil⌝ or ⌜in⌝ can be trivially removed.

Languages for specifying workflows based on propositional temporal logics [Attie et al., 1993; Montali et al., 2010] are potential alternatives to Precedence. Precedence is eventoriented, which lends itself well to our setting: events naturally model message emission and reception and parameter binding. Moreover, Precedence is simpler with only one temporal operator before, which captures event order more naturally than the alternative approaches, which are based on until and produce unwieldy formulas even for simple requirements [Attie et al., 1993]. Also, Precedence eschews the next-time operator, which is ill-defined in decentralized systems.

Mambo brings up interesting directions for future work. One, we might combine its representations with protocol verification tools for other paradigms. In particular, we posit that our query language is well-suited to efficient online evaluation and would facilitate synthesis with runtime verification [Ancona et al., 2021] and monitoring [Dastani et al., 2018]. Likewise, for tools for meaning-based representations [Yolum, 2007; G¨unay et al., 2015; Dastani et al., 2017], we can investigate automatically generating Mambo queries from commitments and goals [Harland et al., 2017].

Two, we need techniques for verifying protocol-based agents to modularly verify a multiagent system by verifying them separately once the protocol is verified. Doing so would combat the potential high cost of system verification. An effective approach should tackle the fact that an agent would participate in multiple systems; e.g., an agent may play BUYER in Sale and a PATIENT in a healthcare protocol, e.g., to buy prescribed drugs.

Three, instead of verifying protocols, we could synthesize protocols from specifications in a higher-level language. Langshaw [Singh et al., 2024] is such a language. Its novel idea is separating the specification of communicative acts and the coordination required between them. Coordination is specified via abstractions for conflicting actions and prioritized saysos of roles over parameters in the communicative acts. Langshaw specifications are more compact than the protocols synthesized from them. Mambo suggests an alternative approach for specifying coordination requirements: as formulas in Precedence. That is, it would be interesting to explore protocol synthesis given a specification of communicative acts and a set of requirements. Comparing the resulting approach with Langshaw would help develop intuitions about higher-level languages.

Four, agentic models combine generative AI with information and abilities to sense and act, e.g., via web services. Generative AI can help overcome the knowledge engineering bottleneck in building flexible agents. Current agentic frameworks compose agents via workflows [LangGraph, 2024; Dibia et al., 2024]. However, a major and long-recognized shortcoming of workflows is their rigidity [Chrysanthis and Ramamritham, 1994; Singh and Huhns, 1994], which limits agent autonomy and responsiveness to exceptions [Singh, 2011a; Singh, 2012; Singh, 2011b]. Thus powerful agents built with generative AI can be stymied by the inability to act flexibly. Mambo enables engineering MAS based on correct, flexible protocols. An important direction would be to investigate how flexible protocol-based interaction could be applied within agentic models in lieu of workflows.

9 Reproducibility

The appendix and all software, including the protocols mentioned, are available at https://gitlab.com/masr/mambo.

Acknowledgments

We thank the anonymous reviewers for their helpful comments. We thank the US National Science Foundation (grant IIS-1908374) for partial support.