Mixed Choice in Asynchronous Multiparty Session Types

Laura Bocchi; Raymond Hu; Adriana Laura Voinea; Simon Thompson

cs.DCFeb 27, 2026

Mixed Choice in Asynchronous Multiparty Session Types

Authors: Laura Bocchi, Raymond Hu, Adriana Laura Voinea, Simon Thompson

Organizations: University of Kent, UK · Queen Mary University of London, UK · University of Glasgow, UK

Abstract

We present a multiparty session type (MST) framework with asynchronous mixed choice (MC). We propose a core construct for MC that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state. We prove the correctness of our system by establishing a progress property and an operational correspondence between global types and distributed local type projections. Based on our theory, we implement a practical toolchain for specifying and validating asynchronous MST protocols featuring MC, and programming compliant gen_statem processes in Erlang/OTP. We test our framework by using our toolchain to specify and reimplement part of the amqp_client of the RabbitMQ broker for Erlang.

Figures & tables

Panel of Figure 1 — Figure 1. A multiparty timeout pattern as a safe mMST protocol using asynchronous mixed choice.

Panel of Figure 2 — Figure 2. Local mMST protocols for each role of Timeout as EFSMs in Erlang gen_statem .

⬇ 1 % Extract from role A 2 s1 ( internal , a1 , Data ) -> 3 gen_a : send_s1_a1 ( BPid , Data ), { next_state , s2 , 4 Data , [{ next_event , internal , a2 }]}; 5 s1 ( cast , { BPid , ’TOa’ }, Data ) -> { stop , normal , Data }. 6 7 s2 ( internal , a2 , Data ) -> 8 gen_a : send_s2_a2 ( CPid , Data ), { next_state , s3 , Data }; 9 s2 ( cast , { BPid , ’TOa’ }, Data ) -> { stop , normal , Data }. 10 11 s3 ( cast , { BPid , a4 }, Data ) -> { next_state , s4 , Data }; 12 s3 ( cast , { BPid , ’TOa’ }, Data ) -> { stop , normal , Data }. 13 14 s4 ( cast , { CPid , a5 }, Data ) -> { stop , normal , Data }. 15 16 17 % Extract from role B 18 s1 ( internal , ’TOa’ , Data ) -> 19 case make_choice_TOa ( Data ) of 20 1 -> { keep_state , Data }; 21 2 -> gen_b : send_s1_TOa ( APid , Data ), { next_state , s3 , 22 Data , [{ next_event , internal , ’TOc’ }]} 23 end ; % Continued on the right

⬇ 24 % Continued from the left 25 s1 ( cast ,{ APid , a1 }, Data ) -> 26 case make_choice_a1 ( Data ) of 27 1 -> { next_state , s2 , Data , 28 [{ next_event , internal , a3 }]}; 29 2 -> gen_b : send_s1_TOa ( APid , Data ), 30 { next_state , s5 , Data , 31 [{ next_event , internal , ’TOc’ }]} 32 end . 33 34 s5 ( internal , ’TOc’ , Data ) -> 35 gen_b : send_s5_TOc ( CPid , Data ), 36 { stop , normal , Data }. 37 38 s2 ( internal , a3 , Data ) -> 39 gen_b : send_s2_a3 ( CPid , Data ), { next_state , s3 , 40 Data , [{ next_event , internal , a4 }]}. 41 42 s3 ( internal , a4 , Data ) -> 43 gen_b : send_s3_a4 ( APid , Data ), 44 { stop , normal , Data }. 45 46

Figure 3. Extracts from the user-facing callback modules generated for A and B in the Timeout protocol.

Panel of Figure 4 — Figure 4. Global semantics: standard rules (top) and new rules for MC (bottom)

Panel of Figure 6 — Figure 6. Projection of global types to local types and input FIFOs

