∃$\exists$ ∀$\forall$ θ$\theta$ τ$\tau$ φ$\varphi$ ξ$\xi$ ζ$\zeta$ ψ$\psi$
π$\pi$ α$\alpha$ β$\beta$ γ$\gamma$ δ$\delta$ ε$\varepsilon$ κ$\kappa$
λ$\lambda$ μ$\mu$ ρ$\rho$ σ$\sigma$ ω$\omega$ Γ$\Gamma$ Φ$\Phi$ Δ$\Delta$
Σ$\Sigma$ Π$\Pi$ ∑$\Sigma$ ∏$\Pi$ Θ$\Theta$ Ω$\Omega$ ⇒$\Rightarrow$
⇐$\Leftarrow$ ⇔$\Leftrightarrow$ →$\rightarrow$ ←$\leftarrow$
↔$\leftrightarrow$ ¬$\neg$ ∧$\land$ ∨$\lor$ ≠$\neq$ ≡$\equiv$ ∼$\sim$
≈$\approx$ ≥$\geq$ ≤$\leq$ ≫$\gg$ ≪$\ll$ ∅$\emptyset$ ⊆$\subseteq$ ⊂$\subset$
∩$\cap$ ⋂$\cap$ ∪$\cup$ ⋃$\cup$ ⊎$\uplus$ ∈$\in$ ∉$\not\in$ ⊤$\top$ ⊥$\bot$ ₀0
₁1 ₂2 ₃3 ₄4 ₅5 ₆6 ₇7 ₈8 ₉9 ⁰0 ¹1 ²2 ³3 ⁴4 ⁵5 ⁶6 ⁷7 ⁸8 ⁹9 𝔹$\mathbb{B}$
ℝ$\mathbb{R}$ ℕ$\mathbb{N}$ ℂ$\mathbb{C}$ ℚ$\mathbb{Q}$ 𝕋$\mathbb{T}$
𝕏$\mathbb{X}$ ℤ$\mathbb{Z}$ ✓51 ✗55 ◊$\lozenge$ □$\square$ 𝓐$\mathcal{A}$
𝓑$\mathcal{B}$ 𝓒$\mathcal{C}$ 𝓓$\mathcal{D}$ 𝓔$\mathcal{E}$ 𝓕$\mathcal{F}$
𝓖$\mathcal{G}$ 𝓗$\mathcal{H}$ 𝓘$\mathcal{I}$ 𝓙$\mathcal{J}$ 𝓚$\mathcal{K}$
𝓛$\mathcal{L}$ 𝓜$\mathcal{M}$ 𝓝$\mathcal{N}$ 𝓞$\mathcal{O}$ 𝓟$\mathcal{P}$
𝓠$\mathcal{Q}$ 𝓡$\mathcal{R}$ 𝓢$\mathcal{S}$ 𝓣$\mathcal{T}$ 𝓤$\mathcal{U}$
𝓥$\mathcal{V}$ 𝓦$\mathcal{W}$ 𝓧$\mathcal{X}$ 𝓨$\mathcal{Y}$ 𝓩$\mathcal{Z}$
…$\ldots$ ∗$\ast$ ⊢$\vdash$ ⊧$\models$ ′′ ″′′ ‴′′′ ∥$\|$ ⊕$\oplus$ ⁺+
⊇$\supseteq$ ∘$\circ$ ∙$\cdot$ ⋅$\cdot$ ≈$\approx$ ×$\times$ ∞$\infty$
⊑$\sqsubseteq$

11institutetext: New York University 11email<EMAIL_ADDRESS><EMAIL_ADDRESS>22institutetext: Max Planck Institute for Software Systems 22email:
<EMAIL_ADDRESS>33institutetext: SonarSource 33email:
<EMAIL_ADDRESS>
# Complete Multiparty Session Type Projection with Automata

Authors withheld  Elaine Li equal contribution11 Felix Stutz* 22 Thomas Wies
11 Damien Zufferey 33

###### Abstract

Multiparty session types (MSTs) are a type-based approach to verifying
communication protocols. Central to MSTs is a _projection operator_ : a
partial function that maps protocols represented as global types to correct-
by-construction implementations for each participant, represented as a
communicating state machine. Existing projection operators are syntactic in
nature, and trade efficiency for completeness. We present the first projection
operator that is sound, complete, and efficient. Our projection separates
synthesis from checking implementability. For synthesis, we use a simple
automata-theoretic construction; for checking implementability, we present
succinct conditions that summarize insights into the property of
implementability. We use these conditions to show that MST implementability is
PSPACE-complete. This improves upon a previous decision procedure that is in
EXPSPACE and applies to a smaller class of MSTs. We demonstrate the
effectiveness of our approach using a prototype implementation, which handles
global types not supported by previous work without sacrificing performance.

