Paper deep dive
Provable Coordination for LLM Agents via Message Sequence Charts
Benedikt Bollig, Matthias Függer, Thomas Nowak
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 97%
Last extracted: 4/27/2026, 8:35:20 AM
Summary
The paper introduces a domain-specific language (DSL) and a framework called ZipperGen for specifying and generating provably correct coordination protocols for multi-agent systems built on Large Language Models (LLMs). The approach uses Message Sequence Charts (MSCs) to separate the deterministic message-passing structure from the stochastic LLM actions. By using 'owned control flow' (where a specific agent decides the branch of a conditional or loop) and 'action blocks' (treating LLM calls as opaque functions), the framework allows for a syntax-directed projection from a global workflow to local, deadlock-free agent programs. This ensures that coordination properties like deadlock-freedom are maintained even when workflows are dynamically generated by a planning LLM at runtime.
Entities (12)
Relation Signals (8)
Domain-Specific Language → basedon → Message Sequence Charts
confidence 100% · We introduce a domain-specific language for specifying agent coordination based on message sequence charts (MSCs).
ZipperGen → implements → Message Sequence Charts
confidence 100% · An open-source Python implementation of our framework is available as ZipperGen.
ZipperGen → implements → Domain-Specific Language
confidence 100% · An open-source Python implementation of our framework is available as ZipperGen.
Message Sequence Charts → isextendedby → Owned Control Flow
confidence 100% · We extend standard MSCs with two constructs: action blocks... and owned control flow
LangGraph → isrelatedto → LLM Agents
confidence 100% · Frameworks like LangGraph [17], AutoGen [25], and CrewAI [5] provide convenient infrastructure for building such systems.
ZipperGen → providescoordinationfor → LLM Agents
confidence 100% · An open-source Python implementation of our framework is available as ZipperGen.
Domain-Specific Language → guarantees → Deadlock-freedom
confidence 90% · Deadlock-freedom is then guaranteed by the projection.
Owned Control Flow → guarantees → Deadlock-freedom
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Multi-agent systems built on large language models (LLMs) are difficult to reason about. Coordination errors such as deadlocks or type-mismatched messages are often hard to detect through testing. We introduce a domain-specific language for specifying agent coordination based on message sequence charts (MSCs). The language separates message-passing structure from LLM actions, whose outputs remain unpredictable. We define the syntax and semantics of the language and present a syntax-directed projection that generates deadlock-free local agent programs from global coordination specifications. We illustrate the approach with a diagnosis consensus protocol and show how coordination properties can be established independently of LLM nondeterminism. We also describe a runtime planning extension in which an LLM dynamically generates a coordination workflow for which the same structural guarantees apply. An open-source Python implementation of our framework is available as ZipperGen.
Tags
Links
- Source: https://arxiv.org/abs/2604.17612v1
- Canonical: https://arxiv.org/abs/2604.17612v1
Trouble viewing inline? Open PDF directly →
Full Text
137,442 characters extracted from source content.
Expand or collapse full text
11institutetext: Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, France 22institutetext: Institut Universitaire de France, Paris, France Provable Coordination for LLM Agents via Message Sequence Charts Benedikt Bollig Matthias Függer Thomas Nowak Abstract Multi-agent systems built on large language models (LLMs) are difficult to reason about. Coordination errors such as deadlocks or type-mismatched messages are often hard to detect through testing. We introduce a domain-specific language for specifying agent coordination based on message sequence charts (MSCs). The language separates message-passing structure from LLM actions, whose outputs remain unpredictable. We define the syntax and semantics of the language and present a syntax-directed projection that generates deadlock-free local agent programs from global coordination specifications. We illustrate the approach with a diagnosis consensus protocol and show how coordination properties can be established independently of LLM nondeterminism. We also describe a runtime planning extension in which an LLM dynamically generates a coordination workflow for which the same structural guarantees apply. An open-source Python implementation of our framework is available as ZipperGen. 1 Introduction Multi-agent systems built on large language models (LLMs) are increasingly common. They combine the capabilities of individual AI components with the structural advantages of distributed systems, such as concurrency, separation of concerns, and explicit communication patterns. A typical example is a group of LLM agents that iteratively exchange assessments until they reach agreement on a task, such as giving a medical diagnosis. These systems are, however, hard to design and to reason about. While classical distributed systems are already notoriously error prone, the stochastic nature of LLM outputs further complicates reasoning about such systems. When agents exchange messages and collaborate, problems such as deadlocks or lost messages are difficult to rule out through testing alone. Frameworks like LangGraph [17], AutoGen [25], and CrewAI [5] provide convenient infrastructure for building such systems, but offer no formal guarantees. The broader engineering challenges of such systems, such as transparency, traceability, and error attribution, are well-documented [7]. Applying formal methods to this setting is therefore natural. Contributions. For this purpose, we propose a domain-specific language (DSL) for agent coordination based on message sequence charts (MSCs) [16], an International Telecommunication Union (ITU) standard for communication protocols. MSCs combine a visual notation with a formal semantics. They represent both the local progress of individual agents (their lifelines) and the messages exchanged between them, making causal dependencies in a system execution easy to track. Abstractly, an MSC describes a single execution. Higher-level formalisms compose simple MSCs into sets (or languages). They can be thought of as global workflows: specifications of what a distributed system should do, independently of how it is implemented. Much research has addressed the question of how such global specifications can be realized in a distributed fashion. The conceptually cleanest approach is projection: deriving a local program for each participant by restricting the global specification to that participant’s view. This has been pursued both for MSC-based formalisms [1, 10, 3] and for multiparty session types (MPST) [15, 18]. These works follow an automata-theoretic route: a realizability condition is checked, local machines are constructed, and correctness is established by language equivalence. Our approach works with structured programs rather than automata and targets LLM components directly. Workflow-level specifications suit LLM agents well: rather than following a finite transition graph, agents maintain variable-length context, evaluate local conditions, and branch based on their own state. Moreover, the projected local programs are programs again: they can be embedded in larger workflows, exposed as APIs, or composed with other components without further translation. Existing LLM-based multi-agent frameworks do not address the synthesis of provably correct distributed agent programs. The same holds when the coordination structure is not fixed in advance but generated at runtime by a planning LLM. Asking such a system to produce deadlock-free distributed code directly is unreasonable: it would have to ensure that every send by one agent is matched by a receive of another, in every branch and under every execution order. With our language, the planner needs only to produce a syntactically valid global workflow. Deadlock-freedom is then guaranteed by the projection. The language is therefore not only a programming interface for humans, but also a natural target for LLM-based planning. We extend standard MSCs with two constructs: action blocks, which treat LLM computations as opaque typed functions, and owned control flow, where each conditional and loop has an explicit decider. The first extension separates what can be guaranteed statically (the message-passing structure, which has a precise operational semantics) from what cannot: the stochastic outputs of LLM calls. The second makes projection syntax-directed: it is a structural recursion on the global workflow, and the correctness proof is a structural induction. No automaton is constructed at any point. Related work. Our work connects two lines of research. The first is the formal side: realizability for MSCs and communicating automata [1, 9, 10, 3, 21, 20, 19, 24, 11] addresses the question of whether a global specification admits a deadlock-free distributed implementation. Rather than solving this problem post-hoc, we follow a by-construction approach: the global language is designed so that projection is always syntax-directed and yields well-structured local programs directly. Closest to our approach is [9], which also inserts control messages automatically to synthesize local controllers, but works with automaton-based global specifications and is not designed for LLM-based agents. Multiparty session types (MPSTs) [14, 15, 18, 6, 4, 8] also project a global description to local views, but require well-formedness conditions for projection to be defined, notably that uninvolved participants have consistent local behaviors across branches. Scribble [26] is a prominent practical MPST-based protocol language, and its refinement-typed extension [27] further adds data-level verification, an orthogonal direction we do not pursue. In contrast, our language is designed so that projection is always defined for its constructs: owned control flow together with explicit control broadcasts eliminates the need for such consistency conditions (often formulated as branch-mergeability [8]) in standard MPST settings. Process calculi [13, 22] work in the opposite direction: local processes are composed to obtain global behavior, rather than projected from a global specification. The second line concerns practical multi-agent frameworks such as LangGraph, AutoGen, and CrewAI [17, 25, 5]. These treat coordination as an engineering concern, relying on testing and runtime monitoring for correctness. We separate the coordination layer from the LLM layer and reason about the former independently; in particular, deadlock-freedom holds even for runtime-generated workflows, which to our knowledge no existing framework guarantees. Outline. Section 2 presents introductory examples. Sections 3–4 define the syntax and semantics of global and local programs. Section 5 presents the projection, proves correctness and deadlock-freedom, and describes the ZipperGen implementation (https://zippergen.io). Section 6 illustrates the framework. Section 7 concludes. Proofs are deferred to the appendix. 2 Introductory Examples We illustrate our language on a simple multi-agent workflow. Listing 1: Review workflow (lifeline and most variable declarations omitted). ⬇ 1workflow reviewed_execution(task: str @ Planner) -> str 2 var critique: str = "no review" @ Orchestrator 3 act Planner : (plan, plan_needs_review) = make_plan(task) 4 5 if plan_needs_review@Planner then 6 msg Planner(plan) -> Reviewer(plan) 7 act Reviewer : critique = review_plan(plan) 8 msg Reviewer(critique) -> Orchestrator(critique) 9 else 10 act Planner : review_skipped = record_no_review(plan) 11 12 13 msg Planner(plan) -> Executor(plan) 14 act Executor : result = execute_plan(plan) 15 msg Executor(result) -> Orchestrator(result) 16 act Orchestrator : summary = finalize(critique, result) 17 return summary @ Orchestrator 18 The program in Listing 1 specifies a review-before-action workflow with four lifelines: Planner, Reviewer, Executor, and ℎOrchestrator. Planner receives a task, produces a plan, and decides whether it needs review. In the first scenario (__plan\_needs\_review is true), Planner sends the plan to Reviewer, who critiques it and forwards the critique to Orchestrator. In the second scenario, the review is skipped. In both cases, Planner forwards the plan to Executor, whose result is sent to Orchestrator, which finalizes the outcome. Figure 1 gives a graphical view of the workflow, abstracting away variable declarations and types. The dashed box separates the two branches of the conditional; the figure thus represents two MSCs, one per scenario. Action blocks such as :(,__)=_() act\ Planner:(plan,plan\_needs\_review)=make\_plan(task) model opaque AI computations. The conditional __@ if\ plan\_needs\_review@Planner has an owned decider: only Planner chooses the branch, and Reviewer participates only in the true branch. The last action depends on both critique and result. Thus, computations remain opaque, but the coordination around them is made explicit. The return statement designates the output lifeline; it is not part of the MSC but specifies which lifeline’s value is returned to the caller. Note that the critique is sent to ℎOrchestrator rather than back to Planner: the review influences the final outcome but does not block execution. PlannerReviewerOrchestr.Executormake_plan[plan_needs_review]planreview_plancritique[else]no reviewplanexecute_planresultfinalize Figure 1: MSC for reviewed_execution. Filled dots are local actions (opaque computations), arrows are messages labelled by the value sent. Planner owns the conditional. The true branch involves Reviewer; in the false branch, Planner records that review was skipped. After the conditional, Planner forwards the plan to Executor, whose result is finalized by Orchestrator. The program above is written from a global viewpoint: it describes the full coordination of all lifelines in a single text. In practice, each agent runs its own local program and communicates with the others exclusively by sending and receiving messages over first-in first-out (FIFO) channels. FIFO channels allow agents to overlap their work. A sender can deposit a message and continue immediately, and the receiver picks it up whenever its local execution reaches the corresponding receive. This allows agents that do not depend on each other to proceed in parallel. One obvious implementation strategy is simple polling: each agent repeatedly checks its incoming channels and processes the first available message. But this is not sufficient even for programs satisfying the local property of [10] or the local-choice property of [2, 12]. Consider the true branch of reviewed_execution. Once Planner has sent the plan to Reviewer, its participation in the if-block is complete, and it immediately sends the plan to Executor. As a result, Reviewer and Executor run concurrently and both send their outputs to ℎOrchestrator. Because the channels are asynchronous, Executor may finish and deliver result to ℎOrchestrator before Reviewer has even dequeued the plan. This prefix execution is reachable under polling, yet it cannot be extended to a valid completion: ℎOrchestrator dequeues result before critique arrives. Our projection overcomes this by having Planner broadcast an explicit control message that tells ℎOrchestrator which branch was taken. ℎOrchestrator’s local program then enforces the correct receive order (cf. Section 5). In fact, such control messages are necessary in general. Consider the program below, where A repeatedly tosses a coin and B performs a local step in each iteration: ℎ@AA:ℎ=();B:b=()ε while\ heads @A\ do\ \\, act\ A:heads=toss()\ ;\ act\ B:b=step()\\ \,\\ exit\ \\, \,\ A and B must execute the same number of iterations, yet the iteration count is determined solely by A’s coin tosses, which are private to A. There is no user message that B could observe to recover it. Any correct distributed implementation must therefore send B an explicit control signal at each iteration, exactly as our projection does. Most work on MSC realizability, e.g., [1, 21, 19, 10, 20, 24], formulates the question as a decision problem (given a global specification, does a deadlock-free distributed implementation exist?) or identifies sufficient syntactic criteria for it. In practice, one wants simply to write a program and have it run. The constraint is even less realistic when workflows are generated at runtime by a planning LLM, which cannot be expected to produce only specifications satisfying a non-trivial syntactic condition. Our language is designed with this in mind. 3 Global Workflows A global workflow describes the full coordination structure of a multi-agent system in a single, centralized specification. Rather than programming each agent separately, the developer writes one workflow that captures which agents communicate, in what order, and who owns each control decision. This section defines the formal syntax and semantics of such global workflows. 3.1 Syntax Throughout this section, fix a finite set ℒ L of lifelines and a set ℱ F of action symbols. We use A,B∈ℒA,B∈ L for lifelines, f∈ℱf∈ F for local computations such as LLM calls or deterministic helper functions, x→,y→ x, y for payload tuples, and c for Boolean conditions involving Boolean variables of designated lifelines. Communication proceeds over directed unbounded FIFO channels: for every ordered pair (A,B)(A,B) of distinct lifelines there is one channel A→BA→ B. Definition 1(Abstract syntax) The set Work of global workflows is generated by the following grammar: P::= P~::=~ ε∣A(x→)→B(y→)∣A:y→=f(x→)∣P1;P2∣ ~ ~ msg\ A( x)→ B( y)~ ~ act\ A: y=f( x)~ ~P_1;P_2~ ~ c@BP⊤P⊥∣c@BPP if\ c@B\ then\ P_ \ else\ P_ ~ ~ while\ c@B\ do\ P_body\ exit\ P_exit For message statements, we require distinct endpoints: in A(x→)→B(y→) msg\ A( x)→ B( y) we assume A≠BA≠ B (no self channels). Payload components in x→=(x1,…,xm) x=(x_1,…,x_m) and y→=(y1,…,yn) y=(y_1,…,y_n) may be variables or concrete values, such as the truth values ⊤ (true) and ⊥ (false). In action statements A:y→=f(x→) act\ A: y=f( x), the outputs y→ y must be variables (assignment targets), while the inputs x→ x may be variables or constants. Each lifeline maintains its own local variable store. Variable names are scoped per lifeline, so distinct lifelines may use the same name independently. We emphasize that the grammar contains no return statement. A return is not a coordination step: it does not send a message, perform a computation, or affect any other lifeline. It names the lifeline that produces the final value and the variable holding it. We therefore treat it as a declaration outside the formal language and it plays no role in the projection or the correctness proofs. In the ZipperGen implementation, return var @ A serves as this declaration and is checked syntactically. The statements have the following intuitive meaning (Listing 1 illustrates all of them except the while construct): • A(x→)→B(y→) msg\ A( x)→ B( y): a communication step in which A sends a payload tuple and B receives it, possibly binding components to local variables. • A:y→=f(x→) act\ A: y=f( x): a local computation performed by lifeline A; in Listing 1, examples are _make\_plan, _review\_plan, and finalize. • c@BP⊤P⊥ if\ c@B\ then\ P_ \ else\ P_ : a conditional whose branch is chosen exclusively by lifeline B. The annotation @B@B records this ownership explicitly, even though the branch programs P⊤P_ and P⊥P_ may themselves involve several lifelines. • c@BPP while\ c@B\ do\ P_body\ exit\ P_exit: an owned loop in which B decides whether another iteration of P_body is executed or whether control exits through P_exit. Again, the body and exit programs may involve multiple lifelines. 3.2 Semantics The semantics assigns to each global workflow a set of MSCs, each describing one possible global execution. Figure 1 gives the intended intuition, but it should be read as depicting two MSCs, one for each branch of the conditional shown by the dashed case distinction. In general, an execution is represented by one vertical word per lifeline, together with FIFO-matching edges between sends and receives on each channel. Local actions appear as internal events on a single lifeline, while owned conditionals and loops contribute explicit choice events recording which branch or loop outcome was selected. We now make this precise by defining MSCs as tuples of local words. Definition 2(Local Alphabets) For each lifeline A∈ℒA∈ L, the (infinite) local-word alphabet ΣA _A contains: • send letters A(x→)→B send\ A( x)→ B and receive letters A(y→)←B recv\ A( y)← B, where x→ x and y→ y range over tuples of constants and variables, • local action letters A:y→=f(x→) act\ A: y=f( x), where x→ x ranges over tuples of constants and variables and y→ y over tuples of variables, • choice letters ⊤(c@A),⊥(c@A),⊤(c@A),⊥(c@A) if_ (c@A), if_ (c@A), while_ (c@A), while_ (c@A) for condition c. We let ΣA∗ _A^* denote the set of finite words over ΣA _A, which includes the empty word ε . We use u⋅vu· v or uvuv for the concatenation of words u and v. Though an MSC will be defined as a tuple of local words, one must also specify which send events are matched with which receive events across each channel. Since our execution model uses FIFO channels, this matching is determined canonically by pairing the first send on a channel with the first receive on that channel, the second send with the second receive, and so on. The next definition extracts this channel-wise FIFO matching from a tuple of local words. Definition 3(Tuple FIFO Relations) Fix a tuple of local words M=(wA)A∈ℒM=(w_A)_A∈ L with wA∈ΣA∗w_A∈ _A^* for each A∈ℒA∈ L. We write |wA||w_A| for the length of wAw_A and wA[j]w_A[j] for its jjth symbol (starting at index 1). The event set of M is EM=(A,i)∣A∈ℒ, 1≤i≤|wA|.E_M=\(A,i) A∈ L,\ 1≤ i≤|w_A|\. For each channel A→BA→ B, define the send-event sequence A→B(M)=(s1,…,sm) snd_A→ B(M)=(s_1,…,s_m) where (si)i(s_i)_i are exactly the events (A,j)∈EM(A,j)∈ E_M such that wA[j]w_A[j] is of the form A(⋅)→B send\ A(·)→ B, listed in increasing local index j. Define analogously the receive-event sequence B←A(M)=(r1,…,rn) rcv_B← A(M)=(r_1,…,r_n) where (ri)i(r_i)_i are exactly the events (B,j)∈EM(B,j)∈ E_M such that wB[j]w_B[j] is of the form B(⋅)←A recv\ B(·)← A, again listed in increasing local index. The FIFO relation ⊲M⊆EM×EM _M E_M× E_M contains, for each channel A→BA→ B, the pairs (si,ri)(s_i,r_i) for all 1≤i≤minm,n1≤ i≤ \m,n\. Definition 4(Payload Matching) Let x→ x be a sender payload tuple and let y→ y be a receiver payload tuple, whose components may be variables or constants. We write (x→,y→) match( x, y) if the following hold: (1) |x→|=|y→|| x|=| y|; (2) for each index i: if yiy_i is a constant, then xix_i is the same constant; if yiy_i is a variable of type τ, then xix_i is either a constant of type τ or a variable of type τ. Applied to a source-level A(x→)→B(y→) msg\ A( x)→ B( y), this condition is checked statically as part of well-typedness (see Definition 5 below). When yiy_i is a constant, the distributed implementation can additionally verify at runtime that the received value equals that constant, raising an error if not (a lightweight consistency check requiring no extra specification). The same conditions also describe runtime payload agreement for the control-tag payloads introduced later by the projection. Payload matching isolates the only place where sender and receiver payloads are allowed to differ syntactically: receivers may bind variables or require distinguished constants. The raw workflow grammar itself does not enforce that messages match in this sense, nor that actions and guards are locally consistent. We therefore restrict attention to a well-typed fragment. Definition 5(Well-Typed Global Workflows) A global workflow P is well typed if all the following conditions hold: (1) every message subprogram A(x→)→B(y→) msg\ A( x)→ B( y) satisfies (x→,y→) match( x, y); (2) every action subprogram A:y→=f(x→) act\ A: y=f( x) is locally type-correct, i.e., the invocation f(x→)f( x) is assumed to produce values compatible with the variables y→ y; (3) every control condition c@Bc@B occurring in an if or while statement is well typed for lifeline B, i.e., c is a Boolean expression over variables available at B. Throughout the remainder of the paper, we consider only well-typed global workflows. In fact, only item (1) is needed to ensure that the inductive MSC semantics below is well defined. Items (2)–(3) record additional static consistency conditions expected of executable programs, but are not used explicitly in the semantic constructions below. We can now say which tuples of local words actually represent executions. Intuitively, a valid MSC must have every receive matched by a send, matched events must agree on their payloads, and the causal dependencies induced by local order and communication must not form cycles. Definition 6(MSC) An MSC is a tuple of local words M=(wA)A∈ℒM=(w_A)_A∈ L with wA∈ΣA∗w_A∈ _A^* such that: (1) every receive event in wAw_A is matched in ⊲M _M; (2) whenever a send event with payload tuple x→ x is matched to a receive event with payload tuple y→ y, they satisfy (x→,y→) match( x, y) (in particular, receiver constants are matched by value equality); (3) the transitive closure of the binary relation ⊲M∪((A,i),(A,i+1))∣A∈ℒ,i∈1,…,|wA|−1 _M∪\((A,i),(A,i+1)) A∈ L,\,i∈\1,…,|w_A|-1\\ is a strict partial order (i.e., acyclic). We call M complete if every send event is matched in ⊲M _M. To compose executions sequentially, we use componentwise concatenation: M1∘M2=(uAvA)A∈ℒM_1 M_2=(u_Av_A)_A∈ L for M1=(uA)A,M2=(vA)AM_1=(u_A)_A,\ M_2=(v_A)_A. The concatenation of two MSCs is not necessarily an MSC. However, we have the following closure facts: Lemma 1(Concatenation with a Complete Prefix) Let M1M_1 be a complete MSC and M2M_2 be an MSC. Then M1∘M2M_1 M_2 is an MSC. If moreover M2M_2 is complete, then M1∘M2M_1 M_2 is complete. Lemma 2(Stripping a Complete Prefix) Conversely, let C=(uA)AC=(u_A)_A be a complete MSC and let N=(vA)AN=(v_A)_A be a tuple of local words. If C∘N=(uAvA)AC N=(u_Av_A)_A is an MSC, then N is an MSC. If C∘NC N is a complete MSC, then N is a complete MSC. With these ingredients in place, the semantics can be defined compositionally. The base cases are canonical one-step MSCs for the atomic workflow constructs. Sequential composition uses concatenation of MSCs, and owned conditionals and loops contribute explicit choice events on the deciding lifeline. Definition 7(Canonical MSCs) Fix A,B∈ℒA,B∈ L, tuples x→,y→ x, y, action f∈ℱf∈ F, and choice letter γ∈⊤(c@B),⊥(c@B),⊤(c@B),⊥(c@B)γ∈\ if_ (c@B), if_ (c@B), while_ (c@B), while_ (c@B)\ for some condition c. We define the following canonical MSCs: • MεM_ is the MSC with no events on any lifeline; • MγB=(wX)X∈ℒM_γ^B=(w_X)_X∈ L, where wB=γw_B=γ and wX=ε(X≠B)w_X= ~(X≠ B); • Mx→,y→A,f=(wX)X∈ℒM_ x, y^A,f=(w_X)_X∈ L, where wA=A:y→=f(x→)w_A= act\ A: y=f( x) and wX=ε(X≠A)w_X= ~(X≠ A); • Mx→,y→A→B=(wX)X∈ℒM_ x, y^A→ B=(w_X)_X∈ L, where wA=A(x→)→Bw_A= send\ A( x)→ B, wB=B(y→)←Aw_B= recv\ B( y)← A, and wX=ε(X∉A,B)w_X= ~(X∉\A,B\). MεM_ AABBMγBM_γ^BAABBγ →,y→A,fM_ x, y^A,fAABBf(x→)/y→f( x)/ yMx→,y→A→BM_ x, y^A→ BAABBx→,y→ x, y Figure 2: Canonical one-step MSCs used in Definition 7. The schematic figure shows the empty MSC, a local choice event, a local action event, and a single message exchange. Definition 8(Inductive MSC Semantics) The semantics ⟦P⟧ P of a well-typed global workflow P is a set of MSCs. It is defined by structural recursion with the rules given in Table 1. Table 1: Inductive MSC semantics of global workflows. ⟦ε⟧=Mε⟦A(x→)→B(y→)⟧=Mx→,y→A→B⟦A:y→=f(x→)⟧=Mx→,y→A,f⟦P1;P2⟧=M1∘M2∣M1∈⟦P1⟧,M2∈⟦P2⟧⟦c@BP⊤P⊥⟧=M⊤(c@B)B∘M∣M∈⟦P⊤⟧∪M⊥(c@B)B∘M∣M∈⟦P⊥⟧⟦c@BPP⟧=⋃k≥0M1⊤∘⋯∘Mk⊤∘M⊥∣M1,…,Mk∈⟦P⟧,M∈⟦P⟧ array[]rcl &=&\M_ \\\[3.00003pt] msg\ A( x)→ B( y) &=&\M_ x, y^A→ B\\\[3.00003pt] act\ A: y=f( x) &=&\M_ x, y^A,f\\\[3.00003pt] P_1;P_2 &=&\M_1 M_2 M_1∈ P_1 ,\ M_2∈ P_2 \\\[3.00003pt] if\ c@B\ then\ P_ \ else\ P_ &=& array[t]@l@\M_ if_ (c@B)^B M M∈ P_ \\\ ∪\,\M_ if_ (c@B)^B M M∈ P_ \ array\\[15.00002pt] while\ c@B\ do\ P_body\ exit\ P_exit &=& _k≥ 0 \ array[]@l@M_1 ·s M_k M_exit \ \\[1.99997pt] M_1,…,M_k∈ P_body ,\\ M_exit∈ P_exit array \ array where Mi⊤=M⊤(c@B)B∘MiM_i =M_ while_ (c@B)^B M_i and M⊥=M⊥(c@B)B∘M_exit =M_ while_ (c@B)^B M_exit. One observes that for every well-typed global workflow P and every M∈⟦P⟧M∈ P , the MSC M is complete. This follows by structural induction on P from the semantic clauses. 4 Distributed Agent Programs A distributed agent program assigns one local program to each lifeline. The local program at A∈ℒA∈ L describes the steps visible at A: sends and receives on A’s channels, local actions, and control steps arising from branching decisions that A either owns or observes via a received control signal. Definition 9(Local Syntax) For each lifeline A∈ℒA∈ L, let A LocProg_A be the set of local programs at A, generated by the grammar S::= S::= ε∣A(x→)→B∣A(y→)←B∣A:y→=f(x→)∣S1;S2∣ send\ A( x)→ B recv\ A( y)← B act\ A: y=f( x) S_1;S_2 c@AS⊤S⊥∣A(y→)←BS⊤S⊥∣ if\ c@A\ then\ S_ \ else\ S_ if\ A( y)← B\ then\ S_ \ else\ S_ c@ASS∣A(y→)←BSS while\ c@A\ do\ S_body\ exit\ S_exit while\ A( y)← B\ do\ S_body\ exit\ S_exit where c ranges over source guards. Here, each occurrence of B ranges over lifelines in ℒ∖A L \A\. In A(x→)→B send\ A( x)→ B and A(y→)←B recv\ A( y)← B, x→ x and y→ y range over tuples of constants and variables. In action statements, y→ y must be variables (assignment targets). For constructs /A(y→)←B if/ while\ A( y)← B, y→ y is a non-empty tuple of constants and variables whose first component y1y_1 is a Boolean variable. Definition 10(Distributed Programs) A distributed program is a tuple =(SA)A∈ℒD=(S_A)_A∈ L with SA∈AS_A∈ LocProg_A for each A. The message and action constructs are the local counterparts of the corresponding workflow constructs, as are the owner-side conditional control-flow constructs c@A if\ c@A and c@A while\ c@A: they still represent source-level local control owned by A. The receive-guarded forms /A(y→)←B if/ while\ A( y)← B are different: they do not evaluate a guard locally, but instead react to a control decision that has already been made by B and communicated explicitly. The semantics of a local program is a language of local traces, one word over the alphabet ΣA _A from Definition 2 for each possible execution of lifeline A. The semantics of a distributed program then contains the tuples of such local traces that together form an MSC. In this way, the distributed semantics reuses the MSC notion from Section 3, but starts from already projected local behavior rather than from a global workflow directly. For S∈AS∈ LocProg_A, we define ⟨S⟩⊆ΣA∗ -1.99997pt S -1.99997pt _A^*, the set of local traces of S, by induction. The receive-guarded control constructs /A(y→)←B if/ while\ A( y)← B consume control-tagged messages from B and branch on the first component (⊤ or ⊥ ). The formal definition is given in Table 2; there, we write y→[ν/y1] y[ν/y_1] for the tuple obtained by replacing y1y_1 by ν. To reason about partial executions and to formalize deadlock-freeness, we order local words and MSC tuples by the componentwise prefix relation. For words u,u′∈ΣA∗u,u ∈ _A^*, write u⪯u′u u if there is v∈ΣA∗v∈ _A^* such that u′=uvu =uv. We write u≺u′u u if u⪯u′u u and u≠u′u≠ u . Table 2: Local trace semantics for ⟨S⟩ -1.99997pt S -1.99997pt . ⟨ε⟩=ε⟨A(x→)→B⟩=A(x→)→B⟨A(y→)←B⟩=A(y→)←B⟨A:y→=f(x→)⟩=A:y→=f(x→)⟨S1;S2⟩=u1u2∣u1∈⟨S1⟩,u2∈⟨S2⟩⟨c@AS⊤S⊥⟩=(⊤(c@A)⋅u∣u∈⟨S⊤⟩∪⊥(c@A)⋅u∣u∈⟨S⊥⟩)⟨A(y→)←BS⊤S⊥⟩=(A(y→[⊤/y1])←B⋅u∣u∈⟨S⊤⟩∪A(y→[⊥/y1])←B⋅u∣u∈⟨S⊥⟩) array[]rcl -1.99997pt -1.99997pt &=&\ \\\ -1.99997pt send\ A( x)→ B -1.99997pt &=&\ send\ A( x)→ B\\\ -1.99997pt recv\ A( y)← B -1.99997pt &=&\ recv\ A( y)← B\\\ -1.99997pt act\ A: y=f( x) -1.99997pt &=&\ act\ A: y=f( x)\\\ -1.99997pt S_1;S_2 -1.99997pt &=&\u_1u_2 u_1∈ -1.99997pt S_1 -1.99997pt ,\ u_2∈ -1.99997pt S_2 -1.99997pt \\\[3.00003pt] -1.99997pt if\ c@A\ then\ S_ \ else\ S_ -1.99997pt &=& ( array[]rl&\ if_ (c@A)· u u∈ -1.99997pt S_ -1.99997pt \\\ ∪&\ if_ (c@A)· u u∈ -1.99997pt S_ -1.99997pt \ array )\\[10.00002pt] -1.99997pt if\ A( y)← B\ then\ S_ \ else\ S_ -1.99997pt &=& ( array[]rl&\ recv\ A( y[ /y_1])← B· u u∈ -1.99997pt S_ -1.99997pt \\\ ∪&\ recv\ A( y[ /y_1])← B· u u∈ -1.99997pt S_ -1.99997pt \ array ) array ⟨c@ASS⟩=⋃k≥0⊤(c@A)⋅u1⋅⋮⊤(c@A)⋅uk⋅⊥(c@A)⋅v|u1,…,uk∈⟨S⟩,v∈⟨S⟩ aligned -1.99997pt while\ c@A\ do\ S_body\ exit\ S_exit -1.99997pt &=\\ & _k≥ 0 \ array[]l while_ (c@A)· u_1·\\ \\ while_ (c@A)· u_k·\\ while_ (c@A)· v array\; |\; array[]lu_1,…,u_k∈ -1.99997pt S_body -1.99997pt ,\\ v∈ -1.99997pt S_exit -1.99997pt array \ aligned ⟨A(y→)←BSS⟩=⋃k≥0A(y→[⊤/y1])←B⋅u1⋅⋮A(y→[⊤/y1])←B⋅uk⋅A(y→[⊥/y1])←B⋅v|u1,…,uk∈⟨S⟩,v∈⟨S⟩ aligned -1.99997pt while\ A( y)← B\ do\ S_body\ exit\ S_exit -1.99997pt &=\\ & -68.00012pt _k≥ 0 \ array[]l recv\ A( y[ /y_1])← B· u_1·\\ \\ recv\ A( y[ /y_1])← B· u_k·\\ recv\ A( y[ /y_1])← B· v array\; |\; array[]lu_1,…,u_k∈ -1.99997pt S_body -1.99997pt ,\\ v∈ -1.99997pt S_exit -1.99997pt array \ aligned A language L⊆ΣA∗L _A^* is called prefix-free if no two distinct words in L are prefix-comparable. Lemma 3(Complete Local Traces Are Prefix-Free) For every local program S∈AS∈ LocProg_A, the language ⟨S⟩ -1.99997pt S -1.99997pt is prefix-free. Now that we have defined the local trace languages, the semantics of a distributed program is obtained by considering the tuples with one local trace for each lifeline, and keeping exactly those tuples that satisfy the MSC conditions from Definition 6. We define two semantics for distributed programs: one for complete executions and one for partial executions, where each local trace may be a prefix of a complete one. Given a distributed program =(SA)A∈ℒD=(S_A)_A∈ L, its complete MSC semantics is ⟦⟧=M=(wA)A∈ℒ|wA∈⟨SA⟩for all A,Mis a complete MSC. = \M=(w_A)_A∈ L\ |\ array[]lw_A∈ -1.99997pt S_A -1.99997pt \ for all A,\\ M\ is a complete MSC array \. For S∈AS∈ LocProg_A, we consider the prefix closure ⟨S⟩⊆ΣA∗ -1.99997pt S -1.99997pt _ pref _A^*, defined as ⟨S⟩=u∈ΣA∗∣∃v∈⟨S⟩:u⪯v -1.99997pt S -1.99997pt _ pref=\u∈ _A^* ∃ v∈ -1.99997pt S -1.99997pt u v\. The distributed prefix semantics is ⟦⟧=M=(wA)A∈ℒ|wA∈⟨SA⟩for all A,Mis an MSC. _ pref= \M=(w_A)_A∈ L\ |\ array[]lw_A∈ -1.99997pt S_A -1.99997pt _ pref\ for all A,\\ M\ is an MSC array \. Clearly, ⟦⟧⊆⟦⟧ _ pref. In particular, ⟦⟧ contains only complete MSCs (hence MSCs) by Definition 6. Note that MSC-ness is defined directly on tuples of local words, independently of any global workflow. For tuples M=(wA)A∈ℒM=(w_A)_A∈ L and M′=(wA′)A∈ℒM =(w _A)_A∈ L, define M⪯M′M M if, for all A∈ℒA∈ L, we have wA⪯wA′w_A w _A. Definition 11(Deadlock-Freeness) A distributed program D is deadlock-free if, for all M∈⟦⟧M∈ _ pref, there is M′∈⟦⟧M ∈ such that M⪯M′M M . In a general distributed system, the same prefix MSC can arise from two different branch histories, one completable and one not, so a complete extension need not witness genuine progress. In our framework, prefix-freeness of local trace languages ensures that every prefix uniquely identifies the branch history taken, so a complete extension always witnesses genuine progress, and deadlock-freeness (Definition 11) is a meaningful guarantee. 5 From Global to Distributed Programs This section explains how a global workflow is turned into a distributed program. We first define the syntax-directed projection itself, and then state its correctness with respect to the MSC semantics. 5.1 Projection We now pass from global workflows to executable local programs. The projection is syntax-directed: each workflow construct is translated locally for every lifeline, and the resulting local programs together form the distributed program that will be executed. Three ingredients are needed. First, for owned control constructs, the deciding lifeline must know which other lifelines may participate in the continuation. Second, the projected implementation uses explicit control broadcasts that are not present in the global semantics, so we compare projected executions to global ones only after erasing these auxiliary events. To determine which lifelines may need to observe a control decision, we use a simple structural participation analysis. Definition 12(Structural Participation Sets) For a global workflow P, the participation set ℒ(P) L(P) is defined inductively as follows: ℒ(A(x→)→B(y→)) L( msg\ A( x)→ B( y)) =A,B,ℒ(ε)=∅, =\A,B\, L( )= , ℒ(A:y→=f(x→)) L( act\ A: y=f( x)) =A,ℒ(P1;P2)=ℒ(P1)∪ℒ(P2), =\A\, L(P_1;P_2)= L(P_1)∪ L(P_2), ℒ(c@BP⊤P⊥) L( if\ c@B\ then\ P_ \ else\ P_ ) =B∪ℒ(P⊤)∪ℒ(P⊥), =\B\∪ L(P_ )∪ L(P_ ), ℒ(c@BPP) L( while\ c@B\ do\ P_body\ exit\ P_exit) =B∪ℒ(P)∪ℒ(P). =\B\∪ L(P_body)∪ L(P_exit). Using these sets, projection turns each owned decision into an explicit broadcast from the decider to the lifelines that may continue afterwards. Fix a total order ⊏ on lifelines. For R⊆ℒ∖BR L \B\, we write ∏A∈R⊏B(ν,κP)→A∈BΠ _A∈ R send\ B(ν, _ ctrl^P)→ A∈ LocProg_B for the sequence of decision sends in ⊏ -order, where ν∈⊤,⊥ν∈\ , \ is the decision value and P is the construct being projected; if R=∅R= , the product is the empty program ε . Each control-flow construct P uses a dedicated control tag κP _ ctrl^P (indexed by that construct), reserved so that source-level user messages never carry it. Two constructs that share a tag must be syntactically equal and therefore cannot be nested inside each other. Thus, control messages of nested constructs always carry distinct tags and are syntactically distinguishable. These control broadcasts are implementation details: they are needed to realize owned control in distributed code, but they should not appear in the global workflow semantics. We therefore compare projected executions to global executions only after erasing them. For each lifeline A, let A:ΣA∗→ΣA∗ erase_A: _A^*→ _A^* delete all decision-broadcast send/receive letters introduced by projection for control constructs (the B(⊤/⊥,κP)→A send\ B( / , _ ctrl^P)→ A and A(⊤/⊥,κP)←B recv\ A( / , _ ctrl^P)← B events, for any control construct P, used only for control decisions). For an MSC M=(wA)AM=(w_A)_A, define (M)=(A(wA))A∈ℒ. erase(M)=( erase_A(w_A))_A∈ L. Lemma 4(Erasure Preserves MSC and Completeness) If M is an MSC, then (M) erase(M) is an MSC. If M is a complete MSC, then (M) erase(M) is complete. With these conventions fixed, the projection rules themselves are straightforward. Atomic statements are projected pointwise to the relevant endpoints or owner lifeline. Sequential composition is projected componentwise. The only interesting case is owned control: the owner keeps its source-level if/while, emits explicit control messages, and each recipient branches by receiving a reserved control token from the owner. For each lifeline A∈ℒA∈ L, we define πA:→A _A Work→ LocProg_A. The projection rules are given in Tables 3, 4, and 5, where we let ℛ=(ℒ(P⊤)∪ℒ(P⊥))∖BR_if=( L(P_ )∪ L(P_ )) \B\ and ℛℎ=(ℒ(P)∪ℒ(P))∖BR_while=( L(P_body)∪ L(P_exit)) \B\. For recipient-side control constructs, (z,κP)(z, _ ctrl^P) is the received payload, where z is a Boolean variable not occurring in P and κP _ ctrl^P is the control tag of the enclosing construct P. For a global workflow P, we write P=(πA(P))A∈ℒD_P=( _A(P))_A∈ L for its projected distributed program. Let |P||P| be the number of syntactic nodes of P and n=|ℒ|n=| L|. Each global construct contributes at most one local node per lifeline, giving at most n|P|n|P| nodes overall. Moreover, each control construct adds at most two owner-side broadcast sequences, each of length at most n−1n-1. Hence the total size of all projections is at most n|P|+2(n−1)|P|=O(n|P|)n|P|+2(n-1)|P|=O(n|P|), and so each individual projection πX(P) _X(P) is also O(n|P|)O(n|P|). Table 3: Projection rules for atomic and sequential constructs. πA(ε)=επA(P1;P2)=πA(P1);πA(P2)πA(X(x→)→Y(y→))=X(x→)→Yif A=XY(y→)←Xif A=YεotherwiseπA(X:y→=f(x→))=X:y→=f(x→)if A=Xεotherwise array[]rcl _A( )&=& 18.49988pt _A(P_1;P_2)= _A(P_1); _A(P_2)\\[1.93748pt] _A( msg\ X( x)→ Y( y))&=& cases send\ X( x)→ Y&if A=X\\ recv\ Y( y)← X&if A=Y\\ &otherwise cases\\[19.37492pt] _A( act\ X: y=f( x))&=& cases act\ X: y=f( x)&if A=X\\ &otherwise cases array Table 4: Projection rule for P=c@BP⊤P⊥P= if\ c@B\ then\ P_ \ else\ P_ . πA(c@BP⊤P⊥)=(c@B∏C∈ℛ⊏B(⊤,κP)→C;πB(P⊤)∏C∈ℛ⊏B(⊥,κP)→C;πB(P⊥))if A=B(A(z,κP)←BπA(P⊤)πA(P⊥))if A∈ℛεotherwise _A( if\ c@B\ then\ P_ \ else\ P_ )= cases ( array[]@l@ if\ c@B\ then\\ 15.00002ptΠ _C _if send\ B( , _ ctrl^P)→ C;\\ 15.00002pt _B(P_ )\\ else\\ 15.00002ptΠ _C _if send\ B( , _ ctrl^P)→ C;\\ 15.00002pt _B(P_ ) array )&if A=B\\[43.05542pt] ( array[]@l@ if\ A(z, _ ctrl^P)← B\ then\\ 15.00002pt _A(P_ )\\ else\\ 15.00002pt _A(P_ ) array )&if A _if\\[25.83325pt] &otherwise cases Table 5: Projection rule for P=c@BPP= while\ c@B\ do\ P_body\ exit\ P_exit. πA(c@BPP)=(c@B∏C∈ℛℎ⊏B(⊤,κP)→C;πB(P)∏C∈ℛℎ⊏B(⊥,κP)→C;πB(P))if A=B(A(z,κP)←BπA(P)πA(P))if A∈ℛℎεotherwise gathered to0.0pt $ _A( while\ c@B\ do\ P_body\ exit\ P_exit)=$\\ cases ( array[]@l@ while\ c@B\ do\\ 15.00002ptΠ _C _while send\ B( , _ ctrl^P)→ C;\\ 15.00002pt _B(P_body)\\ exit\\ 15.00002ptΠ _C _while send\ B( , _ ctrl^P)→ C;\\ 15.00002pt _B(P_exit) array )&if A=B\\[43.05542pt] ( array[]@l@ while\ A(z, _ ctrl^P)← B\ do\\ 15.00002pt _A(P_body)\\ exit\\ 15.00002pt _A(P_exit) array )&if A _while\\[25.83325pt] &otherwise cases gathered Two design choices for local control keep the formal layer compact. First, we keep dedicated recipient-side constructs /A(z,κP)←B if/ while\ A(z, _ ctrl^P)← B rather than rewriting them into plain recv followed by ordinary / if/ while: this preserves an explicit receive-to-branch coupling without introducing guard evaluation machinery. Second, control broadcasts use constant values ⊤,⊥ , tagged with the per-construct tag κP _ ctrl^P. Indexing the tag by the construct P ensures that control messages of distinct nested constructs are syntactically distinguishable, which simplifies the decision-prefix attribution argument in the proof of Lemma 5. The tag also cleanly separates control traffic from user messages and identifies exactly the events removed by the erasure map. In particular, payload matching ensures that a receive expecting (⊤,κP)( , _ ctrl^P) cannot match a send carrying (⊥,κP)( , _ ctrl^P), and conversely. 5.2 Correctness We can now state the main correctness result of the projection. The theorem establishes that global and projected executions agree up to control messages: every global execution is realized by a distributed one after inserting the necessary control broadcasts, and every complete distributed execution yields a global one once control messages are removed. Theorem 5.1(Inductive Correctness) Let P be a well-typed global workflow. Then the following hold: (1) For every M∈⟦P⟧M∈ P , there exists M^∈⟦P⟧ M∈ _P such that (M^)=M erase( M)=M. (2) For every M^∈⟦P⟧ M∈ _P , (M^)∈⟦P⟧ erase( M)∈ P . Our semantics ranges only over finite, complete MSCs and their finite prefixes. Accordingly, Theorem 5.1 is a partial-correctness statement about terminating workflow executions: whenever a global or projected run reaches a complete finite execution, the erasure-based correspondence holds. In particular, every while loop is assumed to terminate, i.e., the owner’s condition eventually becomes false. The theorem is not a separate claim that arbitrary subsymbolic actions terminate, nor does it address infinite reactive behavior. This restriction is appropriate for the protocol workflows considered here. Extending the framework to reactive settings with infinite executions would require a corresponding semantic extension. Both items are proved by structural induction on P. Completeness (item 1) is straightforward: each case follows directly by induction. Soundness (item 2) is harder in the sequential composition case: given a distributed execution of P1;P2P_1;P_2, one must show that the P1P_1- and P2P_2-parts of each local trace together form valid MSCs. The Zipper lemma resolves exactly this difficulty. Deadlock-freeness (Corollary 1) then follows directly: applying the Zipper lemma with empty suffix extends any prefix execution to a complete one. Definition 13(Zipper postcondition) Let P be a well-typed global workflow, and let U=(uX)X∈ℒU=(u_X)_X∈ L, U¯=(u¯X)X∈ℒ U=( u_X)_X∈ L, and V=(vX)X∈ℒV=(v_X)_X∈ L be tuples of local words. We write P(U,U¯,V) ZipPost_P(U, U,V) if the following hold: (1) for every X∈ℒX∈ L, uX⪯u¯Xu_X u_X, u¯X∈⟨πX(P)⟩ u_X∈ -1.99997pt _X(P) -1.99997pt , and (vX≠ε⟹u¯X=uX)(v_X≠ ~ ~ u_X=u_X); (2) U¯ U is a complete MSC; (3) (uXvX)X∈ℒ(u_Xv_X)_X∈ L is an MSC; (4) (u¯XvX)X∈ℒ( u_Xv_X)_X∈ L is an MSC. The key result is that the Zipper postcondition is always satisfiable. Lemma 5(Zipper lemma) Let P be a well-typed global workflow. Let U=(uX)X∈ℒU=(u_X)_X∈ L and V=(vX)X∈ℒV=(v_X)_X∈ L be tuples of local words such that: • for every lifeline X∈ℒX∈ L, uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt _ pref; • for every lifeline X∈ℒX∈ L, vX≠ε⟹uX∈⟨πX(P)⟩v_X≠ ~ ~u_X∈ -1.99997pt _X(P) -1.99997pt . Define M=(uXvX)X∈ℒM=(u_Xv_X)_X∈ L. If M is an MSC, then there exists a tuple U¯=(u¯X)X∈ℒ U=( u_X)_X∈ L such that P(U,U¯,V). ZipPost_P(U, U,V). Intuitively, the lemma addresses the key difficulty of asynchronous sequential composition: in an execution of P1;P2P_1;P_2, different lifelines may cross the P1/P2P_1/P_2-boundary at different times, leaving some still inside P1P_1 while others have already begun P2P_2. The lemma guarantees that P1P_1 can always be completed consistently with whatever P2P_2-work has started. This is the situation illustrated by reviewed_execution. Three auxiliary consequences of P(U,U¯,V) ZipPost_P(U, U,V) will be used below. First, the prefix tuple U is itself an MSC. Second, if each component uXu_X is already a complete local trace of πX(P) _X(P), then U is in fact a complete MSC. Third, V is an MSC: conditions 2 and 4 together with Lemma 2 give this directly, so it need not be imposed separately in the definition. The first two facts are stated formally in Appendix 0.A as Lemma 8, Lemma 9, and Corollary 2. Corollary 1(Deadlock-freeness) For every well-typed global workflow P, the distributed program PD_P is deadlock-free in the sense of Definition 11. Corollary 1 is a semantic prefix-extension property: every prefix MSC of the projected distributed program can be extended to a complete MSC. This is the no-stuck property formalized in Definition 11. It is not, by itself, a claim about fairness or lock-freedom of every possible runtime scheduler. 5.3 The ZipperGen System ZipperGen, available at https://zippergen.io, is a Python implementation of the framework described in this paper. Its internal structure follows the formal development step by step. Workflows are written as ordinary Python functions and are decorated with @workflow. The decorator rewrites the function body into an immutable internal representation (IR) whose nodes mirror the formal grammar of Section 3: typed inputs become owned initial variables, message and action statements become message and action nodes, and Python if/while statements with conditions of the form expr @ Lifeline become owned control nodes. LLM and pure actions are declared separately with @llm and @pure. They attach prompts or pure implementations to the symbolic coordination layer, while the workflow itself remains a coordination object. Execution follows the projected semantics closely. ZipperGen projects the global workflow, spawns one thread per lifeline, and connects lifelines by FIFO queues, one per directed channel. Control broadcasts use per-construct tags κP _ ctrl^P, so they remain disjoint from user traffic and from each other across nested constructs. The LLM backend is pluggable, and a mock backend is available for testing workflows without API access. ZipperChat, the companion browser UI, streams execution events and renders them as a live MSC-style view. In this way, the prototype does not only implement the formal model, but also displays its executions in essentially the same visual language as the semantics. Runtime Planning. The framework as presented treats workflows as static specifications. ZipperGen also supports a @planner decorator for cases where the coordination structure is not known in advance. A planner action is declared like any other action and can be used directly inside a @workflow: Listing 2: A planner action in actual Python syntax. ⬇ 1@planner( 2 description="A workflow planner for professional writing tasks.", 3 lifelines=["Worker1", "Worker2"], 4 allow=["llm", "if"], 5 instructions="Use Worker1 to draft, Worker2 to assess quality; " 6 "route back to Worker1 for revision if needed.", 7) 8def write_document(request: str, job_desc: str, cv_sketch: str) -> str: ... At runtime, ZipperGen builds a hidden system prompt from all of the following: the description, an auto-generated summary of the available workers, DSL rules, and any allow extensions. An optional actions parameter supplies a pre-defined vocabulary. Since every ZipperGen action (@llm, @pure, @planner, or @workflow) presents the same interface of typed inputs and a typed output, any of these may in principle appear in the vocabulary. The planner receives their signatures and may call them directly in the generated workflow. The allow parameter controls what else the generated workflow may use: "pure" and "llm" permit the LLM to define new actions beyond the supplied vocabulary, while "if" and "while" enable conditional branching and loops. By default only linear workflows over the supplied action vocabulary are permitted. The optional instructions parameter lets the user guide how workers are assigned to tasks. Without it the runtime encourages the planner to use as many workers as reasonable. The designated LLM also receives the actual values of all input variables, so it sees what it is working with rather than just variable names, and generates a complete sub-workflow in the ZipperGen DSL. ZipperGen validates the generated workflow, projects it, and executes it. Worker lifelines are declared by name in @planner and created implicitly for the sub-workflow’s isolated scope, with their own threads and channels. Worker names must be distinct from the calling lifeline, since the caller appears as a participant in the sub-workflow itself. Nested planners work without any additional declaration. Under these conditions the same projection and deadlock-freedom guarantees apply as for handwritten workflows. Runtime generation does introduce uncertainty: the sub-workflow is LLM-produced and may not behave as intended. Three properties of the framework help manage this. First, each sub-workflow is isolated: it runs within its own lifeline scope and cannot affect the outer workflow except through its declared return value. Second, structural invariants are checked before execution. In particular, the sub-workflow must end with a worker sending the result back to the planner followed by a return, so the boundary with the outer workflow is always explicit. Third, ZipperGen renders each sub-workflow as a separate, inspectable MSC in ZipperChat, making it straightforward to see exactly what the generated workflow did. 6 Example: Medical Diagnosis Consensus We illustrate the language with a consensus workflow for medical diagnosis (Listing 3). Two independent LLMs analyze patient notes to determine whether a diagnosis (e.g., sepsis) applies. Each makes an independent assessment, then they exchange verdicts and reasoning, iterating until consensus. The loop continues until both agents reach agreement, at which point the final verdict is returned to the user. LLM1 owns the loop and broadcasts the continuation decision to LLM2 at each iteration; deadlock-freedom (Corollary 1) guarantees that every partial execution can be extended to a complete one. Listing 3: Consensus workflow (lifeline and variable declarations omitted). ⬇ 1workflow diagnosis_consensus(notes: str @ User, diagnosis: str @ User) -> str 2 // Distribute notes to both LLMs 3 msg User(notes, diagnosis) -> LLM1(notes, diagnosis) 4 msg User(notes, diagnosis) -> LLM2(notes, diagnosis) 5 6 // Independent initial assessments 7 act LLM1 : (verdict, reason) = assess(notes, diagnosis) 8 act LLM2 : (verdict, reason) = assess(notes, diagnosis) 9 msg LLM2(verdict) -> LLM1(other_verdict) 10 act LLM1 : agreed = check_agreement(verdict, other_verdict) 11 12 // Consensus loop: exchange, reconsider, check (LLM1 owns loop) 13 while (not agreed and trials < max_rounds)@LLM1 14 msg LLM1(verdict, reason) -> LLM2(other_verdict, other_reason) 15 msg LLM2(verdict, reason) -> LLM1(other_verdict, other_reason) 16 17 // Reconsider given other’s reasoning 18 act LLM1 : (verdict, reason) = reconsider(notes, diagnosis, 19 verdict, reason, 20 other_verdict, other_reason) 21 act LLM2 : (verdict, reason) = reconsider(notes, diagnosis, 22 verdict, reason, 23 other_verdict, other_reason) 24 25 // LLM2 sends updated verdict to LLM1 for agreement check 26 msg LLM2(verdict) -> LLM1(other_verdict) 27 28 // Check agreement and advance trial counter 29 act LLM1 : agreed = check_agreement(verdict, other_verdict) 30 act LLM1 : trials = inc_trials(trials) 31 exit epsilon 32 33 // Final result computed locally, then sent unconditionally 34 act LLM1 : result = choose_result(verdict, agreed) 35 msg LLM1(result) -> User(result) 36 return result @ User 37 The LLM action definition of assess is shown in Listing 4. The action reconsider is analogous. The remaining actions check_agreement, inc_trials, and choose_result are simple (non-LLM) functions. LLM1 owns the loop. Both LLMs appear in the body, so LLM2 receives a control broadcast at each iteration to learn whether execution continues or exits. The initial assessments are structurally independent: both LLMs act on the same notes without seeing each other’s reasoning before the first verdict exchange. This independence is visible in the global workflow and requires no additional annotation or runtime enforcement. Listing 4: Representative action definitions for the consensus workflow. ⬇ 1llm assess(notes: str, diag: str) -> (verdict: str, reason: str) 2 system: "You are a medical expert. Analyze the notes and 3 determine if the diagnosis applies. 4 Return verdict (yes/no/unknown) and your reasoning." 5 user: "Notes: notes : diag" 6 parse: json // "verdict": "yes"/"no"/"unknown", "reason": "..." 7 Additional executable examples, including a planning-based parallel arithmetic evaluator, are included in the companion ZipperGen artifact. Verifiable properties. The workflow is deadlock-free by construction. The control structure bounds the number of reconsideration rounds by max_rounds. This is a bound on the coordination pattern, not a termination guarantee for individual LLM calls. If execution reaches the final result-selection step, the returned value is either the agreed verdict or the conservative fallback unknown. 7 Conclusion We presented a domain-specific language for multi-agent LLM coordination based on message sequence charts, together with a syntax-directed projection that derives correct local programs from a global workflow specification. The projection is always defined, requires no realizability check, and guarantees deadlock-freedom by construction. The framework further extends to runtime-generated sub-workflows: a planning LLM produces a syntactically valid global workflow, which is then projected and executed with the same correctness guarantees as a statically written program. Future work includes a formal treatment of stale or non-returning LLM calls, where timeout mechanisms and their semantic consequences will be essential. A second direction is the integration of coregions [16], which relax the total order on receptions within a lifeline and allow a more flexible treatment of concurrency. Finally, the precise operational semantics of the framework makes it a natural setting for runtime verification: monitors can be derived from the global workflow and used to enforce safety properties at the boundary of the non-verifiable LLM components, providing trust guarantees that static analysis alone cannot offer. Recent work on trace-based assurance for agentic systems [23] illustrates the kind of runtime contracts and failure classes that such monitors could target. Acknowledgments This work was partly supported by the “France 2030” government investment plan managed by ANR, under the reference ANR-23-PEIA-0006. References [1] Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. Realizability and verification of MSC graphs. Theor. Comput. Sci., 331(1):97–114, 2005. [2] Hanêne Ben-Abdallah and Stefan Leue. Syntactic detection of process divergence and non-local choice in message sequence charts. In Ed Brinksma, editor, Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS ’97, Enschede, The Netherlands, April 2-4, 1997, Proceedings, Lecture Notes in Computer Science, pages 259–274. Springer, 1997. [3] Benedikt Bollig, Marie Fortin, and Paul Gastin. High-level message sequence charts: Satisfiability and realizability revisited. In Elvio Gilberto Amparore and Lukasz Mikulski, editors, Application and Theory of Petri Nets and Concurrency - 46th International Conference, PETRI NETS 2025, Paris, France, June 22-27, 2025, Proceedings, Lecture Notes in Computer Science, pages 109–129. Springer, 2025. [4] Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party session. Log. Methods Comput. Sci., 8(1), 2012. [5] CrewAI, Inc. Crewai: Multi-agent orchestration framework. https://github.com/crewaiinc/crewai, 2024. Accessed: 2026-04-10. [6] Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, Lecture Notes in Computer Science, pages 194–213. Springer, 2012. [7] Victor Dibia. Designing Multi-Agent Systems: Principles, Patterns, and Implementation for AI Agents. Victor Dibia, 2025. [8] Luca Fossati, Raymond Hu, and Nobuko Yoshida. Multiparty session nets. In Matteo Maffei and Emilio Tuosto, editors, Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers, Lecture Notes in Computer Science, pages 112–127. Springer, 2014. [9] Blaise Genest. On implementation of global concurrent systems with local asynchronous controllers. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, Lecture Notes in Computer Science, pages 443–457. Springer, 2005. [10] Blaise Genest, Anca Muscholl, Helmut Seidl, and Marc Zeitoun. Infinite-state high-level mscs: Model-checking and realizability. J. Comput. Syst. Sci., 72(4):617–647, 2006. [11] Cinzia Di Giusto, Étienne Lozes, and Pascal Urso. Realisability and complementability of multiparty session types. In Malgorzata Biernacka, Carlos Olarte, Francesco Ricca, and James Cheney, editors, Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming, PPDP 2025, Rende, Italy, September 10-11, 2025, pages 11:1–11:12. ACM, 2025. [12] Loïc Hélouët and Claude Jard. Conditions for synthesis of communicating automata from HMSCs. In A. Rennoch, editor, 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), pages 203–224, Berlin, Germany, 2000. [13] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. [14] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, Lecture Notes in Computer Science, pages 122–138. Springer, 1998. [15] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1–9:67, 2016. [16] ITU-T. Recommendation Z.120: Message sequence chart (MSC). Technical report, International Telecommunication Union, 2011. [17] LangChain, Inc. Langgraph: Building stateful multi-agent applications with llms. https://github.com/langchain-ai/langgraph, 2024. Accessed: 2026-04-10. [18] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I, Lecture Notes in Computer Science, pages 350–373. Springer, 2023. [19] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Characterizing implementability of global protocols with infinite states and data. Proc. ACM Program. Lang., 9(OOPSLA1):1434–1463, 2025. [20] Elaine Li and Thomas Wies. Certified implementability of global multiparty protocols. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025, LIPIcs, pages 15:1–15:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. [21] Markus Lohrey. Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci., 309(1-3):529–554, 2003. [22] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and I. Inf. Comput., 100(1):1–77, 1992. [23] Ciprian Paduraru, Petru-Liviu Bouruc, and Alin Stefanescu. A trace-based assurance framework for agentic AI orchestration: Contracts, testing, and governance, 2026. [24] Felix Stutz. Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming, ECOOP 2023, Seattle, Washington, United States, July 17-21, 2023, LIPIcs, pages 32:1–32:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. [25] Qingyun Wu, Gagan Bansal, Jieyu Zhang, Yiran Wu, Shaokun Zhang, Erkang Zhu, Beibin Li, Li Jiang, Xiaoyun Zhang, and Chi Wang. Autogen: Enabling next-gen LLM applications via multi-agent conversation framework. CoRR, abs/2308.08155, 2023. [26] Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The Scribble protocol language. In Martín Abadi and Alberto Lluch-Lafuente, editors, Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, Lecture Notes in Computer Science, pages 22–41. Springer, 2014. [27] Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang., 4(OOPSLA):148:1–148:30, 2020. Appendix 0.A Proofs 0.A.1 Proof of Lemma 1 (Concatenation with a Complete Prefix) For the MSC part, consider M1=(uA)AM_1=(u_A)_A complete and M2=(vA)AM_2=(v_A)_A an MSC. Every receive event of M1∘M2M_1 M_2 lies either in the prefix M1M_1 or in the suffix M2M_2. Prefix receives are matched inside M1M_1 because M1M_1 is complete. Suffix receives are matched inside M2M_2 because M2M_2 is an MSC. Hence FIFO matching is defined on M1∘M2M_1 M_2, and label compatibility is inherited componentwise from M1M_1 and M2M_2. For acyclicity, note that all cross-component causality edges go from events of M1M_1 to events of M2M_2: local successor edges cross the concatenation boundary only in that direction, and message-matching edges cannot point from M2M_2 back into M1M_1 because every send in M1M_1 is already matched inside the complete prefix M1M_1. Thus a cycle in M1∘M2M_1 M_2 would restrict to a cycle in M1M_1 or M2M_2, impossible since both are MSCs. Therefore M1∘M2M_1 M_2 is an MSC. If M2M_2 is complete as well, then every send in the concatenation is matched inside its own factor, so M1∘M2M_1 M_2 is complete. ∎ 0.A.2 Proof of Lemma 2 (Stripping a Complete Prefix) For the MSC part, every receive event occurring in the suffix N is matched in C∘NC N. Because C is complete, no such suffix receive can be matched to a send from the prefix C. Otherwise, the corresponding channel would have an unmatched send in C. Hence all suffix receives are matched by suffix sends, so FIFO matching is defined on N. Label compatibility is inherited from C∘NC N. Acyclicity is preserved because the causality relation of N is the restriction of the causality relation of C∘NC N to suffix events. If C∘NC N is complete, then every suffix send is matched in C∘NC N. Again, because C is complete, a suffix send cannot be matched to a receive in the prefix C. Therefore every suffix send is matched inside N, so N is complete. 0.A.3 Proof of Lemma 3 By structural induction on S. The atomic cases are singletons and therefore prefix-free. For sequential composition, let uv,u′v′∈⟨S1;S2⟩uv,\ u v ∈ -1.99997pt S_1;S_2 -1.99997pt with u,u′∈⟨S1⟩u,u ∈ -1.99997pt S_1 -1.99997pt and v,v′∈⟨S2⟩v,v ∈ -1.99997pt S_2 -1.99997pt , and assume uv⪯u′v′uv u v . Then u and u′u are both prefixes of the word u′v′u v , hence they are comparable by ⪯ . By IH on S1S_1, the language ⟨S1⟩ -1.99997pt S_1 -1.99997pt is prefix-free, so u=u′u=u . It follows that v⪯v′v v , and IH on S2S_2 gives v=v′v=v . Thus uv=u′v′uv=u v . For each control construct, we distinguish two projection cases: the owner case, where the true and false branches begin with distinct choice letters (namely ⊤(c@A) if_ (c@A) versus ⊥(c@A) if_ (c@A)), and the recipient case, where they begin with distinct receive events (A(y→[⊤/y1])←B recv\ A( y[ /y_1])← B versus A(y→[⊥/y1])←B recv\ A( y[ /y_1])← B). In both cases the argument is the same: two traces starting with different initial letters are incomparable by ⪯ , and if they begin with the same letter, prefix-freeness follows from IH on the selected branch. For the two while-cases, every complete trace has the form d⊤u1⋯d⊤ukd⊥vd u_1·s d u_kd v where d⊤d and d⊥d are the corresponding top/bot decision letters, u1,…,uk∈⟨S⟩u_1,…,u_k∈ -1.99997pt S_body -1.99997pt , and v∈⟨S⟩v∈ -1.99997pt S_exit -1.99997pt . If two such traces have different numbers of top-decisions, then at the first position where the shorter one exits and the longer one continues, one sees a ⊥ -decision versus a ⊤ -decision, so neither word is a prefix of the other. If the numbers of top-decisions agree, compare the body traces one by one. IH on S_body forces equality of each uiu_i, and IH on S_exit then forces equality of the final exit traces. Hence the complete traces are prefix-free. 0.A.4 Proof of Lemma 4 (Erasure Preserves MSC Structure) The map erase deletes only control-broadcast send/receive events introduced by projection and leaves all other local letters unchanged. Therefore the local successor order on the remaining events is preserved. If M is an MSC, every receive event that survives erasure was already a non-control receive in M, and its matching send also survives erasure. Conversely, deleting matched control send/receive pairs cannot create unmatched receives among the remaining events. Label compatibility is inherited from M, and acyclicity is preserved because (M) erase(M) is obtained by restricting the causality relation of M to the surviving events. Hence (M) erase(M) is an MSC. If M is complete, then every surviving send event in (M) erase(M) was already matched in M by a surviving receive event, since only control broadcast pairs are deleted. Thus every send in (M) erase(M) is still matched, so we have that (M) erase(M) is complete. 0.A.5 Boundary-Aligned Sequential Factorization Lemma 6(Boundary-aligned sequential factorization) Let A∈ℒA∈ L, let S1,S2∈AS_1,S_2∈ LocProg_A be local programs at lifeline A, and let u∈⟨S1;S2⟩u∈ -1.99997pt S_1;S_2 -1.99997pt _ pref. Then there exist words u1,u2∈ΣA∗u_1,u_2∈ _A^* such that u=u1u2,u1∈⟨S1⟩,u2∈⟨S2⟩,u=u_1u_2, u_1∈ -1.99997pt S_1 -1.99997pt _ pref, u_2∈ -1.99997pt S_2 -1.99997pt _ pref, and, moreover, u2≠ε⟹u1∈⟨S1⟩.u_2≠ ~ ~u_1∈ -1.99997pt S_1 -1.99997pt . Proof(Proof of Lemma 6) Since u∈⟨S1;S2⟩u∈ -1.99997pt S_1;S_2 -1.99997pt _ pref, there exists w∈⟨S1;S2⟩w∈ -1.99997pt S_1;S_2 -1.99997pt with u⪯wu w. By the definition of the sequential composition semantics, choose x∈⟨S1⟩x∈ -1.99997pt S_1 -1.99997pt and y∈⟨S2⟩y∈ -1.99997pt S_2 -1.99997pt such that w=xyw=xy. Since u is a prefix of the concatenation xyxy, there are two cases. If u⪯xu x, set u1=u_1=u and u2=εu_2= . Then u1∈⟨S1⟩u_1∈ -1.99997pt S_1 -1.99997pt _ pref and u2∈⟨S2⟩u_2∈ -1.99997pt S_2 -1.99997pt _ pref. Otherwise, u crosses the S1/S2S_1/S_2-boundary, so u=xu2u=xu_2 for some prefix u2⪯yu_2 y. Set u1=xu_1=x. Then u1∈⟨S1⟩u_1∈ -1.99997pt S_1 -1.99997pt and u2∈⟨S2⟩u_2∈ -1.99997pt S_2 -1.99997pt _ pref. This yields the required factorization. ∎ 0.A.6 Proof of Lemma 5 (Zipper lemma) We proceed by structural induction on P. Throughout the proof, M=(uXvX)XM=(u_Xv_X)_X is the MSC from the hypotheses. Condition 3 of ZipPost (that (uXvX)X(u_Xv_X)_X is an MSC) is therefore always satisfied by M itself and requires no further argument. Case P=εP= . Then uX=εu_X= for every X (because uX∈⟨πX(ε)⟩=εu_X∈ -1.99997pt _X( ) -1.99997pt _ pref=\ \). Set u¯X=ε u_X= . Hence U¯=(u¯X)X U=( u_X)_X is a complete MSC and M¯=(u¯XvX)X=(vX)X=M M=( u_Xv_X)_X=(v_X)_X=M is an MSC. Thus ε(U,U¯,V) ZipPost_ (U, U,V) holds. Cases P=…P= msg…, P=…P= act…. Assume M=(uXvX)XM=(u_Xv_X)_X satisfies the hypotheses. For each X, define u¯X=uXif vX≠ε,uXtXif vX=ε, u_X= casesu_X&if v_X≠ ,\\[5.69054pt] u_Xt_X&if v_X= , cases where tXt_X is chosen such that uXtX∈⟨πX(P)⟩u_Xt_X∈ -1.99997pt _X(P) -1.99997pt . Such a word exists because uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt _ pref. Let U¯=(u¯X)X U=( u_X)_X and M¯=(u¯XvX)X M=( u_Xv_X)_X. First, U¯ U is a complete MSC. Indeed, for each X we have u¯X∈⟨πX(P)⟩ u_X∈ -1.99997pt _X(P) -1.99997pt by construction. For each channel A→BA→ B, the number of A→BA→ B sends in u¯A u_A equals the number of A→BA→ B receives in u¯B u_B because these numbers are fixed by the same completed trace of the single statement P. We show that M¯ M is an MSC. First, ⊲M¯ _ M is defined: pairs already matched in M remain matched because FIFO matching is defined by channel indices and we only append events at the end of local words. Any new receives appear only in some tBt_B (hence vB=εv_B= ). Fix such a receive on a channel A→BA→ B. Since u¯A∈⟨πA(P)⟩ u_A∈ -1.99997pt _A(P) -1.99997pt and u¯B∈⟨πB(P)⟩ u_B∈ -1.99997pt _B(P) -1.99997pt , the projection of P ensures that the corresponding send appears in u¯A u_A, hence the receive is matched. Second, the causality relation of M¯ M (local order together with FIFO constraints) is acyclic. Compared with M, we only append events at the end of lifelines and add causality constraints incident to these new events, so no new constraint can point backward in local order. Thus M¯ M is an MSC. Thus P(U,U¯,V) ZipPost_P(U, U,V) holds. Auxiliary notation (decision prefixes). Let P be a control construct (if or while) with decider B, and fix a branch value ν∈⊤,⊥ν∈\ , \. Let ℛR be the recipient set of that construct. Write γBν _B^ν for the choice letter that B emits when it decides ν: this is ⊤(c@B) if_ (c@B) (resp. ⊥(c@B) if_ (c@B)) for an if-construct, and ⊤(c@B) while_ (c@B) (resp. ⊥(c@B) while_ (c@B)) for a while-construct. Define the decision-prefix word dXνd_X^ν on each lifeline X by dXν=γBν⋅∏A∈ℛ⊏B(ν,κP)→Aif X=B,X(ν,κP)←Bif X∈ℛ,εif X∉ℛ∪B.d_X^ν= cases _B^ν· _A send\ B(ν, _ ctrl^P)→ A&if X=B,\\[3.00003pt] recv\ X(ν, _ ctrl^P)← B&if X ,\\[3.00003pt] &if X ∪\B\. cases Note that the owner’s component now starts with the choice letter γBν _B^ν, which records the branch taken before any control message is sent. In the if-case, this ensures the decomposition πB(P)=dBν;πB(Qν) _B(P)=d_B^ν; _B(Q_ν) holds on the decider lifeline, where QνQ_ν denotes the branch subprogram of P corresponding to ν. Let Dν=(dXν)X∈ℒD^ν=(d_X^ν)_X∈ L. Lemma 7(Decision-Prefix Stripping) Let P be a projected if- or while-construct with decision-prefix tuple Dν=(dXν)XD^ν=(d_X^ν)_X for some ν∈⊤,⊥ν∈\ , \. Let M=(wX)XM=(w_X)_X be an MSC such that, for every lifeline X, wX≺dXνorwX=dXνsXw_X d_X^ν w_X=d_X^νs_X for some word sXs_X. Define rX=εif wX≺dXν,sXif wX=dXνsX,M′=(rX)X.r_X= cases &if w_X d_X^ν,\\ s_X&if w_X=d_X^νs_X, cases M =(r_X)_X. Then M′M is an MSC. Proof(Proof of Lemma 7) The deleted events on each lifeline form an initial segment of the decision-prefix block dXνd_X^ν. We check that no unmatched receive is created. Consider a control channel B→AB→ A (owner to recipient). The owner’s send B(ν,κP)→A send\ B(ν, _ ctrl^P)→ A appears in dBνd_B^ν, and the recipient’s matching receive A(ν,κP)←B recv\ A(ν, _ ctrl^P)← B is the sole event of dAνd_A^ν. If the send is present in wBw_B, it lies in dBνd_B^ν and is absent from rBr_B. The receive is either also present in wAw_A (so wA=dAνtAw_A=d_A^νt_A and it is likewise absent from rAr_A), or absent from wAw_A entirely. In both sub-cases no unmatched receive appears in M′M . If the send is absent (wB≺dBνw_B d_B^ν), then M being an MSC ensures the receive is absent from wAw_A as well (otherwise it would be unmatched in M), so nothing changes for A. In all cases no unmatched receive is introduced. Since dXνd_X^ν consists entirely of control events (the choice letter and control sends/receives), non-control events appear only in the suffix sXs_X and are fully preserved in M′M , hence no unmatched receive or send is introduced on non-control channels either. Label compatibility holds because M′M retains a subset of M’s events with the same labels. Acyclicity of the happens-before order is preserved because any cycle in M′M would be a cycle in M, contradicting M being an MSC. Hence M′M is an MSC. ∎ If-construct case. Let P=c@BQ⊤Q⊥.P= if\ c@B\ then\ Q_ \ else\ Q_ . Since M=(uXvX)XM=(u_Xv_X)_X is an MSC and control messages are distinguishable, any choice letter, control send, or control receive of this if-construct already present in the tuple determines ν uniquely: the owner’s choice letter γBν _B^ν directly records which branch was taken, and FIFO matching on channels B→AB→ A forces all control sends and receives to carry the same value. Hence there exists a branch value ν∈⊤,⊥ν∈\ , \ consistent with all lifelines, and this value is unique whenever any such event is present. If neither the choice letter nor any control message of this if-construct appears in the current prefix tuple, both values are compatible and we choose one arbitrarily. In this situation, no participating lifeline can already have entered the continuation of either branch: by the local trace semantics of the projected if-construct, every such local trace starts with the corresponding decision-prefix word dXνd_X^ν. Unfolding the projection and local prefix semantics with this value yields, for each X: uX≺dXνoruX=dXνuX′with uX′∈⟨πX(Qν)⟩.u_X d_X^ν u_X=d_X^νu _X\ with \ u _X∈ -1.99997pt _X(Q_ν) -1.99997pt _ pref. These are exactly the two prefix forms of the sequential decomposition πX(P)=dXν;πX(Qν) _X(P)=d_X^ν; _X(Q_ν). For each X, define the remainder rX=εif uX≺dXν,uX′if uX=dXνuX′for some uX′∈⟨πX(Qν)⟩.r_X= cases &if u_X d_X^ν,\\ u _X&if u_X=d_X^νu _X\ for some u _X∈ -1.99997pt _X(Q_ν) -1.99997pt _ pref. cases Moreover, for each X, if vX≠εv_X≠ , then uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt by hypothesis. Therefore the first alternative uX≺dXνu_X d_X^ν is impossible, hence uX=dXνuX′u_X=d_X^νu _X and uX′∈⟨πX(Qν)⟩u _X∈ -1.99997pt _X(Q_ν) -1.99997pt . Apply Lemma 7 to M=(uXvX)XM=(u_Xv_X)_X with wX=uXvXw_X=u_Xv_X. The two conditions of the lemma are satisfied: M is an MSC by hypothesis, and each wXw_X either satisfies wX≺dXνw_X d_X^ν (which forces vX=εv_X= by the Zipper side condition, so wX=uX≺dXνw_X=u_X d_X^ν) or satisfies wX=dXν(uX′vX)w_X=d_X^ν(u _Xv_X) (when uX=dXνuX′u_X=d_X^νu _X). The lemma yields that M′=(rXvX)XM =(r_Xv_X)_X is an MSC. Since πX(P)=dXν;πX(Qν) _X(P)=d_X^ν; _X(Q_ν), we have rX∈⟨πX(Qν)⟩r_X∈ -1.99997pt _X(Q_ν) -1.99997pt _ pref for every X; and if vX≠εv_X≠ then rX=uX′∈⟨πX(Qν)⟩r_X=u _X∈ -1.99997pt _X(Q_ν) -1.99997pt . Apply IH to QνQ_ν with respect to the factorization M′=(rXvX)XM =(r_Xv_X)_X. We obtain a completion U¯ν=(r¯X)X U_ν=( r_X)_X such that Qν((rX)X,U¯ν,V). ZipPost_Q_ν((r_X)_X, U_ν,V). Define u¯X=dXνr¯X. u_X=d_X^ν r_X. We verify the four conditions of P(U,U¯,V) ZipPost_P(U, U,V). Condition 1. Since rX⪯r¯Xr_X r_X by Condition 1 of Qν ZipPost_Q_ν, we have uX⪯u¯Xu_X u_X (either uX≺dXν⪯u¯Xu_X d_X^ν u_X, or uX=dXνuX′=dXνrX⪯dXνr¯X=u¯Xu_X=d_X^νu _X=d_X^νr_X d_X^ν r_X= u_X). Also u¯X=dXνr¯X∈⟨πX(P)⟩ u_X=d_X^ν r_X∈ -1.99997pt _X(P) -1.99997pt since r¯X∈⟨πX(Qν)⟩ r_X∈ -1.99997pt _X(Q_ν) -1.99997pt . If vX≠εv_X≠ , then r¯X=rX=uX′ r_X=r_X=u _X by Condition 1 of Qν ZipPost_Q_ν, so u¯X=dXνuX′=uX u_X=d_X^νu _X=u_X. Condition 2. U¯ν=(r¯X)X U_ν=( r_X)_X is a complete MSC by Condition 2 of Qν ZipPost_Q_ν, and DνD^ν is a complete MSC by construction, so U¯=Dν∘U¯ν U=D^ν U_ν is a complete MSC by Lemma 1. Condition 3. (uXvX)X=M(u_Xv_X)_X=M is an MSC by hypothesis. Condition 4. (u¯XvX)X=Dν∘(r¯XvX)X( u_Xv_X)_X=D^ν ( r_Xv_X)_X is an MSC by Lemma 1, since DνD^ν is a complete MSC and (r¯XvX)X( r_Xv_X)_X is an MSC by Condition 4 of Qν ZipPost_Q_ν. Thus P(U,U¯,V) ZipPost_P(U, U,V) holds. While-construct case. Let P=c@BQE.P= while\ c@B\ do\ Q\ exit\ E. We argue by a secondary induction on the number m≥0m≥ 0 of already-started decision blocks of this while-construct visible in the tuple M=(uXvX)XM=(u_Xv_X)_X. More precisely, since the decision-prefix events of P carry the tag κP _ ctrl^P (distinct from the tags of all nested constructs) they are syntactically distinguishable from events of any other construct. Thus m is the number of complete decision-prefix blocks dXνd_X^ν of P that appear as an initial segment of uXu_X (for owner B and all participating recipients). By FIFO matching and the MSC property of M, this count agrees across all participating lifelines and the resulting sequence of decisions has the form ν1…νm∈⊤∗∪⊤∗⊥. _1… _m∈\ \^*∪\ \^* . Base case m=0m=0. Then no decision-prefix event (choice letter, control send, or control receive) of this while-construct has yet started in the tuple. In particular, for every lifeline X whose projected local while-word starts with the current decision-prefix block, one has uX=εu_X= . Equivalently, no participating lifeline has yet entered either the loop body or the exit continuation, because every participating local trace of the projected while-program begins with the first decision-prefix block. Moreover, if vX≠εv_X≠ , then by the zipper side condition uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt holds. Thus, such an X cannot participate in the while-construct, because every complete local trace of a participating projection of P begins with a decision-prefix event (a choice letter on the owner, a control receive on each recipient). Since here uX=εu_X= , the only way uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt can hold is that πX(P)=ε _X(P)= , i.e., X does not participate in the while-construct at all. In particular, X∉ℒ(E)X∉ L(E), so πX(E)=ε _X(E)= . We choose the first decision value to be ⊥ . Let rX=εfor all X∈ℒ,r_X= all X∈ L, and consider the tuple M′=(rXvX)X=(vX)X.M =(r_Xv_X)_X=(v_X)_X. For every X, one has rX=ε∈⟨πX(E)⟩,r_X= ∈ -1.99997pt _X(E) -1.99997pt _ pref, and if vX≠εv_X≠ , then X does not participate in the while-construct, hence also rX=ε∈⟨πX(E)⟩.r_X= ∈ -1.99997pt _X(E) -1.99997pt . Therefore the structural induction hypothesis applies to E and M′=(rXvX)XM =(r_Xv_X)_X. We obtain a tuple R¯=(r¯X)X R=( r_X)_X such that E((rX)X,R¯,V). ZipPost_E((r_X)_X, R,V). Now define u¯X=dX⊥r¯Xfor all X∈ℒ, u_X=d_X \, r_X all X∈ L, and let U¯=(u¯X)X U=( u_X)_X. Since uX=ε⪯u¯Xu_X= u_X, Condition 1a holds. If vX≠εv_X≠ , then X does not participate in the while-construct (shown above), so dX⊥=εd_X = and u¯X=ε=uX u_X= =u_X, and Condition 1c holds. u¯X∈⟨πX(P)⟩ u_X∈ -1.99997pt _X(P) -1.99997pt for every X (Condition 1b), because a ⊥ -decision followed by an E-trace is exactly a complete local trace of the projected while-program. Furthermore, U¯=D⊥∘R¯ U=D R is a complete MSC (Condition 2), and M¯=(u¯XvX)X=D⊥∘(r¯XvX)X M=( u_Xv_X)_X=D ( r_Xv_X)_X is an MSC by Lemma 1, since D⊥D is a complete MSC (Condition 4). Hence P(U,U¯,V) ZipPost_P(U, U,V) holds. This yields the required completion in the base case. Induction step m>0m>0. Let ν=ν1∈⊤,⊥ν= _1∈\ , \ be the first visible decision value. By unfolding the definitions of projection for P and of ⟨⋅⟩ -1.99997pt · -1.99997pt _ pref, each local prefix uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt _ pref is of one of the following forms: • uX≺dXνu_X d_X^ν, • uX=dX⊤uX′u_X=d_X u _X with uX′∈⟨πX(Q;P)⟩u _X∈ -1.99997pt _X(Q;P) -1.99997pt _ pref, • uX=dX⊥uX′u_X=d_X u _X with uX′∈⟨πX(E)⟩u _X∈ -1.99997pt _X(E) -1.99997pt _ pref. Since ν is the first visible decision value forced by the decision-prefix events already present in M, only the branch corresponding to this ν can occur. Define the remainder rX=εif uX≺dXν,uX′if uX=dXνuX′.r_X= cases &if u_X d_X^ν,\\ u _X&if u_X=d_X^νu _X. cases Moreover, if vX≠εv_X≠ , then by hypothesis uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt , so the alternative uX≺dXνu_X d_X^ν is impossible. Thus whenever vX≠εv_X≠ , the first decision block has already been fully consumed on X. Apply Lemma 7 to M=(uXvX)XM=(u_Xv_X)_X with wX=uXvXw_X=u_Xv_X: since vX≠εv_X≠ implies uX=dXνuX′u_X=d_X^νu _X, each wXw_X satisfies the prefix condition. The lemma yields that M′=(rXvX)XM =(r_Xv_X)_X is again an MSC. We now distinguish the two possible values of ν. Subcase ν=⊥ν= . Then for every X, rX∈⟨πX(E)⟩,r_X∈ -1.99997pt _X(E) -1.99997pt _ pref, and whenever vX≠εv_X≠ , since uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt and uX=dX⊥uX′u_X=d_X u _X, every complete local trace of πX(P) _X(P) starting with dX⊥d_X continues in ⟨πX(E)⟩ -1.99997pt _X(E) -1.99997pt , hence rX=uX′∈⟨πX(E)⟩.r_X=u _X∈ -1.99997pt _X(E) -1.99997pt . Hence the structural induction hypothesis applies to E and M′=(rXvX)XM =(r_Xv_X)_X. We obtain a completion R¯=(r¯X)X R=( r_X)_X such that E((rX)X,R¯,V). ZipPost_E((r_X)_X, R,V). Define u¯X=dX⊥r¯X, u_X=d_X \, r_X, and let U¯=(u¯X)X U=( u_X)_X. For every X, uX⪯u¯Xu_X u_X: if uX=dX⊥rXu_X=d_X r_X then uX=dX⊥rX⪯dX⊥r¯X=u¯Xu_X=d_X r_X d_X r_X= u_X by Condition 1 of E ZipPost_E: if uX≺dX⊥u_X d_X then uX⪯dX⊥⪯u¯Xu_X d_X u_X. If vX≠εv_X≠ , then uX=dX⊥rXu_X=d_X r_X (shown above) and r¯X=rX r_X=r_X by Condition 1 of E ZipPost_E, hence u¯X=dX⊥r¯X=dX⊥rX=uX u_X=d_X r_X=d_X r_X=u_X. Therefore Condition 1 of P(U,U¯,V) ZipPost_P(U, U,V) holds. u¯X∈⟨πX(P)⟩ u_X∈ -1.99997pt _X(P) -1.99997pt for every X (Condition 1b), and U¯=D⊥∘R¯ U=D R is a complete MSC (Condition 2), while M¯=(u¯XvX)X=D⊥∘(r¯XvX)X M=( u_Xv_X)_X=D ( r_Xv_X)_X is an MSC by Lemma 1, since D⊥D is a complete MSC (Condition 4). Hence P(U,U¯,V) ZipPost_P(U, U,V) holds. Subcase ν=⊤ν= . Then for every X, rX∈⟨πX(Q;P)⟩,r_X∈ -1.99997pt _X(Q;P) -1.99997pt _ pref, and whenever vX≠εv_X≠ , since uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt and uX=dX⊤uX′u_X=d_X u _X, every complete local trace of πX(P) _X(P) starting with dX⊤d_X continues in ⟨πX(Q;P)⟩ -1.99997pt _X(Q;P) -1.99997pt , hence rX=uX′∈⟨πX(Q;P)⟩.r_X=u _X∈ -1.99997pt _X(Q;P) -1.99997pt . By the prefix semantics of sequential composition, factor rX=bXsXr_X=b_Xs_X with bX∈⟨πX(Q)⟩andsX∈⟨πX(P)⟩.b_X∈ -1.99997pt _X(Q) -1.99997pt _ pref s_X∈ -1.99997pt _X(P) -1.99997pt _ pref. By Lemma 6, we may choose this factorization boundary-aligned, i.e., sX≠ε⟹bX∈⟨πX(Q)⟩.s_X≠ ~ ~b_X∈ -1.99997pt _X(Q) -1.99997pt . The remaining case needed for the IH side condition is sX=εs_X= and vX≠εv_X≠ : then rX=bX∈⟨πX(Q)⟩r_X=b_X∈ -1.99997pt _X(Q) -1.99997pt _ pref, and the condition established above (vX≠ε⟹rX∈⟨πX(Q;P)⟩v_X≠ r_X∈ -1.99997pt _X(Q;P) -1.99997pt ) gives rX∈⟨πX(Q;P)⟩r_X∈ -1.99997pt _X(Q;P) -1.99997pt . Since bX∈⟨πX(Q;P)⟩b_X∈ -1.99997pt _X(Q;P) -1.99997pt , it factors as bX=cXdXb_X=c_Xd_X with cX∈⟨πX(Q)⟩c_X∈ -1.99997pt _X(Q) -1.99997pt and dX∈⟨πX(P)⟩d_X∈ -1.99997pt _X(P) -1.99997pt . Let eX∈⟨πX(Q)⟩e_X∈ -1.99997pt _X(Q) -1.99997pt be a complete trace with bX⪯eXb_X e_X (which exists because bX∈⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt _ pref). Then cX⪯bX⪯eXc_X b_X e_X with cX,eX∈⟨πX(Q)⟩c_X,e_X∈ -1.99997pt _X(Q) -1.99997pt ; by prefix-freeness of ⟨πX(Q)⟩ -1.99997pt _X(Q) -1.99997pt , this forces cX=eXc_X=e_X, hence dX=εd_X= and bX=cX∈⟨πX(Q)⟩b_X=c_X∈ -1.99997pt _X(Q) -1.99997pt . Hence in all cases, sXvX≠ε⟹bX∈⟨πX(Q)⟩.s_Xv_X≠ ~ ~b_X∈ -1.99997pt _X(Q) -1.99997pt . Now consider N=(bX(sXvX))X.N=(b_X(s_Xv_X))_X. Since N=(rXvX)X=M′N=(r_Xv_X)_X=M is an MSC and bX∈⟨πX(Q)⟩,b_X∈ -1.99997pt _X(Q) -1.99997pt _ pref, with the required side condition established above, the structural induction hypothesis applies to Q and N. Hence there exists a completion U¯Q=(b¯X)X U_Q=( b_X)_X such that Q((bX)X,U¯Q,(sXvX)X). ZipPost_Q((b_X)_X, U_Q,(s_Xv_X)_X). In particular, M′=(sXvX)XM =(s_Xv_X)_X is an MSC. Furthermore, if vX≠εv_X≠ , then sXvX≠εs_Xv_X≠ , hence b¯X=bX∈⟨πX(Q)⟩ b_X=b_X∈ -1.99997pt _X(Q) -1.99997pt . Since bXsX=rX∈⟨πX(Q;P)⟩,b_Xs_X=r_X∈ -1.99997pt _X(Q;P) -1.99997pt , factor bXsX=cXdXb_Xs_X=c_Xd_X with cX∈⟨πX(Q)⟩c_X∈ -1.99997pt _X(Q) -1.99997pt and dX∈⟨πX(P)⟩d_X∈ -1.99997pt _X(P) -1.99997pt . Since bX,cX∈⟨πX(Q)⟩b_X,c_X∈ -1.99997pt _X(Q) -1.99997pt are comparable by the prefix order (as bX⪯cXdXb_X c_Xd_X), prefix-freeness of ⟨πX(Q)⟩ -1.99997pt _X(Q) -1.99997pt forces cX=bXc_X=b_X, hence sX=dX∈⟨πX(P)⟩.s_X=d_X∈ -1.99997pt _X(P) -1.99997pt . Thus vX≠ε⟹sX∈⟨πX(P)⟩v_X≠ s_X∈ -1.99997pt _X(P) -1.99997pt , i.e., the zipper side condition holds for M′=(sXvX)XM =(s_Xv_X)_X with respect to P. It remains to justify the decrease of the secondary induction measure. Recall that m counts the length of the maximal common visible prefix ν1…νm _1… _m of decision-prefix events of this particular while-construct in M, where ν1=⊤ _1= in the present subcase. The first transformation, M⟶M′=(rXvX)X,M\; \;M =(r_Xv_X)_X, removes exactly the first visible decision block D⊤D of this while-construct, by Lemma 7. The second transformation, M′⟶M′=(sXvX)X,M \; \;M =(s_Xv_X)_X, removes the Q-prefix bXb_X from each lifeline via the factorization rX=bXsXr_X=b_Xs_X, where bX∈⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt _ pref and sX∈⟨πX(P)⟩s_X∈ -1.99997pt _X(P) -1.99997pt _ pref. Here Q is the loop body executed after the first ⊤ -decision, whereas P is the recursive continuation of the same while-program after that body iteration. Now bXb_X contains no decision-prefix events of the enclosing while-construct: all such events for the current iteration were already removed in the passage from M to M′M , and every later decision block of the same while occurs only in the recursive continuation P, not in the body prefix Q. Thus removing bXb_X cannot delete any further decision block of this while. It follows that in M′M the first visible decision block ν1=⊤ _1= has disappeared, while the remaining visible decision blocks ν2…νm _2… _m are preserved. Hence the new maximal common visible prefix has length at least m−1m-1. Conversely, its length is at most m−1m-1, because the initial ⊤ -decision block is no longer present in M′M and no new decision-prefix events are introduced by either transformation. Therefore the secondary induction measure of M′M is exactly m−1m-1. The secondary induction hypothesis therefore applies to M′M . Hence there exists a completion S¯=(s¯X)X S=( s_X)_X such that P((sX)X,S¯,V). ZipPost_P((s_X)_X, S,V). Define u¯X=dX⊤b¯Xs¯X, u_X=d_X \, b_X\, s_X, and let U¯=(u¯X)X U=( u_X)_X. For every X, one has uX=dX⊤bXsX⪯dX⊤b¯Xs¯X=u¯Xu_X=d_X b_Xs_X d_X b_X s_X= u_X, and if vX≠εv_X≠ , then b¯X=bX b_X=b_X (from Q((bX)X,U¯Q,(sXvX)X) ZipPost_Q((b_X)_X, U_Q,(s_Xv_X)_X)) and s¯X=sX s_X=s_X (from P((sX)X,S¯,V) ZipPost_P((s_X)_X, S,V)), hence u¯X=uX u_X=u_X. Therefore Condition 1 of P(U,U¯,V) ZipPost_P(U, U,V) holds. Moreover, u¯X∈⟨πX(P)⟩ u_X∈ -1.99997pt _X(P) -1.99997pt for every X, because a ⊤ -decision followed by a Q-trace and then a P-trace is exactly a complete local trace of the projected while-program. Since U¯Q U_Q is a complete MSC and (s¯XvX)X( s_Xv_X)_X is an MSC (from P((sX)X,S¯,V) ZipPost_P((s_X)_X, S,V)), Lemma 1 yields that (b¯Xs¯XvX)X=U¯Q∘(s¯XvX)X( b_X s_Xv_X)_X= U_Q ( s_Xv_X)_X is an MSC. Moreover, U¯=D⊤∘U¯Q∘S¯ U=D U_Q S is a complete MSC, and M¯=(u¯XvX)X=D⊤∘(b¯Xs¯XvX)X M=( u_Xv_X)_X=D ( b_X s_Xv_X)_X is an MSC by another application of Lemma 1, since D⊤D is a complete MSC. In both subcases, we have constructed a tuple U¯=(u¯X)X U=( u_X)_X such that the condition P(U,U¯,V) ZipPost_P(U, U,V) holds. This concludes the while case. Composition case. Let P=Q1;Q2P=Q_1;Q_2. Since we have uX∈⟨πX(Q1;Q2)⟩u_X∈ -1.99997pt _X(Q_1;Q_2) -1.99997pt _ pref, apply Lemma 6 to obtain a factorization uX=uX(1)uX(2),uX(1)∈⟨πX(Q1)⟩,uX(2)∈⟨πX(Q2)⟩,u_X=u_X^(1)u_X^(2), u_X^(1)∈ -1.99997pt _X(Q_1) -1.99997pt _ pref, u_X^(2)∈ -1.99997pt _X(Q_2) -1.99997pt _ pref, with the additional guarantee that uX(2)≠ε⟹uX(1)∈⟨πX(Q1)⟩.u_X^(2)≠ ~ ~u_X^(1)∈ -1.99997pt _X(Q_1) -1.99997pt . We now show that the two IH side conditions hold for this factorization. First side condition (uX(2)vX≠ε⟹uX(1)∈⟨πX(Q1)⟩u_X^(2)v_X≠ u_X^(1)∈ -1.99997pt _X(Q_1) -1.99997pt ). If uX(2)≠εu_X^(2)≠ , this follows directly from the guarantee of Lemma 6. If uX(2)=εu_X^(2)= and vX≠εv_X≠ , then uX=uX(1)u_X=u_X^(1) and the zipper hypothesis gives uX(1)∈⟨πX(Q1;Q2)⟩u_X^(1)∈ -1.99997pt _X(Q_1;Q_2) -1.99997pt . Hence there exist w1∈⟨πX(Q1)⟩w_1∈ -1.99997pt _X(Q_1) -1.99997pt and w2∈⟨πX(Q2)⟩w_2∈ -1.99997pt _X(Q_2) -1.99997pt with uX(1)=w1w2u_X^(1)=w_1w_2. Since uX(1)∈⟨πX(Q1)⟩u_X^(1)∈ -1.99997pt _X(Q_1) -1.99997pt _ pref, there exists t∈⟨πX(Q1)⟩t∈ -1.99997pt _X(Q_1) -1.99997pt with uX(1)⪯tu_X^(1) t. Then w1⪯uX(1)⪯tw_1 u_X^(1) t with w1,t∈⟨πX(Q1)⟩w_1,t∈ -1.99997pt _X(Q_1) -1.99997pt . By prefix-freeness of ⟨πX(Q1)⟩ -1.99997pt _X(Q_1) -1.99997pt , w1=tw_1=t, so uX(1)⪯w1u_X^(1) w_1. Combined with w1⪯uX(1)w_1 u_X^(1), we get uX(1)=w1∈⟨πX(Q1)⟩u_X^(1)=w_1∈ -1.99997pt _X(Q_1) -1.99997pt and w2=εw_2= . Second side condition (vX≠ε⟹uX(2)∈⟨πX(Q2)⟩v_X≠ u_X^(2)∈ -1.99997pt _X(Q_2) -1.99997pt ). Assume vX≠εv_X≠ . Since vX≠εv_X≠ implies uX(2)vX≠εu_X^(2)v_X≠ , the first side condition gives uX(1)∈⟨πX(Q1)⟩u_X^(1)∈ -1.99997pt _X(Q_1) -1.99997pt . The zipper hypothesis gives uX=uX(1)uX(2)∈⟨πX(Q1;Q2)⟩=⟨πX(Q1)⟩⋅⟨πX(Q2)⟩u_X=u_X^(1)u_X^(2)∈ -1.99997pt _X(Q_1;Q_2) -1.99997pt = -1.99997pt _X(Q_1) -1.99997pt · -1.99997pt _X(Q_2) -1.99997pt , so there exist w1′∈⟨πX(Q1)⟩w_1 ∈ -1.99997pt _X(Q_1) -1.99997pt and w2′∈⟨πX(Q2)⟩w_2 ∈ -1.99997pt _X(Q_2) -1.99997pt with uX(1)uX(2)=w1′w2′u_X^(1)u_X^(2)=w_1 w_2 . From uX(1)uX(2)=w1′w2′u_X^(1)u_X^(2)=w_1 w_2 , one of w1′⪯uX(1)w_1 u_X^(1) or uX(1)⪯w1′u_X^(1) w_1 holds (possibly both, when w1′=uX(1)w_1 =u_X^(1)). Since both uX(1)u_X^(1) and w1′w_1 lie in ⟨πX(Q1)⟩ -1.99997pt _X(Q_1) -1.99997pt , prefix-freeness forces w1′=uX(1)w_1 =u_X^(1), hence uX(2)=w2′∈⟨πX(Q2)⟩u_X^(2)=w_2 ∈ -1.99997pt _X(Q_2) -1.99997pt . Write U(1)=(uX(1))XU^(1)=(u_X^(1))_X and W=(uX(2)vX)XW=(u_X^(2)v_X)_X. Apply IH to Q1Q_1 and M=(uX(1)(uX(2)vX))XM=(u_X^(1)(u_X^(2)v_X))_X. This yields Q1(U(1),U¯(1),W) ZipPost_Q_1(U^(1), U^(1),W). In particular, W is an MSC by conditions 2 and 4 of Q1 ZipPost_Q_1 and Lemma 2. For the second IH application, assume vX≠εv_X≠ . Then uX(2)∈⟨πX(Q2)⟩u_X^(2)∈ -1.99997pt _X(Q_2) -1.99997pt by the boundary-aligned choice above. So the side condition for IH on Q2Q_2 holds. Apply IH to Q2Q_2 and W. This yields Q2(U(2),U¯(2),V) ZipPost_Q_2(U^(2), U^(2),V). Setting u¯X=u¯X(1)u¯X(2) u_X= u_X^(1) u_X^(2) gives the required completion for P. Let U¯=(u¯X)X U=( u_X)_X. Completeness of U¯ U follows from completeness of the factors and Lemma 1. Moreover, since U¯(1) U^(1) is a complete MSC and (u¯X(2)vX)X( u_X^(2)v_X)_X is an MSC, Lemma 1 yields that (u¯XvX)X( u_Xv_X)_X is an MSC. Therefore for every X, uX⪯u¯Xu_X u_X: the second IH gives uX(2)⪯u¯X(2)u_X^(2) u_X^(2) unconditionally; when uX(2)vX≠εu_X^(2)v_X≠ , the first IH additionally gives u¯X(1)=uX(1) u_X^(1)=u_X^(1), so uX=uX(1)uX(2)⪯uX(1)u¯X(2)=u¯X(1)u¯X(2)=u¯Xu_X=u_X^(1)u_X^(2) u_X^(1) u_X^(2)= u_X^(1) u_X^(2)= u_X; when uX(2)=εu_X^(2)= and vX=εv_X= , the first IH gives uX=uX(1)⪯u¯X(1)⪯u¯Xu_X=u_X^(1) u_X^(1) u_X. Moreover, if vX≠εv_X≠ , then u¯X(2)=uX(2) u_X^(2)=u_X^(2) (second IH) and uX(2)vX≠εu_X^(2)v_X≠ , so u¯X(1)=uX(1) u_X^(1)=u_X^(1) (first IH), hence u¯X=uX u_X=u_X. Thus Condition 1 of Q1;Q2(U,U¯,V) ZipPost_Q_1;Q_2(U, U,V) holds, and Q1;Q2(U,U¯,V) ZipPost_Q_1;Q_2(U, U,V) holds. 0.A.7 Auxiliary Consequences of ZipPost Lemma 8 If P(U,U¯,V) ZipPost_P(U, U,V) holds, then U is an MSC. Proof(Proof of Lemma 8) Acyclicity and label compatibility are inherited from (uXvX)X(u_Xv_X)_X (an MSC by Condition 3 of P(U,U¯,V) ZipPost_P(U, U,V)) by restriction to prefix events. For the receive-matching condition, suppose that on some channel A→BA→ B, the prefix uBu_B contains more receives than uAu_A contains sends. Since U¯ U is a complete MSC (Condition 2), the completion u¯A u_A must contain an additional send on that channel, hence u¯A≠uA u_A≠ u_A. By Condition 1, this implies vA=εv_A= , so the full word for A in (uXvX)X(u_Xv_X)_X is just uAu_A. But then (uXvX)X(u_Xv_X)_X has an unmatched receive on channel A→BA→ B, contradicting Condition 3. Hence U has no unmatched receives and is therefore an MSC. ∎ Lemma 9 Let P be a well-typed global workflow, and let M=(uX)X∈ℒM=(u_X)_X∈ L be a tuple such that uX∈⟨πX(P)⟩for every X∈ℒ.u_X∈ -1.99997pt _X(P) -1.99997pt every X∈ L. If M is an MSC, then M is a complete MSC. Proof(Proof of Lemma 9) Apply Lemma 5 with U=(uX)XU=(u_X)_X and V=(ε)XV=( )_X. Since each uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt , one has in particular uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt _ pref, and because every vXv_X is ε , the zipper side condition is vacuous. As M=(uX)XM=(u_X)_X is an MSC by hypothesis, Lemma 5 yields a tuple U¯=(u¯X)X U=( u_X)_X such that P(U,U¯,V) ZipPost_P(U, U,V) holds. For every lifeline X, Condition 1 of P(U,U¯,V) ZipPost_P(U, U,V) gives uX⪯u¯Xandu¯X∈⟨πX(P)⟩.u_X u_X u_X∈ -1.99997pt _X(P) -1.99997pt . Since complete local trace languages are prefix-free by Lemma 3, it follows that uX=u¯Xu_X= u_X for every X. Hence U=U¯U= U. Now Condition 2 of P(U,U¯,V) ZipPost_P(U, U,V) states that U¯ U is a complete MSC. Therefore we have that M=UM=U is a complete MSC as well. ∎ Corollary 2 If P(U,U¯,V) ZipPost_P(U, U,V) holds and uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt for every lifeline X, then U is a complete MSC. Proof(Proof of Corollary 2) By Lemma 8, the tuple U=(uX)XU=(u_X)_X is an MSC. Since uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt for every lifeline X, Lemma 9 implies that U is a complete MSC. ∎ 0.A.8 Control Decomposition We use the decision-prefix notation Dν=(dXν)XD^ν=(d_X^ν)_X introduced in the proof of Lemma 5. Lemma 10(Control Decomposition) Let P be a well-typed global workflow. (1) If P=c@BQ⊤Q⊥P= if\ c@B\ then\ Q_ \ else\ Q_ and M^∈⟦P⟧ M∈ _P , then there exist a unique ν∈⊤,⊥ν∈\ , \ and an MSC M^ν∈⟦Qν⟧ M_ν∈ _Q_ν such that M^=Dν∘M^ν. M=D^ν M_ν. (2) If P=c@BQEP= while\ c@B\ do\ Q\ exit\ E and M^∈⟦P⟧ M∈ _P , then there exist k≥0k≥ 0, M^1,…,M^k∈⟦Q⟧ M_1,…, M_k∈ _Q , and M^∈⟦E⟧ M_ex∈ _E such that M^=(D⊤∘M^1)∘⋯∘(D⊤∘M^k)∘(D⊥∘M^). M= (D M_1 ) ·s (D M_k ) (D M_ex ). Proof(Proof of Lemma 10) If-case. By Table 4, for every lifeline X the complete local trace language of πX(P) _X(P) consists of words of the form dXν⋅tXd_X^ν· t_X with ν∈⊤,⊥ν∈\ , \ and tX∈⟨πX(Qν)⟩t_X∈ -1.99997pt _X(Q_ν) -1.99997pt . Hence the X-component of M M starts with dXνXd_X _X for some νX _X. The value νX _X is the same for every X. By Table 4, the owner B’s complete local trace begins with a single control broadcast of some ν∈⊤,⊥ν∈\ , \ to all recipients. By label compatibility of matched send/receive events (Definition 6) and FIFO ordering on each B→XB→ X control channel, every recipient X’s component of M M also begins with ν; idle agents have dXν=εd_X^ν= . Call this common value ν. Write the X-component of M M as dXν⋅tXd_X^ν· t_X (with tX=εt_X= for idle agents where dXν=εd_X^ν= ) and define M^ν=(tX)X M_ν=(t_X)_X, so M^=Dν∘M^ν M=D^ν M_ν. Since DνD^ν is a complete MSC by construction and M M is a complete MSC, Lemma 2 yields that M^ν M_ν is a complete MSC. Each component tX∈⟨πX(Qν)⟩t_X∈ -1.99997pt _X(Q_ν) -1.99997pt , so M^ν∈⟦Qν⟧ M_ν∈ _Q_ν . Uniqueness of M^ν M_ν follows because concatenation with the fixed prefix DνD^ν is injective: if Dν∘N=Dν∘N′D^ν N=D^ν N then N=N′N=N . While-case. We argue by induction on the number k≥0k≥ 0 of ⊤ -decision blocks in the owner B’s component of M M. Base case k=0k=0. Since k=0k=0, the owner B’s component begins with dB⊥d_B (a ⊥ -decision block). By label compatibility (Definition 6) and FIFO ordering on each B→XB→ X control channel, every recipient X’s component of M M also begins with dX⊥d_X ; idle agents have dX⊥=εd_X = . The tuple D⊥=(dX⊥)XD =(d_X )_X is a complete MSC because the control sends on B are matched to the corresponding control receives on each recipient by the FIFO matching of M M. By Table 5, every complete local trace of πX(P) _X(P) that starts with a ⊥ -decision has the form dX⊥⋅eXd_X · e_X with eX∈⟨πX(E)⟩e_X∈ -1.99997pt _X(E) -1.99997pt . Write the X-component of M M as dX⊥⋅eXd_X · e_X (with eX=εe_X= for idle agents where dX⊥=εd_X = ) and define M^=(eX)X M_ex=(e_X)_X, so M^=D⊥∘M M=D M_ex. Since D⊥D is a complete MSC and M M is complete, Lemma 2 yields that M M_ex is a complete MSC with each eX∈⟨πX(E)⟩e_X∈ -1.99997pt _X(E) -1.99997pt , hence M^∈⟦E⟧ M_ex∈ _E . Inductive step k>0k>0. Since k>0k>0, the owner B’s component begins with dB⊤d_B (a ⊤ -decision block). By label compatibility (Definition 6) and FIFO ordering on each B→XB→ X control channel, every recipient X’s component of M M also begins with dX⊤d_X ; idle agents have dX⊤=εd_X = . The tuple D⊤=(dX⊤)XD =(d_X )_X is a complete MSC by the same matching argument. By Table 5, every complete local trace of πX(P) _X(P) that starts with a ⊤ -decision has the form dX⊤⋅sXd_X · s_X with sX∈⟨πX(Q;P)⟩s_X∈ -1.99997pt _X(Q;P) -1.99997pt : after the ⊤ -decision block the body Q executes completely, followed by the recursive continuation P. Write the X-component of M M as dX⊤⋅sXd_X · s_X (with sX=εs_X= for idle agents where dX⊤=εd_X = ) and define N=(sX)XN=(s_X)_X, so M^=D⊤∘N M=D N. Since D⊤D is a complete MSC and M M is complete, Lemma 2 yields that N is a complete MSC with sX∈⟨πX(Q;P)⟩s_X∈ -1.99997pt _X(Q;P) -1.99997pt for every X. Since sX∈⟨πX(Q;P)⟩s_X∈ -1.99997pt _X(Q;P) -1.99997pt , the semantics of sequential composition gives a factorization sX=bXwXs_X=b_Xw_X with bX∈⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt and wX∈⟨πX(P)⟩w_X∈ -1.99997pt _X(P) -1.99997pt . The factorization is unique by prefix-freeness of ⟨πX(Q)⟩ -1.99997pt _X(Q) -1.99997pt (Lemma 3). Apply Lemma 5 to Q with U=(bX)XU=(b_X)_X and V=(wX)XV=(w_X)_X. The prefix condition bX∈⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt _ pref holds since bX∈⟨πX(Q)⟩⊆⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt -1.99997pt _X(Q) -1.99997pt _ pref. The zipper side condition wX≠ε⟹bX∈⟨πX(Q)⟩w_X≠ b_X∈ -1.99997pt _X(Q) -1.99997pt holds trivially since bX∈⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt for every X. The tuple (bXwX)X=N(b_Xw_X)_X=N is an MSC by the above. The lemma yields U¯ U with Q(U,U¯,V) ZipPost_Q(U, U,V). Since bX∈⟨πX(Q)⟩b_X∈ -1.99997pt _X(Q) -1.99997pt for every X, Corollary 2 gives that M^1=(bX)X M_1=(b_X)_X is a complete MSC, hence M^1∈⟦Q⟧ M_1∈ _Q . Since N=M^1∘WN= M_1 W with W=(wX)XW=(w_X)_X and both N and M^1 M_1 complete MSCs, Lemma 2 yields that W is a complete MSC. For each X, wX∈⟨πX(P)⟩w_X∈ -1.99997pt _X(P) -1.99997pt , so W∈⟦P⟧W∈ _P . The owner’s component in W contains exactly k−1k-1 ⊤ -decision blocks: the first block dB⊤d_B was consumed in passing from M M to N, and the B-component of M^1 M_1 lies in ⟨πB(Q)⟩ -1.99997pt _B(Q) -1.99997pt and contains no κP _ ctrl^P-tagged events. Applying the induction hypothesis to W yields W=(D⊤∘M^2)∘⋯∘(D⊤∘M^k)∘(D⊥∘M^).W= (D M_2 ) ·s (D M_k ) (D M_ex ). Prepending D⊤∘M^1D M_1 gives M^=D⊤∘N=D⊤∘M^1∘W=(D⊤∘M^1)∘⋯∘(D⊤∘M^k)∘(D⊥∘M^), M=D N=D M_1 W= (D M_1 ) ·s (D M_k ) (D M_ex ), which is the desired factorization. ∎ 0.A.9 Proof of Theorem 5.1 Fix a well-typed global workflow P over lifelines ℒ L. We prove the two items. (1) Completeness of realization. We show: for every M∈⟦P⟧M∈ P there exists M^∈⟦P⟧ M∈ _P with (M^)=M erase( M)=M. Proceed by structural induction on P. Base cases: ε , msg, act. If P=εP= , take M^=Mε M=M_ . If P is msg/ act, then πX(P) _X(P) produces exactly the corresponding local letters on the endpoints/owner and ε elsewhere, so the unique global one-step MSC (for that statement) is realized directly. No control letters occur, and thus erase is the identity. If-construct. Let P=c@BQ⊤Q⊥P= if\ c@B\ then\ Q_ \ else\ Q_ and M∈⟦P⟧M∈ P . Then either M=M⊤(c@B)B∘M⊤M=M_ if_ (c@B)^B M_ with M⊤∈⟦Q⊤⟧M_ ∈ Q_ or M=M⊥(c@B)B∘M⊥M=M_ if_ (c@B)^B M_ with M⊥∈⟦Q⊥⟧M_ ∈ Q_ . Assume the ⊤ -case; the other case is analogous. By IH applied to Q⊤Q_ , obtain M^⊤∈⟦Q⊤⟧ M_ ∈ _Q_ with (M^⊤)=M⊤ erase( M_ )=M_ . Let M^=D⊤∘M^⊤ M=D M_ , where D⊤D is the complete decision block consisting of the owner-side choice event on B, the projection-introduced control sends on B, and the matching control receives on all recipients A∈(ℒ(Q⊤)∪ℒ(Q⊥))∖BA∈( L(Q_ )∪ L(Q_ )) \B\. The prepended decision block is a complete MSC, and M^⊤ M_ is a complete MSC by IH because it lies in ⟦Q⊤⟧ _Q_ . Hence Lemma 1 yields that M M is a complete MSC. Therefore M^∈⟦P⟧ M∈ _P by definition of the projections πX(P) _X(P) and the local trace semantics, and erasing the control letters yields exactly M⊤(c@B)B∘M⊤=M_ if_ (c@B)^B M_ =M. While-construct. Let P=c@BQEP= while\ c@B\ do\ Q\ exit\ E and M∈⟦P⟧M∈ P . Then M has the shape M=(M⊤(c@B)B∘M1)∘⋯∘(M⊤(c@B)B∘Mk)∘(M⊥(c@B)B∘M)M= (M_ while_ (c@B)^B M_1 ) ·s (M_ while_ (c@B)^B M_k ) (M_ while_ (c@B)^B M_ex ) for some k≥0k≥ 0, where each Mi∈⟦Q⟧M_i∈ Q and M∈⟦E⟧M_ex∈ E . Apply IH to each MiM_i and M_ex to obtain realizations M^i∈⟦Q⟧ M_i∈ _Q and M^∈⟦E⟧ M_ex∈ _E that erase to the corresponding global MSCs. In each body iteration prepend, on B, the choice letter ⊤(c@B) while_ (c@B) followed by the projection-introduced decision broadcasts to all A∈ℛ=(ℒ(Q)∪ℒ(E))∖BA =( L(Q)∪ L(E)) \B\. For the exit prepend ⊥(c@B) while_ (c@B) on B and the corresponding broadcasts. (When ℛ=∅R= there are no broadcasts, but the choice letter is still prepended on B.) Concatenate the resulting MSCs. Each prepended decision block is a complete MSC, and each realized body/exit fragment is a complete MSC by IH. Repeated application of Lemma 1 therefore shows that the concatenation is a complete MSC. By construction this yields M^∈⟦P⟧ M∈ _P , and erasing the κP _ ctrl^P broadcasts (the only events removed by erase) yields exactly M. Composition. Let P=P1;P2P=P_1;P_2 and M∈⟦P⟧M∈ P . Then M=M1∘M2M=M_1 M_2 with M1∈⟦P1⟧M_1∈ P_1 and M2∈⟦P2⟧M_2∈ P_2 . By IH, obtain M^1∈⟦P1⟧ M_1∈ _P_1 and M^2∈⟦P2⟧ M_2∈ _P_2 such that (M^i)=Mi erase( M_i)=M_i. Let M^=M^1∘M^2 M= M_1 M_2. Since M^1 M_1 and M^2 M_2 are complete MSCs, Lemma 1 shows that M M is again a complete MSC. By the definition of ; in the MSC semantics, M^∈⟦P1;P2⟧=⟦P⟧ M∈ _P_1;P_2 = _P . Moreover (M^)=M erase( M)=M. This concludes (1). (2) Soundness of realization. We show: for every M^∈⟦P⟧ M∈ _P , (M^)∈⟦P⟧ erase( M)∈ P . Proceed by structural induction on P. Base cases and control cases. For P=εP= and for P equal to msg/ act, projection introduces no control letters and erase is the identity. The result follows immediately from the correspondence between projection and the canonical one-step MSCs. For the if-case, let P=c@BQ⊤Q⊥.P= if\ c@B\ then\ Q_ \ else\ Q_ . By Lemma 10, every M^∈⟦P⟧ M∈ _P has the form M^=Dν∘M^ν M=D^ν M_ν for a unique ν∈⊤,⊥ν∈\ , \ and some M^ν∈⟦Qν⟧ M_ν∈ _Q_ν . The erasure map deletes only the control broadcasts inside DνD^ν, leaving exactly the corresponding global choice MSC M⊤(c@B)BM_ if_ (c@B)^B or M⊥(c@B)BM_ if_ (c@B)^B. Since M^∈⟦P⟧ M∈ _P is a complete MSC, Lemma 4 gives that (M^) erase( M) is a complete MSC. By IH, (M^ν)∈⟦Qν⟧ erase( M_ν)∈ Q_ν . Hence (M^)∈⟦P⟧. erase( M)∈ P . For the while-case, let P=c@BQE.P= while\ c@B\ do\ Q\ exit\ E. By Lemma 10, every M^∈⟦P⟧ M∈ _P decomposes as M^=(D⊤∘M^1)∘⋯∘(D⊤∘M^k)∘(D⊥∘M^) M= (D M_1 ) ·s (D M_k ) (D M_ex ) for some k≥0k≥ 0, with each M^i∈⟦Q⟧ M_i∈ _Q and M^∈⟦E⟧ M_ex∈ _E . Erasing the κP _ ctrl^P-messages removes only the control broadcasts inside the decision blocks D⊤,D⊥D ,D , leaving the corresponding owner choice events M⊤(c@B)BM_ while_ (c@B)^B and M⊥(c@B)BM_ while_ (c@B)^B. By IH, (M^i)∈⟦Q⟧and(M^)∈⟦E⟧. erase( M_i)∈ Q erase( M_ex)∈ E . Since M^∈⟦P⟧ M∈ _P is a complete MSC, Lemma 4 gives that (M^) erase( M) is a complete MSC. Therefore (M^) erase( M) has exactly the global while-shape from Definition 8, so (M^)∈⟦P⟧ erase( M)∈ P . Composition. Let P=P1;P2P=P_1;P_2 and M^=(wX)X∈⟦P⟧ M=(w_X)_X∈ _P . Then we have wX∈⟨πX(P1);πX(P2)⟩w_X∈ -1.99997pt _X(P_1); _X(P_2) -1.99997pt , so factor wX=uXvXw_X=u_Xv_X with uX∈⟨πX(P1)⟩u_X∈ -1.99997pt _X(P_1) -1.99997pt and vX∈⟨πX(P2)⟩v_X∈ -1.99997pt _X(P_2) -1.99997pt . Thus the zipper side condition vX≠ε⟹uX∈⟨πX(P1)⟩v_X≠ u_X∈ -1.99997pt _X(P_1) -1.99997pt holds trivially. Since M M is complete, it is in particular an MSC. Thus ⊲M _ M is defined and the causality order is acyclic (Definition 6), so Lemma 5 applies. Applying Lemma 5 to M^=(uXvX)X M=(u_Xv_X)_X yields that V=(vX)XV=(v_X)_X is an MSC. Also, U=(uX)XU=(u_X)_X is a complete MSC by Corollary 2 (since each uX∈⟨πX(P1)⟩u_X∈ -1.99997pt _X(P_1) -1.99997pt ), hence U∈⟦P1⟧U∈ _P_1 . Since U and M^=U∘V M=U V are both complete MSCs, Lemma 2 yields that V is a complete MSC. Moreover V∈⟦P2⟧V∈ _P_2 since each vX∈⟨πX(P2)⟩v_X∈ -1.99997pt _X(P_2) -1.99997pt by the sequential composition semantics. By IH, (U)∈⟦P1⟧ erase(U)∈ P_1 and (V)∈⟦P2⟧ erase(V)∈ P_2 . Finally, (M^)=(U)∘(V) erase( M)= erase(U) erase(V), hence we have (M^)∈⟦P1;P2⟧=⟦P⟧ erase( M)∈ P_1;P_2 = P . This concludes (2). 0.A.10 Proof of Corollary 1 Let M=(uX)X∈⟦P⟧M=(u_X)_X∈ _P _ pref. By definition of prefix semantics, uX∈⟨πX(P)⟩u_X∈ -1.99997pt _X(P) -1.99997pt _ pref for every X∈ℒX∈ L, and M is an MSC. Apply Lemma 5 with U=(uX)XU=(u_X)_X and V=(ε)XV=( )_X. The zipper side condition is vacuous since vX=εv_X= for all X. Hence the lemma yields U¯=(u¯X)X U=( u_X)_X with P(U,U¯,V) ZipPost_P(U, U,V). By Condition 1, uX⪯u¯Xu_X u_X and u¯X∈⟨πX(P)⟩ u_X∈ -1.99997pt _X(P) -1.99997pt for every X. By Condition 2, U¯ U is a complete MSC, hence U¯∈⟦P⟧ U∈ _P , and M=(uX)X⪯(u¯X)X=U¯.M=(u_X)_X ( u_X)_X= U. This is exactly Definition 11. ∎