Information-Driven Interaction-Oriented Programming: BSPL, the Blindingly Simple Protocol Language

Reference: Munindar P. Singh (2011). Proc. 10th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2011), Taipei, Taiwan, May 2–6, 2011, pp. 491–498. IFAAMAS. URL. PDF

Summary

Singh introduces BSPL, a declarative language for multiagent interaction protocols built from exactly two constructs: a message schema (a single message is an atomic protocol) and the composition of existing protocols. The paper’s programme is interaction-oriented programming (IOP): treat the protocol as an engineering abstraction in its own right, specify it in terms of the information it needs in order to proceed and the information it produces when enacted, and let agents be independently designed and operated, judged only by their participation in the specified interactions. BSPL states no constraints on the ordering or occurrence of messages. Every ordering and exclusion requirement that a traditional protocol notation would express with control-flow or choice operators is instead derived from the information model of the messages.

The mechanism is parameter adornment. Each protocol and each message carries parameters, and each parameter is adorned ⌜in⌝ (its binding must come from outside, that is from a prior message), ⌜out⌝ (its binding originates here, with declarative force) or ⌜nil⌝ (the sender must not know a binding at emission time). Some parameters are marked as the key: a key binding identifies an enactment, and any parameter may be bound at most once per key binding. From these follow BSPL’s three commitments to the relational view of protocols as tables of enactments: uniqueness (one enactment per key), integrity (every public parameter bound in a complete enactment) and immutability (bindings never change, which is what makes the design robust to asynchrony). Ordering emerges as ⌜out⌝-before-⌜in⌝ on a shared parameter; mutual exclusion emerges as two messages both adorning the same parameter ⌜out⌝ for the same key; conventional orderings that carry no information (pay before delivery) are captured by introducing a token parameter. Composition renames parameters through references, so the foreign-exchange case study (bilateral price discovery composed with itself into multilateral price discovery, from Desai et al.) needs no access to the constituents’ internals, unlike the AUML nesting and data-flow-axiom approaches it is compared against.

The semantics is sketched rather than formalised (that is the work of Semantics and Verification of Information-Based Protocols). A role’s history is the sequence of messages it has sent or received; a history vector collects one history per role; it is quiescent when every sent message has been received and viable when every emission was made by a role that knew all ⌜in⌝ bindings and no ⌜out⌝ or ⌜nil⌝ binding at the time. A protocol’s intension is its set of quiescent viable history vectors. Three conflict kinds organise correctness: ⌜out⌝–⌜in⌝ (ordering, handled by causality), ⌜nil⌝–⌜in⌝ and ⌜nil⌝–⌜out⌝ (knowledge, local to one role) and ⌜out⌝–⌜out⌝ (occurrence, which has no general solution but can be checked to be under one role’s control). Meaning is deliberately separated from structure: a means clause may attach a commitment to a message, and BSPL is offered as the operational substrate that commitment-based approaches such as Commitment Machines - Yolum and Singh previously lacked.

Key Ideas

Two constructs only. A protocol is one message schema or a composition of protocols; there is no distinction between atomic and composite protocols, and no sequence, choice or loop operator.
Information orientation and explicit causality. Every causal dependency is an information dependency: a message can be sent only when its ⌜in⌝ parameters are already bound in the sender’s local history. There are no hidden flows of causality because there are no hidden flows of information.
Adornments ⌜in⌝ / ⌜out⌝ / ⌜nil⌝ and keys. Adornments are relative to the protocol, not to a role. A top-level enactable protocol adorns all public parameters ⌜out⌝; a protocol with a public ⌜in⌝ parameter is not enactable on its own and must be composed.
Uniqueness, integrity, immutability. Enactments are immutable tuples keyed by the key parameters; a parameter bound twice for the same key is an integrity violation, which is how exclusive choice is expressed.
Shared-nothing enactment. No global state or repository is needed: everything relevant to the social state of an interaction is in the parameter bindings of the messages exchanged. Each agent acts from its local history alone.
Ordering and exclusion are derived. ⌜out⌝ precedes ⌜in⌝ on the same parameter; two ⌜out⌝ adornments of the same parameter make the messages mutually exclusive; ⌜nil⌝ forces a message before a role learns a binding.
Specification patterns. Duplicating a parameter, generating an identifier, local (hidden) parameters, standing offers with composite keys (Insurance Claims), flexible sourcing of ⌜out⌝ parameters, in-out polymorphism (an unadorned parameter accepts either direction), forwarding, mixed initiative, and digressions in the sense of Yolum and Singh.
Composition without breaking encapsulation. Multilateral price discovery is a composition of the generalised bilateral protocol with itself, with adornments in the two references doing the coordination work that Desai et al.’s data-flow axioms and Odell et al.’s AUML nesting required.
Comparison with procedural notations. Choreographies (WS-CDL, message sequence charts), AUML and RASA specify orderings directly; BSPL avoids the enactability failures Desai and Singh call blindness because the only way to state an ordering is a causally sound ⌜out⌝-to-⌜in⌝ flow. Nonlocal choice is not automatically avoided but is analysable.
Meaning stays separate. means clauses attach commitments to messages; BSPL supplies the operational underpinning that meaning-based protocol approaches assumed.
Named future work. Multiple keys, compositional verification of enactability, multicast (several agents playing one role) and discovery protocols with late role binding. Kohei Honda is thanked in the acknowledgements, a direct line to the Session Types tradition.

Connections

BSPL (concept hub)
Information Protocols
Enactability
Interaction Protocols
Semantics and Verification of Information-Based Protocols: the formal semantics and verifier for this language
Kiko - Programming Agents to Enact Interaction Protocols: the programming model built on it
Commitment Machines - Yolum and Singh
Flexible Protocol Specification and Execution
Commitment-Based Protocol
Commitment-based Semantics
ACL Rethinking Principles: the same author’s earlier argument for public, protocol-based ACL semantics
FIPA-ACL Specifications: the ordering-based interaction protocols BSPL positions itself against
Coordinating Agents Using ACL Conversations
Endpoint Projection
Session Types
Multiparty Asynchronous Session Types
Choreographic Programming
Knowledge of Choice
Realizability and Verification of MSC Graphs: the nonlocal-choice problem BSPL inherits from message sequence charts
Message Sequence Charts - A Survey
Declarative Specification
CALM Theorem: monotone local knowledge as the basis for coordination-free enactment
CBCL - Safe Self-Extending Agent Communication: the nearest contemporary relative; see the contrast on BSPL

Conceptual Contribution

Claim: Multiagent protocols can be specified without any control-flow constructs. Modelling messages by the information they require and produce, with adornments and keys, yields all necessary ordering and exclusion constraints, supports shared-nothing asynchronous enactment from local knowledge, composes without breaking encapsulation, and leaves meaning to a separate layer.
Mechanism: Message schemas with ⌜in⌝/⌜out⌝/⌜nil⌝ parameter adornments and key parameters; protocol composition by reference with parameter renaming; a relational reading of enactments (uniqueness, integrity, immutability); a sketched semantics of quiescent viable history vectors; a conflict taxonomy (ordering, knowledge, occurrence); a foreign-exchange case study against Desai et al.’s commitment-protocol formalisation.
Concepts introduced/used: Information Protocols, BSPL, Enactability, Interaction Protocols, Declarative Specification, Commitment-based Semantics, Knowledge of Choice, Realizability
Stance: language design / foundational
Relates to: Continues Singh’s programme from ACL Rethinking Principles (public, verifiable protocol semantics instead of mental states) and supplies the operational layer under Commitment Machines - Yolum and Singh and Flexible Protocol Specification and Execution. It is the multiagent-systems counterpart to Multiparty Asynchronous Session Types and Choreographic Programming: where those derive per-role behaviour from a global type by Endpoint Projection and presuppose a compiler and ordered channels, BSPL has no projection step at all, because every role acts directly on the global protocol using only its own history over an unordered transport. CBCL - Safe Self-Extending Agent Communication later arrives at a similar causal, coordination-free protocol layer from the LangSec side, with content-addressed predecessors and signatures in place of parameter keys.

Tags

#interaction-protocols #bspl #information-protocols #declarative #causality #decentralization #asynchrony #aamas

Backlinks

Linked Pages

CBCL - Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication

Reference: O’Connor, H. (2026). “CBCL: Safe Self-Extending Agent Communication.” 2026 IEEE Symposium on Security and Privacy Workshops (SPW), pp. 39–48. Preprint: arXiv:2604.14512v1 [cs.CR], 16 Apr 2026. Source file: oconnor-cbcl-langsec26.pdf. URL. Reference implementation: https://codeberg.org/anuna/cbcl-rs.

Summary

Building on McCarthy’s 1975/1982 Common Business Communication Language vision and the language-theoretic security programme of Sassaman, Patterson, Bratus and Locasto (Security Applications Of Formal Language Theory), this paper presents a contemporary CBCL: an agent communication language designed so that all messages — including runtime language extensions — remain within the deterministic context-free (DCFL) complexity class. The motivating diagnosis is that contemporary agent communication has slid up the Chomsky hierarchy without acknowledging the security cost: KQML and FIPA-ACL are CFL with informal extensibility, but MCP and LLM-based agent frameworks operate over inputs whose effective complexity is recursively-enumerable, where the validity of an arbitrary message is undecidable and “weird machines” (Exploit Programming - From Buffer Overflows To Weird Machines) become unavoidable. CBCL takes the opposite tack: minimal core (8 performatives — tell, ask, reply, hello, bye, ok, error, cancel) plus a homoiconic dialect mechanism that lets agents define, transmit, and adopt domain-specific vocabularies as first-class CBCL messages, with three machine-checked safety invariants — R1 (no recursion in dialect templates), R2 (declared resource bounds on depth, expansion size, verification time), R3 (core-vocabulary preservation) — that together guarantee DCFL preservation under arbitrary finite sequences of dialect installations.

The paper accompanies the design with a Lean 4 formalization (≈5,400 lines, 16 modules, 176 machine-checked theorems, zero sorry gaps, no custom axioms) covering parser correctness (soundness + completeness), R1–R3 verification, pipeline totality, and the central dcfl_preserved closure theorem; a verified parser binary cbcl-parse is extracted from the proofs. A separately-developed Rust reference implementation (cbcl-rs, ≈11,000 lines, no_std-compatible core) ships a hand-rolled O(n) parser, dialect verification engine, gossip-based dialect propagation (O(log n) convergence per Demers et al.), C FFI/WASM bindings, property-based and differential tests, and cargo-fuzz targets; differential tests cross-validate the Rust parser against the Lean-extracted binary, eliminating spec-implementation parser differentials. Five example dialects (precision agriculture, AI planning, cross-chain asset transfer, artifact management, email) are R1–R3-verified end-to-end. A draft IETF Internet-Draft specifying application/cbcl and a Nostr transport binding (cbcl-nostr) accompany the paper. The Discussion explicitly aligns the design with Singh’s social-agency programme: dialect installation is treated as a public commitment to the dialect’s declared semantics — semantic divergence becomes a breach of commitment, observable and accountable, rather than a hidden failure of shared mental state — sidestepping the unverifiable mentalistic semantics critique of Verifiable Semantics for ACLs.

