On the Monitorability of Session Types, in Theory and Practice

Reference: Bartolo Burlò, C., Francalanza, A. & Scalas, A. (2021). 35th European Conference on Object-Oriented Programming (ECOOP 2021), LIPIcs vol. 194: 20:1–20:30. DOI: 10.4230/LIPIcs.ECOOP.2021.20. Extended version: arXiv:2105.06291. Source file: bartolo-burlo-francalanza-scalas-ecoop21.pdf. URL

Summary

Bartolo Burlò, Francalanza and Scalas address the monitorability problem for Session Types — the question of whether a runtime monitor, observing only the messages a process exchanges, can faithfully detect violations of a session-type specification. Session types are the dominant PL formalism for typing communicating processes (Honda, Vasconcelos, Yoshida), and they admit static type-checking when source is available; the runtime question matters because in many practical settings (third-party code, foreign-language components, dynamic deployments) only message traces are observable. The authors formalise session-monitored processes — a process algebra in which a monitor sits on the wire and interrupts ill-typed exchanges — and prove the central correctness pair: soundness (a monitor flags only processes that are actually ill-typed) and completeness (a monitor flags every ill-typed process whose violation is detectable from its observable trace).

The theoretical core is a precise characterisation of which session-type properties are monitorable from observable traces alone — distinguishing what static type-checking can decide (everything in the type) from what a dynamic monitor can decide (a strictly smaller class, characterised by the paper). On the practical side, the authors build a Scala toolkit that automatically generates session-type monitors from session-type specifications; the generated monitors instrument black-box processes written in any language, and the paper benchmarks the runtime overhead. The result is a working bridge from the theory of session types to deployable runtime conformance checking — and, by structural analogy, an off-the-shelf playbook for the same operation on commitment-based and choreographic protocols.

Key Ideas

Session-monitored processes: a process algebra extended with explicit monitors that observe message exchanges and rule them in or out against a session type.
Soundness of monitoring: a monitor never flags a well-typed process as a violator. (Verbatim: “monitors only flag ill-typed processes”.)
Completeness of monitoring: a monitor flags every ill-typed process whose violation is observable from the message trace.
Monitorability gap: not every session-type property is monitorable from observable traces — the paper characterises exactly which ones are.
Connection to static type-checking: the monitorable fragment is a strict sub-class of the statically-decidable fragment, and the paper precisely locates the gap.
Scala monitor toolkit: automatic generation of executable monitors from session-type specifications; works on black-box processes.
Empirical evaluation: benchmarks of monitor overhead on representative communication-heavy workloads.

Connections

Conceptual Contribution

Claim: Session types — like commitment-based protocols — admit a precise monitoring theory in which a runtime monitor observing only the message trace can be proved sound and complete with respect to a session-type specification, modulo a precisely-characterised gap between what is statically decidable and what is observable from traces alone; this theory can be discharged into an automatic toolkit that generates working monitors from specifications.
Mechanism: Define session-monitored processes as a process algebra with explicit on-wire monitors; formalise soundness (monitor flags only ill-typed processes) and completeness (every observable violation is flagged); characterise the monitorable fragment of session-type properties; implement an automatic monitor generator in Scala and benchmark its overhead on instrumented black-box processes.
Concepts introduced/used: Session Types, Runtime Verification, Monitorability, soundness, completeness, process algebra, Choreographic Programming, Endpoint Projection, Conversation Protocols
Stance: formal-semantic + engineering
Relates to: Structural sibling of the commitment-machine / commitment-protocol tradition: session types and commitment-based protocols are independently-developed formalisms for the same thing — typing communicating processes against a publicly-observable global protocol — and the runtime-monitoring theory developed here lifts almost directly to the commitment-machine setting (where Yolum-Singh’s “complete iff every base-level commitment is discharged” is the commitment-protocol analogue of session-type monitorability). Provides the theoretical engine for a runtime-conformance layer over choreographic protocols — choreographies project to per-role session types, which can then be monitored using this paper’s machinery, closing the gap that the Pact review opened (Pact has design-time game-theoretic analysis but no runtime conformance check). For CBCL - Safe Self-Extending Agent Communication, the paper supplies an analogue for the in-flight version of R5: where R5 checks contract well-formedness at install time, monitorability theory is the runtime story for the per-message-trace check. Companion to Verifiable Semantics for ACLs (Wooldridge 1998) in the unverifiability-becomes-decidability line: Wooldridge showed that mentalistic ACL semantics is undecidable; this paper shows that public, trace-based semantics admits sound-and-complete monitoring.