⬇ 1 % -------- Callback specifications -------- 2 - callback s5 ( term (), { atom ()}, state_data ()) -> { stop , normal , state_data ()}. 3 - callback s1 ( term (), { atom ()} | { pid (), { term ()}}, state_data ()) -> 4 { next_state , s5 , state_data (), [{ next_event , internal , { ’TOc’ }}]} | { keep_state , state_data ()} | 5 { keep_state , state_data (), [ postpone ]} | { next_state , s2 , state_data (), [{ next_event , internal , { a3 }}]}. 6 - callback s2 ( term (), { atom ()}, state_data ()) -> 7 { next_state , s3 , state_data (), [{ next_event , internal , { a4 }}]} | { keep_state , state_data ()}. 8 - callback s3 ( term (), { atom ()}, state_data ()) -> { stop , normal , state_data ()}. 9 %% -------- Record and type definitions for maintaining state -------- 10 - record ( data , { a_pid :: pid (), c_pid :: pid () }). %% Process identifiers for roles A and C. 11 %% -------- Send helpers -------- 12 send_s1_TOa ( APid , Data ) -> gen_statem : cast ( APid , { self (), { ’TOa’ }, Path }). 13 send_s5_TOc ( CPid , Data ) -> gen_statem : cast ( CPid , { self (), { ’TOc’ }, Path }). 14 send_s3_a4 ( APid , Data ) -> gen_statem : cast ( APid , { self (), { a4 }, Path }). 15 send_s2_a3 ( CPid , Data ) -> gen_statem : cast ( CPid , { self (), { a3 }, Path }). 16 %% ---------- Callback function definitions delegate the processing to the CM ---------- 17 s1 ( EventType , { APid , { a1 }, Pi }, Data ) -> 18 case stale ( Pi , left ) of 19 true -> { keep_state , Data }; 20 false -> Side = CallbackModule : s1 ( EventType , { APid , { a1 }}, Data ) 21 case Side of { next_state , s6 , _ } -> commit_entry (? MC1 , left ), Side ; 22 { next_state , s3 , _ } -> commit_entry (? MC1 , right ), Side 23 end ; 24 end ; 25 s1 ( EventType , { ’TOa’ }, Data ) -> Side = CallbackModule : s1 ( EventType , { ’TOa’ }, Data ) 26 case Side of { next_state , s6 , _ } -> commit_entry (? MC1 , left ), Side ; 27 { next_state , s3 , _ } -> commit_entry (? MC1 , right ), Side 28 end . 29 s5 ( EventType , ’TOc’ , Data ) -> CallbackModule : s5 ( EventType , ’TOc’ , Data ). 30 s2 ( EventType , a3 , Data ) -> CallbackModule : s2 ( EventType , a3 , Data ). 31 s3 ( EventType , a4 , Data ) -> CallbackModule : s3 ( EventType , a4 , Data ).

Figure 7. Extract from the RM generated for B in Timeout , implementing its protocol- and role-specific gen_statem behaviour and declaring the callback functions to be implented by the CM.

M=Multiparty B/S=Branch/Select Rec=Recursion nMC=nested MC ndMC=non-directed MC GC=purging
Example	M	B/S	Rec	MC	nMC	ndMC	GC	Source
Calculator	$\checkmark$	$\checkmark$		$\checkmark$			$\checkmark$	[Hu and Yoshida, 2016]
CircuitBreaker	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$		$\checkmark$	$\checkmark$	[Lagaillardie, Neykova and Yoshida 2022]
DistributedLogging		$\checkmark$	$\checkmark$	$\checkmark$			$\checkmark$	[Lagaillardie, Neykova and Yoshida 2022]
Fibonacci		$\checkmark$	$\checkmark$	$\checkmark$			$\checkmark$	[Hu and Yoshida, 2016]
SMTP		$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$		$\checkmark$	[Hu and Yoshida, 2016]

Table 1. MST examples extended with asynchronous mixed choice (MC).

⬇ // roles: C

=

Consumer, H

=

Channel, S

=

Server global protocol AMQP ( role C , role H , role S ) { register_default_consumer () from C to H ; basic_consume ( consumer_tag , nowait ) from C to H ; basic_consume ( consumer_tag , nowait ) from H to S ; basic_consume_ok ( consumer_tag ) from S to H ; basic_consume_ok ( consumer_tag ) from H to C ; rec SelectiveMessageDelivery { mixed { basic_deliver ( consumer_tag , delivery_tag , exchange , routing_key ) from S to H ; // Continued on right column...

⬇ process_message () from H to C ; basic_deliver ( consumer_tag , delivery_tag , exchange , routing_key ) from H to C ; processing_complete ( delivery_tag ) from C to H ; update_delivery_state ( delivery_tag ) from H to S ; continue SelectiveMessageDelivery ; } or { basic_cancel ( consumer_tag , nowait ) from C to H ; basic_cancel ( consumer_tag , nowait ) from H to S ; basic_cancel_ok ( consumer_tag ) from S to H ; basic_cancel_ok ( consumer_tag ) from H to C ; } } }

