dest}(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}).\;{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\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{p}}}}!m_{1}\notin
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_{2}\ldots)}\enspace.\end{array}$

Subset Projection. We are now ready to define our projection operator.

######  Definition 7 (Subset Projection of $\mathbf{G}$)

The _subset projection_
$\mathscr{P}(\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}}}})$
of $\mathbf{G}$ onto
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
$\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}}}})$
if it satisfies Send Validity and Receive Validity. We lift this operation to
a partial function from global types to CSMs in the expected way.

We conclude our discussion with an observation about the syntactic structure
of the subset projection: Send Validity implies that no state has both
outgoing send and receive transitions (also known as mixed choice).

######  Corollary 1 (No Mixed Choice)

If
$\mathscr{P}(\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, then for all
$s\xrightarrow{x_{1}}s_{1},s\xrightarrow{x_{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}}}}$,
$x_{1}\in\Sigma_{!}$ iff $x_{2}\in\Sigma_{!}$.

##  6 Soundness

In this section, we prove the soundness of our subset projection, stated as
follows.

theoremsoundnessTheorem Let $\mathbf{G}$ be a global type and
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
be the subset projection. Then,
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
implements $\mathbf{G}$.

Recall that implementability is defined as protocol fidelity and deadlock
freedom. Protocol fidelity consists of two language inclusions. The first
inclusion,
$\mathcal{L}(\mathbf{G})\subseteq\mathcal{L}(\\{\\!\\!\\{{\mathscr{P}(\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}})$,
enforces that the subset projection generates at least all behaviors of the
global type. We showed in Definition 3 that this holds for the subset
construction alone (without Send and Receive Validity).

The second inclusion,
$\mathcal{L}(\\{\\!\\!\\{{\mathscr{P}(\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}})\subseteq\mathcal{L}(\mathbf{G})$,
enforces that no new behaviors are introduced. The proof of this direction
relies on a stronger inductive invariant that we show for all traces of the
subset projection. As discussed in §5, violations of implementability occur
when roles commit to global runs that are inconsistent with the local views of
other roles. Our inductive invariant states the exact opposite: that all local
views are consistent with one another. First, we formalize the local view of a
role.

######  Definition 8 (Possible run sets)

Let $\mathbf{G}$ be a global type and $\mathsf{GAut}(\mathbf{G})$ be the
corresponding state machine. Let
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 and $w\in Σ_{\mathit{async}}^{*}$ be a word. We define the set of
possible runs
$\operatorname{R}^{\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}}}}}(w)$
as all maximal runs of $\mathsf{GAut}(\mathbf{G})$ that are consistent 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{p}}}}$’s
local view of $w$:

$\operatorname{R}^{\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}}}}}(w)\coloneq\\{\rho\text{
is a maximal run of }\mathsf{GAut}(\mathbf{G})\mid
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{p}}}}}\leq\texttt{split}(\texttt{trace}(\rho)){\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}}}}}\\}\enspace.$

While Definition 8 captures the set of maximal runs that are consistent with
the local view of a single role, we would like to refer to the set of runs
that is consistent with the local view of all roles. We formalize this as the
intersection of the possible run sets for all roles, which we denote as

$I(w)\coloneq\bigcap_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}\operatorname{R}^{\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}}}}}(w)\enspace.$

With these definitions in hand, we can now formulate our inductive invariant:
lemmaintersNonempty Let $\mathbf{G}$ be a global type and
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
be the subset projection. Let $w$ be a trace of
$\\{\\!\\!\\{{\mathscr{P}(\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}}$.
It holds that $I(w)$ is non-empty.

The reasoning for the sufficiency of Section 6 is included in the proof of
Section 6, found in Appendix 0.C. In the rest of this section, we focus our
efforts on how to show this inductive invariant, namely that the intersection
of all roles’ possible run sets is non-empty.

We begin with the observation that the empty trace $\varepsilon$ is consistent
with all runs. As a result,
$I(\varepsilon)=\bigcap_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}\operatorname{R}^{\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}}}}}(\varepsilon)$
contains all maximal runs in $\mathsf{GAut}(\mathbf{G})$. By definition, state
machines for global types include at least one run, and the base case is
trivially discharged. Intuitively, $I(w)$ shrinks as more events are appended
to $w$, but we show that at no point does it shrink to $\emptyset$. We
consider the cases where a send or receive event is appended to the trace
separately, and show that the intersection set shrinks in a principled way
that preserves non-emptiness. In fact, when a trace is extended with a receive
event, Receive Validity guarantees that the intersection set does not shrink
at all.

$x={\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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$,
$w\in
Σ_{\mathit{async}}^{*}$$\operatorname{R}^{\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}}}}}(wx)$$\bigcap_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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\mathcal{P}}\operatorname{R}^{\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}}}}}(w)$$\operatorname{R}^{\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}}}}}(w)$$y={\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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$,
$w^{\prime}=wxu$ with $u\in
Σ_{\mathit{async}}^{*}$$\operatorname{R}^{\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}}}}}(w^{\prime})$$\operatorname{R}^{\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{q}}}}}(w^{\prime}y)$$\operatorname{R}^{\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{q}}}}}(w^{\prime})$$\bigcap_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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\mathcal{P}}\operatorname{R}^{\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}}}}}(w^{\prime})$
Figure 3: Evolution of $\operatorname{R}^{\mathbf{G}}_{\hbox{-}}(\hbox{-})$
sets 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}}}}$
sends a message $m$ 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}}}}$
receives it.

lemmarcvIntersectionSetEquality Let $\mathbf{G}$ be a global type and
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
be the subset projection. Let $wx$ be a trace of
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
such that $x\in\Sigma_{?}$. Then, $I(w)=I(wx)$.

To prove this equality, we further refine our characterization of intersection
sets. In particular, we show that in the receive case, the intersection
between the sender and receiver’s possible run sets stays the same, i.e.

$\operatorname{R}^{\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}}}}}(w)\cap\operatorname{R}^{\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{q}}}}}(w)=\operatorname{R}^{\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}}}}}(wx)\cap\operatorname{R}^{\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{q}}}}}(wx)\enspace.$

Note that it is not the case that the receiver only follows a subset of the
sender’s possible runs. In other words,
$\operatorname{R}^{\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{q}}}}}(w)\subseteq\operatorname{R}^{\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}}}}}(w)$
is not inductive. The equality above simply states that a receive action can
only eliminate runs that have already been eliminated by its sender. Fig. 3
depicts this relation.

