1 Introduction↩︎

Enterprise and other applications, e.g., in business and healthcare, involve interactions between social entities such as humans and organizations [1] based on technical resources such as databases. A sociotechnical system (STS) involves social and technical entities [2], [3] and provides a useful abstraction for such applications. Today, an STS is implemented using a conceptually central service through which its entities interact. In contrast, we address the challenges of implementing a decentralized multiagent system (MAS) to realize an STS. Here, each principal maps to an agent; the agents interact with each other via asynchronous messaging.

The messages sent by an agent represent its public decisions. For example, a Quote by Seller (for an item and price) represents a decision by it; an Accept (of some Quote) sent by Buyer represents a decision of Buyer; and so on. To coordinate their decisions, the agents rely on an interaction protocol. By specifying the constraints on messaging, a protocol specifies the constraints on decision making between the agents in a MAS. For example, a Purchase protocol in the above-introduced e-business setting may specify that the price is offered by the seller, and payment is required for delivery.

A protocol is specified abstractly with reference to roles to be adopted by agents in a multiagent system. Implementing an agent according to a role means fleshing out the role with private (internal) decision logic that results in messages being emitted, that is, decisions being made [4]. For example, suppose agents Bob and Sally play Buyer and Seller, respectively, in Purchase. Sally’s decision logic may be to send Quotes with lower prices to repeat buyers. Bob’s decision logic may be to Accept a Quote if the price fits within its budget. Such decision logic is the essence of an agent.

Supporting the common desire [5], [6] for programming models that separate business logic from other components—and combating complexity in agent communication [7], in general—proves challenging. Traditional protocol languages [8]–[12] specify message ordering, which limits flexibility [13]. JADE [14], [15], a programming model for multiagent systems, is noteworthy for its early support for FIPA protocols [16]; however, the FIPA approach is long outdated [17] and the FIPA protocols are limited to a few patterns of interaction specified in terms of message ordering. Agent-oriented programming models such as Jason [18] and JaCaMo [19] provide cognitive abstractions for encoding an agent’s internal reasoning but do not support protocols. Existing commitment-based approaches [20], [21] either rely on centralized commitment stores [22] or do not adequately address operationalizing asynchronous communication [23]; some approaches map the problem to protocols [24], [25]—and hence within the scope of this paper. Traditional agent-oriented methodologies [26]–[28] emphasize and incorporate protocols as design abstractions. However, the protocol specifications in these approaches are informal (usually UML interaction diagrams), which rules out protocol-based software abstractions for engineering agents. In a nutshell, today we lack a protocol-based programming model for agents that supports flexible, decentralized decision making via asynchronous messaging.

Our contribution, Kiko, addresses this gap. Specifically, Kiko advances a novel decision-oriented programming model that enables structuring and implementing agents based on the protocol roles they play. Kiko’s fundamental abstraction is that of a decision maker, a construct for capturing the decision logic that selects and makes a set of decisions from those currently available. The agent developer’s primary task is to write the set of decision makers.

Kiko guarantees an agent’s compliance with the roles its plays. Kiko supports practical decision-making patterns that challenge other approaches, including correlation, cross-enactment reasoning, emission sets, and multiprotocol reasoning. Notably, in providing a decision-based programming interface, Kiko abstracts away the communication service that transports messages between agents. In particular, decision making in Kiko avoids having to deal with the order in which messages are received. Actual message emission is also handled transparently in the programming model.

In addition, we contribute a formalization of the programming model and prove its soundness and completeness with respect to possible protocol enactments. We also present an optimized compliance-checking method and establish its validity.

2 Information Protocols Introduced↩︎

A protocol-based programming model for agents presumes a language in which to specify protocols. We adopt BSPL [29], a declarative protocol language that eschews the specification of message ordering and instead specifies information constraints.

Purchase {
  roles Buyer, Seller
  parameters out ID key, out item, out price, out done
  
  Buyer -> Seller: RFQ[out ID key, out item]
  Seller -> Buyer: Quote[in ID key, in item, out price]
  Buyer -> Seller: Buy[in ID key, in item, in price, out done]
  Buyer -> Seller: Reject[in ID key, in price, out done]
}