###### Keywords:

Protocol verification Multiparty session types Communicating state machines
Protocol fidelity Deadlock freedom.

##  1 Introduction

Communication protocols are key components in many safety and operation
critical systems, making them prime targets for formal verification.
Unfortunately, most verification problems for such protocols (e.g. deadlock
freedom) are undecidable [11]. To make verification computationally tractable,
several restrictions have been proposed [14, 10, 3, 2, 32, 42]. In particular,
multiparty session types (MSTs) [24] have garnered a lot of attention in
recent years (see, e.g., the survey by Ancona et al. [6]). In the MST setting,
a protocol is specified as a global type, which describes the desired
interactions of all roles involved in the protocol. Local implementations
describe behaviors for each individual role. The implementability problem for
a global type asks whether there exists a collection of local implementations
whose composite behavior when viewed as a communicating state machine (CSM)
matches that of the global type and is deadlock-free. The synthesis problem is
to compute such an implementation from an implementable global type.

MST-based approaches typically solve synthesis and implementability
simultaneously via an efficient syntactic _projection operator_ [24, 18, 41,
33]. Abstractly, a projection operator is a partial map from global types to
collections of implementations. A projection operator proj is sound when every
global type $\mathbf{G}$ in its domain is implemented by
$\texttt{proj}(\mathbf{G})$, and complete when every implementable global type
is in its domain. Existing practical projection operators for MSTs are all
incomplete (or unsound). Recently, the implementability problem was shown to
be decidable for a class of MSTs via a reduction to safe realizability of
globally cooperative high-level message sequence charts (HMSCs) [38]. In
principle, this result yields a complete and sound projection operator for the
considered class. However, this operator would not be practical. In
particular, the proposed implementability check is in EXPSPACE.

Contributions. In this paper, we present the first practical sound and
complete projection operator for general MSTs. The synthesis problem for
implementable global types is conceptually easy [38] – the challenge lies in
determining whether a global type _is_ implementable. We thus separate
synthesis from checking implementability. We first use a standard automata-
theoretic construction to obtain a candidate implementation for a potentially
non-implementable global type. However, unlike [38], we then verify the
correctness of this implementation directly using efficiently checkable
conditions derived from the global type. When a global type is not
implementable, our constructive completeness proof provides a counterexample
trace.

The resulting projection operator yields a PSPACE decision procedure for
implementability. In fact, we show that the implementability problem is
PSPACE-complete. These results both generalize and tighten the decidability
and complexity results obtained in [38].

We evaluate a prototype of our projection algorithm on benchmarks taken from
the literature. Our prototype benefits from both the efficiency of existing
lightweight but incomplete syntactic projection operators[24, 18, 41, 33], and
the generality of heavyweight automata-based model checking techniques [35,
28]: it handles protocols rejected by previous practical approaches while
preserving the efficiency that makes MST-based techniques so attractive.

##  2 Motivation and Overview