Given that the intersection set strictly shrinks, the burden of eliminating
runs must then fall upon send events. We show that send transitions shrink the
possible run set of the sender in a way that is _prefix-preserving_. To make
this more precise, we introduce the following definition on runs.

######  Definition 9 (Unique splitting of a possible run)

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{p}}}}$
a role, and $w\in Σ_{\mathit{async}}^{*}$ a word. Let $\rho$ be a possible run
in
$\operatorname{R}^{\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}}}}}(w)$.
We define the longest prefix of $\rho$ matching $w$:

$\alpha^{\prime}\coloneq\max\\{\rho^{\prime}\mid\rho^{\prime}\leq\rho~{}\wedge~{}\texttt{split}(\texttt{trace}(\rho^{\prime})){\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}}}}}\leq
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{p}}}}}\\}\enspace.$

If $\alpha^{\prime}\neq\rho$, we can split $\rho$ into $\rho=\alpha\cdot
G\xrightarrow{l}G^{\prime}\cdot\beta$ where $\alpha^{\prime}=\alpha\cdot G$,
$G^{\prime}$ denotes the state following $G$, and $\beta$ denotes the suffix
of $\rho$ following $\alpha\cdot G\cdot G^{\prime}$. We call $\alpha\cdot
G\xrightarrow{l}G^{\prime}\cdot\beta$ the unique splitting of $\rho$ 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}}}}$
matching $w$. We omit the 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}}}}$
when obvious from context. This splitting is always unique because the maximal
prefix of any
$\rho\in\operatorname{R}^{\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}}}}}(w)$
matching $w$ is unique.

When 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}}}}$
fires a send transition
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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$,
any run $\rho=\alpha\cdot G\xrightarrow{l}G^{\prime}\cdot\beta$ in
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
possible run with
$\texttt{split}(l){\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}}}}}\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}}}}\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$
is eliminated. While the resulting possible run set could no longer contain
runs that end with $G^{\prime}\cdot\beta$, Send Validity guarantees that it
must contain runs that begin with $\alpha\cdot G$. This is formalized by the
following lemma.

lemmasndPrefixPreservation Let $\mathbf{G}$ be a global type and
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
be the subset projection. Let $wx$ be a trace of
$\\{\\!\\!\\{{\mathscr{P}(\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}}$
such that
$x\in\Sigma_{!}\cap\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 some
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 $\rho$ be a run in $I(w)$, and $\alpha\cdot
G\xrightarrow{l}G^{\prime}\cdot\beta$ be the unique splitting of $\rho$ 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}}}}$
with respect to $w$. Then, there exists a run $\rho^{\prime}$ in $I(wx)$ such
that $\alpha\cdot G\leq\rho^{\prime}$.

This concludes our discussion of the send and receive cases in the inductive
step to show the non-emptiness of the intersection of all roles’ possible run
sets. The full proofs and additional definitions can be found in Appendix 0.C.

##  7 Completeness

In this section, we prove completeness of our approach. While soundness states
that if a global type’s subset projection is defined, it then implements the
global type, completeness considers the reverse direction.

[Completeness]theoremcompletenessThm If $\mathbf{G}$ is implementable, then
$\\{\\!\\!\\{{\mathscr{P}(\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 defined.

We sketch the proof and refer to Appendix 0.D for the full proof.

From the assumption that $\mathbf{G}$ is implementable, we know there exists a
witness CSM that implements $\mathbf{G}$. While the soundness proof picks our
subset projection as the existential witness for showing implementability –
thereby allowing us to reason directly about a particular implementation –
completeness only guarantees the existence of some witness CSM. We cannot
assume without loss of generality that this witness CSM is our subset
construction; however, we must use the fact that it implements $\mathbf{G}$ to
show that Send and Receive Validity hold on our subset construction.

We proceed via proof by contradiction: we assume the negation of Send and
Receive Validity for the subset construction, and show a contradiction to the
fact that this witness CSM implements $\mathbf{G}$. In particular, we
contradict protocol fidelity (Definition 1(i)), stating that the witness CSM
generates precisely the language $\mathcal{L}(\mathbf{G})$. To do so, we
exploit a simulation argument: we first show that the negation of Send and
Receive Validity forces the subset construction to recognize a trace that is
not a prefix of any word in $\mathcal{L}(\mathbf{G})$. Then, we show that this
trace must also be recognized by the witness CSM, under the assumption that
the witness CSM implements $\mathbf{G}$.

To highlight the constructive nature of our proof, we convert our proof
obligation to a witness construction obligation. To contradict protocol
fidelity, it suffices to construct a witness trace $v_{0}$ satisfying two
properties, where
$\\{\\!\\!\\{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]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 our witness CSM:

  1. (a)

$v_{0}$ is a trace of
$\\{\\!\\!\\{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]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$,
and

  2. (b)

the run intersection set of $v_{0}$ is empty:
$I(v_{0})=\bigcap_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}\operatorname{R}^{\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}}}}}(v_{0})=\emptyset$.

We first establish the sufficiency of conditions a and b. Because
$\\{\\!\\!\\{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]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 by assumption, every prefix extends to a maximal trace. Thus,
to prove the inequality of the two languages
$\mathcal{L}(\\{\\!\\!\\{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]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}})$
and $\mathcal{L}(\mathbf{G})$, it suffices to prove the inequality of their
respective prefix sets. In turn, it suffices to show the existence of a prefix
of a word in one language that is not a prefix of any word in the other. We
choose to construct a prefix in the CSM language that is not a prefix in
$\mathcal{L}(\mathbf{G})$. We again leverage the definition of intersection
sets (Definition 8) to weaken the property of language non-membership to the
property of having an empty intersection set as follows. By the semantics of
$\mathcal{L}(\mathbf{G})$, for any $w\in\mathcal{L}(\mathbf{G})$, there exists
$w^{\prime}\in\texttt{split}(\mathcal{L}(\mathsf{GAut}(\mathbf{G})))$ with
$w\sim w^{\prime}$. For any
$w^{\prime}\in\texttt{split}(\mathcal{L}(\mathsf{GAut}(\mathbf{G})))$, it
trivially holds that $w^{\prime}$ has a non-empty intersection set. Because
intersection sets are invariant under the indistinguishability relation
$\sim$, $w$ must also have a non-empty intersection set. Since intersection
sets are monotonically decreasing, if the intersection set of $w$ is non-
empty, then for any $v\leq w$, the intersection set of $v$ is also non-empty.
Modus tollens of the chain of reasoning above tells us that in order to show a
word is not a prefix in $\mathcal{L}(\mathbf{G})$, it suffices to show that
its intersection set is empty.

Having established the sufficiency of properties a and b for our witness
construction, we present the steps to construct $v_{0}$ from the negation of
Send and Receive Validity respectively. We start by constructing a trace 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}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
that satisfies b, and then show that
$\\{\\!\\!\\{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]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
also recognizes the trace, thereby satisfying a. In both cases, let
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 the role and $s$ be the state for which the respective validity condition
is violated.

Send Validity (Definition 5). Let
$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}}}}\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}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 such that