Figure 9. Subset of AMQP using a recursive MC in our extended Scribble.

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

⬇ 1 global protocol Heartbeat ( role Alice , role Carol ){ 2 ping () from Carol to Alice ; 3 pong () from Alice to Carol ; 4 }

⬇ 1 global protocol Request ( role Alice , role Bob ) { 2 request () from Bob to Alice ; 3 response () from Alice to Bob ; 4 }

Appendix

Figure 10. Two simple protocols for an example multi-session program.

⬇ 1 s7 ( internal , { pong }, Data ) -> 2 gen_alice : send_s7_pong ( CarolPid , Data ), 3 _ = gen_alice2 : start_link ( alice2 , []); 4 { stop , normal , Data }. 5 6 7

⬇ 1 s5 ( cast , { BobPid , { request }}, Data ) -> 2 case LocalCond of 3 true -> 4 { next_state , s7 , Data , [{ next_event , internal , { response }}]}; 5 _ -> 6 defer ({ BobPid , { request }}, 50), { keep_state , Data } 7 end .

Appendix

Figure 11. Basic inter-session dependencies internal to a local Erlang program: trigger vs. defer

Panel of Figure 12 — Figure 12. Global semantics: standard rules (top) and new rules for MC (bottom)

Agent Communication Protocols

Agent communication protocols define how AI agents discover one another, exchange messages and state, coordinate tasks, and enforce trust.

See all 47 papers

MPAC: A Multi-Principal Agent Coordination Protocol for Interoperable Multi-Agent Collaboration
Apr 10, 2026Kaiyang Qian, Xinmin Fang, Zhengxiong LiMulti-Agent Coordination Agent Communication Protocols
University of Colorado Denver (CU Denver)
Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
Jul 30, 2026Yang Li, Ping Hou, Nobuko YoshidaLLM-Based Program Synthesis Formal Verification
University of Oxford Computer Science Oxford, United Kingdom
Token Coherence: Adapting MESI Cache Protocols to Minimize Synchronization Overhead in Multi-Agent LLM Systems
Mar 16, 2026Vladyslav ParakhinMulti-Agent LLM Systems Multi-Agent Communication
Independent Researcher

Apr 10, 2026J/K move · Enter open · S save

MPAC: A Multi-Principal Agent Coordination Protocol for Interoperable Multi-Agent Collaboration

Kaiyang Qian, Xinmin Fang, Zhengxiong Li

University of Colorado Denver (CU Denver)

Multi-Agent Coordination Agent Communication Protocols AI Agent Governance Shared-Memory Multi-Agent Systems

Open paper AskPDF arXiv

The AI agent ecosystem has converged on two protocols: the Model Context Protocol (MCP) for tool invocation and Agent-to-Agent (A2A) for single-principal task delegation. Both assume a single controlling principal, meaning one person or organization that owns every agent. When independent principals' agents must coordinate over shared state, such as engineers' coding agents editing the same repository, family members planning a shared trip, or agents from different organizations negotiating a joint decision, neither protocol applies, and coordination collapses to ad-hoc chat, manual merging, or silent overwrites. We present MPAC (Multi-Principal Agent Coordination Protocol), an application-layer protocol that fills this gap with explicit coordination semantics across five layers: Session, Intent, Operation, Conflict, and Governance. MPAC makes intent declaration a precondition for action, represents conflicts as first-class structured objects, and supports human-in-the-loop arbitration through a pluggable governance layer. The specification defines 21 message types, three state machines with normative transition tables, Lamport-clock causal watermarking, two execution models, three security profiles, and optimistic concurrency control on shared state. We release two interoperable reference implementations in Python and TypeScript with 223 tests, a JSON Schema suite, and seven live multi-agent demos. A controlled three-agent code review benchmark shows a 95 percent reduction in coordination overhead and a 4.8 times wall-clock speedup versus a serialized human-mediated baseline, with per-agent decision time preserved. The speedup comes from eliminating coordination waits, not compressing model calls. Specification, implementations, and demos are open source.

Abstract

Agent Communication Protocols

Explore similar work

MPAC: A Multi-Principal Agent Coordination Protocol for Interoperable Multi-Agent Collaboration

Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models

Token Coherence: Adapting MESI Cache Protocols to Minimize Synchronization Overhead in Multi-Agent LLM Systems