Implementation status (post-paper, cbcl-rs). The reference implementation has shipped two further safety invariants the paper sketches as future work, plus a richer Lean formalisation: R4 (Integrity) — Ed25519-style signatures over canonical encodings via an algorithm-agnostic Signer trait, with three-valued install verdicts (Valid / Unsigned / Invalid) — and R5 (Contract Well-formedness) — optional (protocol …) and (shape …) clauses on a dialect, expressing causal Merkle DAG protocols and per-performative shape contracts; R5 enforces acyclicity, reachability from begin, performative definedness with ancestor closure for extends, step uniqueness, and depth-bound respect, all decidable in linear fuel at install time. The §VII-D structural-contracts vision is therefore live (SPEC-002, SPEC-003): verify_monotone, verify_all_is_meet, and verify_eventually_consistent are proved theorems showing causal-protocol verification is a lattice homomorphism that joins coordination-free under G-Set store merge — explicit CALM Theorem alignment. The Lean codebase has grown to 380+ declarations across 19 files (still zero sorry, only the standard axioms propext / Classical.choice / Quot.sound); the workspace ships 837 tests including 584 cbcl-core unit tests, 37 proptest cases, 21 differential integration tests against the Lean-extracted binary, libFuzzer harnesses, and cargo-mutants mutation testing at a 90% kill threshold. The crate layout has grown from the paper’s five to seven: the original cbcl-core / cbcl-parser / cbcl-cli / cbcl-wasm / cbcl-ffi plus cbcl-erl (Erlang/LFE binding, SPEC-009 — with SPEC-010 binding-conformance suite) and cbcl-arena (Agent Arena platform, SPEC-012 — composable referee on cbcl-lfe-router with capability-keyed message routing and signed receipt logs). A worked sealed-bid auction dialect (SPEC-004) demonstrates structural defence against false-claim manipulation — concrete evidence that the R5 contract layer is rich enough to encode mechanism-design integrity properties decidably. The earlier Scheme prototype (anuna-research/cbcl) is superseded; architecture decisions live as ADRs under .hence/ (purity boundary, parser library choice, error handling, WASM API surface, R4 adversarial review).

Key Ideas

DCFL as the Goldilocks complexity class: Regular is too weak for nested envelopes/dialects; general CFL admits ambiguous grammars and parser-differential attacks; context-sensitive is PSPACE-complete; Type-0 is undecidable. DCFL is the minimal class that supports nested structure with class-level unambiguity (parser equivalence under language evolution).
Homoiconic self-extension: Dialect definitions are themselves valid CBCL messages, parsed by the same recogniser used for ordinary communication — a single attack surface, no separate meta-language. Inspired by Racket’s #lang mechanism.
Three safety invariants R1–R3: declarative pattern-template substitution only (no recursion, no iteration, no reflection); declared resource bounds (depth ≤ 64, expansion ≤ 8192 chars, verification ≤ 1000 ms); the eight core performatives cannot be redefined.
DCFL preservation theorem: dialect invocations must appear inside a (lang name …) wrapper; the lang tag plus a unique dialect name forms a prefix-free partition that lets a deterministic pushdown automaton dispatch to the appropriate subgrammar without extra lookahead — circumventing the fact that DCFLs are not closed under union in general. Mechanised in Lean 4 as dcfl_preserved.
Lean 4 formalization with extraction: 176 theorems, 0 sorry gaps, no custom axioms; the verified parser binary cbcl-parse is extracted from the proofs and runs the same fuel-bounded recursive-descent parser as the model.
Rust reference implementation: cbcl-core (no_std, no unsafe), cbcl-parser, cbcl-cli, cbcl-ffi, cbcl-wasm. Differential tests against the Lean-extracted binary; cargo-fuzz over five entry points.
Eight core performatives (tell, ask, reply, hello, bye, ok, error, cancel) plus four message categories (simple, meta, lang-scoped, wrapped); keyword parameters in Common-Lisp style (:thread, :in-reply-to).
Single-pass template expansion: terminates in time linear in the template plus argument size; not Turing-complete; output is not fed back into the expander, ruling out unbounded re-expansion.
Epidemic dialect propagation: gossip-based with Demers et al.’s O(log n) convergence bound; agents independently verify R1–R3 and signatures before installing.
Canonical serialization per RFC 9804 for cryptographic operations — deterministic byte representation as a precondition for signature verification.
Dialect identity by content hash: name collisions resolved by canonical-form hash; downgrade attacks rejected at installation.
Self-expression vs self-adaptation (Zambonelli et al.): traditional ACLs support only parameter tuning within fixed structure; CBCL is a self-expressive protocol whose vocabulary structurally evolves under safety constraints.
Singh-aligned reading of dialect installation: a public commitment to declared semantics, with :examples clauses providing machine-checkable behavioural anchors — semantic divergence as observable breach rather than hidden mental-state mismatch.
Stated limitations: DCFL ceiling means no recursive transformations, no cross-field references (e.g. checksums over fields), no aggregation over variable-length collections, no context-sensitive validation. Standish-taxonomy paraphrastic only — no Orthophrase, no Metaphrase. Trust infrastructure (key distribution, revocation) and dialect-curation policy left to deployment.
Structural-contracts extension (sketched in §VII-D, shipped post-paper as R4 + R5): Ed25519-style dialect signatures plus protocol constraints as causal Merkle DAGs over performative-typed messages, with Visibly Pushdown Languages for shape constraints and coordination-free monotonic verification over an append-only store. Lean-mechanised lattice-homomorphism theorems (verify_monotone, verify_all_is_meet, verify_eventually_consistent) establish that replica verdicts join under G-Set merge.

Connections

Common Business Communication Language — McCarthy’s 1975/1982 origin; CBCL is the formally-verified realisation of that vision.
Security Applications Of Formal Language Theory — Sassaman et al.’s LangSec foundations.
Proof-Carrying Code - Necula — Necula 1997, the architectural ancestor of CBCL’s R4 split (host runs a small certified verifier; producer ships the proof).
Enforceable Security Policies - Schneider — Schneider 2000, the formal warrant for R5 monotone-verdict trace monitoring.
An Axiomatic Basis for Computer Programming - Hoare — Hoare 1969, root of the contract-based verification line CBCL inherits.
Authentication in Distributed Systems - Lampson Abadi Burrows Wobber — Lampson et al. 1992, the Speaks-For Calculus for delegated commitments.
Articulating Reasons - Brandom — Brandom 2000, the philosophical underwriting of Public Semantics (entry point).
Making It Explicit - Brandom — Brandom 1994, the full inferentialist treatise.
Empiricism and the Philosophy of Mind - Sellars — Sellars 1956, the Myth of the Given that makes Semantics-Without-Minds possible.
Philosophical Investigations - Wittgenstein — Wittgenstein 1953, Meaning As Use / language-games / rule-following.
Two Dogmas of Empiricism - Quine — Quine 1951, Semantic Holism.
Assertion - Stalnaker — Stalnaker 1978, Common Ground update semantics — operational analogue of CBCL’s verdict ledger.
Languages and Language - Lewis — Lewis 1975, Convention of Truthfulness picture of how an abstract language gets in force in a population.
Communicative Actions for Artificial Agents - Cohen Levesque — Cohen & Levesque 1995, the Mentalistic Semantics high-water mark CBCL deliberately is not.
FIPA-ACL Specifications — the engineering of FIPA-ACL (envelope, conversation-id, ontology slot) CBCL inherits; the semantics it replaces.
An Ontology for Commitments in Multiagent Systems - Singh — Singh 1999, the formal commitment ontology CBCL’s dialect contracts instantiate.
Jones-Sergot Normative Systems — Jones & Sergot 1993, the Counts-As Relation that gives wire events institutional meaning under a dialect contract.
Exploit Programming - From Buffer Overflows To Weird Machines — weird-machine analysis CBCL is designed to preclude at the parser layer.
PKI Layer Cake - Kaminsky Patterson Sassaman — concrete parser-differential attacks; CBCL’s class-level unambiguity rules these out at the grammar level.
The Halting Problems of Network Stack Insecurity
A Language-Based Approach To Prevent DDoS
LangSec
KQML as an Agent Communication Language
KQML - A Language And Protocol For Knowledge And Information Exchange
FIPA-ACL
ACL Rethinking Principles — Singh’s social-agency critique that CBCL’s “dialect installation as public commitment” inherits.
Agent Communication Languages - Rethinking the Principles
Verifiable Semantics for ACLs
A Common Ontology Of ACLs
Commitment-based Semantics
BSPL: Singh’s Information Protocols (AAMAS 2011) are the nearest multiagent-systems precedent for the R5 causal protocols and the R6 role layer: declarative, asynchronous, decentralised enactment from local history with no ordering assumptions. CBCL adds content-addressed predecessors, an adversarial threat model with signature-bound roles, the DCFL bound, runtime dialect installation, and a mechanised local-to-global correspondence; Enactability is the BSPL-side notion nearest to causal locality.
The State of the Art in Agent Communication Languages
Trends in Agent Communication Language
Toward Principles for the Design of Ontologies Used for Knowledge Sharing — Gruber’s ontological-commitment principle CBCL inherits.
Some Philosophical Problems from the Standpoint of Artificial Intelligence — McCarthy & Hayes’s representation/computation separation.
Elephant 2000 - A Programming Language Based on Speech Acts — McCarthy’s intra-program speech-act counterpart to CBCL’s inter-organisational vision.
Adjectival Modifiers
S-expression
Homoiconicity
Code as Data
Creating Languages in Racket — Flatt’s #lang mechanism that inspired CBCL’s homoiconic self-extension.
Extensibility in Programming Language Design - Standish
Language Extensibility Taxonomy
Paraphrase
Orthophrase
Metaphrase
Self-Expression
Self-Adaptation Self-Expression Self-Awareness ASCENS
Dialects and Idiolects
Keeping CALM - When Distributed Consistency is Easy — CALM theorem underwriting the forthcoming coordination-free contracts extension.
Visibly Pushdown Languages
MCP Landscape Security Threats And Future Research Directions
Survey Of AI Agent Protocols
Survey Of Agent Interoperability Protocols
ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems — concrete LLM-agent worm whose root-cause analysis CBCL’s lang-scoped provenance addresses.
Why AI Agents Communicate In Human Language
Why Do Multi-Agent LLM Systems Fail
Gossiping in Distributed Systems
Gossip-based Aggregation in Large Dynamic Networks

Conceptual Contribution