$\operatorname{tr-
orig}(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}}}}\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}s^{\prime})\neq
s\enspace.$

First, we find a trace $u$ 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}}}})_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
that satisfies:  (1) 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}}}}$
is in state $s$ in the CSM configuration reached via $u$, and  (2) the run of
$\mathsf{GAut}(\mathbf{G})$ on $u$ visits a state in
$s\setminus\operatorname{tr-
orig}(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}}}}\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}s^{\prime})$.
We obtain such a witness $u$ from the $\texttt{split}(\texttt{trace}(-))$ of a
run prefix of $\mathsf{GAut}(\mathbf{G})$ that ends in some state in
$s\setminus\operatorname{tr-
orig}(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}}}}\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}s^{\prime})$.
Any prefix thus obtained satisfies (1) by definition 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}}}})$,
and satisfies (2) by construction. Due to the fact that send transitions are
always enabled in a CSM,
$u\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{q}}}}!m$
must also be 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{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}}$,
thus satisfying property a by a simulation argument. We then argue that
$u\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{q}}}}!m$
satisfies property b, stating that
$I(u\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{q}}}}!m)$
is empty: the negation of Send Validity gives that there exist no run
extensions from our candidate state in $s\setminus\operatorname{tr-
orig}(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}}}}\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}s^{\prime})$
with the immediate next action
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\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}}}}:m$,
and therefore there exists no maximal run in $\mathsf{GAut}(\mathbf{G})$
consistent with
$u\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{q}}}}!m$.

Receive Validity (Definition 6). Let
$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}$
and
$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}}}}$
be two transitions, and let $G_{2}\in\operatorname{tr-
dest}(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})$
such 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{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}\text{
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}}}}_{1}\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{p}}}}!m_{1}\in
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_{2}\ldots)}\enspace.$

Constructing the witness $v_{0}$ pivots on finding a trace $u$ 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}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 both
$u\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}}}}\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}$
and
$u\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}}}}\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}$
are traces 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}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$.
Equivalently, we show there exists a reachable configuration 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}}}})}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
in 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{p}}}}$
can receive either message from distinct senders
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$
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}}}}_{2}$.
Formally, the local 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}}}}$
has two outgoing states 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{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}$
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}}}}_{2}?m_{2}$,
and the channels
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}_{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}}}}$
have $m_{1}$ and $m_{2}$ at their respective heads. We construct such a $u$ by
considering a run in $\mathsf{GAut}(\mathbf{G})$ that contains two 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{q}}}}_{1}\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}}}}:m_{1}$
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}}}}_{2}\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}}}}:m_{2}$.
Such a run must exist due to the negation of Receive Validity. We start with
the split trace of this run, and argue that, from the definition of
$M(\hbox{-})$ and the indistinguishability relation $\sim$, we can perform
iterative reorderings using $\sim$ to bubble the send action
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\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{p}}}}!m_{1}$
to the position before the receive action
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$.
Then, a for
$u\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}}}}\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}$
holds by a simulation argument. We then separately show that b holds 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}}}}\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}$
using similar reasoning as the send case to complete the proof that
$u\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}}}}\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}$
suffices as a witness for $v_{0}$.

It is worth noting that the construction of the witness prefix $v_{0}$ in the
proof immediately yields an algorithm for computing counterexample traces to
implementability.

######  Remark 1 (Mixed Choice is Not Needed to Implement Global Types)

Section 7 basically shows the necessity of Send Validity for implementability.
Corollary 1 shows that Send Validity precludes states with both send and
receive outgoing transitions. Together, this implies that an implementable
global type can always be implemented without mixed choice. Note that the
syntactic restrictions on global types do not inherently prevent mixed choice
states from arising in a role’s subset construction, as evidenced 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{r}}}}$
in the following 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{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}}}}\\!:\\!l.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!m.\,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}}}}\\!:\\!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}}}}\\!\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.\,0.$
Our completeness result thus implies that this type is not implementable. Most
MST frameworks [18, 24, 30] implicitly force _no mixed choice_ through
syntactic restrictions on local types. We are the first to prove that mixed
choice states are indeed not necessary for completeness. This is interesting
because mixed choice is known to be crucial for the expressive power of the
synchronous $\pi$-calculus compared to its asynchronous variant [31].

##  8 Complexity

In this section, we establish PSPACE-completeness of checking implementability
for global types.

###### Theorem 8.1

The MST implementability problem is in PSPACE.

###### Proof

We first establish the upper bound. The decision procedure enumerates 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}}}}$
the subsets 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}}}}}$.
This can be done in polynomial space and exponential time. For each
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 $s\subseteq Q_{\mathbf{G}}$, it then  (i) checks membership of $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}}}}}$
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}}}})$,
and  (ii) if $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}}}}$,
checks whether all outgoing transitions of $s$ 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}}}})$
satisfy Send and Receive Validity.  Check (i) can be reduced to the
intersection non-emptiness problem for nondeterministic finite state machines,
which is in PSPACE [44]. It is easy to see that check (ii) can be done in
polynomial time. In particular, the computation of available messages for
Receive Validity only requires a single unfolding of every loop in
$\mathbf{G}$.

Note that the synthesis problem has the same complexity. The subset
construction to 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}}}}}$
can be done using a PSPACE transducer. While the output can be of exponential
size, it is written on an extra tape that is not counted towards memory usage.
However, this means we need to perform the validity checks as described above
instead of using the computed deterministic state machines.

