Formalizing Communication Protocols for Multiagent Systems

1 Introduction

Protocols streamline communication and enable the development of interoperable agents by independent vendors. The participants in a protocol should be able to exploit opportunities offered by the environment, negotiate and exploit special relationships with others, and handle exceptions. Unfortunately, conventional engineering techniques for specifying and enacting protocols are tedious and result in interactions that are unnecessarily rigid [Yolum and Singh, 2002].

Work on commitment machines (CMs) shows how representing and inferencing on commitments can produce flexible protocols while providing a basis for compliance [Chopra and The above papers observe that the original NetBill is quite rigid. It cannot handle natural situations such as (1) a merchant proactively sending a quote, mimicking the idea of advertising a price; (2) a customer sending an "accept" message before requesting a quote (as in cases of trust or urgency); (3) a merchant sending the goods prior to the customer accepting (as in a trial offer). These papers show how to model protocols based on commitments, enabling each participant to perform a wider variety of actions yet ensure its own compliance and check others' compliance based on their actions.

∗This research was partially supported by the National Science Foundation under grant DST-0139037.

Although promising, previous work on CMs is not sufficiently general, rigorous, or clear in its assumptions. Yolum and Singh model actions in restrictively. Their approach only indirectly models the discharge of a commitment. Their strong point is a compilation of CMs to finite state machines. Winikoff et al. use the event calculus to reconstruct some of Yolum and Singh's work. They improve the methodology by which commitments are modeled, but don't study compilation as such. Chopra and Singh consider a richer, nonmonotonic theory of action based on causal logic. They don't discuss compilation except the general translation of causal logic into a transition system.

As a case in point, current and emerging financial protocols are not adequately formalized. For example, price discovery protocols, which are crucial for wholesale foreign exchange transactions, are conventionally described via scenarios and text descriptions [TWIST, 2006]. However, such descriptions are ambiguous and unwieldy. They treat each of several cases separately, losing opportunities for generalization and compactness. Our preliminary work with TWIST captures the key commitments and succinctly represents multiple scenarios using a few primitive patterns, that can be validated modularly. The value of commitments in modeling and analysis is clear; this paper strengthens their operational aspects.

Previous work assumes that a CM necessarily includes all states that are reachable through the actions modeled. However, the design of a protocol can involve considerations such as which states to include, e.g., to respect integrity and security constraints, and participants' preferences. This is especially so when subtle organizational requirements or complex roles are involved. Likewise, although nonmonotonic specifications can be valuable, monotonic representations that enumerate the modeled conditions facilitate verification of simplified, high-performance automaton-based implementations that nevertheless follow a specified protocol.

This paper introduces generalized commitment machines (GCMs), which are a more general and rigorous version of CMs. It introduces a simple approach for modeling actions, so that we can clearly state the key requirements on them. The action models can be expressed in a variety of existing formalisms, including causal logic and event calculus. This paper handles the complete set of commitment operations.

Additionally, the semantics of GCMs is based on infinite computations, thus providing a proper treatment of nonterminating (and even terminating) protocols. To motivate nontermination, notice that protocols can readily have cycles. Figure 1(c) introduces a reject transition, which induces a cycle. Thus unbounded computations can be produced. However, if our model is a traditional finite automaton, each computation would terminate in a final state of the automaton. By contrast, if we automatically restart NetBill upon sending a receipt and interpret it as not having a final state but requiring that a good state (say, state 6) occurs infinitely often, then we would bring about infinite computations (Figure 1(r)). A good state is one in which some desirable condition, relative to design goals, is achieved. In traditional applications of automata, a good state is typically one where a stimulus has been responded to. For GCMs, a simple domain-independent basis may be that a good state is one where there are no pending commitments.

More natural nonterminating protocols involve maintaining a relationship (as in an organization) rather than completing a transaction. Participants of such protocols would continually send messages and respond as often as required. One can think of the underlying relationship as a standing agreement, analogous to those in real-life organizations or distributed systems. You don't want a multiagent system to terminate any more than you want your OS to terminate.

GCMs are specified modularly via sets of inference rules. We cleanly separate rules involving (1) generic expectations from action theories, (2) commitment operations, (3) how commitment operations are "constituted" in the setting being modeled, and (4) how a protocol should function, i.e., "regulative" rules in force. Here, (1) and (2) are fixed; (3) and (4) vary for each protocol. The above kinds of rules can be captured in a variety of existing action formalisms. Importantly, GCMs are compiled in a novel manner into deterministic B¨uchi automata, a well-known model of infinite computations [Thomas, 1990]. Automata facilitate verification; deterministic representations can be directly executed by a computer using a single thread, in constant space.

Briefly, our contributions are as follows. We seek a computational model of protocols that is natural for humans: thus it must reflect semantics. In general, producing an executable, deterministic representation can cause an exponential blow up and include unnatural states. Using semantics, we can map GCMs to deterministic automata with natural states.

2 Technical Framework

We introduce our action representation, and review commitments and B¨uchi automata. Below, x, y, z are agents; p, q, etc. are formulas; and α is an atomic proposition or its negation: identify α with ¬¬α.

2.1 Generic Action Theory

The meaning of an action is specified in terms of the proposition it brings about (reflecting "causes" in causal logic or "initiates" in event calculus) under different conditions. Each action is described via an action theory, Δ, i.e., a set of axioms that capture how the state of a protocol evolves when an action occurs. For simplicity, the performer of the action is kept implicit in the action label. Definition 1 describes action axiom schemas, which correspond to potential transitions (some of which might be allowed in a GCM).

Definition 1 p a ↪→q means that q is a consequence of performing action a in a state where p holds.

If p holds and p a ↪→q, then performing a yields q. When q is ¬p, a overturns p; when q is false, that means a is impossible if p holds. The relation a ↪→ is closed under the inference rules below. An action theory Δ must respect these rules. Below p ⊢ q means that q is a logical consequence of p.

The following is not an inference rule but a requirement that the a ↪→ relation preserve consistency.

INERTIA specifies that if α holds before a and isn't overturned by a, then α continues to hold after a. INERTIA is not required here but is a convenient property of action theories.

Example 1 Example of overturn and inertia: Consider a state s where goods ∧ ¬pay holds. Now if payment is made, the new state is s′ where goods ∧ pay holds.

2.2 Commitments

A commitment is an explicitly manipulable directed obligation (in a context, ignored here for simplicity).

Definition 2 A commitment Cx,yp relates a debtor x, a creditor y, and a condition p. Specifically, x commits to y to bring about p.

Commitment Actions

The creation and manipulation of commitments can be described using the following operations, modeled as actions.

• true create(x,Cx,yp) ↪→ Cx,yp: establish
• p ∧Cx,yp discharge(x,Cx,yp) ↪→ ¬Cx,yp: resolve and remove
• Cx,yp cancel(x,Cx,yp) ↪→ ¬Cx,yp: remove (by debtor)
• Cx,yp release(y,Cx,yp) ↪→ ¬Cx,yp: remove (by creditor)
• Cx,yp assign(y,z,Cx,yp) ↪→ Cx,zp ∧¬Cx,yp: change creditor
• Cx,yp delegate(x,z,Cx,yp) ↪→ Cz,yp ∧¬Cx,yp: change debtor

A debtor who cancels a commitment may be subject to penalties whereas a creditor may release a commitment (typically for organizational reasons) with no penalties.

Definition 3 A conditional commitment CCx,y(p, r) means that if antecedent p becomes true, then the debtor x will become committed to bringing about consequent r.

When a conditional commitment's antecedent becomes true, it is discharged and a commitment for its consequent is created (typically, z = y):

When a conditional commitment's consequent becomes true, it is discharged and nothing else is needed (typically, z = x):

Constituting Commitment Actions

The above rules provide the semantics of commitment actions. In each setting, the actionswould be performed in some domain-specific manner. In protocols, commitment actions correspond to message types. In some cases, the messages may combine the effects of multiple commitment actions. Or, as in the case of partial returns and payments, multiple messages may be needed to implement one action. For example, paying $3 would replace a commitment to pay $9 by a commitment to pay $6. The domain action theory would capture such requirements.

Example 2 Consider the conditional commitment CCm,c(pay, receipt) meaning that the merchant would commit to sending a receipt if the customer pays.

• The customer pays first, making pay true. The conditional commitment is terminated and a new commitment, Cm,creceipt, is created in its stead (detach). When the merchant actually sends the receipt, i.e., when the proposition receipt becomes true, then the commitment Cm,creceipt is discharged (discharge).
• Before the customer pays, the merchant sends the receipt, making receipt true. The conditional commitment is terminated, but no other commitment is created: the customer did not commit to paying (eliminate).

2.3 Mapping to Existing Logics

The inference schemas on a ↪→ defined above are generic and can be represented in more than one existing formalism. Hence, an interpreter for any of these formalisms can be plugged in to derive appropriate inferences. The following causal laws show how some commitment actions are captured in causal logic [Chopra and Singh, 2004, § 4.1].

1. Discharge: p causes ¬Cx,yp if Cx,yp
2. Detach: maps to two expressions p causes ¬CCx,y(p, r) if CCx,y(p, r) p causes Cx,yr if CCx,y(p, r)
3. Eliminate: r causes ¬CCx,y(p, r) if CCx,y(p, r)

The following event calculus expressions capture the same actions as the above [Winikoff et al., 2005, Fig. 7] (time is explicit here, but not specifically used i this formalization):

1. Discharge: Terminates(e, Cx,yp, t) ← HoldsAt(Cx,yp, t) ∧ Happens(e, t) ∧ Subsumes(p′ , p) ∧ Initiates(e, p′ , t)
2. Detach: maps to two expressions Initiates(e, Cx,yp, t) ← HoldsAt(CCx,y(p, q), t) ∧ Happens(e, t) ∧ Subsumes(p′ , p) ∧ Initiates(e, p′ , t) Terminates(e, CCx,y(p, q), t) ← HoldsAt(CCx,y(p, q), t) ∧ Happens(e, t) ∧ Subsumes(p′ , p) ∧ Initiates(e, p′ , t)
3. Eliminate: Terminates(e, CCx,y(p, q), t) ← HoldsAt(CCx,y(p, q), t) ∧ Happens(e, t) ∧ Subsumes(q′ , q) ∧ Initiates(e, q′ , t)

We could just as easily use ECASL, the Extended Cognitive Agent Specification Language [Khan and Lesp´erance, 2006].

2.4 B¨uchi Automata

Finite state machines (FSMs) have long been used to specify protocols. The acceptance condition of FSMs requires termination in a final state. But, as Section 1 argues, many interesting protocols are nonterminating. To model such protocols requires that we consider automata over infinite words.

B¨uchi automata (BA) have finitely many states and the same transition rules as FSMs. However, their acceptance condition handles nonterminating computations by requiring that a good state (see Section 1) be visited infinitely often.

Definition 4 A B¨uchi automaton is a five-tuple, B = 〈S,A, s0,G, δ〉, where S is a set of states, A is the alphabet, s0 ∈ S is the start state, G ⊆ S is a set of good states, and δ ⊆ S × A × S is the transition relation.

Below, ω is the first infinite ordinal. A computation τ = 〈s0, a0, s1, . . .〉 is an ω-long alternating series of states and intervening actions. For a computation τ, inf(τ) is the set of states that occur infinitely often in τ. Throughout this paper, B is a BA and τ is a computation.

Definition 5 τ is realized by B if and only if (∀i ∈ ω, 〈si, ai, si+1〉 ∈ δ) and inf(τ) ∩ G ̸= ∅.

Figure 1(r) is an example BA with S = the set of vertices, A = the set of edge labels, s0 = 1, G={6} shown in reverse video, and δ = the set of edges. The computation that cycles through states 1, 2, 3, 4, 5, 6, namely, 〈1, C : rfq, 2,M : offer, 3, C : accept, 4,M : goods, 5, C : pay, 6,M : receipt, . . .〉 is accepted by this BA, because it visits state 6 infinitely often. The computation that cycles through states 1, 2, 3 is not accepted because it does not visit state 6. Figure 2 shows BA for the languages a(ba+b)ω and a(a+b)ω , respectively. Notice that Figure 2(r) accepts aω , but Figure 2(l) doesn't. Thus, viewed in automata theoretic terms, the two are obviously not equivalent.

The move to infinite computations complicates some aspects of the automata. Importantly, whereas all nondeterministic FSMs have an equivalent deterministic FSM, some nondeterministic BA have no equivalent deterministic BA. Figure 2(l) is a famous example of a BA that cannot be determinized. A deterministic BA can be efficiently emulated by a script: if the BA is correct we know the script complies with the given protocol. This paper shows how to produce (if possible) a correct deterministic BA for a protocol.

3 Generalized Commitment Machines

A generalized commitment machine (GCM) is specified via states whose content is captured via logical expressions, actions and an action theory to transition between the states, and a set of good states. Terminating computations can be modeled by transitioning at their end to an artificial good state with a self-loop. Given a state, the new state reached by performing an action is logically inferred. In effect, a GCM specifies meanings of the states, and lets inferencing do the rest.

Since we construct BA from the same set of states and actions as GCMs, we use the same symbols S, s0, G, and A in both definitions. Below, p ≡ q means that p and q are logically equivalent, that is, p ⊢ q and q ⊢ p.

Definition 6 A GCM is a tuple P = 〈S, A, s0, Δ, G〉, where S is a finite set of states, A is a finite set of actions, , s0 ∈ S is the start state, Δ is an action theory, and G⊆S is a set of good states. Members of S are logically distinct: (∀si, sj ∈ S : (si ≡ sj) ⇒ (si = sj)); false ̸∈ S; any state stronger than a good state is also good: (∀si ∈ G, sj ∈ S : (sj ⊢ si) ⇒ (sj ∈ G)).

Definition 7 τ is generated by a GCMP if and only if (∀i ∈ ω : si ∈ S, (∃ai ∈ A : si ai ↪→ si+1)), and inf(τ) ∩ G ̸= ∅.

Throughout this paper, P (for "protocol") is a GCM. Given q, r ∈ S, a ∈ A, P transitions from q to r under action a if and only if q a ↪→r. In effect, a GCM functions as an inferencedriven (nondeterministic) BA.

Example 3 Previous work formalizes NetBill and other terminating protocols as commitment machines. A similar approach applies here. Briefly, the modeling steps are:

• Model the atomic propositions, such as request or pay.
• Introduce the commitments needed. For example, accept abbreviates CCc,m(goods, pay), i.e., if customer c receives the goods, he would pay merchant m.
• Identify the states in S. For example, state 3 in Figure 1 means that the merchant has made an offer thus committing to delivering goods and sending a receipt upon payment: formally, request ∧ promiseReceipt ∧ promiseGoods.
• Identify the actions in A: these are the messages exchanged, e.g., sendAccept and sendGoods.
• Assert action theory axioms, Δ: (1) sending an accept: true sendAccept ↪→ accept; (2) delivering the goods and promising receipt: true sendGoods ↪→ goods∧promiseReceipt.
• Identify the good states in G. For example, (1) the customer has made a request but no commitments have been made: request; (2) the merchant has delivered the goods and the receipt and the customer has paid: request ∧ goods ∧ pay ∧ receipt .

Example 4 A GCM analogous to Figure 2(l). State 1 is p∨q; state 2 (∈ G) is p ∧ q, and Δ includes the following axioms: (1) p ∨ q a ↪→p ∧ q, (2) p ∧ q b ↪→p ∧ q, and (3) p ∧ q b ↪→ p ∨ q.

This example helps relate GCMs to the well-known BA of Figure 2(l) (revisited in Section 4). A scenario where such a GCM may occur is if p and q refer to some organizational relationships. Action a strengthens the relationship from p or q to p ∧ q. Action b confirms the relationship or can weaken it. (One can imagine that b was originally specified for two organizational roles, now being played by the same party.)

4 Compiling GCMs into B¨uchi Automata

Reasoning with declarative representations at runtime can be expensive, may increase the code footprint of the agents. Many applications such as financial transactions [TWIST, 2006] call for flexibility when designing a protocol but rigid enactment to make performance guarantees. Also, the popularity of AJAX indicates the potential for simplified interacting agents. Compiling a GCM into a deterministic BA is thus highly desirable. A GCM is in essence a nondeterministic BA. In general, an equivalent deterministic BA may not exist. But we can exploit the semantics of the protocol to produce (if possible) a deterministic BA that for practical purposes is equivalent.

4.1 Determinism and Soundness

The states, initial state, and good states of a GCM map straight to those of a BA. More importantly, to ensure determinism, we can choose no more than one transition for a given state and action: this is what Algorithm 1 does.

To understand the min calculation in Algorithm 1, imagine that the GCM states are partially ordered according to logical consequence: si is placed below sj iff si ⊢ sj. For S ⊆ S, min(S) is the unique minimum, if any, of S according to this order. For example, assume that performing a in s1 could yield s2 and s3, where s2 ̸≡ s3. If s2 ⊢ s3, Algorithm 1 would select s2; if s3 ⊢ s2, it would select s3; if neither, Algorithm 1 would select nothing, thus omitting the a transition from s1. Theorem 1 shows that the result is deterministic.

Theorem 1 Algorithm 1 yields a deterministic BA B. Proof. Assume B has two transitions for the same state and action, i.e., 〈si, a, sj〉 and 〈si, a, sk〉. Algorithm 1 ensures sj ⊢ sk and sk ⊢ sj, i.e., sj ≡ sk. Definition 6 ensures sj = sk. Thus, B is deterministic.

δ = { }; 1 foreach si ∈ S, a ∈ A do 2 Si = {sk ∈ S : si a ↪→ sk}; 3 if sj = min(Si) then δ := δ ∪ 〈si, a, sj〉 4

Example 5 On Example 4, Algorithm 1 would yield the BA of Figure 2(r) with states 1 and 2, state 2 in G, and transitions 〈1, a, 2〉 (based on the axiom for a), 〈2, a, 2〉 (based on applying CONSEQUENCE on the axiom for a), 〈2, b, 2〉 (〈2, b, 1〉 is not included, based on line 4 of the algorithm). Thus, even though Figure 2(l) and Figure 2(r) are not equivalent, based on our knowledge of the meanings, they are practically equivalent.

Example 5 is fortunate. The compilation doesn't always work. The following develops additional steps to make compilation work, or to determine that it cannot work. Correctness has two main aspects. Soundness means that the compiled BA won't realize a computation that the GCM wouldn't have generated. Completeness means that if the GCM can generate a computation, the compiled BA can realize it. Because the BA's transitions are chosen from among those in the GCM, soundness is guaranteed. This is Theorem 2.

Theorem 2 Let P be compiled into B. Then any computation realized by B is generated by P .

4.2 Completeness via Coherence

In general, because the BA may not include all the transitions of the GCM, it would not be complete. First, the BA may have no transition for a state and action, because none is the (unique) strongest, as required by Algorithm 1. To address this, the basic idea is to restrict GCMs such that if there is a transition for a state and action, then there is a strongest transition for the same state and action: by exploiting the action rule CONJUNCTION. Definition 8 captures this as coherence. However, Figure 3(l) shows a situation where a may occur in p and produce q1 and q2. That is, p a ↪→ q1 and p a ↪→ q2 both hold. In this situation, q1 ∧ q2 ̸∈ S. That is, coherence is violated.

Definition 8 For s ∈ S, a ∈ A, the projection of a on s, πa,s, is the set of states s′ in S such that s a ↪→ s′ . A GCM is coherent if (∀s ∈ S, a ∈ A : πa,s ̸= ∅ ⇒ (∃n ∈ S : s a ↪→ n and (∀s′ ∈ πa,s : n ⊢ s′ ))). Here, n is the supremal state for s and a, meaning it is the strongest resulting state.

Second, a GCM computation may involve a transition that doesn't exist in the BA. To address this, the basic idea is that because of the action rule CONSEQUENCE, although a specific GCM computation may not be realized in the BA, a computation taking the strongest state at each step would be realized. Thus the BA would be complete for practical purposes. Definition 9 and Lemma 3 capture this intuition.

Definition 9 A computation τ ′ = 〈s0, a0, s′1 , . . .〉 is the semantic supremum of a computation τ = 〈s0, a0, s1, . . .〉 if and only if τ ′ begins at the same state, involves the same action sequence as τ , and for each transition 〈si, ai, si+1〉 exercised by τ, τ ′ exercises a transition 〈s′i , ai, s′i+1 〉 where s′i+1 is the strongest consequence of performing a in s′i .

Lemma 3 Any computation that begins from s0 and is the semantic supremum of some computation in the GCM can be realized by the BA produced by Algorithm 1.

Proof. The proof is simply by transfinite induction on

computations: consider prefixes of length from 0 to ω.

Theorem 4 establishes our main completeness result finessed for coherent GCMs and supremal computations.

Theorem 4 Given a coherent GCM compiled into a BA, for any computation generated by the GCM that begins from s0, there exists a semantic supremum computation realized by the BA.

Proof. By construction of a coherent GCM and Lemma 3.

4.3 Producing Coherent GCMs

Let's now consider the question of whether and how an arbitrary GCM P can be mapped into an equivalent coherent GCM P ′ . Producing a coherent GCM requires ensuring that supremal states exist for each action allowed in each state.

Algorithm 2's first foreach block maintains a set of the known minimal states in the GCM P ′ being constructed, and examines each of them (including those newly added) to determine what new states are needed to ensure coherence. For Figure 3(l), this would add q1 ∧ q2 to U (and possibly to S′ ).

Although this would yield a coherent GCM P ′ , P ′ may generate computations that are unrelated to the computations in P. Consider Figure 3(r). Here q1 ∧ q2 is added to S′ . Assume it turns out that our action theory supports q1 ∧ q2 b ↪→ s but does not support that b can occur at q1 or at q2 (i.e., neither q1 b ↪→true nor q1 b ↪→true hold). Thus introducing q1∧q2 would generate a computation 〈. . . , p, a, q1 ∧q2, b, . . .〉, which is not generated by P . Algorithm 2's second foreach block checks if the newly added states allow transitions that weren't allowed by any of the original states they entail. If so, the new GCM would generate computations not allowed by the original GCM, and so the algorithm terminates in failure. This establishes Theorem 5.

Theorem 5 For an arbitrary GCM P , if Algorithm 2 succeeds, it produces a coherent GCM whose computations are generated by or are suprema of computations generated by P .

5 Discussion

GCMs capture the intuitions of CMs and provide additional descriptions and expressiveness. They put the work on CMs on a sound footing and show how to incorporate them in conventional settings. GCMs can apply to a wider variety of commitment protocols, not just those relating to terminating transactions. In general, BA cannot be determinized, but taking advantage of the semantics we can compile a GCM in many cases.

Other classes of automata on infinite computations exist. For example, BA can be determinized into M¨uller automata. However, determinizing involves at least an exponential blow up in the number of states. More importantly, doing so yields states that are not intuitive. This paper exploits meaning to find semantically equivalent automata. In essence, it maps an ω-language into a different ω-language, but one whose computations convey the same meaning as the original.

Previous work on CMs has shown how CMs can enhance a protocol by naturally allowing a wider range of computations while ensuring compliance. In general, a GCM need not include all the states possible from a given set of states and the action theory, which would lead to large BA.

It is important to note that protocols or GCMs are merely engineering artifacts. Specifically, if Algorithm 2 ends in failure, one might consider altering the GCM so that an acceptable coherent GCM is produced. From the standpoint of engineering, the selection of states is an important decision: not all states that are possible are created equal. When states are selected, criteria such as the following ensure that the resulting GCM captures a meaningful protocol: (1) from each state where a commitment holds, we can reach a state where the commitment is discharged; (2) like above, but for other commitment operations; (3) eventually the commitment or a commitment resulting from an operation on it is discharged. We lack the space to discuss methodology further. Suffice it to say that such requirements can be readily verified via reachability analysis on the BA representation of a protocol.

Previous work on protocols either takes an operational stance or discusses semantics, but generally doesn't relate the two. Labrou and Finin [1997] describe a grammar for constructing conversations or protocols. They also give a belief and intention based semantics, but the grammar and semantics are unrelated. By contrast, GCMs provide a semantics for messages that is directly operationalized.

McBurney and Parsons' posit spaces protocol consists of five locutions: propose, accept, delete, suggest revoke, and ratify revoke [2003]. Propose and accept are similar to conditional commitments. Delete corresponds to release or discharge. Suggest revoke and ratify revoke enable canceling of posits. Unlike GCMs, posit spaces do not support compilation to an automata representation.

Endriss et al. [2003] study protocol conformance for an interaction protocol that is defined as a deterministic finite automaton (DFA). The DFA is completely specified directly, meaning that it would be rigid or unwieldy for humans to study. Endriss et al. do not provide formalisms to enable agents to reason about their interactions as we have done here.

Acknowledgments

Thanks to Martin Purvis for hosting me at the University of Otago, Dunedin, New Zealand, where this paper was mostly written. Thanks also to Amit Chopra, Stephen Cranefield, and the anonymous reviewers for helpful comments.