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⟩ riff(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 (typicallytrue). - Three reasoning rules over commitments: (1)
Cₓpdischarges whenpholds; (2)Cₓ(p ; r)collapses to base-levelCₓrwhenpholds; (3)Cₓ(p ; r)ceases whenrholds beforep, with no new commitment. - Compilation to deterministic FSM under two restrictions: (R1) no transition
mᵢ → mⱼifmᵢ ⊢ 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
Mand the path to a final meaning still exists.
Connections
- Flexible Protocol Specification and Execution
- A Commitment-Based Approach to Agent Communication
- Agent Communication And Institutional Reality
- ACL Rethinking Principles
- Verifiable Semantics for ACLs
- A Common Ontology Of ACLs
- Commitment-Based Protocol
- Commitment-based Semantics
- Public Semantics
- Social Commitment
- Conditional Commitment
- Commitment
- NetBill Protocol
- Conversation Protocols
- Endpoint Projection
- Choreographic Programming
- Pact - A Choreographic Language for Agentic Ecosystems
- Speech Act Theory
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 setsMand final-meaning setsF(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
precommitmentstate 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 #commitments #protocol-specification #fsm-compilation #verifiability #foundational #social-agency