Second, we prove the lower bound. The proof is inspired by the proof for
Theorem 4 [4] in which Alur et al. prove that checking safe realizability of
bounded HMSCs is PSPACE-hard. We reduce the PSPACE-complete problem of
checking universality of an NFA $M=(Q,\Delta,\delta,q_{0},F)$ to checking
implementability. Without loss of generality, we assume that every state can
reach a final state. We construct a global type $\mathbf{G}$ 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}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{r}}}}$
that is implementable iff $\mathcal{L}(M)=\Delta^{\negthinspace*}$. For this,
we define subterms $G_{l}$ and $G_{r}$ as well as $G_{q}$ for every $q\in Q$
and $G_{*}$. We use a fresh letter $\bot$ to handle final states of $M$. We
also define
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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$
as an abbreviation 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}}}}\\!\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\,.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{p}}}}\\!:\\!m$.

$\mathbf{G}\coloneq G_{l}+G_{r}$
$G_{l}\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}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!l\,.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!go\,.\,G_{q_{0}}\\\
$
$G_{q}\coloneq\begin{cases}\sum_{(a,q^{\prime})\in\delta(q)}\mathopen{}\mathclose{{}\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{r}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!a\,.\,G_{q^{\prime}}}\right)&\text{
if }q\notin 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{r}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!\bot\,.\,0\;+\;\sum_{(a,q^{\prime})\in\delta(q)}\mathopen{}\mathclose{{}\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{r}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!a\,.\,G_{q^{\prime}}}\right)&\text{
if }q\in F\end{cases}$
$G_{r}\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}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!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}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!go\,.\,G_{*}\\\
$
$G_{*}\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{r}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!\bot\,.\,0+\sum_{a\in\Delta}\mathopen{}\mathclose{{}\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{r}}}}\\!\leftrightarrow\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\!:\\!a\,.\,G_{*}}\right)\\\
$

The global type $\mathbf{G}$ is constructed such 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}}}}$
first decides whether words from $\mathcal{L}(M)$ or from
$\Delta^{\negthinspace*}$ are sent subsequently. This decision is known 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}}}}$
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}}}}$
but not 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}}}}$.
The protocol then continues 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}}}}$
sending letters from $\Delta$ 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}}}}$
is not involved. Intuitively,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$
is able to receive these letters if and only if
$\mathcal{L}(M)=\Delta^{\negthinspace*}$. From Sections 6 and 7, we know 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}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$ if $\mathbf{G}$ is implementable.

We claim 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}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$ if and only if
$\mathcal{L}(M)=\Delta^{\negthinspace*}$.

First, assume that $\mathcal{L}(M)\neq\Delta^{\negthinspace*}$. Then, there
exists $w\notin\mathcal{L}(M)$. We can construct the following run 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}}}})_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
that deadlocks. 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 the left subterm $G_{l}$ and, subsequently,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$
sends $w$ 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}}}}$.
We do a case analysis on whether $w$ contains a prefix $w^{\prime}$ such that
$w^{\prime}\notin\operatorname{pref}(\mathcal{L}(M))$. If so, sending the last
letter of a minimal prefix leads to a deadlock 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}}}}\\}\\!\\!\\}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$,
contradicting deadlock freedom. If not, it holds that $w$ is a prefix of a
word in $\mathcal{L}(M)$. Still, 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}}}}$
can send $\bot$, which cannot be received, also contradicting deadlock
freedom.

Second, assume that $\mathcal{L}(M)=\Delta^{\negthinspace*}$. With this, it is
fine 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}}}}$
does not know the branch. 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}}}}$
will be able to receive all messages since
$\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{q}}}})$
can receive, letter by letter, $w.\bot$ for every $w\in\mathcal{L}(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}}}}$.
Thus, protocol fidelity and deadlock freedom hold, concluding the proof.

Note that PSPACE-hardness only holds if the size of $\mathbf{G}$ does not
account for common subterms multiple times. Because every message is
immediately acknowledged, the constructed global type specifies a universally
$1$-bounded [23] language, proving that PSPACE-hardness persists for such a
restriction. For our construction, it does not hold that
$\mathcal{V}(\mathcal{L}(G_{l}){\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{q}}}},?}})=\mathcal{L}(M)$.
We chose so to have a more compact protocol. However, we can easily fix this
by sending the decision 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}}}}$
first 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}}}}$,
allowing to omit the messages $\bot$ 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}}}}$.
∎

This result and the fact that local languages are preserved by the subset
projection (Definition 3) leads to the following observation.

###### Corollary 2

Let $\mathbf{G}$ be an implementable global type. Then, the subset projection
$\\{\\!\\!\\{{\mathscr{P}(\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 a local language preserving implementation for $\mathbf{G}$, i.e.,
$\mathcal{L}(\mathscr{P}(\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}}}}))=\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{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}}}}$,
and can be computed in PSPACE.

######  Remark 2 (MST implementability with directed choice is PSPACE-hard)

Theorem 8.1 is stated for global types with sender-driven choice but the
provided type is in fact directed. Thus, the PSPACE lower bound also holds for
implementability of types with directed choice.

##  9 Evaluation

We consider the following three aspects in the evaluation of our approach:
(E1) difficulty of implementation  (E2) completeness, and  (E3) comparison to
state of the art.

For this, we implemented our subset projection in a prototype tool [1, 37]. It
takes a global type as input and computes the subset projection for each role.
It was straightforward to implement the core functionality in approximately
700 lines of Python3 code closely following the formalization (E1).

We consider global types (and communication protocols) from seven different
sources as well as all examples from this work (cf. 1st column of Table 1).
Our experiments were run on a computer with an Intel Core i7-1165G7 CPU and
used at most 100MB of memory. The results are summarized in Table 1. The
reported size is the number of states and transitions of the respective state
machine, which allows not to account for multiple occurrences of the same
subterm. As expected, our tool can project every implementable protocol we
have considered (E2).

Regarding the comparison against the state of the art (E3), we directly
compared our subset projection to the incomplete approach by Majumdar et al.
[30], and found that the run times are in the same order of magnitude in
general (typically a few milliseconds). However, the projection of [30] fails
to project four implementable protocols (including Example 1). We discuss some
of the other examples in more detail in the next section. We further note that
most of the run times reported by Scalas and Yoshida [35] on their model
checking based tool are around 1 second and are thus two to three orders of
magnitude slower.