Claim: Agent communication languages can be simultaneously expressive, runtime-extensible, and tractably verifiable iff every message — including those that extend the language — is constrained to the deterministic context-free language class; this constraint is compatible with first-class self-extension, can be machine-checked end-to-end, and converts the unverifiable-mental-state problem of mentalistic ACLs into a public-commitment problem at the protocol layer.
Mechanism: Eight-performative core grammar (LL(1), DCFL); homoiconic dialect mechanism — dialect definitions are valid CBCL messages with extend clauses describing pattern-template substitutions; three safety invariants R1–R3 enforced at installation (no recursion via DFS cycle detection, declared resource bounds, core-vocabulary preservation); (lang name …) wrapper providing prefix-free deterministic dispatch into per-dialect sub-grammars so the union remains DCFL. Lean 4 formalization (LeanCbcl, ~5,400 LoC, 176 theorems) covering parser soundness/completeness, R1–R3, pipeline totality, and dcfl_preserved; verified parser extracted to a runnable binary (cbcl-parse). Rust reference implementation (cbcl-rs, ~11,000 LoC) with a ResourceContext-tracked single-pass expander, gossip-based dialect propagation (O(log n) per Demers et al.), canonical RFC-9804 serialization for signing, algorithm-agnostic Signer trait, C FFI / WASM bindings, property-based + differential tests, fuzz targets. Draft IETF application/cbcl Internet-Draft and Nostr transport binding.
Concepts introduced/used: Deterministic Context-Free Language, LangSec, Homoiconicity, S-expression, Dialects and Idiolects, Performatives, Self-Expression, Paraphrase, Orthophrase, Metaphrase, Visibly Pushdown Languages, CALM Theorem, Commitment-based Semantics, Public Semantics, Verifiable Semantics, Adjectival Modifiers, Ontological Commitment, Lean 4, Property-Based Testing, Parser Differential Attack, Weird Machine, Gossip Protocols, Canonical Serialization, Nostr, hence
Stance: engineering / formal-methods, with explicit position-taking on the agent-communication design space
Relates to: Realises McCarthy’s Common Business Communication Language vision (1975/1982) by giving formal safety guarantees McCarthy could only gesture at. Sits squarely in the LangSec programme of Security Applications Of Formal Language Theory and Exploit Programming - From Buffer Overflows To Weird Machines, extending it from input-validation analysis to protocol design — claiming, plausibly, to be the first ACL designed from LangSec principles and the first to demonstrate that LangSec is compatible with runtime self-extension. Inherits the DCFL-vs-ambiguous-CFG argument from PKI Layer Cake - Kaminsky Patterson Sassaman and applies it at the message layer rather than the certificate layer. Builds explicitly on Singh’s social-agency critique (ACL Rethinking Principles) and Wooldridge’s verifiability programme (Verifiable Semantics for ACLs) by treating dialect installation as a public commitment whose semantics are anchored by the :examples clause — a machine-checkable analogue of the commitment-trace conformance that Flexible Protocol Specification and Execution (Yolum & Singh) and Commitment Machines - Yolum and Singh establish for protocol actions. Where Pact - A Choreographic Language for Agentic Ecosystems takes the individual-rationality fork to answer “why follow a protocol?”, CBCL takes the publicness/verifiability fork: the meaning of a message is fully determined by the formal grammar plus declared semantics, with no mental-state inference required. Inherits Gruber’s ontological-commitment architecture but replaces “out-of-band agreement” with in-protocol propose/query/teach. The extensibility design draws on Creating Languages in Racket (Flatt’s #lang) and respects the boundary set by Extensibility in Programming Language Design - Standish: paraphrastic only, deliberately excluding orthophrase/metaphrase to keep the attack surface bounded. The forthcoming structural-contracts extension uses Visibly Pushdown Languages for shape constraints and the CALM Theorem for coordination-free verification — a natural bridge to commitment-machine semantics. The LLM-agent threat-model framing (ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems, MCP Landscape Security Threats And Future Research Directions) positions CBCL as the structural alternative to MCP/JSON-RPC-with-natural-language: same extensibility, vastly tighter security envelope.

Endpoint Projection

The mechanical translation from a global choreographic program — which describes the joint behaviour of all participants — to a per-participant local program that, when run in parallel with the others, realises the choreography. Endpoint projection is the operation that makes Choreographic Programming practical: the global program is the source of truth, and projection to each role is a syntactic/semantic transformation that preserves the communication structure and (under standard well-formedness conditions) deadlock-freedom. Implementations differ in how role information is tracked — type-system roles (Choral, ChoRus), census polymorphism (Bates et al. 2025), or algebraic-effect handlers (Pact, Effectful) — but all share the global-to-local move that distinguishes choreographic from session-typed programming. The structural analogue in commitment-based protocol theory is Commitment Machines, which compiles a global commitment specification to per-role finite-state machines. The multiagent-systems tradition also reaches decentralised endpoints by a route with no projection step at all: in BSPL Information Protocols every role acts directly on the global protocol using only its local history, and Enactability plays the part that projectability and knowledge of choice play here.

In this vault

Choreographic Programming
Structured Communication-Centred Programming for Web Services — origin of the Theorem of End-Point Projection
Multiparty Asynchronous Session Types — multiparty projection G ↾ p
Introduction to Choreographies
Session Types
Pact - A Choreographic Language for Agentic Ecosystems
Commitment Machines
Algebraic Effects
BSPL: decentralised enactment without projection; Enactability as the counterpart condition
Information Protocols

Choreographic Programming

A programming paradigm in which a single global program describes the joint behaviour of all participants in a distributed protocol, and a mechanical endpoint projection derives the local program for each participant. Choreographic languages are designed so that well-typed choreographies are deadlock-free by construction — every send is matched by a corresponding recv in the projected counterpart. Originating in WS-CDL and formalised in the π-calculus / session-types community (Carbone, Honda, Yoshida), the paradigm has since been embedded in production languages (Choral for Java, ChoRus for Rust, HasChor for Haskell, Bates et al.’s census-polymorphic projection at PLDI 2025) and extended towards adversarial settings via cryptographic primitives (Sarkar & Russo; Veiga). Structurally adjacent to the Commitment-Based Protocol tradition: both specify protocols globally and project to local roles, but choreographic semantics is operational/communicational while commitment-based semantics is normative/social.

In this vault

Endpoint Projection
Structured Communication-Centred Programming for Web Services — Carbone, Honda & Yoshida ESOP 2007 / TOPLAS 2012, the foundational paper
Multiparty Asynchronous Session Types — Honda, Yoshida & Carbone POPL 2008, multiparty generalisation
Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming — Carbone & Montesi POPL 2013, deadlock-freedom by construction across interleaved sessions
Introduction to Choreographies — Montesi 2023 (Cambridge), the canonical textbook
On the Monitorability of Session Types — Bartolo Burlò, Francalanza & Scalas ECOOP 2021, runtime monitoring
Session Types
Pact - A Choreographic Language for Agentic Ecosystems
Commitment-Based Protocol
Commitment Machines
Flexible Protocol Specification and Execution
Algebraic Effects

Multiparty Asynchronous Session Types

Reference: Honda, K., Yoshida, N. & Carbone, M. (2008). Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08), San Francisco, CA, pp. 273–284. ACM. DOI: 10.1145/1328438.1328472. Journal version: Journal of the ACM 63(1):9, 2016, DOI: 10.1145/2827695. Source file: honda-yoshida-carbone-popl08.pdf. URL

Summary

Honda, Yoshida and Carbone generalise the binary session-type discipline of Honda (1993) and Honda-Vasconcelos-Kubo (1998) to multiparty asynchronous communication: a single global type describes the interaction protocol among N ≥ 2 participants, and per-participant local types are derived by a syntactic projection function that translates each global statement into the participant’s local view of it. A process calculus extending the asynchronous π-calculus is typed against these local types; the central technical result is the subject reduction and progress theorem: a system of well-typed processes is deadlock-free, communication-safe (no message-type mismatch), and session-fidelity-preserving (the runtime trace conforms to the global type, projected). This three-tier structure — global types, local types via projection, processes typed against local types — is the formal foundation that the entire contemporary multiparty session-types and choreographic-programming literature inherits.

The paper’s intellectual contribution is to make the global protocol a typed object whose well-formedness can be checked once, with the well-typedness of every projected role following automatically. Where binary session types describe the obligations of two endpoints separately and rely on duality, multiparty session types describe the joint protocol once and project to as many roles as needed, with a coherence condition (each branching point is observed by every relevant participant) ensuring projections are mutually consistent. The treatment is asynchronous: send is non-blocking, messages are buffered in per-channel queues, and the type system tracks the resulting message-order obligations. The framework is the direct precursor of contemporary choreographic-programming languages (Choral, HasChor, ChoRus, Pact) and of the runtime-monitoring theory developed in On the Monitorability of Session Types.

Key Ideas

Global type: a single typing artefact G describing the interaction among N participants — primitives include p → q : ⟨S⟩.G (participant p sends a value of type S to q, then G), branching p → q : {ℓᵢ : Gᵢ}, recursion μt.G, and parallel composition.
Local type / projection: G ↾ p is the projection of G to participant p, syntactically translating each global statement into the corresponding send/receive/select/branch from p’s perspective.
Coherence (well-formedness): a global type is well-formed iff every choice point is observed by every relevant participant — the multiparty analogue of the connectedness condition in Structured Communication-Centred Programming for Web Services.
Asynchronous π-calculus substrate: processes communicate over typed session channels with non-blocking send and FIFO queues; each session is opened with a fresh name and closed structurally.
Subject reduction: well-typedness is preserved under reduction.
Communication safety: no well-typed system ever sends a value whose type the receiver does not expect.
Session fidelity / progress: the runtime trace of a well-typed system is a refinement of the projected local types, and well-typed systems whose buffers are empty cannot deadlock.
Type-driven engineering payoff: type-check the global protocol once, get communication-safety guarantees for every role for free.

Connections

Conceptual Contribution

Claim: Multiparty distributed communication is best disciplined by a single global type describing the joint protocol of all participants, from which per-participant local types are derived by mechanical projection; well-typedness of the global type plus a coherence condition ensuring choice points are observed by all relevant parties is sufficient to guarantee that every projected process is communication-safe, deadlock-free, and faithful to the global protocol.
Mechanism: Define global types as a calculus over N ≥ 2 participants with sending, branching, recursion, parallel composition; define local types as session types with send/receive/select/branch; define a syntactic projection G ↾ p from global to local types per participant; type processes (extended asynchronous π-calculus with FIFO message buffers) against the projected local types; prove subject reduction (well-typedness preserved under reduction), communication safety (no type-mismatched messages), and progress (well-typed systems with empty buffers do not deadlock).
Concepts introduced/used: Session Types, multiparty session types, global type, local type, projection, coherence, subject reduction, asynchronous π-calculus, communication safety, session fidelity
Stance: foundational / formal-semantic
Relates to: Companion to Structured Communication-Centred Programming for Web Services (Carbone-Honda-Yoshida ESOP 2007 / TOPLAS 2012) — the two papers together establish the modern global types → local types → processes pipeline that all subsequent choreographic-programming and multiparty session-types work inherits. Without the multiparty extension here, the binary session-type substrate of Carbone-Honda-Yoshida 2007 cannot scale to the N-participant choreographies that real protocols need. Underwrites the contemporary textbook Introduction to Choreographies (Montesi 2023). Provides the type-system substrate that On the Monitorability of Session Types (Bartolo Burlò et al. ECOOP 2021) lifts into a runtime-monitoring theory, and that Pact - A Choreographic Language for Agentic Ecosystems adds game-theoretic operators on top of. The structural counterpart in the agent-communication tradition is Commitment Machines - Yolum and Singh / Flexible Protocol Specification and Execution: both lineages (multiparty session types ↔ Yolum-Singh commitment protocols) take a globally-specified N-participant protocol, project to per-role views, and prove the projection preserves a key correctness property (communication safety here, commitment discharge there). The π-calculus substrate descends from Communicating Sequential Processes (Hoare 1978) and Milner’s π-calculus.

Tags

Flexible Protocol Specification and Execution

Flexible Protocol Specification and Execution: Applying Event Calculus Planning Using Commitments

Reference: Yolum, P. & Singh, M.P. (2002). Proceedings of the 1st International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS ’02), pp. 527–534. ACM, Bologna. Source file: yolum-singh-2002-flexible-protocol.pdf. URL