Tags

#session-types #runtime-verification #monitorability #process-algebra #choreographic-programming #conversation-protocols #foundational

Backlinks

Linked Pages

Verifiable Semantics for ACLs

Verifiable Semantics for Agent Communication Languages

Reference: Michael Wooldridge (1998). ICMAS-98 (International Conference on Multi-Agent Systems). Source file: icmas98.pdf. URL

Summary

Wooldridge tackles a central problem for ACL standardization: how can an external observer verify that an agent conforms to an ACL’s semantics when semantics are expressed in modal BDI logic (beliefs, desires, intentions)? He formalizes an agent communication framework as a tuple containing agent programs, local states, a communication language, a semantic language, and interpretation functions, and defines precisely what it means for a framework to be verifiable: whether one can decide, from program text alone, that the semantic conditions for a sent message are satisfied.

He shows that KQML and FIPA-97 ACL, which define the “sincerity condition” for an inform act using multi-modal quantified logics like SL, are not practically verifiable — deciding whether an agent program really believes what it says requires checking undecidable properties. In contrast, he gives two example frameworks with verifiable (even co-NP-complete) semantics by grounding meaning in program states rather than unobservable mental attitudes. The paper’s upshot: practical ACL conformance testing requires public, state-based semantics.

Key Ideas

Formal agent communication framework as a 2n+4 tuple.
Verifiability = decidability of semantic conformance from program text.
KQML and FIPA-97 semantics (SL modal logic) are not practically verifiable.
Grounding semantics in program states yields co-NP-complete verifiability.
Motivates social/public commitment-based ACL semantics.

Connections

KQML
FIPA-ACL
Speech Act Theory
Agent Communication Languages
Verifiable Semantics
Public Semantics
Commitment-based Semantics
Mental State
Mentalistic Semantics
BDI
CBCL - Safe Self-Extending Agent Communication — O’Connor 2026: a verifiable ACL grounded in DCFL grammars and Lean-checked safety invariants, answering Wooldridge’s challenge in the LLM-agent era.

Conceptual Contribution

Claim: An ACL standard is only useful if one can check whether an implementation respects it; existing ACLs (KQML, FIPA-97) whose semantics are given in multi-modal BDI logics are not practically verifiable, so ACL semantics should instead be grounded in program states.
Mechanism: Formalises an agent communication framework as a (2n+4)-tuple of agent programs, local states, communication language L_C, semantic language L_S, and interpretations; defines verifiability as decidability (in polynomial time) of whether an agent program respects a message’s semantic precondition; shows FIPA’s SL semantics undecidable; constructs two verifiable example frameworks (classical propositional logic, grounded propositional epistemic logic) with co-NP-complete verification.
Concepts introduced/used: Verifiable Semantics, Agent Communication Framework, Sincerity Condition, Grounded Semantics, Program Semantics, Model Checking, BDI Logic, Mentalistic Semantics
Stance: formal-semantic / critique
Relates to: Formal companion to ACL Rethinking Principles — Singh’s social-agency argument becomes Wooldridge’s verifiability theorem. Undermines the semantic ambitions of KQML Overview and FIPA-ACL; motivates commitment-based approaches such as Agent Communication And Institutional Reality and the program-grounded framework in Foundations Of Illocutionary Logic.

Tags

CBCL - Safe Self-Extending Agent Communication

CBCL: Safe Self-Extending Agent Communication

Reference: O’Connor, H. (2026). LangSec Workshop, IEEE Security and Privacy Workshops (SPW 2026). 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
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.

Pact - A Choreographic Language for Agentic Ecosystems

Pact: A Choreographic Language for Agentic Ecosystems

Reference: Gopinathan, K., Feser, J., Naim, M., Tavares, Z. & Bingham, E. (2026). 2nd International Workshop on Choreographic Programming (CP 2026), Boulder, CO, June 15–19. arXiv:2605.03143v1 [cs.PL], 4 May 2026 (talk paper). Basis Research Institute. URL