Source | Name | Impl. | Subset Proj. | Size | $|𝓟|$ | Size | [30]
---|---|---|---|---|---|---|---
|  |  | (complete) |  |  | Proj’s | (incomplete)
[34] | Instrument Contr. Prot. A | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.4$ ms | $22$ | $3$ | $61$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms
Instrument Contr. Prot. B | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.3$ ms | $17$ | $3$ | $47$ | $\boldsymbol{\checkmark}$ |  $0.1$ ms
OAuth2 | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.1$ ms | $10$ | $3$ | $23$ | $\boldsymbol{\checkmark}$ |  $<\negthinspace 0.1$ ms
[33] | Multi Party Game | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.5$ ms | $21$ | $3$ | $67$ | $\boldsymbol{\checkmark}$ |  $0.1$ ms
[24] | Streaming | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms | $13$ | $4$ | $28$ | $\boldsymbol{\checkmark}$ |  $<\negthinspace 0.1$ ms
[13] | Non-Compatible Merge | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms | $11$ | $3$ | $25$ | $\boldsymbol{\checkmark}$ |  $0.1$ ms
[45] | Spring-Hibernate | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $1.0$ ms | $62$ | $6$ | $118$ | $\boldsymbol{\checkmark}$ |  $0.7$ ms
[30] | Group Present | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.6$ ms | $51$ | $4$ | $85$ | $\boldsymbol{\checkmark}$ |  $0.6$ ms
Late Learning | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.3$ ms | $17$ | $4$ | $34$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms
Load Balancer ($n=10$) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $3.9$ ms | $36$ | $12$ | $106$ | $\boldsymbol{\checkmark}$ |  $2.4$ ms
Logging ($n=10$) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $71.5$ ms | $81$ | $13$ | $322$ | $\boldsymbol{\checkmark}$ |  $10.0$ ms
[38] | 2 Buyer Protocol | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.5$ ms | $22$ | $3$ | $60$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms
2B-Prot. Omit No | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.4$ ms | $19$ | $3$ | $56$ | ($\times$) |  $0.1$ ms
2B-Prot. Subscription | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.7$ ms | $46$ | $3$ | $95$ | ($\times$) |  $0.3$ ms
2B-Prot. Inner Recursion | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.4$ ms | $17$ | $3$ | $51$ | $\boldsymbol{\checkmark}$ |  $0.1$ ms
New | Odd-even (Example 1) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.5$ ms | $32$ | $3$ | $70$ | ($\times$) |  $0.2$ ms
$\mathbf{G}_{r}$ – Receive Val. Violated (§2) | $\times$ | $\times$ |  $0.1$ ms | $12$ | $3$ | - | ($\times$) |  $<\negthinspace 0.1$ ms
$\mathbf{G}^{\prime}_{r}$ – Receive Val. Satisfied (§2) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms | $16$ | $3$ | $35$ | $\boldsymbol{\checkmark}$ |  $0.1$ ms
$\mathbf{G}_{s}$ – Send Val. Violated (§2) | $\times$ | $\times$ |  $<\negthinspace 0.1$ ms | $8$ | $3$ | - | ($\times$) |  $<\negthinspace 0.1$ ms
$\mathbf{G}^{\prime}_{s}$ – Send Val. Satisfied (§2) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $<\negthinspace 0.1$ ms | $7$ | $3$ | $17$ | $\boldsymbol{\checkmark}$ |  $<\negthinspace 0.1$ ms
$\mathbf{G}_{\operatorname{fold}}$ (§10) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.4$ ms | $21$ | $3$ | $50$ | ($\times$) |  $0.1$ ms
$\mathbf{G}_{\operatorname{unf}}$ (§10) | $\boldsymbol{\checkmark}$ | $\boldsymbol{\checkmark}$ |  $0.4$ ms | $30$ | $3$ | $61$ | $\boldsymbol{\checkmark}$ |  $0.2$ ms

Table 1: Projecting Global Types. For every protocol, we report whether it is
implementable $\boldsymbol{\checkmark}$ or not $\times$, the time to compute
our subset projection and the generalized projection by Majumdar et al. [30]
as well as the outcome as $\boldsymbol{\checkmark}$ for “implementable”,
$\times$ for “not implementable” and ($\times$) for “not known”. We also give
the size of the protocol (number of states and transitions), the number of
roles, the combined size of all subset projections (number of states and
transitions).

##  10 Discussion

Success of Syntactic Projections Depends on Representation. Let us illustrate
how unfolding recursion helps syntactic projection operators to succeed.
Consider this implementable global type, which is not syntactically
projectable:

$\mathbf{G}_{\operatorname{fold}}\coloneq+\;\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}.\,\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}.\,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}.\,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{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,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}.\,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}.\,0)\end{cases}$
.

Similar to projection by erasure, a syntactic projection erases events that a
role is not involved in and immediately tries to _merge_ different branches.
The merge operator is a partial operator that checks sufficient conditions for
implementability. Here, the merge operator fails 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}}}}$
because it cannot merge a recursion variable binder and a message reception.
Unfolding the global type preserves the represented protocol and resolves this
issue:

$\mathbf{G}_{\operatorname{unf}}\coloneq+\;\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}.\,\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]{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}.\,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,.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}.\,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}.\,0)\end{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,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,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}.\,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}.\,0)\end{cases}$
.

(We refer to Fig. 4 in Section 0.E.1 for visual representations of both global
types.) This global type can be projected with most syntactic projection
operators and shows that the representation of the global type matters for
syntactic projectability. However, such unfolding tricks do not always work,
e.g. for the odd-even protocol (Example 1). We avoid this brittleness using
automata and separating the synthesis from checking implementability.

Entailed Properties from the Literature. We defined implementability for a
global type as the question of whether there exists a deadlock-free CSM that
generates the same language as the global type. Various other properties of
implementations and protocols have been proposed in the literature. Here, we
give a brief overview and defer to Section 0.E.2 for a detailed analysis.
_Progress_ [18], a common property, requires that every sent message is
eventually received and every expected message will eventually be sent. With
deadlock freedom, our subset projection trivially satisfies progress for
finite traces. For infinite traces, as expected, fairness assumptions are
required to enforce progress. Similarly, our subset projection prevents
_unspecified receptions_ [14] and _orphan messages_ [21, 9], respectively
interpreted in our multiparty setting with sender-driven choice. We also
ensure that every local transition of each role is _executable_ [14], i.e. it
is taken in some run of the CSM. Any implementation of a global type has the
_stable property_ [28], i.e., one can always reach a configuration with empty
channels from every reachable configuration. While the properties above are
naturally satisfied by our subset projection, the following ones can be
checked directly on an implementable global type without explicitly
constructing the implementation. A global type is _terminating_ [35] iff it
does not contain recursion and _never-terminating_ [35] iff it does not
contain term $0$.

##  11 Related Work