Summary

Yolum and Singh argue that finite-state-machine and Petri-net protocol formalisms over-constrain multi-agent interactions because they fix legal sequences of message tokens without regard to what those messages mean. They develop a commitment-based alternative in which each protocol action is reified as an operation on social commitments — Create, Discharge, Cancel, Release, Assign, Delegate — and the rules for how commitments evolve are formalised in a variant of the Event Calculus (Kowalski-Sergot, in Shanahan’s planner formulation). Base-level commitments C(x,y,p) and conditional commitments CC(x,y,p,q) become event-calculus fluents whose Initiates/Terminates clauses constitute the protocol specification.

The running example is the NetBill e-commerce protocol. Three reasoning postulates capture how a base-level commitment is discharged when its content holds, how a conditional commitment resolves into a base-level commitment when its precondition fires, and how CC is consumed when its consequent already holds. An abductive event-calculus planner (Shanahan) is then used to generate protocol runs from an initial state to a goal state, allowing agents to skip steps, reorder messages, or repair exceptions at runtime — provided every base-level commitment created during the run is eventually discharged. The result satisfies Singh’s three social-semantic desiderata: meaningful (content captured), verifiable (compliance checkable from public commitment trace), and declarative (specifies what each action achieves, not how to sequence actions).

Key Ideas

Commitment as fluent in event calculus: C(x,y,p) and CC(x,y,p,q) represented by the EC predicates Initiates, Terminates, HoldsAt, Happens, etc.
Six commitment operations (Create, Discharge, Cancel, Release, Assign, Delegate) compiled into Initiates/Terminates clauses.
Three postulates link content fluents to commitment fluents: discharging on content satisfaction, conditional-commitment resolution, and conditional consumption when consequent already true.
A protocol run is a sequence of Happens events; complete iff no base-level commitment is left holding — incomplete runs identify non-compliant agents.
Abductive planning (Shanahan) generates legal protocol runs from initial-state + goal-state descriptions, restoring autonomy/flexibility lost in FSM models.
Skipping steps and reordering (e.g. send-goods-before-accept) is supported because preconditions are over commitment state, not over a path through an FSM.
Permissions encoded via action preconditions; prohibitions encoded as commitments-not-to-bring-about.

Connections

Conceptual Contribution

Claim: Multi-agent protocols should be specified by the meaning of their actions — concretely, by how each action transforms the agents’ social commitments — rather than by legal token sequences; doing so simultaneously delivers meaningful, verifiable, and declarative semantics, and lets agents skip, reorder, or repair steps via runtime planning while still being held to their obligations.
Mechanism: Reify commitments as event-calculus fluents and define the six manipulation operations (Create/Discharge/Cancel/Release/Assign/Delegate) as Initiates/Terminates clauses; add three reasoning postulates governing base-level discharge and conditional-commitment resolution; use Shanahan’s abductive event-calculus planner to compute runs (sets of Happens clauses with a partial order) from initial states to goal states under the protocol’s preconditions; declare a run complete iff no base-level commitment is left holding, providing an objective compliance criterion.
Concepts introduced/used: Commitment, Conditional Commitment, Commitment-Based Protocol, Commitment-based Semantics, Event Calculus, Abductive Planning, Public Semantics, Verifiable Semantics, Conversation Protocols, Interaction Protocols, NetBill Protocol, Commitment Machines
Stance: formal-semantic / engineering
Relates to: Direct response to FSM- and Petri-net-based protocol traditions critiqued in ACL Rethinking Principles; supplies the operational machinery whose mentalistic counterpart (KQML/FIPA-SL) is shown unverifiable in Verifiable Semantics for ACLs. Companion to Singh’s social-agency programme and to the institutional-reality strand of Agent Communication And Institutional Reality. Conditional-commitment treatment derives from Colombetti’s earlier work and is contemporaneous with A Commitment-Based Approach to Agent Communication (Fornara & Colombetti AAMAS-02 / AAI-04), which gives a complementary object-oriented account of the same primitives (those authors note Yolum-Singh as the closest relative). Commitment-machine compilation to FSMs is the subject of the authors’ parallel ATAL-01 paper. Empire of mentalistic semantics from Intention Is Choice with Commitment is the foil — here intentions/persistence are not needed because the protocol semantics is exhausted by the public commitment trace.

Tags

Commitment Machines - Yolum and Singh

Commitment Machines

Reference: Yolum, P. & Singh, M.P. (2002). Intelligent Agents VIII: Agent Theories, Architectures, and Languages (ATAL-01), LNAI 2333, pp. 235–247. Springer. (A preliminary version appeared in WET-ICE 2000.) Source file: yolum-singh-2002-commitment-machines.pdf. URL

Summary

Yolum and Singh propose commitment machines (CMs) as a protocol formalism that, unlike finite-state machines or Petri nets, attaches declarative meaning to states and actions in terms of the participants’ Social Commitments. A CM is a triple ⟨M, Δ, F⟩ of a finite minimal set of meanings (formulas in a propositional language extended with a commitment operator Cₓp and a strict-implication operator ;), a set of actions ⟨a : e⟩ whose effect e is itself a meaning, and a set of consistent final meanings. Transitions are not enumerated — they are inferred from the logical consequences of applying an action’s effect to the current meaning. The running example is the NetBill Protocol, specified by atomic propositions (request, goods, pay, receipt) and abbreviations for conditional commitments (accept = C_c(goods ; pay), promiseGoods = C_m(accept ; goods), etc.); three reasoning rules govern how commitments evolve as content propositions are made true.

The paper’s central technical contribution is a compilation procedure that turns any complete CM (one whose meaning set is closed under antecedence) into a deterministic FSM that can be executed in constant space without commitment reasoning at run time. The procedure is shown sound (Theorem 2 — every realised computation is generated by the source CM) and complete (Theorem 3 — every CM-generated computation has a semantically-strongest, efficient FSM-realised counterpart from true), via a chain of lemmas about semantic superiority, efficient computations, and endpoint equivalence. Because the meanings of states are explicit, agents executing the CM directly can plan paths through the protocol that exploit opportunities (e.g. a merchant proactively quoting without a request, “try before you buy” deals) and handle exceptions, recovering autonomy that pure-token FSM/Petri-net specifications eliminate.

Key Ideas

Commitment machine ⟨M, Δ, F⟩: state space is a finite minimal set of meanings (formulas) rather than tokens; actions ⟨a : e⟩ carry effect-meanings; final states are a consistent subset of meanings.
Inferred transitions: q ⊨_⟨a:e⟩ r iff (q ∧ e) ⊢ r — transitions are derived from logical entailment, not enumerated edges.
No fixed start state: a CM has no s₀; participants may begin from any meaning whose commitments they accept (typically true).
Three reasoning rules over commitments: (1) Cₓp discharges when p holds; (2) Cₓ(p ; r) collapses to base-level Cₓr when p holds; (3) Cₓ(p ; r) ceases when r holds before p, with no new commitment.
Compilation to deterministic FSM under two restrictions: (R1) no transition mᵢ → mⱼ if mᵢ ⊢ mⱼ (no information-free moves); (R2) the target meaning must dominate all alternatives entailed by the action (forcing maximal information).
Completeness requires “complete” CMs — meaning set closed under antecedence — so that a unique strongest target meaning always exists; trivially achieved by closing under conjunction.
Soundness, completeness, determinism established as theorems over the computation abstraction (sequences of meanings interleaved with actions); computations are compared by semantic superiority and endpoint equivalence rather than literal action-sequence equality.
Flexibility recovered for free: since states encode meanings, agents can skip steps, reorder, or take unsolicited shortcuts whenever the resulting meaning is still in M and the path to a final meaning still exists.

Connections

Conceptual Contribution

Claim: Multi-agent protocols should be specified by giving states and actions declarative meaning in terms of the participants’ commitments — not by enumerating legal token sequences — and any such specification can be soundly and completely compiled to a deterministic FSM, recovering executability without forfeiting flexibility, autonomy, or the ability to handle exceptions and exploit opportunities.
Mechanism: A propositional language with a commitment operator Cₓ and strict-implication ;; meaning sets M and final-meaning sets F (consistent w.r.t. logical consequence); action effects given as meanings; transitions inferred via (q ∧ e) ⊢ r. Compilation Procedure 1 maps ⟨M, Δ, F⟩ → ⟨S=M, Σ={a}, s₀=true, Q=F, δ⟩ under the two information-monotonicity restrictions; Procedure 2 promotes a computation to its semantically strongest counterpart, Procedure 3 removes redundant self-transitions, yielding efficient semantically-strongest computations that are realised by the compiled FSM. Soundness (Thm 2), determinism (Thm 1), and completeness for complete CMs (Thm 3) are proved.
Concepts introduced/used: Commitment Machines, Commitment-Based Protocol, Commitment-based Semantics, Conditional Commitment, Social Commitment, Public Semantics, Verifiable Semantics, NetBill Protocol, Endpoint Projection (structural analogue), Conversation Protocols, Speech Act Theory
Stance: formal-semantic / engineering
Relates to: Direct precursor and structural sibling of Flexible Protocol Specification and Execution (Yolum & Singh, AAMAS-02), which lifts the same six commitment operations (Create / Discharge / Cancel / Release / Assign / Delegate) into the Event Calculus and adds an abductive planner; ATAL-01 here is the FSM-compilation half of that programme. Companion to A Commitment-Based Approach to Agent Communication (Fornara & Colombetti, AAMAS-02 / AAI-04), which gives an OO/FSM operational semantics for the same primitives plus a precommitment state for directives. Carries forward the social-agency programme of ACL Rethinking Principles (Singh 1998) and answers Wooldridge’s challenge in Verifiable Semantics for ACLs by grounding meaning in publicly-observable commitment formulas rather than agent mental state. The Discussion explicitly contrasts with Smith et al.’s joint-intention–based protocols (mental constructs vs. social constructs) — the same fork that Intention Is Choice with Commitment anchors on the mental side. Structurally a direct analogue of choreographic Endpoint Projection: both compile a globally-specified protocol artefact to a per-role executable, the CM/FSM compilation losing declarative meaning for runtime efficiency much as endpoint projection loses the global view for distributable execution. This makes ATAL-01 the load-bearing reference for the constructive synthesis suggested in the Pact - A Choreographic Language for Agentic Ecosystems entry — choreographies could carry both communication structure (Pact-side) and a CM-style commitment trace (Singh-side), with one compilation step yielding both deadlock-freedom and conformance-checkability.

Tags

ACL Rethinking Principles

Agent Communication Languages: Rethinking the Principles

Reference: Munindar P. Singh (1998). IEEE Computer, December 1998, pp. 40-47. Source file: computer-acl-98.pdf. URL

Summary

Singh surveys the state of Agent Communication Languages (ACLs) such as KQML and FIPA/Arcol, and argues that their dominant mental-agency semantics (defining communicative acts in terms of beliefs and intentions) is conceptually unsatisfying and practically untestable because we cannot read agents’ minds. He proposes a conceptual shift to social agency: ACL semantics should be grounded in a public perspective on commitments, roles, and societies, so compliance with the standard is observable and testable.

