Multiparty Compatibility in Communicating Automata

Reference: Deniélou, P.-M. & Yoshida, N. (2013). Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In Proc. 40th International Colloquium on Automata, Languages and Programming (ICALP 2013), Part II, Riga, Latvia, LNCS 7966, pp. 174–186. Springer. DOI 10.1007/978-3-642-39212-2_18. Companion: Deniélou & Yoshida, Multiparty Session Types Meet Communicating Automata, ESOP 2012. URL.

Summary

This paper builds the bridge between two independently-developed theories of distributed communication: communicating finite-state machines (CFSMs) — Brand and Zafiropulo’s automata that exchange messages over unbounded FIFO channels — and multiparty session types (MPST), in which a single global type specifies a protocol among many participants and is projected to per-role local types. In the binary (two-party) case, safety follows from a simple duality condition between the two endpoints. Deniélou and Yoshida ask what the right generalisation of duality is for N participants, and answer with multiparty compatibility: a semantic condition on a system of CFSMs that guarantees the classic safety and liveness properties — no deadlock, no orphan (never-received) messages, and no unspecified reception — for the asynchronous communicating system.

Their two main results are a characterisation and a synthesis. On the characterisation side, they prove that a system of CFSMs is multiparty-compatible exactly when it is the behavioural image of a well-formed global session type: multiparty compatibility is precisely the property that makes a collection of communicating machines “look like” the projection of some global protocol. On the synthesis side, they give an algorithm that constructs a global session type from a compatible system of CFSMs, recovering the global protocol from its distributed endpoints. Together these results turn the informal correspondence “session types are a well-behaved subclass of communicating automata” into a precise equivalence, and give a route from legacy automata-based endpoint descriptions to type-level global specifications with their safety guarantees.

Key Ideas

CFSMs meet MPST: relates Brand–Zafiropulo communicating finite-state machines (asynchronous, FIFO-channel automata) to multiparty session types and their global/local type structure.
Multiparty compatibility: the N-party generalisation of binary-session duality — a semantic condition on a CFSM system ensuring safety.
Safety & liveness guaranteed: compatible systems enjoy deadlock-freedom, no orphan messages, and no unspecified receptions.
Characterisation: a CFSM system is multiparty-compatible iff it is behaviourally equivalent to the projection of a well-formed global session type.
Synthesis: an algorithm reconstructs a global session type from any multiparty-compatible system of CFSMs.
Bidirectional bridge: projection (global type → local CFSMs) and synthesis (compatible CFSMs → global type) make the correspondence an equivalence, not just an analogy.

Connections

Conceptual Contribution

Claim: Multiparty compatibility is the correct N-party generalisation of session-type duality: a system of communicating automata is safe-by-construction exactly when it is the behavioural projection of a well-formed global session type, and that global type can be mechanically recovered.
Mechanism: Define multiparty compatibility as a semantic condition on CFSM systems; prove it characterises exactly the projections of well-formed global types (safety + liveness); and give a synthesis algorithm that builds the global type from a compatible CFSM system.
Concepts introduced/used: Communicating Finite State Machines, multiparty compatibility, global session type, projection, safety (deadlock-freedom, no orphan messages, no unspecified reception).
Stance: formal / type-theoretic
Relates to: The session-type route to the realizability question studied automata-theoretically in Realizability and Verification of MSC Graphs and for choreographies in Deciding Choreography Realizability; extends the global/local projection discipline of Multiparty Asynchronous Session Types; its “no global types needed” counterpoint is Less is More - Multiparty Session Types Revisited. Direct companion to the authors’ ESOP 2012 Multiparty Session Types Meet Communicating Automata.

Tags

#session-types #communicating-automata #multiparty-session-types #realizability #global-types #foundational

Backlinks

Linked Pages

Less is More - Multiparty Session Types Revisited

Less is More: Multiparty Session Types Revisited

Reference: Scalas, A. & Yoshida, N. (2019). Less is More: Multiparty Session Types Revisited. Proceedings of the ACM on Programming Languages, 3(POPL), Article 30, pp. 1–29. ACM (POPL 2019). DOI: 10.1145/3290343. Artifact: mpstk, the Multiparty Session Types toolKit. Preprint (Imperial MRG) · Technical report DTRS18-6 · Artifact

Summary