(a) Odd-even protocol

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}?{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$

(b) Local impl.
for role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$

(c) Local impl.
for role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$

$\\{\textnormal{L}_{1},\textnormal{R}_{1},\textnormal{R}_{2},\textnormal{R}_{4}\\}$$\\{\textnormal{L}_{2},\textnormal{L}_{4},\textnormal{R}_{3}\\}$$\\{\textnormal{L}_{3},\textnormal{R}_{2},\textnormal{R}_{4}\\}$$\\{\textnormal{L}_{5}\\}$$\\{\textnormal{L}_{6}\\}$$\\{\textnormal{R}_{5}\\}$$\\{\textnormal{R}_{6}\\}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$

(d) Local impl.
for role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$

Figure 1: Odd-even: An implementable but not (yet) projectable protocol and
its local implementations

Incompleteness of existing projection operators. A key limitation of existing
projection operators is that the implementation for each role is obtained via
a linear traversal of the global type, and thus shares its structure. The
following example, which is not projectable by any existing approach,
demonstrates how enforcing structural similarity can lead to incompleteness.

######  Example 1 (Odd-even)

Consider the following global type $\mathbf{G}_{oe}$:

$+\;\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,\mu
t_{1}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,t_{1}\;+\;{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0)\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,\mu
t_{2}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,t_{2}\;+\;{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,0)\end{cases}$

A term
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!m$
specifies the exchange of message $m$ between sender
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and receiver
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
The term represents two local events observed separately due to asynchrony: a
send event
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m$
observed by role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
and a receive event
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m$
observed by role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
The $+$ operator denotes choice, $\mu t.\,G$ denotes recursion, and $0$
denotes protocol termination.

Fig. 1(a) visualizes $\mathbf{G}_{oe}$ as an HMSC. The left and right sub-
protocols respectively correspond to the top and bottom branches of the
protocol. Role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
chooses a branch by sending either
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ or
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
On the left,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
echoes this message to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$.
Both branches continue in the same way:
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
sends an arbitrary number of
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
messages to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
each of which is forwarded twice from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$.
Role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
signals the end of the loop by sending
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$ to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
which
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
forwards to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$.
Finally, depending on the branch,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
must send
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ or
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.

Figs. 1(b) and 1(c) depict the structural similarity between the global type
$\mathbf{G}_{oe}$ and the implementations for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
For the “choicemaker” role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
the reason is evident. Role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$’s
implementation collapses the continuations of both branches in the protocol
into a single sub-component. For
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
(Fig. 1(d)), the situation is more complicated. Role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
does not decide on or learn directly which branch is taken, but can deduce it
from the parity of the number of
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
messages received from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$:
odd means left and even means right. The resulting local implementation
features transitions going back and forth between the two branches that do not
exist in the global type. Syntactic projection operators fail to create such
transitions. $\blacktriangleleft$

One response to the brittleness of existing projection operators has been to
give up on global type specifications altogether and instead revert to model
checking user-provided implementations [35, 28]. We posit that what needs
rethinking is not the concept of global types, but rather how projections are
computed and how implementability is checked.

Our automata-theoretic approach. The synthesis step in our projection operator
uses textbook automata-theoretic constructions. From a given global type, we
derive a finite state machine, and use it to define a homomorphism automaton
for each role. We then determinize this homomorphism automaton via subset
construction to obtain a local candidate implementation for each role. If the
global type is implementable, this construction always yields an
implementation. The implementations shown in Figs. 1(b), 1(c), and 1(d) are
the result of applying this construction to $\mathbf{G}_{oe}$ from Example 1.
Notice that the state labels in Fig. 1(d) correspond to sets of labels in the
global protocol.

Unfortunately, not all global types are implementable.

(a) $\mathbf{G}_{r}$

(b) $\mathbf{G}_{r}^{\prime}$

(c) $\mathbf{G}_{s}$

(d) $\mathbf{G}_{s}^{\prime}$

Figure 2: High-level message sequence charts for the global types of Example
2.

###### Example 2

Consider the following four global types also depicted in Fig. 2:

$\displaystyle\mathbf{G}_{r}={}$
$\displaystyle+\;\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0\end{cases}$
$\displaystyle\qquad\mathbf{G}_{s}={}$
$\displaystyle+\;\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,0\end{cases}$
$\displaystyle\mathbf{G}_{r}^{\prime}={}$
$\displaystyle+\;\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0\end{cases}$
$\displaystyle\qquad\mathbf{G}_{s}^{\prime}={}$
$\displaystyle+\;\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,0\end{cases}$

Similar to $\mathbf{G}_{oe}$, in all four examples,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
chooses a branch by sending either
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ or
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
The global type $\mathbf{G}_{r}$ is not implementable because
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
cannot learn which branch was chosen by
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.
For any local implementation of
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
to be able to execute both branches, it must be able to receive
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
in any order. Because the two send events
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
are independent of each other, they may be reordered. Consequently, any
implementation of $\mathbf{G}_{r}$ would have to permit executions that are
consistent with global behaviors not described by $\mathbf{G}_{r}$, such as
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$.
Contrast this with $\mathbf{G}_{r}^{\prime}$, which is implementable. In the
top branch of $\mathbf{G}_{r}^{\prime}$, role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
can only send to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
after it has received from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$,
which prevents the reordering of the send events
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$.
The bottom branch is symmetric. Hence,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
learns
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$’s
choice based on which message it receives first.

For the global type $\mathbf{G}_{s}$, role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
again cannot learn the branch chosen by
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.
That is,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
cannot know whether to send
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ or
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
leading inevitably to deadlocking executions. In contrast,
$\mathbf{G}_{s}^{\prime}$ is again implementable because the expected behavior
of
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
is independent of the choice by
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.
$\blacktriangleleft$

These examples show that the implementability question is non-trivial. To
check implementability, we present conditions that precisely characterize when
the subset construction for $\mathbf{G}$ yields an implementation.

Overview. The rest of the paper is organized as follows. §3 contains relevant
definitions for our work. §4 describes the synthesis step of our projection.
§5 presents the two conditions that characterize implementability of a given
global type. In §6, we prove soundness of our projection via a stronger
inductive invariant guaranteeing per-role agreement on a global run of the
protocol. In §7, we prove completeness by showing that our two conditions hold
if a global type is implementable. In §8, we discuss the complexity of our
construction and condition checks. §9 presents our artifact and evaluation,
and §10 as well as §11 discuss related work.

##  3 Preliminaries

##### Words.

Let $\Sigma$ be a finite alphabet. $\Sigma^{*}$ denotes the set of finite
words over $\Sigma$, $\Sigma^{\omega}$ the set of infinite words, and
$\Sigma^{\infty}\negthinspace$ their union $\Sigma^{*}\cup\Sigma^{\omega}$. A
word $u\in\Sigma^{*}$ is a _prefix_ of word $v\in\Sigma^{\infty}$, denoted
$u\leq v$, if there exists $w\in\Sigma^{\infty}$ with $u\cdot w=v$.

##### Message Alphabet.

Let $\mathcal{P}$ be a set of roles and $\mathcal{V}$ be a set of messages. We
define the set of _synchronous events_
$Σ_{\mathit{sync}}\coloneq\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!m\mid{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}∈\mathcal{P}\text{
and }m∈\mathcal{V}\\}$ where
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!m$
denotes that message $m$ is sent by
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
atomically. This is split for _asynchronous events_. For a role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}$,
we define the alphabet
$\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},!}=\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m\mid{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\in\mathcal{P},\;m\in\mathcal{V}\\}$
of _send_ events and the alphabet
$\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},?}=\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m\mid{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\in\mathcal{P},\;m\in\mathcal{V}\\}$
of _receive_ events. The event
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m$
denotes role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
sending a message $m$ to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m$
denotes role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
receiving a message $m$ from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
We write
$\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}=\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},!}\cup\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},?}$,
$\Sigma_{!}=\bigcup_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},!}$,
and
$\Sigma_{?}=\bigcup_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},?}$.
Finally, $Σ_{\mathit{async}}=\Sigma_{!}\cup\Sigma_{?}$. We say that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is _active_ in $x\in Σ_{\mathit{async}}$ if
$x\in\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$.
For each role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}$,
we define a homomorphism
${\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$,
where
$x{\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}=x$
if
$x\in\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and $\varepsilon$ otherwise. We write $\mathcal{V}(w)$ to project the send and
receive events in $w$ onto their messages. We fix $\mathcal{P}$ and
$\mathcal{V}$ in the rest of the paper.

##### Global Types – Syntax.

Global types for MSTs [30] are defined by the grammar:

$\displaystyle G$ $\displaystyle\Coloneqq 0\hskip 3.0pt\mid\hskip
3.0pt\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!:\\!m_{i}.G_{i}\hskip
3.0pt\mid\hskip 3.0pt\mu t.\;G\hskip 3.0pt\mid\hskip 3.0ptt$

where
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}$
range over $\mathcal{P}$, $m_{i}$ over $\mathcal{V}$, and $t$ over a set of
recursion variables.

