Mixed Choice in Asynchronous Multiparty Session Types
Laura Bocchi ( University of Kent )
- 14:00 19th June 2026 ( week 8, Trinity Term 2026 )Bill Roscoe Lecture Theatre (ex LTB)
Multiparty Session Types (MST) provide a principled framework for specifying message-passing protocols and effectively verifying the programs that implement them. Classical MST enforces a form of global consistency where, at every step, participants agree on the current protocol state.
In many realistic distributed systems, however, global state coherence may be temporarily suspended due to timeouts, exceptions, or network delays. Mixed choice, where a participant may both send and receive at a given point, is a natural primitive for modelling such situations: a process sending a timeout while still expecting a reply (e.g., the receive...after pattern in Erlang), or a participant interrupting an ongoing sequence of inputs. These are all moments where a process must act without knowing the exact state of its peers. In asynchronous systems, where messages are not delivered instantaneously, this creates a fundamental difficulty: participants may temporarily hold inconsistent views of the protocol state, and mixed choice amplifies this.
Rather than enforcing step-by-step consistency, we ask what protocol structure is needed to guarantee that any transient inconsistency is eventually resolved. We propose asymmetric mixed choice as a tractable fragment, characterised by three conditions on the protocol structure — commitment, awareness, and an observer role — which together ensure progress and operational correspondence between global protocols and distributed projections. We accompany the theory with a toolchain for generating compliant Erlang/OTP gen_statem processes.