The paper maps the ACL design space along two critical dimensions — meaning (perspective, type, basis, context, coverage of communicative acts) and agent construction (design vs. execution autonomy) — and shows how both KQML and Arcol emphasize private, mental-state semantics and thus fail to enable true heterogeneous interoperation. Singh’s alternative emphasizes protocols, roles, and “society management” infrastructure as a richer public substrate for ACLs.

Key Ideas

Mental-agency ACL semantics (KQML, Arcol, early FIPA) cannot be verified without inspecting agent internals.
ACLs need a public perspective, conventional meaning, pragmatics, and full coverage of communicative act categories.
Seven categories of communicative acts: assertives, directives, commissives, permissives, prohibitives, declaratives, expressives.
Social agency replaces BDI with commitments, roles, and societies as the semantic basis.
Dialects/idiolects arise when only private perspectives are considered.

Connections

FIPA-ACL
FIPA-ACL Specifications
KQML
Speech Act Theory
Agent Communication Languages
Multi-Agent Systems
Communicative Actions for Artificial Agents - Cohen Levesque — the Mentalistic Semantics high-water mark Singh is critiquing
An Ontology for Commitments in Multiagent Systems - Singh — Singh’s own formal sequel: the four-place commitment ontology
Commitment Machines - Yolum and Singh
A Commitment-Based Approach to Agent Communication
Articulating Reasons - Brandom — the philosophical underwriting of public, commitment-based semantics
Making It Explicit - Brandom
Jones-Sergot Normative Systems — Counts-As Relation for institutional grounding of commitments
CBCL - Safe Self-Extending Agent Communication — O’Connor 2026: contemporary realisation of Singh’s social-agency programme (dialect installation as public commitment) in a Lean-verified LangSec-grounded ACL.

Conceptual Contribution

Claim: Agent Communication Language semantics must abandon mental agency (beliefs/intentions) and be grounded in a public, social perspective (commitments, roles, societies) in order to be testable and support heterogeneous interoperation.
Mechanism: Surveys KQML, Arcol, FIPA; lays out a two-dimensional design space (meaning × agent construction); shows that mental-state semantics cannot determine compliance; proposes social-agency framework using protocols, roles, and “society management” infrastructure.
Concepts introduced/used: Mentalistic Semantics, Public Semantics, Social Agency, Commitments, Communicative Acts, Verifiable Semantics, Interoperability, Dialects and Idiolects
Stance: critique / foundational
Relates to: Direct antecedent to Verifiable Semantics for ACLs (Wooldridge) which formalises the verification problem Singh names. Sharpens the critique of the mentalistic approach underlying KQML Overview and FIPA-ACL, and motivates commitment-based frameworks such as Agent Communication And Institutional Reality.

Tags

Realizability

(page does not exist)

Knowledge of Choice

Reference: Montesi, F. Knowledge of Choice. Bliki entry, fabriziomontesi.com (created 2023-05-15, updated 2024-12-17). URL. The notion is developed in book form in Introduction to Choreographies (Montesi 2023, Cambridge University Press) and traces to Castagna, Dezani-Ciancaglini & Padovani (2012) and Carbone, Honda & Yoshida (2012); automated repair procedures are given by Lanese, Guidi, Montesi & Zavattaro (2013), Basu & Bultan (2016), and Cruz-Filipe & Montesi (2020, 2023).

Summary

Knowledge of choice is a well-formedness property of choreographies (and, dually, of multiparty Session Types): whenever a participant makes an internal choice between alternative behaviours, every participant whose subsequent behaviour depends on that choice must be made aware of which branch was taken. The property is what makes Endpoint Projection possible — a global choreography can only be projected to deadlock-free local programs if each role can locally determine which branch of a conditional it should follow.

The problem arises when one participant’s private decision silently changes what other participants are supposed to do, without any communication conveying the decision. Montesi’s running example is third-party single sign-on: an authenticator a decides whether a credential is valid, but the web service ws must respond differently depending on that verdict. If the choreography never has a tell ws the outcome, ws cannot know which action to perform, and implementers are pushed toward fragile workarounds — undocumented side-channel messages not reflected in the protocol, or hidden shared state (a common database, side-effects) that breaks the decentralisation the choreography was meant to guarantee.

The standard fix is to add explicit selections — communications that carry a constant value such as a label (OK/KO) — so that every dependent participant can infer the choice from a message it actually receives. In the repaired example, a sends OK or KO to ws, which can then branch locally. Transforming a choreography that lacks knowledge of choice into an equivalent one that has it is called amendment (or repair), and can be performed automatically; the dual mechanism in the projection direction is the merging operator on local types, which decides when two branches of a receiver are reconcilable.

Key Ideas

Definition. When a choice is made between alternative behaviours, all affected participants must be made aware of the choice — otherwise the choreography is not realisable as independent local programs.
Failure mode. A participant’s internal decision affects others’ behaviour, yet no communication conveys the decision, so dependent roles cannot select their branch.
Bad workarounds. Adding undocumented out-of-band messages, or introducing hidden side-effects / shared databases — both break the decentralised, protocol-as-written semantics.
Selections. Communications carrying constant values (labels) inserted so dependent participants can infer the choice locally.
Amendment / repair. A (mechanisable) transformation that inserts the missing selections to restore knowledge of choice while preserving behaviour.
Merging operator. The dual device in projection: it determines when a receiver’s alternative continuations can be merged, i.e. when a role does not need to be told the choice.
Why it matters. Knowledge of choice is a precondition for sound endpoint projection, deadlock-freedom, and communication safety in both choreographies and multiparty session types.

Connections

Conceptual Contribution

Claim: A global protocol is realisable as independent, deadlock-free local programs only if every participant whose behaviour depends on a choice is informed of that choice; “knowledge of choice” names exactly this realisability condition and separates well-formed choreographies from ones that secretly rely on shared state.
Mechanism: Conditionals in a choreography induce a dependency from the deciding role to every role that branches on the decision; the property is satisfied by inserting selections (label-carrying messages), and a choreography lacking it can be amended automatically. Dually, Endpoint Projection uses a merging operator to admit receivers that need not be told.
Concepts introduced/used: knowledge of choice, selection, amendment, merging, Endpoint Projection, Choreographic Programming, Session Types
Stance: foundational / definitional (choreographic-programming theory)
Relates to: The realisability counterpart of Endpoint Projection in Introduction to Choreographies; the property whose violation the choreographic foundations (Structured Communication-Centred Programming for Web Services, Multiparty Asynchronous Session Types) are built to exclude; structurally adjacent to the distributed-knowledge tradition of Knowledge and Common Knowledge in a Distributed Environment, where what an agent must know to act correctly is the central question.

Commitment-based Semantics

Approach that grounds ACL message meaning in public social commitments rather than private mental states — making conformance verifiable.

In this vault

ACL Rethinking Principles
Agent Communication Languages - Rethinking the Principles
Agent Communication And Institutional Reality
A Common Ontology Of ACLs
Public Semantics
Mentalistic Semantics
Flexible Protocol Specification and Execution
A Commitment-Based Approach to Agent Communication
CBCL - Safe Self-Extending Agent Communication — modern LangSec-grounded ACL inheriting Singh’s social-agency programme; dialect installation as public commitment

Declarative Specification

A description of what a system should do rather than how; in language workbenches, declarative meta-specifications (grammar, name binding, types, semantics) are compiled into parsers, checkers, and editors.

In this vault

Interaction Protocols

Specifications of legal conversation patterns above the message level. Three families: ordering-based (Petri nets, state machines, AUML, FIPA interaction protocols), type-based (Session Types, Choreographic Programming with Endpoint Projection), and information-based (BSPL Information Protocols, where ordering and exclusion are derived from what each message requires and produces). Commitment-Based Protocols layer meaning over any of them.

In this vault

Enactability

The property that a protocol can actually be carried out by independently acting roles. In BSPL (Semantics and Verification of Information-Based Protocols) a protocol is enactable if and only if its intension is non-empty: there exists a viable history vector, built from emissions each of which the sending role could make from its own knowledge at the time, that binds every public parameter. A protocol with a public ⌜in⌝ parameter is not enactable standalone; Local Conflict, in which two messages from the same role both bind the key, is not enactable because emitting one disables the other. Enactability is entailed by liveness (completion always remains possible) but is weaker than it, and is independent of safety (no parameter bound twice per key).

Desai and Singh’s earlier diagnostics of unenactable business protocols, blindness (a role required to act on information it never receives) and nonlocal choice (two roles free to make incompatible choices), both yield an empty intension, so the single check subsumes them. Enactability is the multiagent-systems counterpart of Realizability for message sequence charts and choreographies (Realizability and Verification of MSC Graphs, Deciding Choreography Realizability) and of Knowledge of Choice and projectability in Choreographic Programming and Session Types: all ask whether local views suffice for the global specification. Stated over local knowledge rather than channel orderings, it is also the closest existing notion to the causal-locality condition under which the CBCL role layer’s Endpoint Projection is sound (CBCL - Safe Self-Extending Agent Communication).

In this vault

BSPL

The Blindingly Simple Protocol Language, Munindar Singh’s declarative language for multiagent interaction protocols (AAMAS 2011) and the reference instance of Information Protocols. A BSPL protocol is a set of message schemas and references to sub-protocols; every parameter is adorned ⌜in⌝ (must already be known to the sender), ⌜out⌝ (bound, with declarative force, by this message) or ⌜nil⌝ (must not yet be known), and a subset of parameters forms the key that identifies an enactment. There are no sequence, choice or loop operators: ordering follows from ⌜out⌝-before-⌜in⌝ on a shared parameter, and exclusive choice from the rule that a parameter is bound at most once per key. Enactment is shared-nothing and asynchronous: each agent decides what it may send from its own history alone, over a transport that need be neither ordered nor reliable, with no central coordinator.

The programme runs from language (BSPL - The Blindingly Simple Protocol Language) through formal semantics and verification of Enactability, safety and liveness (Semantics and Verification of Information-Based Protocols) to programming models for agents (Kiko - Programming Agents to Enact Interaction Protocols, preceded by Stellar, Protocols over Things, Bungie and Mandrake in the same group). The LoST middleware (local state transfer, 2011) is the architectural style; Splee (2017) extends the language with sets and expressions; Tosca (2017) and Clouseau (2020) compile commitment specifications down to information protocols; Chopra, Christie and Singh’s JAIR 2020 evaluation of protocol languages is the group’s own comparative survey.

Relation to session types and choreographies. Multiparty Asynchronous Session Types and Choreographic Programming derive per-role behaviour from a global type by Endpoint Projection and presuppose a compiler, fixed roles and ordered channels. BSPL reaches decentralised enactment without a projection step: every role acts on the global protocol using only its local history, and enactability plays the part that projectability and Knowledge of Choice play on the session-type side. It shares the nonlocal-choice problem with message sequence charts (Realizability and Verification of MSC Graphs) but detects it as an empty intension.

Relation to CBCL. CBCL - Safe Self-Extending Agent Communication’s R5 causal protocols and its later role layer are the nearest contemporary relative: declarative, asynchronous, decentralised verification from local history with no ordering assumptions, in Singh’s public-commitments tradition (ACL Rethinking Principles). The differences are what CBCL adds: dependencies are content-hash edges to concrete message instances rather than parameter values, the threat model is adversarial with roles bound by nomination and signature, the message language is bounded to DCFL, dialects install at runtime, and the local-to-global correspondence is a mechanised theorem rather than a tool-checked property. Any comparison with session types owes BSPL the same paragraph.