We require each branch of a choice to be distinct:
$∀i,j∈I.\,i≠j⇒({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i},m_{i})≠({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{j},m_{j})$,
the sender and receiver of an atomic action to be distinct:
$∀i∈I.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}≠{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}$,
and recursion to be guarded: in $μt.\,G$, there is at least one message
between $μt$ and each $t$ in $G$. When $|I|=1$, we omit $\sum$. For
readability, we sometimes use the infix operator $+$ for choice, instead of
$\sum$. When working with a protocol described by a global type, we write
$\mathbf{G}$ to refer to the top-level type, and we use $G$ to refer to its
subterms. For the size of a global type, we disregard multiple occurrences of
the same subterm.

We use the extended definition of global types from [30] that allows a sender
to send messages to different roles in a choice. We call this _sender-driven
choice_ , as in [38], while it was called generalized choice in [30]. This
definition subsumes classical MSTs that only allow _directed choice_ [24]. The
types we use focus on communication primitives and omit features like
delegation or parametrization. We defer a detailed discussion of different MST
frameworks to Section 11.

##### Global Types – Semantics.

As a basis for the semantics of a global type $\mathbf{G}$, we construct a
finite state machine
$\mathsf{GAut}(\mathbf{G})=(Q_{\mathbf{G}},Σ_{\mathit{sync}},δ_{\mathbf{G}},q_{0,\mathbf{G}},F_{\mathbf{G}})$
where

  * •

$Q_{\mathbf{G}}$ is the set of all syntactic subterms in $\mathbf{G}$ together
with the term $0$,

  * •

$δ_{\mathbf{G}}$ is the smallest set containing
$(\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!:\\!m_{i}.G_{i},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!:\\!m_{i},G_{i})$
for each $i∈I$, as well as $(μt.G^{\prime},ε,G^{\prime})$ and
$(t,ε,μt.G^{\prime})$ for each subterm $\mu t.G^{\prime}$,

  * •