MSTs were introduced by Honda et al. [24] with a process algebra semantics,
and the connection to CSMs was established soon afterwards [20].

In this work, we present a complete projection procedure for global types with
sender-driven choice. The work by Castagna et al. [13] is the only one to
present a projection that aims for completeness. Their semantic conditions,
however, are not effectively computable and their notion of completeness is
“less demanding than the classical ones”[13]. They consider multiple
implementations, generating different sets of traces, to be sound and complete
with regard to a single global type [13, Sec. 5.3]. In addition, the
algorithmic version of their conditions does not use global information as our
message availability analysis does.

MST implementability relates to safe realizability of HMSCs, which is
undecidable in general but decidable for certain classes [29]. Stutz [38]
showed that implementability of global types that are always able to terminate
is decidable.111This syntactic restriction is referred to as 0-reachability in
[38]. The EXPSPACE decision procedure is obtained via a reduction to safe
realizability of globally-cooperative HMSCs, by proving that the HMSC encoding
[39] of any implementable global type is globally-cooperative and generalizing
results for infinite executions. Thus, our PSPACE-completeness result both
generalizes and tightens the earlier decidability result obtained in [38].
Stutz [38] also investigates how HMSC techniques for safe realizability can be
applied to the MST setting – using the formal connection between MST
implementability and safe realizability of HMSCs – and establishes an
undecidability result for a variant of MST implementability with a relaxed
indistinguishability relation.

Similar to the MST setting, there have been approaches in the HMSC literature
that tie branching to a role making a choice. We refer the reader to the work
by Majumdar et al. [30] for a survey.

Standard MST frameworks project a global type to a set of _local types_ rather
than a CSM. Local types are easily translated to FSMs [30, Def.11]. Our
projection operator, though, can yield FSMs that cannot be expressed with the
limited syntax of local types. Consider this implementable 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{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}.\,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]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,0$
. The subset projection 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}}}}$
has two final states connected by a 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]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$.
In the syntax of local types, $0$ is the only term indicating termination,
which means that final states with outgoing transitions cannot be expressed.
In contrast to the syntactic restrictions for global types, which are key to
effective verification, we consider local types unnecessarily restrictive.
Usually, local implementations are type-checked against their local types and
subtyping gives some implementation freedom [17, 16, 27, 12]. However, one can
also view our subset projection as a local specification of the actual
implementation. We conjecture that subtyping would then amount to a variation
of alternating refinement [5].

CSMs are Turing-powerful [11] but decidable classes were obtained for
different semantics: restricted communication topology [32, 42], half-duplex
communication (only for two roles) [14], input-bounded [10], and unreliable
channels [3, 2]. Global types (as well choreography automata [7]) can only
express existentially $1$-bounded, $1$-synchronizable and half-duplex
communication [39]. Key to this result is that sending and receiving a message
is specified atomically in a global type — a feature Dagnino et al. [19]
waived for their deconfined global types. However, Dagnino et al. [19] use
deconfined types to capture the behavior of a given system rather than
projecting to obtain a system that generates specified behaviors.

This work relies on reliable communication as is standard for MST frameworks.
Work on fault-tolerant MST frameworks [43, 8] attempts to relax this
restriction. In the setting of reliable communication, both context-free [40,
25] and parametric [15, 22] versions of session types have been proposed to
capture more expressive protocols and entire protocol families respectively.
Extending our approach to these generalizations is an interesting direction
for future work.

#### Acknowledgements.

This work is funded in part by the National Science Foundation under grant
1815633. Felix Stutz was supported by the Deutsche Forschungsgemeinschaft
project 389792660 TRR 248—CPEC.