In this vault

BSPL - The Blindingly Simple Protocol Language (Singh, AAMAS 2011)
Semantics and Verification of Information-Based Protocols (Singh, AAMAS 2012)
Kiko - Programming Agents to Enact Interaction Protocols (Christie, Singh & Chopra, AAMAS 2023)
Information Protocols
Enactability
Interaction Protocols
Commitment Machines - Yolum and Singh
Commitment-Based Protocol
Commitment-based Semantics
ACL Rethinking Principles
Endpoint Projection
Session Types
Choreographic Programming
Knowledge of Choice
CALM Theorem
CBCL - Safe Self-Extending Agent Communication

Information Protocols

Interaction protocols specified purely by the information that messages require and produce, with no control-flow constructs. Introduced by Singh with BSPL: each message schema names a sender role, a receiver role and parameters adorned ⌜in⌝, ⌜out⌝ or ⌜nil⌝, and a key subset of parameters identifies the enactment. Two constraints do all the work. Information causality: a message may be emitted only when its ⌜in⌝ parameters are already bound in the sender’s local history, so ordering is derived rather than stated. Information integrity: within one enactment (one key binding) a parameter may be bound at most once, so exclusive choice is derived rather than stated. Because both constraints are evaluated against local history and bindings are immutable, enactment is coordination-free and tolerates unordered, lossy delivery; a received message is either consistent with the local store and added, or rejected.

The paradigm’s correctness vocabulary is Enactability (some viable path completes the enactment), safety (no parameter bound twice per key across all roles) and liveness (completion always remains possible). Its programming counterpart is the form, an enabled message with its ⌜in⌝ parameters filled and its ⌜out⌝ parameters awaiting a decision (Kiko - Programming Agents to Enact Interaction Protocols). Meaning is layered separately: a means clause may attach a commitment to a message, connecting information protocols to Commitment-based Semantics.

Contrast with ordering-based specifications (FIPA-ACL interaction protocols, AUML, message sequence charts, WS-CDL) and with type-based ones (Session Types, Choreographic Programming), which fix sequences or derive local behaviour by Endpoint Projection. CBCL - Safe Self-Extending Agent Communication’s causal protocols are the content-addressed, adversarial-setting relative of this idea.

In this vault

CALM Theorem

Consistency As Logical Monotonicity (Hellerstein 2010 conjecture; Ameloot, Neven, Van den Bussche 2013 proof). A distributed program has a consistent, coordination-free implementation if and only if it is expressible in monotonic logic.

Monotonic programs produce a set of outputs that only grows as inputs arrive (S ⊆ T ⟹ P(S) ⊆ P(T)). Such programs are safe under missing information: any conclusion reached on a subset of inputs remains valid when more arrive. Non-monotonic programs may retract earlier conclusions, so they must wait for “all the news” — which is what distributed coordination enforces.

CALM is the positive counterpart to the CAP Theorem: it names the exact class of programs that can satisfy Consistency, Availability, and Partition-tolerance simultaneously.

Why it matters

Moves consistency from a property of storage (linearizability, serializability) to a property of programs — Confluence.
Tells programmers what kinds of features are free (monotonic: set union, counting up, set-containment) and what must be paid for (non-monotonic: set difference, strict aggregation, count-exact, deletions without tombstones).
Gives a design rule for coordination-free systems: build from monotonic primitives — CRDTs, Immutable Data Structures, Tombstones, monotonic accumulators — and only add coordination at non-monotonic boundaries.

Formal statement

Using Relational Transducer networks as the execution model and Confluence as the consistency criterion, Ameloot et al. prove: a query Q has a coordination-free distributed evaluation plan iff Q is monotone.

In this vault

Keeping CALM - When Distributed Consistency is Easy — the definitive survey
CAP Theorem
Confluence
Monotonic Logic
Coordination Avoidance
Relational Transducer
Bloom Language
Dedalus
CRDTs
Non-monotonic Reasoning

Message Sequence Charts - A Survey

Message Sequence Charts: A Survey

Reference: Genest, B. & Muscholl, A. (2005). Message Sequence Charts: A Survey. In Proc. 5th International Conference on Application of Concurrency to System Design (ACSD 2005), St. Malo, France, pp. 2–4. IEEE Computer Society. DOI 10.1109/ACSD.2005.25. (Invited survey; a fuller treatment appears in Genest, Muscholl & Peled, Message Sequence Charts, LNCS 3098, 2004.) URL.

Summary

This invited survey by Genest and Muscholl maps the theory of Message Sequence Charts (MSCs) and their compositional extension, high-level MSCs (HMSCs / MSC-graphs), from the standpoint of concurrency theory and automata. An MSC gives a partial-order (visual) semantics to one communication scenario among asynchronously communicating processes; an HMSC glues MSCs with choice, concatenation and loops to specify infinite families of scenarios. The survey organises the main results of the field: the formal (partial-order and language) semantics of MSCs, the expressiveness and closure properties of HMSC languages, and — crucially — the tight relationship between HMSC specifications and communicating finite-state machines (channel automata) that implement them.

The recurring theme is that unrestricted MSC/HMSC specifications quickly become intractable, so the theory is built around well-behaved subclasses. The survey reviews bounded (channel-bounded) and existentially-bounded MSC languages — those realizable with finite communication buffers — and the notions of safe / local-choice HMSCs that admit deadlock-free distributed implementations, connecting directly to the realizability programme of Realizability and Verification of MSC Graphs. It surveys the decidability frontier for model-checking MSCs against HMSC specifications and for comparing specifications, noting where problems become undecidable and which structural restrictions restore decidability. As a short roadmap paper it is best read as an entry point and index into the MSC literature rather than as a single technical result.

Key Ideas

MSC semantics: a single scenario as a labelled partial order over send/receive events among asynchronous processes.
HMSC / MSC-graph: MSCs composed by choice, sequential concatenation and iteration to describe (possibly infinite) sets of scenarios.
Communicating automata correspondence: HMSC specifications versus their implementation by communicating finite-state machines with message channels — the central object of the theory.
Bounded and existentially-bounded MSCs: the tractable subclasses realizable with finite buffers; the setting in which most positive (decidability) results live.
Realizability & safe/local-choice HMSCs: the structural conditions under which a specification has a deadlock-free distributed implementation.
Decidability landscape: which model-checking and comparison problems are decidable, and which structural restrictions are needed to recover decidability.
Survey scope: a compact roadmap and bibliographic index into the MSC/HMSC literature.

Connections

Conceptual Contribution

Claim: The MSC/HMSC formalism is best understood through its correspondence with communicating automata and through the tractable subclasses (bounded, existentially-bounded, local-choice) for which realizability and verification are decidable; unrestricted specifications are intractable.
Mechanism: A survey that assembles the partial-order semantics of MSCs, the language theory of HMSCs, the channel-automata implementation model, and the decidability results for the well-behaved subclasses into a single map of the field.
Concepts introduced/used: Message Sequence Charts, HMSC / MSC-graph, Communicating Finite State Machines, bounded / existentially-bounded MSC languages, safe / local-choice HMSCs, Realizability.
Stance: survey / expository
Relates to: The companion technical anchor is Realizability and Verification of MSC Graphs (Alur–Etessami–Yannakakis); the same communicating-automata-vs-global-specification tension is later cast in session-type terms by Multiparty Compatibility in Communicating Automata and in service-choreography terms by Deciding Choreography Realizability.

Tags

Realizability and Verification of MSC Graphs

Reference: Alur, R., Etessami, K. & Yannakakis, M. (2001). Realizability and Verification of MSC Graphs. In Proc. 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), Crete, Greece, LNCS 2076, pp. 797–808. Springer. DOI 10.1007/3-540-48224-5_65. Journal version: Theoretical Computer Science 331(1):97–114, 2005, DOI 10.1016/j.tcs.2004.09.034. URL.

Summary

A Message Sequence Chart (MSC) describes a single scenario of communication among distributed processes as a partial order over send/receive events; an MSC-graph (equivalently a high-level MSC, HMSC) composes individual MSCs through choice, concatenation and loops to describe a set of scenarios — an early, visual model of a system amenable to analysis. Alur, Etessami and Yannakakis ask the foundational question of realizability: given such a scenario-based specification, does there exist a distributed implementation (a collection of communicating automata, one per process, exchanging messages over channels) whose behaviours are exactly the scenarios the graph specifies — no more and no fewer?

The paper’s central observation is that a distributed implementation is forced to exhibit implied scenarios: because each process sees only its own local events, any implementation of a set of MSCs also generates every scenario in the closure of that set, and these implied behaviours may not be in the original specification. This gap is the source of unrealizability (the classic culprit being non-local choice, where a branch is decided by one process but not communicated to others). The authors formalise two notions — weak realizability (the implementation’s behaviours match the specification) and safe realizability (additionally the implementation is deadlock-free, so no implied behaviour gets stuck) — and settle their decidability and complexity. For bounded MSC-graphs, weak realizability is undecidable, whereas safe realizability is decidable (in EXPSPACE). They also study verification: to model-check an MSC-graph one must check not just the specified scenarios but the whole closure of implied scenarios that any implementation must include, and they chart the associated complexity.

Key Ideas

MSC-graph / HMSC: individual MSCs (partial orders over messaging events) composed via choice, sequencing and iteration to specify a set of scenarios.
Realizability question: does a distributed implementation exist whose behaviour is exactly the specified set of scenarios?
Implied scenarios / closure: local-only knowledge forces any implementation to also generate the closure of the specified MSCs; the extra behaviours are the obstacle to realizability.
Non-local choice: a branch chosen by one process but invisible to others — the canonical reason a specification is unrealizable.
Weak vs. safe realizability: weak = behaviours match; safe = behaviours match and the implementation is deadlock-free.
Decidability boundary: for bounded MSC-graphs, weak realizability is undecidable while safe realizability is decidable (EXPSPACE).
Verification over the closure: correct model-checking of an MSC-graph must account for implied behaviours, not only the drawn scenarios.

Connections

Conceptual Contribution

Claim: Scenario-based specifications cannot in general be implemented verbatim: any distributed realization is forced to include implied scenarios beyond those drawn, so realizability is a non-trivial (sometimes undecidable) property that must be checked, not assumed.
Mechanism: Model the specification as an MSC-graph, define its closure under local-knowledge-preserving behaviour, and separate weak from safe (deadlock-free) realizability; decide safe realizability of bounded graphs in EXPSPACE while showing weak realizability undecidable.
Concepts introduced/used: Message Sequence Charts, MSC-graph / HMSC, implied scenario, closure, non-local choice, weak vs. safe Realizability.
Stance: formal / theoretical (automata & complexity theory)
Relates to: The distributed-systems root of the modern realizability line pursued for choreographies in Deciding Choreography Realizability and for Communicating Finite State Machines vs. global types in Multiparty Compatibility in Communicating Automata; surveyed alongside HMSC theory in Message Sequence Charts - A Survey. The “non-local choice” pathology is the same phenomenon that Knowledge of Choice addresses in Choreographic Programming.

Tags

Session Types