An information protocol in BSPL specifies the roles, messages between roles, and information constraints that define which message emissions are valid. Information causality captures information dependencies: what information must or must not be known by an agent playing a role to be able to send a message. Information integrity captures consistency in distributed settings: there cannot be two messages sent with conflicting information in the same protocol enactment. Given the local store of an agent (its history of message observations), an agent can send any message that satisfies the specified causality and integrity constraints.

Listing [BSPL:Purchase] illustrates the main ideas of information protocols. It specifies a purchase protocol to be enacted by agents playing roles Buyer and Seller. Purchase composes message schemas, each with its sender and receiver roles and information parameters. For example, RFQ is from Buyer to Seller and its parameters are ID and item. A concrete message instance associates the parameter names with value bindings, e.g., binding ID to a UUID and item to “ball.”

To support information integrity, some parameters in a message schema are annotated key, e.g., ID in all the messages of Listing [BSPL:Purchase]. A tuple of bindings for the key parameters of a message schema uniquely identifies both an instance of the schema and the enactment to which it belongs, in which all nonkey parameters may have at most one binding. For example, say RFQ occurs with bindings [ID: 10, item: ball]. Then, a Quote with [ID: 10, item: hat, price: 10] would violate integrity because for the same binding of ID there are different bindings of item. Conversely, Quote with [ID: 11, item: hat, price: 10] satisfies integrity despite the different binding for item because it has a different binding of the key ID.

In a message schema, every message parameter is adorned \(\ulcorner\mathsf{in}\urcorner\), \(\ulcorner\mathsf{out}\urcorner\), or \(\ulcorner\mathsf{nil}\urcorner\). Adornments capture information causality constraints for the emission of an instance of a schema; \(\ulcorner\mathsf{in}\urcorner\) parameters must be known from prior communications (they are causal dependencies); \(\ulcorner\mathsf{out}\urcorner\) parameters and \(\ulcorner\mathsf{nil}\urcorner\) parameters must not be known, but \(\ulcorner\mathsf{out}\urcorner\) parameters are bound in the emission. For example, in Listing [BSPL:Purchase], Seller must know item before it can send Quote, and in doing so produces a binding for price.

Knowledge of a parameter exists in the context of some binding for the associated key. After receiving an RFQ with bindings [ID: 10, item: ball], Seller knows that in the enactment ID=10 item is bound to ball, and can produce a binding of price by sending Quote.

Integrity and causality apply to protocols generally. In Purchase in Listing [BSPL:Purchase], all protocol parameters are adorned \(\ulcorner\mathsf{out}\urcorner\) in the protocol parameter line, meaning that each enactment of Purchase as identified by the ID generates bindings for all of them. Further, the parameter line enables composition with other protocols.

3 The Kiko Programming Model↩︎

We introduce the architectural basis for the programming model, followed by examples that illustrate its features.

Figure 1 shows the main components of the agent architecture as focused on enacting protocols. The MAS Info and Decision Makers are components provided by the agent programmer (indicated by the border). The Protocol Adapter is a generic component provided by Kiko that understands information protocols and provides an API for plugging in Decision Makers. The adapters of all agents collectively achieve a coordination service and assimilate information received from messages [30]. The Communication Service is anything that provides asynchronous messaging between agents. Our implementation uses UDP, which is unordered and unreliable (lossy).

An information protocol constrains only the emission of messages by agents, based on its causal dependencies. This means that ordered delivery, as provided by TCP or a message queue, is not required for correctly enacting a protocol. Further, message reception is idempotent, so messages can be retransmitted to enact a protocol reliably despite message loss [31], [32]. Thus an unordered, lossy transport like UDP is sufficient for enacting BSPL protocols.

MAS Info (Configuration). A protocol specifies a MAS abstractly via reference to roles. A concrete MAS for a protocol is identified by a UUID and assigns roles to the agents that will play them. MAS identifiers are essential since an agent may play a role in several MAS. The properties of a (concrete) MAS and the mailboxes of the agents in the MAS are common knowledge to the agents in the MAS. Kiko requires each agent to be configured with such knowledge; Listing [lst:agent-config] gives such a configuration for agent Bob.