Summary

Gopinathan et al. extend Choreographic Programming to the open-systems setting where participants are self-interested and may not faithfully execute a protocol. Choreographies (Montesi 2023; Bates et al. 2025) give correct-by-construction, deadlock-free distributed protocols by writing one global program that is mechanically projected to local endpoints, but they assume cooperative participants — they cannot answer why an autonomous agent should follow the projected protocol. Pact answers that question by adding three operators to a core choreographic calculus: agent.choose(τ) for explicit strategic non-determinism, agent.values(x) for declared utility dependencies, and world.choose(τ) for exogenous “nature” variables that capture each agent’s priors over the environment. Every Pact program then maps unambiguously to a formal extensive-form game.

The headline analysis is a decision-policy solver built on the Memo Programming Language (Chandra et al. 2025), a probabilistic-programming DSL for cognitive theory-of-mind models. From the projected Pact program a memo model is constructed in which each role recursively simulates the other to depth ℓ; running inference yields a level-ℓ bounded-rational policy mapping observations to choices. Applied to the canonical book-seller choreography the solver recreates Akerlof’s Market for Lemons: at depth 0 the buyer naïvely treats price as a signal of quality and the seller exploits this; as ℓ grows the acceptance probability flattens. The implementation is an embedded Python DSL on top of the Effectful algebraic-effects library, with endpoint projection realised as effect handlers. The paper is positioned as preliminary work; next steps named are formalising the semantics, proving correctness of projection-to-game, and adding incentive-compatibility / equilibrium / mechanism-design analyses.

Key Ideas

Choreography + game theory: a global protocol gets three game-theoretic operators (choice, value, nature) so that endpoint projection produces both a runnable program and a formal game.
values as type signature, not utility: declarations name the variables that influence an agent’s payoff but not the function — utilities are private and adversarially incentive-incompatible to disclose. The role of values is to constrain which protocols are mutually negotiable.
Theory-of-mind solver via memo: bounded-rational level-ℓ recursion over agent models, with the recursion bottoming out at naïve priors at ℓ = 0.
Lemons re-derived from a choreography: information asymmetry over an exogenous book.quality variable is enough to reproduce Akerlof’s unravelling result on the bookseller protocol.
Algebraic-effects implementation: endpoint projection implemented as effect handlers in Python (effectful); choreography is a single program that runs differently depending on which handler (Endpoint Projection) is installed.
Motivation framed against LLM agent failure modes: prompt injection, sycophancy, and coercion of LLM agents are cited as the reasons untrusted-counterpart coordination needs formal protocol artefacts rather than free-form natural-language negotiation.

Connections

Conceptual Contribution

Claim: Choreographic protocols for autonomous-agent ecosystems should make agent strategy first-class — explicit choices, declared utility dependencies, and exogenous priors — so that every protocol corresponds to a formal game and can be analysed for whether self-interested agents will participate.
Mechanism: Three new constructs added to a core choreographic calculus (agent.choose, agent.values, world.choose); a structural map from Pact programs to extensive-form games; a level-ℓ bounded-rational decision-policy solver built by translating the projected program into a Memo Programming Language theory-of-mind model and running probabilistic inference over it; an embedded-DSL implementation in Python via algebraic effects realising endpoint projection.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Theory of Mind, Memo Programming Language, Bounded Rationality, Market for Lemons, Mechanism Design, Algebraic Effects, Negotiation, Game-Theoretic Trust, Mentalistic Semantics
Stance: position / preliminary engineering (CP 2026 workshop talk paper)
Relates to: A contemporary LLM-era restatement of the individual-rationality answer to “why follow a protocol?” first formalised by Deals Among Rational Agents (Rosenschein & Genesereth 1985) and lifted to mental attitudes by Intention Is Choice with Commitment (Cohen & Levesque 1990). The paper is structurally adjacent to — but does not engage — the entire commitment-protocol tradition: Flexible Protocol Specification and Execution (Yolum & Singh 2002) gives a global protocol semantics in the Event Calculus with explicit Create / Discharge / Cancel / Release / Assign / Delegate operations whose runs project to local agents in a way directly analogous to choreographic endpoint projection, and A Commitment-Based Approach to Agent Communication (Fornara & Colombetti 2004) gives an operational FSM semantics for the same primitives. ACL Rethinking Principles (Singh 1998) and Verifiable Semantics for ACLs (Wooldridge 1998) anticipate the central limitation: a semantics grounded in agent utilities and recursive belief models is unverifiable from message traces alone — the very failure modes the paper opens with (prompt injection, sycophancy, coercion) destabilise the priors and rationality assumptions the solver depends on. The Lemons demo, taken at face value, is an argument for institutional / commitment mechanisms (warranties, refund obligations, certification) of the kind Singh’s programme articulates rather than for theory-of-mind solving. The constructive synthesis the paper does not propose is to layer commitment operations onto the choreographic substrate so that protocols carry both a public, observable commitment trace (Singh-style verifiability) and a game-theoretic acceptability analysis (Pact-style strategic reasoning); choreographies are a particularly natural host because endpoint projection already gives the global-to-local move that Commitment Machines approximates by FSM compilation. On the LLM-agent side the paper’s diagnosis converges with Why AI Agents Communicate In Human Language (formal protocol artefacts beat free-form natural-language negotiation) and complements the standardisation argument of LLM Agent Communication Protocol Requires Urgent Standardization.

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