Scalas and Yoshida revisit the foundations of multiparty session types (MPST) and argue that the classic theory of Honda–Yoshida–Carbone is built on machinery — a well-formed global type, mechanical projection to local types, and endpoint duality — that is both more restrictive and more fragile than it needs to be. They show that the classic global-types-plus-projection pipeline enjoys only a limited subject reduction property: its type-preservation and safety results hold only under side conditions that are easily overlooked, and several published MPST proofs were in fact flawed because those conditions silently failed. Their thesis is that these restrictions are an artefact of the presentation, not of the underlying discipline.

In place of the three-tier apparatus, the paper develops a generalised MPST theory grounded directly on behavioural properties of typing contexts. A typing context here is just a collection of local session types (one per role/channel); it has its own labelled transition system, and one can ask model-checking-style questions about it directly: is it safe (no role ever offers a message the others cannot receive), deadlock-free, live? The central move is to parameterise type soundness over an abstract safety predicate φ: the authors prove that whenever a typing context satisfies φ, the processes typed against it inherit the corresponding runtime guarantee (subject reduction, communication safety, and — for the stronger predicates — deadlock-freedom and liveness). Crucially, no global type and no duality relation are required: a projected global type becomes merely one convenient way to obtain a safe context, a special case the new theory subsumes rather than depends on. Because these behavioural properties are decidable on finite contexts, the authors implement mpstk, a toolkit that discharges safety, deadlock-freedom and liveness by translating typing contexts into the mCRL2 model checker — turning MPST verification into push-button checking and allowing them to certify correct systems that the classic theory rejects.

“Less is more” names the result: by removing global types and duality — the two heaviest ingredients of classic MPST — the theory becomes at once simpler (fewer definitions, fewer side conditions) and strictly more general (it types more well-behaved systems and repairs the soundness gaps of prior work).

Key Ideas

Behavioural typing contexts as first-class objects: a set of local session types is given an LTS of its own, and correctness is stated as properties of that LTS rather than as conformance to a global type.
Type safety parameterised by a property φ: a single meta-theorem shows that φ-safety of the context implies the matching runtime guarantee for typed processes; safety, deadlock-freedom and liveness are instances of increasing strength.
No global types required: global types are recast as an over-approximation — a sufficient (not necessary) recipe for producing a safe context — so classic MPST is a strict special case.
No duality required: binary endpoint duality, the correctness backbone of two-party session types, is dropped in favour of the behavioural predicates.
Repairs limited subject reduction: the classic projection-based theory only preserves typing under restrictive conditions; the generalised theory removes them and fixes flawed safety proofs in the literature.
Decidability and tooling: for finite typing contexts the properties are decidable; mpstk discharges them via the mCRL2 model checker, giving automated verification.
More typable systems: protocols that are safe but not the projection of any well-formed global type (or that violate the classic side conditions) are now typable and provably correct.

Connections

Conceptual Contribution

Claim: The correctness of multiparty session-typed systems does not require a global type, projection, or endpoint duality; it is fully captured by behavioural properties of the local typing context (safety, deadlock-freedom, liveness). Removing the classic machinery yields a theory that is simultaneously simpler and strictly more general, and repairs soundness flaws (the limited subject reduction of projection-based MPST) present in prior work.
Mechanism: Equip a typing context (a multiset of local session types) with a labelled transition system; define an abstract safety predicate φ over such contexts; prove a parameterised soundness theorem — φ-safety of the context implies subject reduction and the corresponding runtime guarantee for processes typed against it; instantiate φ as safety, deadlock-freedom and liveness. Recover classic MPST by exhibiting projected global types as one family of φ-safe contexts. Implement decision procedures for these properties in mpstk on top of the mCRL2 model checker.
Concepts introduced/used: behavioural typing, typing-context safety property (φ), deadlock-freedom, Liveness, subject reduction, generalised MPST without global types or Duality, model-checking-based verification (mpstk / mCRL2).
Stance: foundational / formal-semantic (with an implemented verification tool).
Relates to: A direct revision of Multiparty Asynchronous Session Types (Honda–Yoshida–Carbone POPL 2008), whose global type → projection → local type pipeline it generalises and whose subject-reduction limitations it diagnoses and fixes; the global-programming line of Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming (Carbone & Montesi) obtains deadlock-freedom by construction from a global program, whereas this paper obtains it by verification of a local context, making the two complementary routes to the same guarantee. Shares its verification-of-local-types outlook with On the Monitorability of Session Types (Bartolo Burlò, Francalanza & Scalas) — same second author lineage on the Scalas side — which synthesises runtime monitors rather than static model checks. Later denotational work Denotational Reasoning for Asynchronous Multiparty Session Types (McDermott & Yoshida) revisits asynchronous MPST from a semantic angle. The underlying process substrate is the asynchronous Pi-Calculus (Milner et al.), and the resource-sensitive reading of session types descends from Linear Logic via the Curry–Howard correspondence for sessions.

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

