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

#choreography #realizability #synchronizability #communicating-automata #verification #web-services

Backlinks

Linked Pages

Knowledge of Choice

Reference: Montesi, F. Knowledge of Choice. Bliki entry, fabriziomontesi.com (created 2023-05-15, updated 2024-12-17). URL. The notion is developed in book form in Introduction to Choreographies (Montesi 2023, Cambridge University Press) and traces to Castagna, Dezani-Ciancaglini & Padovani (2012) and Carbone, Honda & Yoshida (2012); automated repair procedures are given by Lanese, Guidi, Montesi & Zavattaro (2013), Basu & Bultan (2016), and Cruz-Filipe & Montesi (2020, 2023).

Summary

Knowledge of choice is a well-formedness property of choreographies (and, dually, of multiparty Session Types): whenever a participant makes an internal choice between alternative behaviours, every participant whose subsequent behaviour depends on that choice must be made aware of which branch was taken. The property is what makes Endpoint Projection possible — a global choreography can only be projected to deadlock-free local programs if each role can locally determine which branch of a conditional it should follow.

The problem arises when one participant’s private decision silently changes what other participants are supposed to do, without any communication conveying the decision. Montesi’s running example is third-party single sign-on: an authenticator a decides whether a credential is valid, but the web service ws must respond differently depending on that verdict. If the choreography never has a tell ws the outcome, ws cannot know which action to perform, and implementers are pushed toward fragile workarounds — undocumented side-channel messages not reflected in the protocol, or hidden shared state (a common database, side-effects) that breaks the decentralisation the choreography was meant to guarantee.

The standard fix is to add explicit selections — communications that carry a constant value such as a label (OK/KO) — so that every dependent participant can infer the choice from a message it actually receives. In the repaired example, a sends OK or KO to ws, which can then branch locally. Transforming a choreography that lacks knowledge of choice into an equivalent one that has it is called amendment (or repair), and can be performed automatically; the dual mechanism in the projection direction is the merging operator on local types, which decides when two branches of a receiver are reconcilable.

Key Ideas

Definition. When a choice is made between alternative behaviours, all affected participants must be made aware of the choice — otherwise the choreography is not realisable as independent local programs.
Failure mode. A participant’s internal decision affects others’ behaviour, yet no communication conveys the decision, so dependent roles cannot select their branch.
Bad workarounds. Adding undocumented out-of-band messages, or introducing hidden side-effects / shared databases — both break the decentralised, protocol-as-written semantics.
Selections. Communications carrying constant values (labels) inserted so dependent participants can infer the choice locally.
Amendment / repair. A (mechanisable) transformation that inserts the missing selections to restore knowledge of choice while preserving behaviour.
Merging operator. The dual device in projection: it determines when a receiver’s alternative continuations can be merged, i.e. when a role does not need to be told the choice.
Why it matters. Knowledge of choice is a precondition for sound endpoint projection, deadlock-freedom, and communication safety in both choreographies and multiparty session types.

Connections

Conceptual Contribution

Claim: A global protocol is realisable as independent, deadlock-free local programs only if every participant whose behaviour depends on a choice is informed of that choice; “knowledge of choice” names exactly this realisability condition and separates well-formed choreographies from ones that secretly rely on shared state.
Mechanism: Conditionals in a choreography induce a dependency from the deciding role to every role that branches on the decision; the property is satisfied by inserting selections (label-carrying messages), and a choreography lacking it can be amended automatically. Dually, Endpoint Projection uses a merging operator to admit receivers that need not be told.
Concepts introduced/used: knowledge of choice, selection, amendment, merging, Endpoint Projection, Choreographic Programming, Session Types
Stance: foundational / definitional (choreographic-programming theory)
Relates to: The realisability counterpart of Endpoint Projection in Introduction to Choreographies; the property whose violation the choreographic foundations (Structured Communication-Centred Programming for Web Services, Multiparty Asynchronous Session Types) are built to exclude; structurally adjacent to the distributed-knowledge tradition of Knowledge and Common Knowledge in a Distributed Environment, where what an agent must know to act correctly is the central question.

Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming

Deadlock-freedom-by-design: Multiparty Asynchronous Global Programming

Reference: Carbone, M. & Montesi, F. (2013). Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13), Rome, Italy. ACM. DOI: 10.1145/2480359.2429101. URL · PDF

Summary