Conversation Protocols

Stateful, multi-turn interaction patterns (Contract Net, auction, query) specified as a finite automaton, Petri net, or role-based dialogue over performatives. Promote tractable ACL use by constraining expected message sequences, and are the unit on which ACRE’s reasoning engine operates.

In this vault

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.

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

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
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

Monitorability

The property of a behavioural specification that admits a sound-and-complete runtime monitor: a passive observer that, watching only the externally-visible trace of a system, can flag exactly the executions that violate the specification. Not every property is monitorable from traces alone — generally, only safety properties are fully monitorable, while liveness properties are not — and the precise characterisation depends on what the monitor is allowed to observe. For Session Types, Bartolo Burlò, Francalanza & Scalas (On the Monitorability of Session Types) give a precise account: the monitorable fragment is a strict sub-class of the statically-decidable fragment, and they exhibit an automatic monitor-synthesis procedure. Structurally adjacent to the conformance theory of commitment-based protocols, where Yolum-Singh’s “every base-level commitment is discharged at run end” is the commitment-protocol analogue of session-type monitorability.

In this vault

Runtime Verification

A lightweight verification technique in which a monitor checks at execution time whether the observed trace of a system satisfies a formal specification, raising alarms or triggering recovery on violation. It complements model checking by handling systems too large or open for exhaustive analysis.

In this vault

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
Flexible Protocol Specification and Execution
Conversation Protocols
Pact - A Choreographic Language for Agentic Ecosystems

Public Semantics

ACL semantics grounded in externally observable facts (commitments, roles, institutional state) rather than private mental state.

In this vault

ACL Rethinking Principles
Agent Communication And Institutional Reality
Commitment-based Semantics
Mentalistic Semantics
CBCL - Safe Self-Extending Agent Communication — dialect installation as a public commitment

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

A Commitment-Based Approach to Agent Communication

Reference: Fornara, N. & Colombetti, M. (2004). Applied Artificial Intelligence 18(9–10): 853–867. DOI: 10.1080/08839510490509054. The journal article is paywalled; the open-access AAMAS-02 conference precursor — Operational Specification of a Commitment-Based Agent Communication Language (pp. 535–542) — captures the same model and is the locally archived source. Source file: fornara-colombetti-aamas02.pdf. URL

Summary

Fornara and Colombetti develop an object-oriented operational semantics for an Agent Communication Language grounded entirely in social commitments, intended for open environments populated by self-interested, heterogeneous agents who cannot be assumed to share an honest mental architecture. A Commitment is an abstract data type with fields Identifier, Debtor, Creditor, State ∈ {empty, cancelled, precommitment, conditional, active, fulfilled, violated}, Content (a temporal proposition), Condition (another temporal proposition), and Time-out. Its evolution is given by an explicit finite-state machine driven by two kinds of transitions: agent-invoked methods (mc, mp, ap, cc, cp, rp) and event-driven update rules triggered when the truth value of the content or condition resolves.