$q_{0,\mathbf{G}}=\mathbf{G}$ and $F_{\mathbf{G}}=\\{0\\}$.

We define a homomorphism split onto the asynchronous alphabet:

$\texttt{split}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!m)\coloneq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m\enspace.$

The semantics $\mathcal{L}(\mathbf{G})$ of a global type $\mathbf{G}$ is given
by
$\mathcal{C}^{\sim}(\texttt{split}(\mathcal{L}(\mathsf{GAut}(\mathbf{G}))))$
where $\mathcal{C}^{\sim}$ is the closure under the indistinguishability
relation $\sim$ [30]. Two events are independent if they are not related by
the _happened-before_ relation [26]. For instance, any two send events from
distinct senders are independent. Two words are indistinguishable if one can
be reordered into the other by repeatedly swapping consecutive independent
events. The full definition is in Section 0.A.2.

##### Communicating State Machine [11].

$\mathcal{A}=\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
is a CSM over $\mathcal{P}$ and $\mathcal{V}$ if
${A}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is a finite state machine over
$\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
for every
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}$,
denoted by
$(Q_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},q_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}},F_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$.
Let
$\prod_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}s_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
denote the set of global states and
$\mathsf{Chan}=\\{({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})\mid{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\in\mathcal{P},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\}$
denote the set of channels. A  _configuration_ of $\mathcal{A}$ is a pair
$(\vec{s},\xi)$, where $\vec{s}\,$ is a global state and
$\xi:\mathsf{Chan}\rightarrow\mathcal{V}^{*}$ is a mapping from each channel
to a sequence of messages. We use
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
to denote the state of
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
in $\vec{s}$. The CSM transition relation, denoted $\rightarrow$, is defined
as follows.

  * •

$(\vec{s},\xi)\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m}(\vec{s}\mkern
2.0mu\vphantom{s}^{\prime},\xi^{\prime})$ if
$(\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m,\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}=\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
for every role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
$\xi^{\prime}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})=\xi({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})\cdot
m$ and $\xi^{\prime}(c)=\xi(c)$ for every other channel $c\in\mathsf{Chan}$.

  * •

$(\vec{s},\xi)\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m}(\vec{s}\mkern
2.0mu\vphantom{s}^{\prime},\xi^{\prime})$ if
$(\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m,\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}=\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
for every role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
$\xi({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})=m\cdot\xi^{\prime}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})$
and $\xi^{\prime}(c)=\xi(c)$ for every other channel $c\in\mathsf{Chan}$.

In the initial configuration $(\vec{s}_{0},\xi_{0})$, each role’s state in
$\vec{s}_{0}$ is the initial state
$q_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
of
$A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
and $\xi_{0}$ maps each channel to $\varepsilon$. A configuration
$(\vec{s},\xi)$ is said to be _final_ iff
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is final for every
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and $\xi$ maps each channel to $\varepsilon$. Runs and traces are defined in
the expected way. A run is _maximal_ if either it is finite and ends in a
final configuration, or it is infinite. The language
$\mathcal{L}(\mathcal{A})$ of the CSM $\mathcal{A}$ is defined as the set of
maximal traces. A configuration $(\vec{s},\xi)$ is a _deadlock_ if it is not
final and has no outgoing transitions. A CSM is _deadlock-free_ if no
reachable configuration is a deadlock.

Finally, implementability is formalized as follows.

######  Definition 1 (Implementability [30])

A global type $\mathbf{G}$ is _implementable_ if there exists a CSM
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
such that the following two properties hold:
(i) _protocol fidelity_ :
$\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})=\mathcal{L}(\mathbf{G})$,
and  (ii) _deadlock freedom_ :
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
is deadlock-free.  We say that
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
implements $\mathbf{G}$.

##  4 Synthesizing Implementations

The construction is carried out in two steps. First, for each role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}$,
we define an intermediate state machine
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
that is a homomorphism of $\mathsf{GAut}(\mathbf{G})$. We call
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
the _projection by erasure_ for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
defined below.

######  Definition 2 (Projection by Erasure)