self = "Bob"
systems = {
  "5feceb66": {
    "protocol": Purchase,
    "roles": {Buyer: self, Seller: "Sally"}}}
agents = {
  self: [("192.168.1.100", 1111)]
  "Sally": [("192.168.1.102", 1111), ("152.1.27.202", 1111)]}

In Listing [lst:agent-config], 5feceb66 is an identifier for a MAS that enacts Purchase with Bob and Sally as Buyer and Seller, respectively. Bob’s and Sally’s mailboxes are given as (IP, port) tuples. An agent may have several mailboxes for receiving messages; in Listing [lst:agent-config], Sally has two. Our focus is not on how a MAS is constituted, but on programming abstractions that enable decentralized decision-making. Listing [lst:agent-config] shows the kind of information needed to configure a MAS, and it could be constructed dynamically at runtime.

Formally, we model an agent using a tuple \(\langle a, H_a, I_a, O_a \rangle\), where the components are the name of the agent, its history, input channel (its mailbox), and output channel respectively. Channels \(I_a\) and \(O_a\) are simply sets of message instances being sent and received, respectively, by agent \(a\). Definition 1 defines a MAS.

Decision Makers. To write an agent, programmers supply the configuration and write one or more decision makers. A decision maker is invoked upon the occurrence of specified events. When invoked, the adapter supplies it with prototypes of message instances that the agent is enabled to send given the agent’s current history of message observations. We refer to these prototypes as forms, after documents with fields that need to be filled. A form of a message schema has bindings for the parameters that are adorned \(\ulcorner\mathsf{in}\urcorner\) in the schema, reflecting that its causal dependencies are satisfied, leaving only the parameters adorned \(\ulcorner\mathsf{out}\urcorner\) to be bound. The purpose of a decision maker is to flesh out some message instances from the forms by supplying bindings for their \(\ulcorner\mathsf{out}\urcorner\) parameters; the adapter collects this set of completed instances as an emission attempt. The adapter verifies whether the attempt as a whole is consistent with the agent’s history and if so, emits the instances in the attempt; else it rejects the attempt.

Suppose Bob’s history is empty (it has observed no messages). Then the only form available to Bob is Bob -> Sally: RFQ[5feceb66, (ID), (item)], with unfilled parameters in parentheses. Since protocol enactments occur within the context of a MAS, each form and any instance produced from it contains a MAS identifier (here, 5feceb66)—conceptually like the value for an implicit parameter system in every message. Bob’s programmer may have written a decision maker that fleshes out the above form into instances such as Bob -> Sally: RFQ[5feceb66, 1, bat] and Bob -> Sally: RFQ[5feceb66, 2, ball] based on some decision logic. These instances are passed on to the adapter for emission. Listing [BSPL:buyer-init] shows a decision maker (in Python) called start that is invoked at system initialization, upon InitEvent. The argument enabled contains the available forms when start is invoked and the body of start contains code to send two instances of the form, one each for bat and ball. The instruction to the adapter to emit the instances is implicit—after the decision maker returns, the adapter goes through all forms to see which ones have been fleshed out into instances and emits them (conditional to validation).

@adapter.decision(event=InitEvent)
def start(enabled):
    for item in ["ball", "bat"]:
        ID = str(uuid.uuid4())
        for m in enabled.messages(RFQ):
            m.bind(ID=ID, item=item)

Consider another example. Suppose Bob’s history contains the above two RFQ instances and Sally -> Bob: Quote[5feceb66, 1, bat, 5]. Then, in addition to the RFQ form specified above, the following forms would also be available to Bob: Bob -> Sally: Buy[5feceb66, 1, bat, 5, (done)] and Bob -> Sally: Reject[5feceb66, 1, bat, (done)]. Bob’s programmer may have implemented a decision maker (as illustrated in Listing [lst:Bob-buy-reject]) that chooses from one of these two available forms based on how acceptable the price is, fleshes it out by binding done, and instructs the adapter to emit the resulting instance.