Carbone and Montesi present a global programming (choreographic) language for asynchronous multiparty sessions whose defining property is that well-typed programs are deadlock-free by construction — even when they interleave several sessions at once. The starting observation is a gap in the multiparty session-types pipeline established by Multiparty Asynchronous Session Types: that discipline guarantees progress within a single session, but a participant engaged in multiple concurrent sessions can still deadlock, because cyclic wait-for dependencies can form across sessions (A waits on B in session s while B waits on A in session s′). Local, per-session typing cannot see those cross-session cycles. The paper’s move is to lift programming back to the global viewpoint of Structured Communication-Centred Programming for Web Services: one writes a single choreography describing who communicates with whom, in what order, across all the sessions involved, and a mechanical Endpoint Projection derives the local process for each role.

Because a choreography sequences interactions from an Olympian, single-program perspective, it cannot express a global cyclic wait — the global description is intrinsically free of the mismatched send/receive orderings that produce deadlock. The technical contribution is to carry that guarantee through projection: the authors define a choreography calculus over an asynchronous, session-typed process model (with message queues), give a typing discipline for choreographies that use and interleave multiple sessions, and prove an endpoint-projection theorem establishing operational correspondence between a choreography and the parallel composition of its projected endpoints. As a corollary, the distributed endpoint system inherits the choreography’s deadlock-freedom and communication safety — including across interleaved sessions — so deadlock-freedom is obtained by design rather than checked or repaired after the fact. The work is a direct precursor of the choreographic-programming languages that follow (Choral, HasChor, ChoRus) and is consolidated in Introduction to Choreographies.

Key Ideas

Global programming over multiparty sessions: programs are choreographies — global descriptions of the joint interaction of all participants — rather than per-role send/receive code, extending the global-calculus idea of Structured Communication-Centred Programming for Web Services to a full programming language.
Cross-session deadlock is the target: single-session progress (à la Multiparty Asynchronous Session Types) does not imply global deadlock-freedom once a participant interleaves multiple sessions; cyclic dependencies can span sessions where no single session’s type can detect them.
Deadlock-freedom by construction: a choreography cannot express a global cyclic wait, so well-typed global programs are deadlock-free by their very structure — the guarantee is intrinsic, not an external check.
Asynchronous session model: communication is non-blocking with message buffers/queues; the type discipline tracks the resulting ordering obligations across the interleaved sessions.
Endpoint Projection (EPP): a mechanical, type-driven transformation mapping a global program to one local process per role, in a session-typed asynchronous process calculus.
Operational correspondence: the projected endpoint system is proven to match the choreography step-for-step, so the endpoints inherit the choreography’s deadlock-freedom and communication safety — the guarantee survives distribution.

Connections

Conceptual Contribution

Claim: Deadlock-freedom for distributed, multiparty, multi-session programs should be obtained by design — by programming the protocol globally as a choreography and projecting to endpoints — rather than by per-session typing, because local session types guarantee only intra-session progress and cannot see the cyclic wait-for dependencies that form when one participant interleaves several sessions; a global program is structurally incapable of expressing such a cycle, and a sound endpoint projection transports that guarantee to the distributed implementation.
Mechanism: A global programming (choreography) language over an asynchronous, session-typed process model with message queues; a typing discipline for choreographies that open and interleave multiple multiparty sessions; an endpoint-projection function from global programs to per-role local processes; and an endpoint-projection theorem proving operational correspondence between a well-typed choreography and the parallel composition of its projections, from which the endpoint system’s deadlock-freedom and communication safety follow as corollaries.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Session Types, global program, session interleaving, Deadlock Freedom, asynchronous π-calculus, communication safety
Stance: foundational / formal-semantic
Relates to: Sequel in the choreography lineage to Structured Communication-Centred Programming for Web Services (Carbone-Honda-Yoshida ESOP 2007 / TOPLAS 2012) and Multiparty Asynchronous Session Types (Honda-Yoshida-Carbone POPL 2008): where those works establish the global-types / local-types / endpoint-projection triangle and guarantee intra-session progress, this paper closes the cross-session deadlock gap by making global programming itself the deadlock-freedom mechanism. Direct ancestor of the production choreographic languages Choral, HasChor and ChoRus, and of the agentic revival in Pact - A Choreographic Language for Agentic Ecosystems; consolidated pedagogically in Introduction to Choreographies (Montesi 2023). The runtime-verification counterpart for the projected endpoints is On the Monitorability of Session Types (Bartolo Burlò et al. ECOOP 2021). The asynchronous π-calculus / Communicating Sequential Processes substrate underlies the endpoint process model.

Tags

Structured Communication-Centred Programming for Web Services