The authors’ key innovation over the Yolum-Singh treatment is the precommitment state, which models the social situation a directive speech act creates: the speaker cannot directly commit the hearer, so a request instantiates a precommitment whose debtor is the hearer; the hearer either accepts it (turning it into an active or conditional commitment), rejects it, fulfills it implicitly by performing the action, or lets the time-out elapse. This machinery yields uniform commitment-based definitions for Searle’s main illocutionary categories — assertives (inform, informIf, informRef), commissives (promise, conditionalPromise), and directives (request, conditionalRequest, accept, reject, yes/noQuestion, whQuestion) — and lets a propose act be defined compositionally as a conditional request conjoined with a conditional promise. A worked auction-style proposal protocol is given as an interaction diagram whose state contents are computed from the speech-act definitions, and whose soundness is checked by requiring that all final-state commitments be empty, fulfilled, or violated.

Key Ideas

Commitment-as-object: a commitment is an abstract data type with a state in {e, c, p, cc, a, f, v} whose dynamics are described by an explicit FSM.
Temporal proposition class: the content/condition of a commitment is a sentence + time interval + ∀/∃ mode + state, resolved by a domain “notifier” — separating what is committed from when and how its truth is observed.
Precommitment models directive speech acts: a request creates C(p, hearer, speaker, P|Q) that the hearer can accept (ap), reject (rp), implicitly fulfil (update rule 5), or let time out.
Conditional commitment with a temporal condition becomes active when the condition is satisfied and is automatically cancelled if the condition fails.
Five update rules link the truth-state of content and condition propositions to commitment-state transitions (active→fulfilled/violated, conditional→active/cancelled, precommitment→fulfilled).
Searle’s taxonomy of illocutionary acts is recovered by composition: inform, promise, request, accept/reject, yes/noQuestion, whQuestion, propose.
Soundness of an interaction protocol is checked by an interaction diagram in which every final state’s commitments are empty, fulfilled, or violated — a structural correctness criterion for negotiation protocols.
The notion of a conversational commitment (a meta-commitment to react to interlocutor speech acts) is sketched as the principled justification for the time-out field.

Connections

Conceptual Contribution

Claim: Speech-act semantics for an ACL should be specified operationally — as state-machine transitions over a public commitment data type — so that meaning is independent of any agent’s internal mental architecture, observable to third parties, and compositional across the speech-act taxonomy; in particular, the directive family requires a dedicated precommitment state because no agent can unilaterally commit another.
Mechanism: Define an abstract Commitment class with seven explicit states and a transition FSM driven by methods (mc/mp/ap/cc/cp/rp) plus five event-driven update rules that read truth-states of Temporal Proposition objects; define each Searle category by a single-line operation on commitment objects (inform := mc(a,b,P,T), request := mp(a,b,P,T), propose := conditionalRequest ∧ conditionalPromise, etc.); validate interaction protocols structurally via a state-content interaction diagram in which final-state commitments must all be empty/fulfilled/violated.
Concepts introduced/used: Commitment, Social Commitment, Precommitment, Conditional Commitment, Temporal Proposition, Commitment-Based Protocol, Commitment-based Semantics, Public Semantics, Verifiable Semantics, Speech Act Theory, Directives, Conversation Protocols, Interaction Protocols, Open Multi-Agent Systems, Conversational Commitment
Stance: formal-semantic / engineering
Relates to: Closest neighbour is Flexible Protocol Specification and Execution (Yolum & Singh, AAMAS-02) — the authors explicitly compare the two approaches: where Yolum-Singh use the Event Calculus and an abductive planner over create/discharge/cancel/release/assign/delegate, Fornara-Colombetti use an OO/FSM data type and add the precommitment apparatus to cover directives. Both belong to the social-semantics programme catalysed by ACL Rethinking Principles and formalised verifiability-style by Verifiable Semantics for ACLs; both are subsumed under the role-based unification of A Common Ontology Of ACLs. Repudiates the mentalistic line of FIPA-ACL / Intention Is Choice with Commitment for interoperable ACL semantics while keeping speech-act theory (Speech Acts - An Essay in the Philosophy of Language, A Taxonomy of Illocutionary Acts) as the organising taxonomy. The 2004 Applied AI version this entry primarily cites elaborates the AAMAS-02 model with extended treatment of negotiation protocols and the soundness-via-conversational-commitment programme that the authors’ later artificial-institutions work develops.