@adapter.decision
def start(enabled):
    for m in enabled.messages(Buy):
        if(m["price"] < 20)
            m.bind(done="cool")
        else
            reject = next(enabled.messages(Reject, ID=m["ID"]))
            reject.bind(done="rejected")

We now give an example where a decision maker’s emission attempt fails because it erroneously contains incompatible instances. Specifically, Listing [lst:contradiction] is erroneous because Bob creates instances for both Buy and Reject in the same enactment. This emission attempt fails because Buy and Reject are mutually exclusive according to Listing [BSPL:Purchase] (because both bind \(\ulcorner\mathsf{out}\urcorner\) done); neither will be emitted.

@adapter.decision
def indecisive(enabled):
  buy = next(enabled.messages(Buy))
  reject = next(enabled.messages(Reject, system=buy.system, ID=buy["ID"]))
  buy.bind(done="accepted")
  reject.bind(done="rejected")

Listing [lst:contradiction]’s error brings out a remarkable aspect of Kiko. Kiko enables decision makers (programmers) to choose sets of instances to emit. Whereas each of the instances in the set (e.g., Buy) would be individually consistent and compatible with the history when the decision maker was invoked and therefore could be emitted by the adapter, collectively, the set of instances chosen by the decision maker could be internally incompatible (Buy and Reject) and therefore fail emission by the adapter. By rejecting incompatible emission sets, the adapter guarantees that an agent will not make noncompliant emissions.

An alternative would be to limit a decision maker to work on at most one form at a time. Then, its emission by the adapter would be guaranteed. Such a decision maker is a special case for Kiko.

A specific triggering event may be specified for a decision maker (e.g., InitEvent in Listing [BSPL:buyer-init]). If such a triggering event is not specified (e.g., as in Listing [lst:Bob-buy-reject]), the adapter automatically invokes the decision maker whenever a communication event occurs. Event-based invocation enables some optimizations: First, the agent need not poll to wait for enough information to make a decision; not polling may be seen as an extension of the pub/sub pattern because a decision can depend on multiple pieces of information from multiple sources. Second, because all constraints are relative to an enactment, and communication events contain keys identifying their enactment, the enactment can be directly looked up, thus avoiding linear scans or joins across an entire database for validation.

However, there are cases where an agent may want to emit messages outside of reacting to a message observation (whether sent or received). For example, if the agent needs to make business decisions only once per day, then waiting and making them all as a batch could be more efficient and accurate. To support a wider variety of behavioral patterns, Kiko uses an internal event queue on which the developer can signal custom events, and decision makers can be registered with custom filters to select which events should trigger them.

We now formalize the concepts introduced in the above section.

An association binds values to some subset of the parameters of a message schema.

We use \(\widehat{m}[...]\) for projecting parameters to their bindings in the message instance; e.g., \(\widehat{m}[\mathscr{s}_m]\) is the sender of \(\widehat{m}\), and \(\widehat{m}[\vec{k}_m]\) is the projection of \(\widehat{m}\)’s key parameters.

A message instance is an association where all parameters are bound.

A form is an association where the \(\ulcorner\mathsf{out}\urcorner\) parameters are unbound.

We introduce the notion of context to capture enactments within a specific MAS.

Associations share context if their MAS and any of their keys have the same bindings. A form is enabled when all of its \(\ulcorner\mathsf{in}\urcorner\) parameter bindings match those from observed instances that share context (consistency), and its \(\ulcorner\mathsf{out}\urcorner\) and \(\ulcorner\mathsf{nil}\urcorner\) parameters do not conflict with any observed instances (compatibility), as given by Definitions 6—10.

Definition 11 says a decision maker constructs only instances that preserve the bindings from message forms.

3.1 Decision-Making Challenges and Solutions↩︎

We highlight select decision making patterns supported by Kiko.

3.1.1 Correlation↩︎