A type discipline for communicating processes — originating with Honda (1993) and developed extensively by Honda, Vasconcelos, Yoshida, and others — in which a process’s communication behaviour is typed by a session type: a structured description of the sequence of messages that may flow on a channel, including alternation (!/?), choice (+/&), recursion, and delegation. Session types come in two flavours: binary (two participants per channel) and multiparty (a global type projected to per-role local types — directly analogous to choreographic Endpoint Projection). When a process can be source-checked, its session-type conformance is decidable statically; when it cannot, runtime monitors can enforce the type from observable message traces (On the Monitorability of Session Types). Structurally adjacent to the commitment-based protocol tradition: session types and Yolum-Singh-style commitment protocols are independently-developed formalisms for typing communicating agents against a publicly-observable global protocol.

In this vault

Multiparty Asynchronous Session Types — Honda, Yoshida & Carbone POPL 2008, the multiparty session-types foundation
Structured Communication-Centred Programming for Web Services — Carbone, Honda & Yoshida 2007/2012, choreographies built on session types
Introduction to Choreographies
On the Monitorability of Session Types
Choreographic Programming
Endpoint Projection
Commitment Machines - Yolum and Singh
BSPL: the multiagent-systems counterpart that dispenses with projection and ordered channels; Enactability in place of projectability
Flexible Protocol Specification and Execution
Conversation Protocols
Pact - A Choreographic Language for Agentic Ecosystems

Coordinating Agents Using ACL Conversations

Coordinating Agents using Agent Communication Languages Conversations

Reference: R. Scott Cost, Yannis Labrou, Tim Finin (2000). Springer-Verlag book chapter, March 2000. Source file: Coordinating_Agents_using_Agent_Communication_Lang.pdf. URL

Summary

This chapter argues that ACLs like KQML and FIPA-ACL provide the vocabulary for exchanging propositional attitudes but not the higher-level coordination structures agents need when carrying out task-oriented interactions. The authors advocate conversation protocols — pre-arranged message-exchange patterns — as the missing layer above individual speech acts, giving context for interpretation and enabling agents to expect and verify sequences of messages.

They survey existing approaches (COOL state machines, Dooley Graphs, Push-Down Transducers, DCGs) and propose a formalism based on Colored Petri Nets (CPNs) for specifying conversation protocols. The CPN-based specification enables concurrency modeling, role/participant tracking, and formal verification of properties like liveness and reachability. The approach positions shareable conversation protocol specifications as “abstract agent interfaces” (AAIs).

Key Ideas

ACLs alone do not encode expectations about response sequences; conversation protocols fill that gap.
Conversation = pre-arranged coordination protocol giving pragmatic context to messages.
Colored Petri Nets offer concurrency and verifiability lacking in FSM-based approaches.
Three issues for conversations: specification, sharing, and aggregation into services.
Specialization and composition of conversations, analogous to OO subclassing.

Connections

Conceptual Contribution

Claim: Isolated speech-act messages are insufficient for agent coordination; shareable, verifiable conversation protocols — best specified as Colored Petri Nets — are the appropriate layer above ACL performatives.
Mechanism: Survey of FSM/DFA/DCG conversation models (COOL, Dooley Graphs, ATM, PDTs) and their expressivity limitations; stepwise translation of a KQML Register conversation from JDFA to an equivalent CPN that captures role constraints, concurrency, message ordering, and a negotiation example; argues CPNs enable liveness/reachability verification.
Concepts introduced/used: Conversation Protocols, Colored Petri Nets, Propositional Attitudes, Abstract Agent Interfaces, Conversation Specialization, Conversation Composition, Speech Acts
Stance: engineering / formal-semantic
Relates to: Complements ACRE Agent Conversation Reasoning Engine (runtime reasoning over conversation state) and shares motivation with Verifiable Semantics for ACLs — both insist ACL semantics be externally checkable. Builds on KQML Overview and FIPA-ACL performative sets.

Tags

FIPA-ACL Specifications

Reference: Foundation for Intelligent Physical Agents (2002). FIPA ACL Message Structure Specification (FIPA00061) and FIPA Communicative Act Library Specification (FIPA00037). Geneva, December 2002. (FIPA was absorbed into the IEEE Computer Society in 2005; specifications remain the canonical reference.) FIPA00061 (Message Structure) · FIPA00037 (Communicative Act Library) · FIPA00067 (Agent Message Transport) · IEEE FIPA standards committee

Summary

The FIPA-ACL specifications are the standards-track distillation of the late-1990s mentalistic ACL programme: the wire format and semantics that “ended up shipping” as the canonical example of an industry-grade agent communication language. The suite splits into three documents that matter for ACL design. FIPA00061 specifies the message structure — the surface syntax of an ACL message as a parameterised performative envelope with :sender, :receiver, :content, :language, :ontology, :protocol, :conversation-id, :reply-with, :in-reply-to, :reply-by, and a small set of related parameters. FIPA00037 specifies the communicative act library — twenty-two performatives (accept-proposal, agree, cancel, cfp, confirm, disconfirm, failure, inform, inform-if, inform-ref, not-understood, propagate, propose, proxy, query-if, query-ref, refuse, reject-proposal, request, request-when, request-whenever, subscribe) — each given by feasibility precondition (FP) and rational effect (RE) expressed in the FIPA Semantic Language (SL) over beliefs, intentions, and uncertainty. FIPA00067 specifies the message transport (HTTP, IIOP, WAP carriers; envelope and routing).

Two features make FIPA-ACL the canonical reference point — and the canonical negative example — for ACL semantics work. First, the direct lineage from Cohen and Levesque: the FP/RE structure of FIPA00037 is a streamlined adaptation of Cohen and Levesque 1995. The semantics of inform(p) is, modulo notation, exactly the Cohen–Levesque definition: the sender believes p, believes the receiver does not know p, and intends the receiver to come to believe p. The semantics of request mirrors attempt over a hearer action. Second, the unverifiability problem: precisely because the semantics is given in terms of sender and receiver mental states, no external observer can determine whether a message is FIPA-conformant. A platform that ships inform(p) in violation of its feasibility preconditions (e.g. the sender does not believe p, i.e. is lying) is indistinguishable on the wire from a platform that ships a conformant inform. This is the deficiency Singh 1998 names, Wooldridge formalises, and the commitment-based semantics tradition fixes.

For this vault, FIPA-ACL is the engineered artefact against which the public-semantics critique runs. The spec is well-engineered as a message format — the envelope, the protocol-id mechanism, the ontology / language slots are all sound — and the wire format itself has aged well. What has not aged well is the semantics by mental-state precondition: it is unverifiable, hostile to heterogeneous deployment, and incompatible with the public-semantics / commitment-based programme that CBCL inherits. The right reading is: keep the engineering, replace the semantics.

Key Ideas

Three-part suite: FIPA00061 (message structure), FIPA00037 (communicative act library), FIPA00067 (message transport).
Message structure: :sender, :receiver, :content, :language, :ontology, :protocol, :conversation-id, :reply-with, :in-reply-to, :reply-by, :performative. Standard envelope; the :content slot carries an arbitrary content-language expression interpreted by the :ontology.
Twenty-two performatives: from accept-proposal through subscribe, organised loosely into Searlean families (assertives, directives, commissives, declaratives). The set is small enough to remember and rich enough to cover most multi-agent interaction patterns.
Semantic Language (SL): FIPA’s formal language for FP/RE definitions; a modal logic over belief, uncertainty, intention, and action, descended from Cohen and Levesque.
Feasibility precondition / rational effect: each performative is defined by an FP (what must hold for the agent to perform the act in good faith) and an RE (what the agent intends to bring about). Both involve nested beliefs and intentions of sender and receiver.
Interaction protocols: FIPA also standardises a small set of interaction protocols (FIPA-Request, FIPA-Query, FIPA-ContractNet, FIPA-IteratedContractNet, FIPA-EnglishAuction, FIPA-DutchAuction, FIPA-Brokering, FIPA-Recruiting, FIPA-Subscribe, FIPA-Propose) — finite state machines over performatives that script common conversational patterns.
Unverifiability is intrinsic: the FP/RE conditions are stated over mental states; no external observer can check conformance without inspecting agent internals — a known design cost and the central target of the social-agency critique.

Connections

Conceptual Contribution

Claim: A standardised ACL can be built from a small set of performatives, each given by mental-state preconditions and intended effects in a modal logic, embedded in a standardised message envelope, with a standard library of interaction protocols. The result is the canonical industry ACL.
Mechanism: Three coordinated specs. FIPA00061 fixes the wire format (envelope parameters and message routing). FIPA00037 fixes the performative semantics in SL, with each of twenty-two performatives given by FP and RE in terms of belief, uncertainty, and intention nested over sender and receiver. FIPA00067 specifies the message transport. A small library of interaction protocols (FIPA-Request, FIPA-ContractNet, etc.) gives canonical conversational patterns as finite state machines over performatives.
Concepts introduced/used: FIPA Performative, Semantic Language (FIPA SL), Feasibility Precondition, Rational Effect, FIPA Interaction Protocol, ContractNet, ACL Message Envelope, Conversation ID.
Stance: standards specification suite / industry deliverable.
Relates to: Direct standardisation of Cohen and Levesque 1995 — the FIPA00037 semantics is essentially that paper’s framework with editorial smoothing. As the canonical engineering artefact of mentalistic ACL semantics, FIPA-ACL is the negative example for Singh 1998, Wooldridge, Yolum & Singh, Fornara & Colombetti, and the public-semantics tradition generally. CBCL reuses the engineering of FIPA-ACL (typed performative envelope, conversation-id, ontology slot, protocol-id) while replacing the semantics with publicly verifiable commitment-based meaning. The modern LLM-agent protocol generation (Model Context Protocol, Agent-to-Agent Protocol, LACP) has retreated from FIPA’s level of semantic ambition; the open question is whether that retreat will repeat the mentalistic mistake under a new guise (sycophantic JSON tool-calls) or learn from the FIPA experience.

Commitment-Based Protocol

An interaction protocol specified not by a fixed message sequence but by the social commitments agents create, discharge, cancel or delegate through their messages. This gives an objective, verifiable semantics that tolerates flexible enactment.

In this vault

Kiko - Programming Agents to Enact Interaction Protocols

Kiko: Programming Agents to Enact Interaction Protocols

Reference: Samuel H. Christie V, Munindar P. Singh & Amit K. Chopra (2023). Proc. 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2023), London, May 29 – June 2, 2023. IFAAMAS, 10 pages. Posted as arXiv:2606.26156v1 [cs.MA], 23 June 2026. URL. Software and appendix: https://gitlab.com/masr/bspl/-/tree/kiko

Summary

Kiko is a protocol-based programming model for agents that enact BSPL information protocols. Its diagnosis is that existing agent programming offers poor abstractions for decision making: JADE hard-wires FIPA’s ordering-based protocols, Jason and JaCaMo give cognitive abstractions but no protocols, commitment-based approaches lean on centralised commitment stores or do not operationalise asynchrony, and agent-oriented methodologies leave protocols as informal UML diagrams. Kiko’s answer is that the messages an agent sends are its public decisions, so the programmer’s job should reduce to writing decision makers: functions that are handed the set of messages the agent is currently enabled to send and choose which of them to complete and emit.