Let $\mathbf{G}$ be some global type with its state machine
$\mathsf{GAut}(\mathbf{G})=(Q_{\mathbf{G}},Σ_{\mathit{sync}},\delta_{\mathbf{G}},q_{0,\mathbf{G}},F_{\mathbf{G}})$.
For each role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}$,
we define the state machine
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\,=(Q_{\mathbf{G}},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\uplus\\{\varepsilon\\},\delta_{\downarrow},q_{0,\mathbf{G}},F_{\mathbf{G}})$
where
$\delta_{\downarrow}\coloneq\\{q\xrightarrow{\texttt{split}(a){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}}q^{\prime}\mid
q\xrightarrow{a}q^{\prime}\in\delta_{\mathbf{G}}\\}$. By definition of
$\texttt{split}(\hbox{-})$, it holds that
$\texttt{split}(a){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\in\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\uplus\\{\varepsilon\\}$.

Then, we determinize
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
via a standard subset construction to obtain a deterministic local state
machine for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.

######  Definition 3 (Subset Construction)

Let $\mathbf{G}$ be a global type and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be a role. Then, the _subset construction_ for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is defined as

$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})=\bigl{(}Q_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}},s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}},F_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\bigr{)}\text{
where }$

  * •

$\delta(s,a)\coloneq\\{q^{\prime}\in Q_{\mathbf{G}}\mid\exists q\in
s,q\xrightarrow{a}\xrightarrow{\varepsilon}\mathrel{\vphantom{\to}{}^{*}}q^{\prime}\in\delta_{\downarrow}\\},$
for every $s\subseteq Q_{\mathbf{G}}$ and
$a\in\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$

  * •

$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\coloneq\\{q\in
Q_{\mathbf{G}}\mid
q_{0,\mathbf{G}}\xrightarrow{\varepsilon}\mathrel{\vphantom{\to}{}^{*}}q\in\delta_{\downarrow}\\}$,

  * •

$Q_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\coloneq\mathrm{lfp}_{\\{s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\\}}^{\subseteq}\lambda
Q.\,Q\cup\\{\delta(s,a)\mid s\in Q\land
a\in\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\\}\setminus\\{\emptyset\\}$
, and

  * •

$\delta_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\coloneq{\delta}|_{Q_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\times\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}}$

  * •

$F_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\coloneq\\{s\in
Q_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\mid
s\cap F_{\mathbf{G}}\neq\emptyset\\}$

Note that the construction ensures that
$Q_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
only contains subsets of $Q_{\mathbf{G}}$ whose states are reachable via the
same traces, i.e. we typically have
$|Q_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}|\ll
2^{|Q_{\mathbf{G}}|}$.

The following characterization is immediate from the subset construction; the
proof can be found in Section 0.B.1.

lemmaconstructionProperties Let $\mathbf{G}$ be a global type,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
be a role, and
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$
be its _subset construction_. If $w$ is a trace of
$\mathsf{GAut}(\mathbf{G})$,
$\texttt{split}(w){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$
is a trace of
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$.
If $u$ is a trace of
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$,
there is a trace $w$ of $\mathsf{GAut}(\mathbf{G})$ such that
$\texttt{split}(w){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}=u$.
It holds that
$\mathcal{L}(\mathbf{G}){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}=\mathcal{L}(\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}))$.

Using this lemma, we show that the CSM
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
preserves all behaviors of $\mathbf{G}$. We briefly sketch the proof here. The
full proof can be found in Section 0.B.1.