## References

  * [1] Prototype Implementation of Subset Projection for Multiparty Session Types, https://gitlab.mpi-sws.org/fstutz/async-mpst-gen-choice/
  * [2] Abdulla, P.A., Aiswarya, C., Atig, M.F.: Data communicating processes with unreliable channels. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. pp. 166–175. ACM (2016). https://doi.org/10.1145/2933575.2934535, https://doi.org/10.1145/2933575.2934535
  * [3] Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, 10th International Conference, CAV’98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1427, pp. 305–318. Springer (1998). https://doi.org/10.1007/BFb0028754, https://doi.org/10.1007/BFb0028754
  * [4] Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. Theor. Comput. Sci. 331(1), 97–114 (2005). https://doi.org/10.1016/j.tcs.2004.09.034, https://doi.org/10.1016/j.tcs.2004.09.034
  * [5] Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR ’98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1466, pp. 163–178. Springer (1998). https://doi.org/10.1007/BFb0055622, https://doi.org/10.1007/BFb0055622
  * [6] Ancona, D., Bono, V., Bravetti, M., Campos, J., Castagna, G., Deniélou, P., Gay, S.J., Gesbert, N., Giachino, E., Hu, R., Johnsen, E.B., Martins, F., Mascardi, V., Montesi, F., Neykova, R., Ng, N., Padovani, L., Vasconcelos, V.T., Yoshida, N.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2-3), 95–230 (2016). https://doi.org/10.1561/2500000031, https://doi.org/10.1561/2500000031
  * [7] Barbanera, F., Lanese, I., Tuosto, E.: Choreography automata. In: Bliudze, S., Bocchi, L. (eds.) Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12134, pp. 86–106. Springer (2020). https://doi.org/10.1007/978-3-030-50029-0_6, https://doi.org/10.1007/978-3-030-50029-0_6
  * [8] Barwell, A.D., Scalas, A., Yoshida, N., Zhou, F.: Generalised multiparty session types with crash-stop failures. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. LIPIcs, vol. 243, pp. 35:1–35:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.CONCUR.2022.35, https://doi.org/10.4230/LIPIcs.CONCUR.2022.35
  * [9] Bocchi, L., Lange, J., Yoshida, N.: Meeting deadlines together. In: Aceto, L., de Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015. LIPIcs, vol. 42, pp. 283–296. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015). https://doi.org/10.4230/LIPIcs.CONCUR.2015.283, https://doi.org/10.4230/LIPIcs.CONCUR.2015.283
  * [10] Bollig, B., Finkel, A., Suresh, A.: Bounded reachability problems are decidable in FIFO machines. In: Konnov, I., Kovács, L. (eds.) 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference). LIPIcs, vol. 171, pp. 49:1–49:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.49, https://doi.org/10.4230/LIPIcs.CONCUR.2020.49
  * [11] Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983). https://doi.org/10.1145/322374.322380, https://doi.org/10.1145/322374.322380
  * [12] Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19–51 (2018). https://doi.org/10.1016/j.tcs.2018.02.010, https://doi.org/10.1016/j.tcs.2018.02.010
  * [13] Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Log. Methods Comput. Sci. 8(1) (2012). https://doi.org/10.2168/LMCS-8(1:24)2012, https://doi.org/10.2168/LMCS-8(1:24)2012
  * [14] Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005). https://doi.org/10.1016/j.ic.2005.05.006, https://doi.org/10.1016/j.ic.2005.05.006
  * [15] Charalambides, M., Dinges, P., Agha, G.A.: Parameterized, concurrent session types for asynchronous multi-actor interactions. Sci. Comput. Program. 115-116, 100–126 (2016). https://doi.org/10.1016/j.scico.2015.10.006, https://doi.org/10.1016/j.scico.2015.10.006
  * [16] Chen, T., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2) (2017). https://doi.org/10.23638/LMCS-13(2:12)2017, https://doi.org/10.23638/LMCS-13(2:12)2017
  * [17] Chen, T., Dezani-Ciancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: Chitil, O., King, A., Danvy, O. (eds.) Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014\. pp. 135–146. ACM (2014). https://doi.org/10.1145/2643135.2643138, https://doi.org/10.1145/2643135.2643138
  * [18] Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) Formal Methods for Multicore Programming - 15th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2015, Bertinoro, Italy, June 15-19, 2015, Advanced Lectures. Lecture Notes in Computer Science, vol. 9104, pp. 146–178. Springer (2015). https://doi.org/10.1007/978-3-319-18941-3_4, https://doi.org/10.1007/978-3-319-18941-3_4
  * [19] Dagnino, F., Giannini, P., Dezani-Ciancaglini, M.: Deconfined global types for asynchronous sessions. In: Damiani, F., Dardha, O. (eds.) Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12717, pp. 41–60. Springer (2021). https://doi.org/10.1007/978-3-030-78142-2_3, https://doi.org/10.1007/978-3-030-78142-2_3
  * [20] Deniélou, P., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7211, pp. 194–213. Springer (2012). https://doi.org/10.1007/978-3-642-28869-2_10, https://doi.org/10.1007/978-3-642-28869-2_10
  * [21] Deniélou, P., Yoshida, N.: Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M.Z., Peleg, D. (eds.) Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II. Lecture Notes in Computer Science, vol. 7966, pp. 174–186. Springer (2013). https://doi.org/10.1007/978-3-642-39212-2_18, https://doi.org/10.1007/978-3-642-39212-2_18
  * [22] Deniélou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Log. Methods Comput. Sci. 8(4) (2012). https://doi.org/10.2168/LMCS-8(4:6)2012, https://doi.org/10.2168/LMCS-8(4:6)2012
  * [23] Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007), http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09
  * [24] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. pp. 273–284. ACM (2008). https://doi.org/10.1145/1328438.1328472, https://doi.org/10.1145/1328438.1328472
  * [25] Keizer, A.C., Basold, H., Pérez, J.A.: Session coalgebras: A coalgebraic view on regular and context-free session types. ACM Trans. Program. Lang. Syst. 44(3), 18:1–18:45 (2022). https://doi.org/10.1145/3527633, https://doi.org/10.1145/3527633
  * [26] Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978). https://doi.org/10.1145/359545.359563, https://doi.org/10.1145/359545.359563
  * [27] Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10203, pp. 441–457 (2017). https://doi.org/10.1007/978-3-662-54458-7_26, https://doi.org/10.1007/978-3-662-54458-7_26
  * [28] Lange, J., Yoshida, N.: Verifying asynchronous interactions via communicating session automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 97–117. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_6, https://doi.org/10.1007/978-3-030-25540-4_6
  * [29] Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309(1-3), 529–554 (2003). https://doi.org/10.1016/j.tcs.2003.08.002, https://doi.org/10.1016/j.tcs.2003.08.002
  * [30] Majumdar, R., Mukund, M., Stutz, F., Zufferey, D.: Generalising projection in asynchronous multiparty session types. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. LIPIcs, vol. 203, pp. 35:1–35:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.CONCUR.2021.35, https://doi.org/10.4230/LIPIcs.CONCUR.2021.35
  * [31] Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci. 13(5), 685–719 (2003). https://doi.org/10.1017/S0960129503004043, https://doi.org/10.1017/S0960129503004043
  * [32] Peng, W., Purushothaman, S.: Analysis of a class of communicating finite state machines. Acta Informatica 29(6/7), 499–522 (1992). https://doi.org/10.1007/BF01185558, https://doi.org/10.1007/BF01185558
  * [33] Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: Müller, P. (ed.) 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain. LIPIcs, vol. 74, pp. 24:1–24:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPIcs.ECOOP.2017.24, https://doi.org/10.4230/LIPIcs.ECOOP.2017.24
  * [34] Scalas, A., Yoshida, N.: Mpstk: The multiparty session types toolkit (2018), https://doi.org/10.1145/3291638
  * [35] Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (2019). https://doi.org/10.1145/3290343, https://doi.org/10.1145/3290343
  * [36] Sipser, M.: Introduction to the theory of computation. PWS Publishing Company (1997)
  * [37] Stutz, F.: Artifact for "Complete Multiparty Session Type Projection with Automata" (Apr 2023). https://doi.org/10.5281/zenodo.7878493, https://doi.org/10.5281/zenodo.7878493
  * [38] Stutz, F.: Asynchronous multiparty session type implementability is decidable – lessons learned from message sequence charts. In: 37th European Conference on Object-Oriented Programming, ECOOP 2023. LIPIcs (2023), https://fstutz.pages.mpi-sws.org/felix-stutz/pdfs/lessons-learned-draft.pdf
  * [39] Stutz, F., Zufferey, D.: Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types. In: Ganty, P., Monica, D.D. (eds.) Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, September 21-23, 2022. EPTCS, vol. 370, pp. 194–212 (2022). https://doi.org/10.4204/EPTCS.370.13, https://doi.org/10.4204/EPTCS.370.13
  * [40] Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. pp. 462–475. ACM (2016). https://doi.org/10.1145/2951913.2951926, https://doi.org/10.1145/2951913.2951926
  * [41] Toninho, B., Yoshida, N.: Certifying data in multiparty session types. J. Log. Algebraic Methods Program. 90, 61–83 (2017). https://doi.org/10.1016/j.jlamp.2016.11.005, https://doi.org/10.1016/j.jlamp.2016.11.005
  * [42] Torre, S.L., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 299–314. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_21, https://doi.org/10.1007/978-3-540-78800-3_21
  * [43] Viering, M., Hu, R., Eugster, P., Ziarek, L.: A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proc. ACM Program. Lang. 5(OOPSLA), 1–30 (2021). https://doi.org/10.1145/3485501, https://doi.org/10.1145/3485501
  * [44] Wehar, M.: On the complexity of intersection non-emptiness problems. Ph.D. thesis, University of Buffalo (2016)
  * [45] Spring and Hibernate Transaction in Java. https://www.uml-diagrams.org/examples/spring-hibernate-transaction-sequence-diagram-example.html