Reference: Carbone, M., Honda, K. & Yoshida, N. (2007/2012). Conference: European Symposium on Programming (ESOP 2007), LNCS 4421: 2–17. Journal: ACM Transactions on Programming Languages and Systems 34(2): 8:1–8:78, June 2012. DOI: 10.1145/2220365.2220367. Source file: carbone-honda-yoshida-toplas12.pdf. URL

Summary

Carbone, Honda and Yoshida introduce the formal foundation of what is now called Choreographic Programming: a programming paradigm in which one writes a global description of how a set of communicating agents interact — who sends what to whom, in what order, under which choices — and a mechanical endpoint projection derives the local program for each participant. The paper presents two formal calculi side by side: a global calculus whose terms describe interaction patterns from an Olympian, single-program perspective (e.g. A → B : op⟨v⟩.G, “A sends op carrying v to B, then continue with G”), and an end-point calculus — a session-typed asynchronous π-calculus — that describes the same interactions from each participant’s local perspective. The bridge between them is a projection function that, given a well-formed global description, produces a tuple of end-point processes, one per participant. The central technical result is a soundness and completeness correspondence (the Theorem of End-Point Projection): the global calculus and the projected end-point system are bisimilar, and the projection produces deadlock-free, communication-safe processes whenever the source global description satisfies a small set of well-formedness conditions (notably connectedness — every participant of a continuation must have been informed of the choice — and thread linearity).

The paper’s intellectual move is to elevate the interaction itself to the status of programmable artefact, replacing the dominant view in which communication patterns are inferred post hoc from local code. The motivation is the W3C Web Services Choreography Description Language (WS-CDL), but the calculus is independent of that context and has since become the foundation of an entire research line: subsequent work generalises the binary session-type substrate to multiparty (Multiparty Asynchronous Session Types, Honda-Yoshida-Carbone POPL 2008), embeds choreographies in production languages (Choral, HasChor, ChoRus), and extends the framework toward adversarial settings via cryptographic primitives. Every contemporary choreographic-programming paper — including Pact — descends from this work.

Key Ideas

Global calculus: a process calculus whose terms describe interactions from a vantage point above all participants. Primitives include sending (A → B : op⟨v⟩.G), branching (A → B : {labelᵢ : Gᵢ}), parallel composition, recursion, and assignment.
End-point calculus: an asynchronous, session-typed π-calculus describing each participant’s local view; communication occurs over named sessions with structured types.
Endpoint projection (EPP): a syntactic transformation ⟦G⟧_A mapping a global description G and a participant A to an end-point process. Type-driven and compositional.
Theorem of End-Point Projection: for every well-formed global description G, the parallel composition of its end-point projections is operationally equivalent (bisimilar) to G itself, and is deadlock-free and communication-safe.
Connectedness condition: a syntactic well-formedness check ensuring every participant in a continuation has been informed of the branch taken — this is what rules out projections in which one participant chooses a branch the others cannot observe.
Thread linearity: each session channel is owned by exactly one thread, making projection unambiguous.
Session types as the substrate: the global calculus is typed by global types, projected to local types per participant; well-typedness of the source guarantees well-typedness of all projections.
Operational correspondence at the core: global reductions are matched step-for-step by end-point system reductions, and vice versa, modulo τ-transitions for internal sequencing.

Connections

Conceptual Contribution

Claim: Distributed communication should be programmed globally — as a single artefact describing the joint interaction of all participants — rather than locally as per-process send/receive code, because the global view exposes the protocol’s structure to type-checking and admits a sound-and-complete mechanical projection to per-role implementations that are deadlock-free and communication-safe by construction.
Mechanism: Two parallel calculi (a global calculus describing interactions and an end-point asynchronous π-calculus describing local processes); a session-type discipline at both levels with a projection theorem showing global types project to local types role-by-role; a syntactic endpoint projection function ⟦G⟧_A mapping global descriptions to local processes; well-formedness conditions (connectedness, thread linearity) sufficient to guarantee that projection preserves operational behaviour and yields communication safety; the central Theorem of End-Point Projection establishing bisimulation between the global system and its projected end-point composition.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Session Types, global type, local type, π-calculus, well-formedness (connectedness, thread linearity)
Stance: foundational / formal-semantic
Relates to: The taproot of the choreographic-programming literature. Sister paper to Multiparty Asynchronous Session Types (Honda-Yoshida-Carbone POPL 2008), which generalises the binary session-type substrate here to N-party interactions; together the two papers establish the modern global-types / local-types / endpoint-projection triangle. Underwrites the contemporary canonical reference Introduction to Choreographies (Montesi 2023). The runtime-monitoring story for the projected end-points is given by On the Monitorability of Session Types (Bartolo Burlò et al. ECOOP 2021). Structurally the exact analogue of Commitment Machines - Yolum and Singh (Yolum-Singh ATAL-01) and Flexible Protocol Specification and Execution (Yolum-Singh AAMAS-02) in the agent-communication tradition: both pairs (Carbone-Honda-Yoshida ↔ Yolum-Singh) take a globally-specified protocol, define a mechanical projection to per-role behaviour, and prove the projection preserves the relevant correctness property — communication safety on the choreography side, commitment discharge on the commitment-protocol side. Direct ancestor of Pact - A Choreographic Language for Agentic Ecosystems (Gopinathan et al. CP 2026), which adds game-theoretic operators on top of this substrate. The π-calculus dependency goes back to Communicating Sequential Processes (Hoare 1978) for the synchronous-communication root.