An agent may simultaneously be involved in several enactments of a protocol. For example, Buyer may be concurrently engaged with Seller in several distinct enactments, each for some item at some price. The programming model should enable correlating communications by enactment.

Kiko supports correlation through the automatic derivation of correlated forms by the adapter (as described above). The adapter computes forms based on all information available, potentially from the observation of multiple correlated instances. Kiko also makes it convenient to find correlated forms where the decision logic requires it. For example, in Listing [lst:Bob-buy-reject], correlated Reject forms are found by the ID of the Buy forms.

3.1.2 Cross-Enactment Decisions↩︎

Agents should be able to use information across enactments in their decision making.

Kiko enables cross-enactment reasoning by providing forms from all currently active contexts, that is, enactments in all systems, to the decision makers together. Thus, the decision maker can select forms from multiple contexts and flesh them out for emission. For example, Bob could participate in multiple systems, all enacting Purchase, to request quotes for the same item from multiple sellers. Then, Bob can send a Buy for the Quote with the lowest price (Listing [Bob:cheapest-buy]).

@adapter.decision
def cheapest(enabled):
  buys = enabled.messages(Buy)
  cheapest = min(buys, key=lambda b: b["price"])
  cheapest.bind(done=True)

3.1.3 Multiple Protocols↩︎

An agent will often play roles in multiple unrelated protocols, using information from one to make decisions in another.

Kiko enables implementing agents that play roles in multiple unrelated protocols. For example, we specify Approval in Listing [BSPL:Approval]. By enacting Approval concurrently with Purchase, Bob can seek Alice’s approval on any purchases. To do so, Bob must map between the protocols inside its decision makers, which is supported by the enabled set containing forms from all the protocols Bob is enacting.

Approval {
  roles Requester, Approver
  parameters out aID key, out request, out approved
  
  Requester -> Approver: Ask[out aID key, out request]
  Approver -> Requester: Approve[in aID, in request, out approved]
}

Listing [lst:request-approval] shows Bob’s decision maker for constructing an Ask (approval) for each Buy as it becomes available as a form, copying Buy’s payload into request.

@adapter.enabled(Buy)
def request_approval(buy):
    ask = next(adapter.enabled_messages.messages(Ask), None)
    return ask.bind(ID=str(uuid.uuid4()), request=buy.payload)

3.1.4 Emission sets↩︎

For additional flexibility, Kiko enables a decision maker to emit multiple instances atomically: if the instances are mutually compatible, then they are all emitted, else none are emitted. Thus, e.g., if an emission set contained Buy and Reject instances for the same enactment, no instance in the set would be emitted. Such atomicity of emission ensures correctness and gives full authority to the decision maker to choose its intended messages; multiple attempts can be made if needed. Selecting some consistent subset of the emission set for emission, by contrast, would be arbitrary and could lead to unintended enactments.

Listing [lst:buyer-implementation] shows a decision maker, where Bob figures out the best combination of items it can buy (as computed by some optimization, whose details are not relevant for our purposes), sending Buys for all those items and Rejects for the others.

@adapter.decision
def select_gifts(enabled):
    best, rest = best_combo(enabled)
    for b in best:  # buy the best items
        b.bind(done=True)
    for r in rest:  # reject the rest
        r.bind(done=True)

Another variety of decision logic where emission sets are valuable is a combination of “front-end” and “back-end” reasoning. For example, imagine Sally has a supplier with whom it engages via some protocol. Suppose Sally wants to order an item from its supplier whenever it delivers an item to a buyer. To accomplish this, it may have a decision maker which puts Deliver (to the buyer) and Reorder (from supplier) in the same emission set.

3.1.5 Reception-Order Freedom↩︎

Requiring agents to receive messages in a particular order can only delay the reception of information, which in turn would limit the agent’s ability to respond flexibly to events.

Kiko takes advantage of the fact that BSPL doesn’t rely on message ordering for correctness, and abstracts away message reception entirely from decision making. An agent’s adapter receives messages as they arrive and depending on the information in them, makes forms available to decision makers. By doing so, Kiko enables agents to respond flexibly to events.