lemmaconstructionPreservesBehaviors For all global types $\mathbf{G}$,
$\mathcal{L}(\mathbf{G})\subseteq\mathcal{L}(\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$.

###### Proof

Given that
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
is deterministic, to prove language inclusion it suffices to prove the
inclusion of the respective prefix sets:

$\text{pref}(\mathcal{L}(\mathbf{G}))\subseteq\text{pref}(\mathcal{L}\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$

Let $w$ be a word in $\mathcal{L}(\mathbf{G})$. If $w$ is finite, membership
in
$\mathcal{L}(\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$
is immediate from the claim above. If $w$ is infinite, we show that $w$ has an
infinite run in
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
using König’s Lemma. We construct an infinite graph $\mathcal{G}_{w}(V,E)$
with $V\coloneq\\{v_{\rho}\mid\texttt{trace}(\rho)\leq w\\}$ and
$E\coloneq\\{(v_{\rho_{1}},v_{\rho_{2}})\mid\exists~{}x\in
Σ_{\mathit{async}}.~{}\texttt{trace}(\rho_{2})=\texttt{trace}(\rho_{1})\cdot
x\\}$. Because
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
is deterministic, $\mathcal{G}_{w}$ is a tree rooted at $v_{\varepsilon}$, the
vertex corresponding to the empty run. By König’s Lemma, every infinite tree
contains either a vertex of infinite degree or an infinite path. Because
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
consists of a finite number of communicating state machines, the last
configuration of any run has a finite number of next configurations, and
$\mathcal{G}_{w}$ is finitely branching. Therefore, there must exist an
infinite path in $\mathcal{G}_{w}$ representing an infinite run for $w$, and
thus
$w\in\mathcal{L}(\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$.

The proof of the inclusion of prefix sets proceeds by structural induction and
primarily relies on Lemma 3 and the fact that all prefixes in
$\mathcal{L}(\mathbf{G})$ respect the order of send before receive events.

##  5 Checking Implementability

We now turn our attention to checking implementability of a CSM produced by
the subset construction. We revisit the global types from Example 2 (also
shown in Fig. 2), which demonstrate that the naive subset construction does
not always yield a sound implementation. From these examples, we distill our
conditions that precisely identify the implementable global types.

In general, a global type $\mathbf{G}$ is not implementable when the agreement
on a global run of $\mathsf{GAut}(\mathbf{G})$ among all participating roles
cannot be conveyed via sending and receiving messages alone. When this
happens, roles can take locally permitted transitions that commit to
incompatible global runs, resulting in a trace that is not specified by
$\mathbf{G}$. Consequently, our conditions need to ensure that when a role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
takes a transition in
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$,
it only commits to global runs that are consistent with the local views of all
other roles. We discuss the relevant conditions imposed on send and receive
transitions separately.

Send Validity. Consider $\mathbf{G}_{s}$ from Example 2. The CSM
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G}_{s},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
has an execution with the trace
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$.
This trace is possible because the initial state of
$\mathscr{C}(\mathbf{G}_{s},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$,
$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$,
contains two states of
$\mathsf{GAut}(\mathbf{G}_{s})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$,
each of which has a single outgoing send transition labeled with
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
respectively. Both of these transitions are always enabled in
$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$,
meaning that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
can send
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
even when
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
has chosen the top branch and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
expects to receive
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
instead of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$.
This results in a deadlock. In contrast, while the state
$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$
in
$\mathscr{C}(\mathbf{G}_{s}^{\prime},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$
likewise contains two states of
$\mathsf{GAut}(\mathbf{G}_{s}^{\prime})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$,
each with a single outgoing send transition, now both transitions are labeled
with
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$.
These two transitions collapse to a single one in
$\mathscr{C}(\mathbf{G}_{s}^{\prime},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$.
This transition is consistent with both possible local views that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
might hold on the global run.

Intuitively, to prevent the emergence of inconsistent local views from send
transitions of
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$,
we must enforce that for every state $s\in
Q_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
with an outgoing send transition labeled $x$, a transition labeled $x$ must be
enabled in all states of
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
represented by $s$. We use the following auxiliary definition to formalize
this intuition subsequently.

######  Definition 4 (Transition Origin and Destination)

Let
$s\xrightarrow{x}s^{\prime}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be a transition in
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$
and $\delta_{\downarrow}$ be the transition relation of
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$.
We define the set of _transition origins_ $\operatorname{tr-
orig}(s\xrightarrow{x}s^{\prime})$ and _transition destinations_
$\operatorname{tr-dest}(s\xrightarrow{x}s^{\prime})$ as follows:

$\displaystyle\operatorname{tr-orig}(s\xrightarrow{x}s^{\prime})\coloneq{}$
$\displaystyle\\{G\in s\mid\exists G^{\prime}\in
s^{\prime}.\,G\xrightarrow{x}\mathrel{\vphantom{\to}{}^{*}}G^{\prime}\in\delta_{\downarrow}\\}\text{
and }$ $\displaystyle\operatorname{tr-
dest}(s\xrightarrow{x}s^{\prime})\coloneq{}$ $\displaystyle\\{G^{\prime}\in
s^{\prime}\mid\exists G\in
s.\,G\xrightarrow{x}\mathrel{\vphantom{\to}{}^{*}}G^{\prime}\in\delta_{\downarrow}\\}\enspace.$

Our condition on send transitions is then stated below.

######  Definition 5 (Send Validity)

$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$
satisfies _Send Validity_ iff every send transition
$s\xrightarrow{x}s^{\prime}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is enabled in all states contained in $s$:

$\forall
s\xrightarrow{x}s^{\prime}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}.~{}x\in\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},!}\implies\operatorname{tr-
orig}(s\xrightarrow{x}s^{\prime})=s\enspace.$

Receive Validity. To motivate our condition on receive transitions, let us
revisit $\mathbf{G}_{r}$ from Example 2. The CSM
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G}_{r},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
recognizes the following trace not in the global type language
$\mathcal{L}(\mathbf{G}_{r})$:

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\cdot{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}\enspace.$

The issue lies with
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
which cannot distinguish between the two branches in $\mathbf{G}_{r}$. The
initial state
$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$
of
$\mathscr{C}(\mathbf{G}_{r},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$
has two states of $\mathsf{GAut}(\mathbf{G}_{r})$ corresponding to the
subterms
$G_{t}\coloneq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0$
and
$G_{b}\coloneq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,0\,$.
Here, $G_{t}$ and $G_{b}$ are the top and bottom branch of $\mathbf{G}_{r}$
respectively. This means that there are outgoing transitions in
$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$
labeled with
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$.
If
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
takes the transition labeled
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$,
it commits to the bottom branch $G_{b}$. However, observe that the message
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
can also be available at this time point if the other roles follow the top
branch $G_{t}$. This is because
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
can send
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$ to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
without waiting for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
to first receive from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.
In this scenario, the roles disagree on which global run of
$\mathsf{GAut}(\mathbf{G}_{r})$ to follow, resulting in the violating trace
above.

Contrast this with $\mathbf{G}_{r}^{\prime}$. Here,
$s_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$
again has outgoing transitions labeled with
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$.
However, if
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
takes the transition labeled
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$,
committing to the bottom branch, no disagreement occurs. This is because if
the other roles are following the top branch, then
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is blocked from sending to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
until after it has received confirmation that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
has received its first message from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.

For a receive transition $s\xrightarrow{x}s_{1}$ in
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$
to be safe, we must enforce that the receive event $x$ cannot also be
available due to reordered sent messages in the continuation $G_{2}\in s_{2}$
of another outgoing receive transition $s\xrightarrow{y}s_{2}$. To formalize
this condition, we use the set $M^{\mathcal{B}}_{(G\ldots)}$ of _available
messages_ for a syntactic subterm $G$ of $\mathbf{G}$ and a set of _blocked_
roles $\mathcal{B}$. This notion was already defined in [30, Sec. 2.2].
Intuitively, $M^{\mathcal{B}}_{(G\ldots)}$ consists of all send events
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\triangleright{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}!m$
that can occur on the traces of $G$ such that $m$ will be the first message
added to channel
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$
before any of the roles in $\mathcal{B}$ takes a step.

##### Available messages.

The set of available messages is recursively defined on the structure of the
global type. To obtain all possible messages, we need to unfold the distinct
recursion variables once. For this, we define a map $\mathit{get\mu}$ from
variable to subterms and write $\mathit{get\mu}_{\mathbf{G}}$ for
$\mathit{get\mu}(\mathbf{G})$:

$\mathit{get\mu}(0)\coloneq[\,]$ $\mathit{get\mu}(t)\coloneq[\,]$
$\mathit{get\mu}(μt.G)\coloneq[t\mapsto G]∪\mathit{get\mu}(G)$

$\mathit{get\mu}(\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!:\\!m_{i}.G_{i})\coloneq\bigcup_{i∈I}\mathit{get\mu}(G_{i})$

The function $M^{\mathcal{B},T}_{(\hbox{-}\ldots)}$ keeps a set of unfolded
variables $T$, which is empty initially.

$M^{\mathcal{B},T}_{(0\ldots)}\coloneq∅\hfill
M^{\mathcal{B},T}_{(μt.G\ldots)}\coloneq
M^{\mathcal{B},T∪\\{t\\}}_{(G\ldots)}\hfill
M^{\mathcal{B},T}_{(t\ldots)}\coloneq\begin{cases}∅&\text{if}~{}t∈T\\\
M^{\mathcal{B},T∪\\{t\\}}_{(\mathit{get\mu}_{\mathbf{G}}(t)\ldots)}&\text{if}~{}t∉T\end{cases}\\\
M^{\mathcal{B},T}_{(\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!:\\!m_{i}.G_{i}\ldots)}\coloneq\begin{cases}\bigcup_{i∈I,m∈\mathcal{V}}(M^{\mathcal{B},T}_{(G_{i}\ldots)}\setminus\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m\\})∪\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m_{i}\\}\quad\hfill\text{if}~{}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}∉\mathcal{B}\\\
\bigcup_{i∈I}M^{\mathcal{B}∪\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\},T}_{(G_{i}\ldots)}\quad\hfill\text{if}~{}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}∈\mathcal{B}\end{cases}$

We write $M^{\mathcal{B}}_{(G\ldots)}$ for
$M^{\mathcal{B},\emptyset}_{(G\ldots)}$. If $\mathcal{B}$ is a singleton set,
we omit set notation and write
$M^{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}_{(G\ldots)}$
for
$M^{\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}}_{(G\ldots)}$.
The set of available messages captures the possible states of all channels
before a given receive transition is taken.

######  Definition 6 (Receive Validity)

$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$
satisfies _Receive Validity_ iff no receive transition is enabled in an
alternative continuation that originates from the same source state:

$\begin{array}[]{l}\forall
s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}?m_{1}}s_{1},\,s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}?m_{2}}s_{2}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}.\\\
\qquad{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}\;\implies\;\forall~{}G_{2}\in\operatorname{tr-