Tags

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
Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming — Carbone & Montesi POPL 2013, deadlock-freedom by construction across interleaved sessions
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

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

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

Message Sequence Charts - A Survey

Message Sequence Charts: A Survey

Reference: Genest, B. & Muscholl, A. (2005). Message Sequence Charts: A Survey. In Proc. 5th International Conference on Application of Concurrency to System Design (ACSD 2005), St. Malo, France, pp. 2–4. IEEE Computer Society. DOI 10.1109/ACSD.2005.25. (Invited survey; a fuller treatment appears in Genest, Muscholl & Peled, Message Sequence Charts, LNCS 3098, 2004.) URL.

Summary

This invited survey by Genest and Muscholl maps the theory of Message Sequence Charts (MSCs) and their compositional extension, high-level MSCs (HMSCs / MSC-graphs), from the standpoint of concurrency theory and automata. An MSC gives a partial-order (visual) semantics to one communication scenario among asynchronously communicating processes; an HMSC glues MSCs with choice, concatenation and loops to specify infinite families of scenarios. The survey organises the main results of the field: the formal (partial-order and language) semantics of MSCs, the expressiveness and closure properties of HMSC languages, and — crucially — the tight relationship between HMSC specifications and communicating finite-state machines (channel automata) that implement them.

The recurring theme is that unrestricted MSC/HMSC specifications quickly become intractable, so the theory is built around well-behaved subclasses. The survey reviews bounded (channel-bounded) and existentially-bounded MSC languages — those realizable with finite communication buffers — and the notions of safe / local-choice HMSCs that admit deadlock-free distributed implementations, connecting directly to the realizability programme of Realizability and Verification of MSC Graphs. It surveys the decidability frontier for model-checking MSCs against HMSC specifications and for comparing specifications, noting where problems become undecidable and which structural restrictions restore decidability. As a short roadmap paper it is best read as an entry point and index into the MSC literature rather than as a single technical result.

Key Ideas

MSC semantics: a single scenario as a labelled partial order over send/receive events among asynchronous processes.
HMSC / MSC-graph: MSCs composed by choice, sequential concatenation and iteration to describe (possibly infinite) sets of scenarios.
Communicating automata correspondence: HMSC specifications versus their implementation by communicating finite-state machines with message channels — the central object of the theory.
Bounded and existentially-bounded MSCs: the tractable subclasses realizable with finite buffers; the setting in which most positive (decidability) results live.
Realizability & safe/local-choice HMSCs: the structural conditions under which a specification has a deadlock-free distributed implementation.
Decidability landscape: which model-checking and comparison problems are decidable, and which structural restrictions are needed to recover decidability.
Survey scope: a compact roadmap and bibliographic index into the MSC/HMSC literature.

Connections

Conceptual Contribution

Claim: The MSC/HMSC formalism is best understood through its correspondence with communicating automata and through the tractable subclasses (bounded, existentially-bounded, local-choice) for which realizability and verification are decidable; unrestricted specifications are intractable.
Mechanism: A survey that assembles the partial-order semantics of MSCs, the language theory of HMSCs, the channel-automata implementation model, and the decidability results for the well-behaved subclasses into a single map of the field.
Concepts introduced/used: Message Sequence Charts, HMSC / MSC-graph, Communicating Finite State Machines, bounded / existentially-bounded MSC languages, safe / local-choice HMSCs, Realizability.
Stance: survey / expository
Relates to: The companion technical anchor is Realizability and Verification of MSC Graphs (Alur–Etessami–Yannakakis); the same communicating-automata-vs-global-specification tension is later cast in session-type terms by Multiparty Compatibility in Communicating Automata and in service-choreography terms by Deciding Choreography Realizability.

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

Communicating Finite State Machines

(page does not exist)

Synchronizability

(page does not exist)

Realizability

(page does not exist)