The enabling abstraction is the form: a prototype message instance whose ⌜in⌝ parameters are already bound from the agent’s history (its causal dependencies are met) and whose ⌜out⌝ parameters are left for the decision maker to fill. A generic protocol adapter computes the enabled forms from the agent’s local store, invokes decision makers on events, and validates each returned set of instances as an emission attempt: either every instance in the set is emitted or none is, so a decision maker that tries to send both Buy and Reject for one enactment is rejected outright rather than partially honoured. The adapter also validates receptions for integrity, and because BSPL constrains only emission, no ordering, reliability or central coordination is required of the transport; the implementation runs over UDP and treats reception as idempotent. Worked patterns include correlation across concurrent enactments, cross-enactment decisions (buy the cheapest of several quotes), playing roles in several unrelated protocols at once, atomic emission sets spanning protocols, reception-order freedom (a Rescind may overtake the Quote it depends on and simply disables the matching Buy), loose coupling under protocol change, and single-form decision makers as a convenient special case.

The formal part models an agent as a history plus input and output channels and gives a transition semantics with three rules: Recv (receive a message not already in the history if it passes the receive-check), Tx (delivery, whose non-application models loss) and Decide (compute enabled forms, apply a decision maker, emit if the send-check passes). Theorem 1 (soundness) states that every reachable state of a Kiko multiagent system simulates some reachable enactment of the protocol, so compliance holds regardless of what the decision makers choose; Theorem 2 shows that an optimised Decide rule that checks only the internal compatibility of the chosen set is equivalent to the full check, since forms are drawn from the enabled set and decision makers preserve their bindings; Theorem 3 (completeness) states that for any reachable enactment there exist decision makers that realise it, assuming all sent messages are received. The discussion relates Kiko to its predecessors in the same programme (Stellar, which introduced forms but used per-message handlers; Protocols over Things; Bungie; Mandrake), invokes the end-to-end argument for building over simple transports, and sketches norm-based forms, accountability, concurrent decision makers as actors, and microservices as directions.

Key Ideas

Messages are decisions. A protocol constrains decision making, not message ordering; an agent’s programming interface should be the set of valid decisions currently open to it.
Forms. Enabled message prototypes with ⌜in⌝ bound and ⌜out⌝ unbound, derived incrementally per enactment context (MAS identifier plus key bindings) from the local store.
Decision makers. Programmer-written functions from sets of forms to sets of instances; invoked on communication events by default, or on custom events via an internal queue, so no polling.
Atomic emission sets. An attempt is emitted in full or rejected in full; partial emission of a consistent subset is ruled out as arbitrary. This is the feature the authors call unique to Kiko.
Adapter architecture. Local Store, Enablement, Checker, Emitter and Receiver; the adapter is generic and understands information protocols, so the communication service is fully abstracted from business logic.
Unordered, lossy transport suffices. BSPL constrains only emission and reception is idempotent, so UDP without ordering or reliability enacts protocols correctly; this is offered as compatibility with the end-to-end argument, and as something ordering-based protocol approaches cannot claim.
Formal definitions. Association, instance, form, context, consistency, out- and nil-compatibility, derivation, enablement, decision maker, send-check and receive-check (Definitions 2 to 13).
Soundness, optimisation, completeness. Reachable states simulate protocol enactments (Thm 1); the internal-compatibility-only Decide is equivalent (Thm 2); any reachable enactment is realisable by some decision makers under delivery (Thm 3).
Loose coupling. Because coupling is by information, adding an indirect bank-transfer path to Purchase leaves the seller’s decision logic unchanged; the adapter derives the Deliver form once payment arrives by either route.
Lineage. Stellar (forms, message handlers), Protocols over Things and Mandrake (fault tolerance), Bungie (extensible application-level protocols), Tosca and Clouseau (commitments compiled to information protocols).

Connections

BSPL
Information Protocols
Enactability
BSPL - The Blindingly Simple Protocol Language
Semantics and Verification of Information-Based Protocols: defines the reachable enactments that Kiko’s states are shown to simulate
Interaction Protocols
Agent-Oriented Programming
AgentSpeak
An Interaction-oriented Agent Framework for Open Environments: the JaCaMo-based commitment framework Kiko contrasts with
Agents and Artifacts
FIPA-ACL Specifications: the JADE/FIPA ordering-based incumbent
Commitment-based Semantics
Actor Model: proposed substrate for concurrent decision makers
Multiparty Asynchronous Session Types: cited as a representative ordering-based protocol language
Endpoint Projection
CALM Theorem
CBCL - Safe Self-Extending Agent Communication

Conceptual Contribution

Claim: Agents should be programmed as sets of decision makers over the messages a protocol currently enables them to send. Given an information protocol, this abstraction guarantees compliance by construction, supports realistic decision patterns that ordering-based models cannot express, and needs only an unordered, unreliable transport.
Mechanism: Forms derived from the local store per enactment context; decision makers returning emission attempts checked atomically; a protocol adapter (store, enablement, checker, emitter, receiver) over UDP; an operational semantics (Recv, Tx, Decide) with soundness, an equivalent optimised check, and completeness relative to BSPL’s reachable enactments.
Concepts introduced/used: Information Protocols, BSPL, Enactability, Agent-Oriented Programming, Actor Model, Interaction Protocols
Stance: programming model / engineering, with formal guarantees
Relates to: Completes the BSPL stack begun in BSPL - The Blindingly Simple Protocol Language and Semantics and Verification of Information-Based Protocols by giving the agent side a programming interface whose correctness is stated against that semantics. It occupies the place that per-role projected programs occupy in Choreographic Programming and per-role monitors occupy in Session Types, but reaches it without Endpoint Projection: the adapter evaluates the global protocol against the agent’s own history. The same “decide from local history, verify from the trace” shape appears in CBCL - Safe Self-Extending Agent Communication’s R5 verifier, which is why Kiko and its BSPL lineage are the nearest multiagent-systems precedent for that work.

Semantics and Verification of Information-Based Protocols

Reference: Munindar P. Singh (2012). Proc. 11th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2012), Valencia, Spain, June 4–8, 2012. IFAAMAS. PDF. Semantic Scholar

Summary

The sequel to BSPL - The Blindingly Simple Protocol Language gives BSPL the formal semantics its flexibility demands, defines three correctness properties, and implements verifiers for them. A protocol denotes a set of enactments over a universe of discourse of roles and message schemas. Each role has a history of the messages it has emitted or received; a history vector collects one per role. Viability is the local rule from the 2011 paper made precise: a role may emit a message only if it knows the bindings of every ⌜in⌝ parameter for the enactment’s key and knows no binding for any ⌜out⌝ or ⌜nil⌝ parameter; reception is always viable and extends knowledge. The intension of a protocol is the set of history vectors that are viable, respect the fundamental causality constraint that a reception is preceded by the corresponding emission, and are covered by the intensions of the protocol’s references.

Three properties are then defined on the intension. A protocol is enactable if its intension is non-empty, that is, some viable path binds all public parameters. It is safe if no history vector binds the same parameter twice for the same key: safety is the distributed integrity property, and the paper’s diagnosis is that across roles it holds precisely when every pair of conflicting ⌜out⌝ emissions is gated by a causally prior branching point controlled by a single role. It is live if from any reachable state the enactment can still legally complete; liveness entails enactability but not the converse. The small examples fix intuitions: Local Conflict is safe but not enactable, Abrupt Cancel (a race between buyer and seller on outcome) is enactable but not safe, Purchase Unsafe drops the private parameter that made accept and reject exclusive, and Purchase No Ship is enactable but not live because after accept nothing can ever bind outcome.

For verification, a protocol’s causal structure is expressed as a set of declarative temporal precedence constraints, and each property is decided by checking the (un)satisfiability of the conjunction of that causal structure with a property-specific formula using a temporal reasoner. The paper reports the clause counts for Purchase and its variants and for the FIPA Request protocol, and lists cheaper design-flaw checks (deadwood messages, parameters that can never be bound or used). The related-work discussion positions BSPL against AUML, message sequence charts and choreography description languages, all of which take a procedural stance on ordering, and notes that both of Desai and Singh’s enactability failures, blindness and nonlocal choice, yield an empty intension and are thereby caught. The LoST middleware (local state transfer) is cited as the architecture that enforces the local constraints at runtime.

Key Ideas

Semantics by enactments. A protocol’s meaning is its intension: the set of viable, causally consistent history vectors covered by its references. Local views and asynchrony are built into the model rather than abstracted away.
Viability is local. Emission requires knowing all ⌜in⌝ bindings and no ⌜out⌝ or ⌜nil⌝ binding for the enactment key; the semantics of a protocol depends only on the specification, never on imagined internal policies of the agents.
Declarative force of ⌜out⌝. An ⌜out⌝ binding is not a report but a declaration (Austin), which is why it may occur only once per key and why a means clause can attach a commitment to it.
Enactability, safety, liveness. Non-empty intension; at most one binding per parameter per key across all roles; completion always remains possible. Liveness entails enactability.
Safety across roles needs a same-role branching point. Two conflicting ⌜out⌝ emissions by different roles are safe only if a causally prior conflict controlled by one role makes them exclusive; the private response parameter in Purchase is the canonical example.
Causal structures. The partial-order structure of a protocol as a set of temporal constraints, mappable to a finite-state machine only with an explosion in states, so reasoning is done declaratively instead.
Verification by satisfiability. Each property is a formula conjoined with the causal structure and handed to a temporal reasoner; validated on Purchase variants and FIPA Request.
Blindness and nonlocal choice both yield empty intensions, so the enactability check subsumes the earlier diagnostics of Desai and Singh.
Design-flaw checks. Deadwood messages, never-bound private parameters, never-used private parameters, protocols with public ⌜in⌝ parameters (empty intension).

Connections

BSPL
Information Protocols
Enactability
BSPL - The Blindingly Simple Protocol Language
Kiko - Programming Agents to Enact Interaction Protocols: the operational semantics whose soundness is stated relative to the reachable enactments defined here
Interaction Protocols
Commitment-based Semantics
Speech Act Theory: the declarative force of ⌜out⌝ bindings
FIPA-ACL Specifications: FIPA Request as a verification benchmark
Knowledge of Choice
Realizability and Verification of MSC Graphs
Deciding Choreography Realizability
Message Sequence Charts - A Survey
Multiparty Compatibility in Communicating Automata
Endpoint Projection
CBCL - Safe Self-Extending Agent Communication

Conceptual Contribution

Claim: An information-based protocol language can be given a formal semantics that respects the locality of each role, the flow of causality across roles and the asynchrony between them, and its central correctness properties (enactability, safety, liveness) can be formulated declaratively and verified mechanically.
Mechanism: Universe of discourse, role histories, history vectors, viability, and intension by cover; Definitions of enactability (non-empty intension), safety (key uniqueness in every history vector) and liveness (completion always possible); causal structure as temporal precedence clauses; verification by (un)satisfiability with a temporal reasoner; evaluation on Purchase variants and FIPA Request.
Concepts introduced/used: Enactability, Information Protocols, BSPL, Realizability, Knowledge of Choice, Interaction Protocols
Stance: formal semantics / verification
Relates to: Enactability is the multiagent-systems analogue of the Realizability problem for message sequence charts and choreographies (Realizability and Verification of MSC Graphs, Deciding Choreography Realizability) and of Knowledge of Choice in Choreographic Programming: all ask whether independently acting endpoints can jointly produce exactly the specified global behaviour. BSPL’s answer is stated over local knowledge rather than channel orderings, which is also the reading that the CBCL role layer’s causal-locality condition takes (CBCL - Safe Self-Extending Agent Communication, Endpoint Projection).