Seller -> Buyer: Rescind[in ID key, in item, in price, out rescinded]
  Buyer -> Seller: Buy[in ID key, ..., nil rescinded]

For example, Listing [BSPL:rescind-quote] extends Purchase by allowing Seller to Rescind a quote. Because it depends on price, Rescind must be sent after Quote, but could reach Bob first. Because reception is not constrained except by integrity (inconsistent messages are rejected), Rescind will be received, checked, and added to the history when it arrives. As such, the matching Buy will be disabled, and Bob need not waste any effort considering it (e.g., by requesting approval).

Note that by programming in terms of enabled forms, a decision maker such as the one in Listing [lst:Bob-buy-reject] that emits Buys need not change at all; the disabled Buys are simply not provided to the decision maker for consideration.

3.1.6 Loose Coupling↩︎

Clearly, protocols support the independent development of agents by capturing the constraints relevant to interoperation between them. In general, if a protocol changes, then one would expect that the agents’ decision making would have to change as well. Because Kiko is based on information though, it is not necessarily the case that protocol changes lead to changes in an agent’s decision making, thus supporting loose coupling even better.

For example, suppose (as illustrated in Listing [BSPL:delivery]) Purchase included a Deliver message from Seller that depended on payment provided by Buy:

Buyer -> Seller: Buy[in ID key, in item, in price, out payment]
  Seller -> Buyer: Deliver[in ID key, in payment, out delivery]

Then, suppose Purchase were extended so that Buyer could pay indirectly via bank transfer (as illustrated in Listing [BSPL:bank-transfer]) . Because the messages in Listing [BSPL:bank-transfer] do not change the messages emitted by Seller, only how it receives the necessary information, Seller’s decision logic need not be changed to support indirect payment. Seller’s adapter will automatically derive the Deliver form when the indirect payment has been received, demonstrating loose coupling between the agents.

Buyer -> Seller: Accept[in ID key, in price, out acceptance]
  Buyer -> Bank: RequestTransfer[in ID key, in price, out txinfo]
  Bank -> Seller: Transfer[in ID key, in txinfo, out payment]

3.1.7 Single Form Decision Makers↩︎

The general decision making pattern of supporting the emission of sets of instances is highly flexible, but for cases in which an agent need emit only instance at a time, Kiko supports the convenient abstraction of single form decision makers. Such decision makers are functions invoked with a single message form; its return value is either a message instance for emission (binding its \(\ulcorner\mathsf{out}\urcorner\) parameters), or a null value canceling the emission. Listing [lst:quote-enablement] shows an example where an enabled form of Quote is fleshed out.

@adapter.enabled(Quote)
def send_quote(msg):
    msg["price"] = random.randint(20, 100)
    return msg

3.2 Adapter Implementation↩︎

Figure 2 blows up the adapter from Figure 1 to highlight its internal components (highlighted in green).

The Emitter and Receiver interface with the communication service, putting messages on and receiving them from the wire, respectively. The Local Store records the agent’s history of emissions and receptions. The Checker validates (checking for satisfaction of causality and integrity constraints in the protocol specifications) any attempt (by a decision maker) to emit a set of messages (Definition 12). If an attempt is validated, then the instances in it are added to the Local Store and passed on the Emitter for emission; else, the attempt is discarded.

The Checker also validates received messages for integrity; if they pass, they are added to the Local Store, else they are discarded (Definition 13).

The Local Store is used by Enablement to compute the forms that the agent is enabled to send. Algorithm [algo:derive] describes how enabled forms are computed for each context. We use an incremental method, so that only those contexts that have new information are updated. First, on Line 3, every context that shares key bindings with the observed instance \(\widehat{o}\) is checked to see if it enables any instances of \(m\). Lines [line:derive-check-outs] and [line:derive-check-nils] check that the \(\ulcorner\mathsf{out}\urcorner\) and \(\ulcorner\mathsf{nil}\urcorner\) parameters of the schema, respectively, are not already bound in the context. Line [line:derive-check-ins] copies the bindings of the \(\ulcorner\mathsf{in}\urcorner\) parameters from the context, Line [line:derive-system] copies the system ID, and Line [line:derive-add-form] adds the form to the result set for processing by decision makers.