##  Appendix 0.A Additional Material for Section 3

###  0.A.1 Additional Definitions

Given a word $w=w_{0}\ldots w_{n}$, we use $w[i]$ to denote the i-th symbol
$w_{i}\in\Sigma$, and $w[0..i]$ to denote the subword between and including
$w_{0}$ and $w_{i}$, $w_{0}\ldots w_{i}$.

###  0.A.2 Indistinguishability Relation [30]

We define a family of _indistinguishability relations_ ${\sim_{i}}\subseteq
Σ_{\mathit{async}}^{*}\times Σ_{\mathit{async}}^{*}$ for $i\geq 0$ as follows.
For all $w\in\Sigma^{*}$, we have $w\sim_{0}w$. For $i=1$, we define:

  1. (1)

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}}}}≠{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$,
then
$w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{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{s}}}}!m^{\prime}.u\;\sim_{1}\;w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{s}}}}!m^{\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}}}}\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.u$.

  2. (2)

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{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{s}}}}$,
then
$w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\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{r}}}}?m^{\prime}.u\;\sim_{1}\;w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\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{r}}}}?m^{\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}}}}\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.u$.

  3. (3)

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}}}}≠{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\land({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{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{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{s}}}})$,
then
$w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{s}}}}\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{r}}}}?m^{\prime}.u\;\sim_{1}\;w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\boldsymbol{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\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{r}}}}?m^{\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}}}}\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.u$.

  4. (4)

If $\lvert
w{\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}}}}\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}}}}!\\_}\rvert>\lvert
w{\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{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}}}}?\\_}\rvert$,
then
$w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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^{\prime}.u\;\sim_{1}\;w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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^{\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}}}}\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.u$.

Let $w,w^{\prime},w^{\prime\prime}$ be sequences of events s.t.
$w\sim_{1}w^{\prime}$ and $w^{\prime}\sim_{i}w^{\prime\prime}$ for some $i$.
Then, $w\sim_{i+1}w^{\prime\prime}$. We define $w\sim u$ if $w\sim_{n}u$ for
some $n$.

It is easy to see that $\sim$ is an equivalence relation. Define
$u\preceq_{\sim}v$ if there is $w\in\Sigma^{*}$ such that $u.w\sim v$. Observe
that $u\sim v$ iff $u\preceq_{\sim}v$ and $v\preceq_{\sim}u$.

For infinite words $u,v\in\Sigma^{\omega}$, we define
$u\preceq_{\sim}^{\omega}v$ if for each finite prefix $u^{\prime}$ of $u$,
there is a finite prefix $v^{\prime}$ of $v$ such that
$u^{\prime}\preceq_{\sim}v^{\prime}$. Define $u\sim v$ iff
$u\preceq_{\sim}^{\omega}v$ and $v\preceq_{\sim}^{\omega}u$.

We lift the equivalence relation $\sim$ on $\Sigma^{\infty}$ to languages:

$\mathcal{C}^{\sim}(L)=\mathopen{}\mathclose{{}\left\\{w^{\prime}\mid\bigvee\begin{array}[]{l}w^{\prime}\in\Sigma^{*}\land∃w∈\Sigma^{*}.\;w\in
L\text{ and }w^{\prime}\sim w\\\ w^{\prime}∈\Sigma^{ω}\land\exists
w\in\Sigma^{\omega}.\;w\in L\text{ and
}w^{\prime}\preceq_{\sim}^{\omega}w\end{array}}\right\\}$

For the infinite case, we take the downward closure w.r.t.
$\preceq_{\sim}^{\omega}$. Notice that the closure operator is asymmetric.
Consider the 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{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)^{ω}$.
Since we do not make any fairness assumption on scheduling, we need to include
in the closure the execution where only the sender is scheduled, i.e.,
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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)^{ω}\preceq_{\sim}^{\omega}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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)^{ω}$.

###  0.A.3 State Machine

A _state machine_ $A$ is a $5$-tuple $(Q,\Delta,\delta,q_{0},F)$ where $Q$ is
a finite set of states, $\Delta$ is a finite alphabet, $\delta\subseteq
Q\times(\Sigma\cup\\{\varepsilon\\})\times Q$ is a transition relation,
$q_{0}\in Q$ is the initial state, and $F\subseteq Q$ is the set of final
states. As is standard, we write $q\xrightarrow{x}q^{\prime}$ for
$(q,x,q^{\prime})\in\delta$ and
$q\xrightarrow{w}\mathrel{\vphantom{\to}}^{*}q^{\prime}$ for its reflexive and
transitive hull for $w\in\Delta^{*}$. We define the runs and traces in the
standard way. A run is maximal if it is infinite or if it ends at a final
state. The _language_ $\mathcal{L}(A)$ is the set of (finite or infinite)
maximal traces.

##  Appendix 0.B Additional Material for Section 4

###  0.B.1 Proofs for Section 4

*

###### Proof

All claims are rather straightforward from the definitions and constructions
and the proofs exploit the connection to the projection by erasure. We still
spell them out to familiarize the reader with these.

We prove the first claim first. By construction, for every run $\rho$ in
$\mathsf{GAut}(\mathbf{G})$, there exists a run $\rho^{\prime}$ in the
projection by erasure
$\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{r}}}}}$.
Let $\rho$ be the run for trace $w$ in $\mathsf{GAut}(\mathbf{G})$. Then,
$\rho$ is also a run in
$\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{r}}}}}$
with trace
$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{p}}}}}$.
Since
$\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{r}}}}}$
might be non-deterministic, we apply the subset construction from Definition
3. For the reachable states, this is equivalent to the definition by Sipser
[36, Thm. 1.39].Thus, the constructed deterministic finite state machine can
mimic any run (which is initial by definition) in