Deciding Choreography Realizability

Reference: Basu, S., Bultan, T. & Ouederni, M. (2012). Deciding Choreography Realizability. In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), Philadelphia, PA, pp. 191–202. ACM. DOI 10.1145/2103656.2103680. URL.

Summary

A choreography specifies the allowable global orderings of message exchanges among the peers of a distributed system — a single state machine (a “conversation protocol”) describing who sends what to whom, in what order. The realizability question asks whether that global contract can actually be implemented: is there a set of distributed peers that, each acting on purely local information and communicating asynchronously over unbounded FIFO channels, together generate exactly the conversations the choreography prescribes — no missing behaviours and no unintended extra ones? Because the peers are obtained from the choreography by projection, the difficulty is that asynchrony lets them race ahead of the global order and produce conversations the choreography never intended.

The paper’s headline result is that, contrary to the prior expectation that unbounded-asynchronous realizability is undecidable, choreography realizability is decidable. The key device is synchronizability: a system of communicating peers is synchronizable when its observable conversation set is the same regardless of channel-buffer size — its behaviour under synchronous (rendez-vous) communication coincides with its behaviour under asynchronous buffering. Synchronizability can be checked by comparing the peers’ synchronous semantics with their 1-bounded asynchronous semantics, a finite check. Realizability is then decided by (i) projecting the choreography to peers, (ii) verifying that the projected system is synchronizable, and (iii) checking that the synchronous behaviour of those peers is language-equivalent to the choreography. When all hold, the finite (synchronous) analysis certifies the behaviour of the full unbounded-asynchronous system, so the otherwise infinite-state realizability question collapses to decidable equivalence checks.

Key Ideas

Choreography as a global contract: a state machine over the send events of all peers, fixing the allowable global message orderings.
Realizability: existence of distributed, locally-driven peers whose asynchronous FIFO interaction reproduces exactly the choreography’s conversation set.
Decidability result: realizability is decidable — even under unbounded asynchronous communication — refuting the assumption that it is not.
Synchronizability: behaviour is invariant to buffer size (synchronous ≡ asynchronous conversation sets); it is the hinge that makes the infinite-state problem finite.
Finite decision procedure: check synchronizability by comparing synchronous and 1-bounded asynchronous behaviour, then compare the synchronous behaviour to the choreography.
Projection + equivalence: project the global spec to peers and reduce realizability to language-equivalence checks over finite (bounded) system semantics.

Connections

Conceptual Contribution

Claim: Whether a global choreography can be faithfully implemented by asynchronously communicating peers is a decidable question, despite unbounded message buffers, provided the projected system is synchronizable.
Mechanism: Project the choreography to peer machines; decide synchronizability by comparing synchronous and 1-bounded asynchronous semantics; then check language-equivalence between the peers’ synchronous behaviour and the choreography — reducing an infinite-state problem to finite equivalence checks.
Concepts introduced/used: choreography / conversation protocol, Realizability, Synchronizability, Endpoint Projection, Communicating Finite State Machines.
Stance: formal / algorithmic (verification)
Relates to: The service-choreography counterpart of the MSC realizability programme in Realizability and Verification of MSC Graphs and Message Sequence Charts - A Survey; complementary to the session-type route to the same question in Multiparty Compatibility in Communicating Automata; the projection machinery is the Endpoint Projection used across Choreographic Programming (Structured Communication-Centred Programming for Web Services, Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming), and the unrealizability pathologies it rules out are those Knowledge of Choice targets.

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

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

Global Types

(page does not exist)

Communicating Finite State Machines

(page does not exist)

Realizability

(page does not exist)

Global Session Types

(page does not exist)

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

Multiparty Session Types

(page does not exist)