4 Operational Semantics↩︎

Protocols are formalized in an online Appendix. Here, we formalize an agent and MAS computations via a transition semantics.

Figure 4 gives the transition semantics.

The Recv rule specifies how messages are received. For agent \(a\) to receive a message instance \(\widehat{m}\) there are three conditions:

If these three conditions are met, then \(\widehat{m}\) is added to \(H_a\).

The Tx rule models message delivery by copying messages from an output channel to the appropriate input channel; unreliability is modeled by not exercising the rule.

Finally, Decide specifies how messages are instantiated for emission: First, a set \(Q\) of message forms is computed based on the agent’s history. Next, a set of instances are derived from the message forms by applying a decision maker \(d\) to the enabled form set. If this set of instances is valid, then it is added to both the agent’s history and output channel. Otherwise, the rule cannot be applied and no messages are sent.

No rules are required for cases where the messages fail a validity check; there is simply no transition in those cases. A transition for a MAS is simply a transition for one of its agents.

Figure 5 shows an alternative version of the Decide rule, \(\mathrm{\small Decide}_2\). Because transitions are atomic, the forms will not be disabled before the transition completes, so they do not need to be rechecked for validity; checking internal compatibility is sufficient (e.g., not selecting both an Accept and Reject in the same enactment). Checking only internal compatibility of a small set of emissions should be faster than a full send-check, which requires both internal compatibility and that the instance is consistent and compatible with the rest of the agent’s history.

Our goal is to show that a MAS developed using our operational semantics to implement a protocol will be both correct (that is, reach only valid states) and complete (it is possible to implement a system that can reach any valid state). As such, we formalize the state of a MAS, which states are reachable according to the operational semantics, and which states match a protocol enactment.

\(\mathcal{E}_P\) (formally defined in the appendix) is the set of reachable enactments of protocol \(P\), where a reachable enactment \(E \in \mathcal{E}_P\) is a set of role histories each constructed by a sequence of viable events according to \(P\)’s specification.

Simulation is the idea that transitions in the MAS should match the reachable enactments in its protocol; each transition may be equivalent to a set of multiple viable extensions because the Decide rule can produce a set of message instances, where viable extensions cover only one instance at a time.

Theorem 1 gives the correctness of our operational semantics by showing that compliant MAS can only reach states that match reachable enactments of a protocol. Even though the states reached by the MAS will depend on the decision makers, they can only select subsets of the enabled forms, and therefore cannot reach an invalid state (that is, one that does not match an enactment that is reachable under the protocol semantics).

Theorem 2 shows that the conditions for Decide are redundant, given that the forms are drawn from \(\textsf{enabled}(a,H_a)\) and decision makers preserve their bindings (and thus consistency and compatibility with history); all that needs to be checked for the selected emissions \(T\) is that they are compatible with each other.

Theorem 3 shows completeness for our operational semantics: the operational semantics do not restrict a MAS from simulating any reachable enactment of the protocol. Or, given a reachable enactment of a protocol, it is possible to construct decision makers for the agents that would reach that enactment. This is not to say that every implementation is complete; proving completeness for a given implementation would require formalizing its decision makers as transition rules.

The proofs of these theorems are in the appendix.

5 Discussion↩︎

Kiko bridges business logic and communications: an agent provides business decisions and the underlying adapter applies the protocol semantics to determine which messages are viable. The underlying causal information semantics captures the information flow and avoids having to generate guards [33]. An agent makes and communicates a set of decisions (as reflected in the forms provided by the adapter) based on some evaluation of the state of the world. The decision making is conceptualized declaratively and suits rule-based programming languages such as Jason.

An interesting direction is to extend Kiko’s notion of forms to support norms-based decision making. For example, the discharge of a commitment by an agent could be made available as a form to be picked and instantiated by the agent. [34] present a model for accountability that is implemented in JaCaMo via obligations and relates to both (the giving of) accounts and recovery strategies when things go wrong. Kiko’s adapter could incorporate standard protocols for demanding accounts from other agents when norm violations occur and incorporate them into further decision making, e.g., to decide from which agent to buy items.

Variants of programming models based on information protocols have been proposed in recent years. The idea of enabled message forms was first introduced in Stellar [35]; however, Stellar lacked support for emission sets and relied on the abstraction of message handlers as opposed to decision makers. Thus, Bob’s implementation in Stellar would be a set of message handlers, one for each type of message it could observe. Within a message handler, one could retrieve a form and instantiate it. Message handling-based abstractions are lower level compared to Kiko’s decision makers, which are information-based. To see this, suppose an agent needed information from two instances, say \(i_1\) and \(i_2\), which it may receive in any order, to be able to send a third instance \(i_3\) (e.g., a shipper may need the address from the buyer and the item from the seller to be able to deliver). Then, in the message handling approach of Stellar, one would write separate message handlers for \(i_1\) and \(i_2\) and in each one check whether the form for \(i_3\) is available. By contrast, in Kiko, one would simply write a single decision maker that completes the form for \(i_3\). The Mandrake [36] and PoT [31] programming models share Stellar’s limitations; however, they both also address application-level fault tolerance, a theme that is a direction for Kiko.

Like Stellar (and Mandrake and PoT), Kiko enables building applications directly over an unordered, unreliable communication service such as UDP for message transport. Kiko is therefore compatible with the influential end-to-end argument [37], which advocates building applications over simple communication services, both for reasons of enabling application-level flexibility and performance. By contrast, message ordering-based protocol approaches would be incompatible with the end-to-end argument. Establishing the performance of Kiko-based agents and MAS compared to traditional application architectures that rely on complex communication services and middleware is a crucial direction. Preliminary evidence from Mandrake and PoT indicates high performance.

Kiko’s features such as support for correlation, cross-enactment reasoning, and multiple protocols are not readily supported in programming models for message ordering-based protocol approaches. This is because all of the above features have to do with querying information, which is inadequately represented in ordering-based protocols. Emission sets are unique to Kiko and are a powerful feature that enables emitting a set of message instances (possibly from different protocols and to different agents) atomically.

In our semantics, decision makers execute atomically with respect to the history, which simplifies checking the internal compatibility of the emission set before emitting all its instances. However, an alternative semantics is possible where decision makers execute concurrently from the same history. Concurrent execution would enable taking advantage of multicore and cloud architectures. Implementation-wise, decision makers could be spawned off as actors [38], [39]. The tradeoff is that the emission sets produced by concurrent decision makers may be in conflict with each other (e.g., one set contains Buy whereas another contains Reject for the same enactment) and therefore an internal compatibility check would no longer suffice. Each emission set would have to be checked for validity against the history, which could be more expensive.

IoT-based paradigms such as edge and fog computing and the industry paradigm of realizing applications via microservices are conceptually decentralized. In the case of microservices especially, decentralization is driven by the scalability afforded by the containerization of application components. Current microservices development approaches tend to avoid distributed database transactions in favor of loose coupling [40]. However, this raises the question: On what basis should microservices coordinate their computations? Information protocols could be thought of as a model for business transactions. Therefore, approaches like Kiko, suitably adapted to microservices, can help.

SARL [41], an agent programming language, supports communication using events in spaces that are akin to environments [42]. SARL would benefit from a protocol-based programming model. Kiko would benefit from a more general treatment of events. Currently, in Kiko, messages model events. However, some domain events don’t map to messages. For example, while a Quote may reasonably be modeled as a message, Shipment may actually correspond to a package traveling in the back of a truck. Receiving a shipment, therefore, requires sensing the arrival of the package. Extending Kiko’s adapter to incorporate observation of events from the environment would be valuable.

Supplementary Material. The appendix and the Kiko software are available at: https://gitlab.com/masr/bspl/-/tree/kiko.

Acknowledgments↩︎

We thank the anonymous reviewers for their comments. We thank the EPSRC (grant EP/N027965/1) and the US National Science Foundation (grant IIS-1908374) for partial support.

References↩︎