t_{2}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!m.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!m.\,0+{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!r.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!r.\,t_{2})\end{cases}.$

Its FSM and the FSM after collapsing erasure is given in Figures 4(a) and
4(b). Intuitively, it would need to recursively merge the parts after both
recursion binders in order to merge the branches with receive event
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m$
but it cannot do so. The full merge can handle this global type. It can
descend beyond $q_{1}$ and $q_{4}$ and is able to merge $q^{\prime}_{1}$ and
$q^{\prime}_{4}$. To obtain $q^{\prime\prime}_{3\mid 5}$, it applies Case (1)
while $q^{\prime}_{1\mid 4}$ is only feasible with Case (2). The result is
embedded into the recursive structure to obtain the FSM in Figure 4(c). It is
equivalent to the (syntactic) result, which renames the recursion variable for
one branch: $\mu
t_{1}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?l.\,t_{1}\,\operatorname*{\&}\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m.\,0\,\operatorname*{\&}\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?r.\,t_{1}).$

$q_{0}$$q_{1}$$q^{\prime}_{1}$$q_{2}$$q^{\prime}_{2}$$q_{3}$$q^{\prime}_{3}$$q_{4}$$q^{\prime}_{4}$$q_{5}$$q^{\prime}_{5}$$q_{6}$$q^{\prime}_{6}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!l$$\varepsilon$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!l$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!m$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!r$$\varepsilon$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!m$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!r$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!l$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!r$

(a) Negative example for semi-full merge
and positive example for full merge

$q_{0}$$q_{1}$$q^{\prime}_{1}$$q^{\prime\prime}_{2}$$q^{\prime\prime}_{3}$$q_{4}$$q^{\prime}_{4}$$q^{\prime\prime}_{5}$$q^{\prime\prime}_{6}$$\varepsilon$$\varepsilon$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m$$\varepsilon$$\varepsilon$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?r$

(b) After collapsing erasure
sth

$q_{1\mid 4}$$q^{\prime}_{1\mid
4}$$q^{\prime\prime}_{2}$$q^{\prime\prime}_{3\mid
5}$$q^{\prime\prime}_{6}$$\varepsilon$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?r$

(c) After full merge
sth

Figure 4:  The FSM on the left represents an implementable global type that is
rejected by the semi-full merge. It is accepted by the full merge: collapsing
erasure yields the FSM in the middle and applying the full merge the FSM on
the right.

######  Example 3.11 (Negative example for full merge).

We consider a simple implementable global type where
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
propagates its decision to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
in the top branch while
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
propagates it in the bottom branch:
$+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!l.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!r.\,0\end{cases}$
. It is illustrated in Figure 3(c). This cannot be projected onto
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
by the full merge operator for which all receive events need to have the same
sender.

######  Remark 3.12 (On sender-driven choice).

Majumdar et al. [46] proposed a classical projection operator that overcomes
this shortcoming. It can project the previous example. In general, allowing to
receive from different senders has subtle consequences. Intuitively, messages
from different senders could overtake each other in a distributed setting and
one cannot rely on the FIFO order provided by the channel of a single sender.
Majumdar et al. employ a message availability analysis to ensure that there
cannot be any confusion about which branch shall be taken. Except for the
possibility to merge cases where a receiver receives from multiple senders,
their merge operator suffers from the same shortcomings as all classical
projection operators. For details, we refer to their work [46].

#### Shortcomings of Classical Projection/Merge Operators

We present slight variations of the two buyer protocol that are implementable
but rejected by all of the presented projection/merge operators.

######  Example 3.13.

We obtain an implementable variant by omitting both message interactions
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{no}$
with which buyer
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}$
notifies seller
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$
that they will not buy the item:

$\mu
t.\,+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{query}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!:\\!\textit{price}.\,\bigl{(}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!:\\!\textit{split}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!:\\!\textit{yes}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{buy}.\,t+{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!:\\!\textit{no}.\,t)+{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!:\\!\textit{cancel}.\,t\bigr{)}\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{done}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!:\\!\textit{done}.\,0\end{cases}.$

This global type cannot be projected onto seller
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$.
The merge operator would need to merge a recursion variable with an external
choice. Visually, the merge operator does not allow to unfold the variable $t$
and try to merge again. However, there is a local type for seller
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$:

$\mu
t_{1}.\,\operatorname*{\&}\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{query}.\,\mu
t_{2}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}!\textit{price}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{buy}.\,t_{1}\operatorname*{\&}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{query}.\,t_{2}\operatorname*{\&}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{done}.\,0)\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{done}.\,0\end{cases}.$

The local type has two recursion variable binders while the global type only
has one. Classical projection operators can never yield such a structural
change: the merge operator can only merge states but not introduce new ones or
introduce new backward transitions.

######  Example 3.14 (Two Buyer Protocol with Subscription).

In this variant, buyer
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}$
first decides whether to subscribe to a yearly discount offer or not — before
purchasing the sequence of items — and notifies buyer
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}$
if it does so:
$\mathbf{G}_{\operatorname{2BPWS}}\;\coloneq\;+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{login}.\,\mathbf{G}_{\operatorname{2BP}}\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{subscribe}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!:\\!\textit{subscribed}.\,\mathbf{G}_{\operatorname{2BP}}\end{cases}.$
The merge operator needs to merge a recursion variable binder $\mu t$ with the
external choice
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\triangleleft{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{subscribed}$.
Still, there is a local type
$L_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}}$
for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}$
such that
$\mathcal{L}(L_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}})=\mathcal{L}(\mathbf{G}_{\operatorname{2BPWS}}){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}}$:

$L_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}}\coloneq\operatorname*{\&}\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{split}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}!\textit{yes}.\,L(t_{1})\operatorname*{⊕}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}!\textit{no}.\,L(t_{2}))\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{cancel}.\,L(t_{3})\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{done}.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{subscribed}.\,L(t_{4})\end{cases}\text{
where }\;L(t)\coloneq\mu
t.\,\operatorname*{\&}\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{split}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}!\textit{yes}.\,t\operatorname*{⊕}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}!\textit{no}.\,t)\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{cancel}.\,t\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}?\textit{done}.\,0\end{cases}.$

In fact, one can also rely on the fact that buyer
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}$
will comply with the intended protocol. Then, it suffices to introduce one
recursion variable $t$ in the beginning and substitute every $L(\hbox{-})$
with $t$, yielding a local type
$L^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}$
with
$\mathcal{L}(L_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}})\subseteq\mathcal{L}(L^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}})$.

Similarly, classical projection operator cannot handle global types where
choices can be disambiguated with semantic properties, e.g., counting modulo a
constant. Scalas and Yoshida [55] also identified another shortcoming: most
classical projection operators require all branches of a loop to contain the
same set of active roles. Thus, they cannot project the following global type.
It is implementable and if it was projectable, the result would be equivalent
to the local types given in their example [55, Fig. 4 (2)].

######  Example 3.15 (Two Buyer Protocol with Inner Recursion).

This variant allows to recursively negotiate how to split the price (and omits
the outer recursion):

$\mathbf{G}_{\operatorname{2BPIR}}\quad\coloneq\quad{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{query}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!:\\!\textit{price}.\,\mu
t.\,+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!:\\!\textit{split}.\,({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!:\\!\textit{yes}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{buy}.\,0+{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!:\\!\textit{no}.\,t)\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{b}}}}\\!:\\!\textit{cancel}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!\textit{no}.\,0\end{cases}.$

These shortcomings have been addressed by some non-classical approaches. For
example, Scalas and Yoshida [55] employ model checking while Castagna et al.
[17] characterise implementable global types with an undecidable well-
formedness condition and give a sound algorithmically checkable approximation.
It is not known whether the implementability problem for global types, neither
with directed or sender-driven choice, is decidable. We answer this question
positively for the more general case of sender-driven choice.

##  4 Implementability for Global Types from MSTs is Decidable

In this section, we show decidability of the implementability problem for
global types with sender-driven choice, using results from the domain of
message sequence charts. We introduce high-level message sequence charts
(HMSCs) and recall an HMSC encoding for global types. In general,
implementability for HMSCs is undecidable but we show that global types, when
encoded as HMSCs, belong to a class of HMSCs for which implementability is
decidable.

###  4.1 High-level Message Sequence Charts

Our definitions of (high-level) message sequence charts follow work by Genest
et al. [31] and Stutz and Zufferey [57]. If reasonable, we adapt terminology
to the MST setting.

######  Definition 4.1 (Message Sequence Charts).

A _message sequence chart (MSC)_ is a $5$-tuple
$M=({\color[rgb]{0.84765625,0.10546875,0.375}\definecolor[named]{pgfstrokecolor}{rgb}{0.84765625,0.10546875,0.375}N},{\color[rgb]{0.1171875,0.53515625,0.8984375}\definecolor[named]{pgfstrokecolor}{rgb}{0.1171875,0.53515625,0.8984375}p},{\color[rgb]{1,0.7578125,0.02734375}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.7578125,0.02734375}f},{\color[rgb]{0,0.30078125,0.25}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.30078125,0.25}l},(\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$
where

  * •

${\color[rgb]{0.84765625,0.10546875,0.375}\definecolor[named]{pgfstrokecolor}{rgb}{0.84765625,0.10546875,0.375}N}$
is a set of send $(S)$ and receive $(R)$ event nodes such that $N=S⊎R$ (where
$\uplus$ denotes disjoint union),

  * •

${\color[rgb]{0.1171875,0.53515625,0.8984375}\definecolor[named]{pgfstrokecolor}{rgb}{0.1171875,0.53515625,0.8984375}p}\colon
N\to\mathcal{P}$ maps each event node to the role acting on it,

  * •

${\color[rgb]{1,0.7578125,0.02734375}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.7578125,0.02734375}f}\colon
S\to R$ is an injective function linking
corresponding send and receive event nodes,

  * •

${\color[rgb]{0,0.30078125,0.25}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.30078125,0.25}l}\colon
N\to Σ$ labels every event node with an event, and

  * •

$(\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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 family of total orders for the
event nodes of each role:
$\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\;\subseteq\;p^{-1}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})\times
p^{-1}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$.

s

$\bm{\mathtt{p}}\triangleright\bm{\mathtt{q}}!m$
---
$\bm{\mathtt{q}}\triangleleft\bm{\mathtt{p}}?m$
---
$\bm{\mathtt{p}}$
---
$\bm{\mathtt{q}}$
---

Figure 5: Highlighting the elements of an MSC
$({\color[rgb]{0.84765625,0.10546875,0.375}\definecolor[named]{pgfstrokecolor}{rgb}{0.84765625,0.10546875,0.375}N},{\color[rgb]{0.1171875,0.53515625,0.8984375}\definecolor[named]{pgfstrokecolor}{rgb}{0.1171875,0.53515625,0.8984375}p},{\color[rgb]{1,0.7578125,0.02734375}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.7578125,0.02734375}f},{\color[rgb]{0,0.30078125,0.25}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.30078125,0.25}l},(\leq_{\bm{\mathtt{p}}})_{\bm{\mathtt{p}}\in\mathcal{P}})$
[57, Fig. 3]

An MSC $M$ induces a partial order $\leq_{M}$ on $N$ that is defined co-
inductively _:_

*[right=proc] e ≤_pe’ e ≤_M e’

*[right=snd-rcv] s ∈$S$ s ≤_M f(s)

*[right=refl] e ≤_M e

*[right=trans] e ≤_M e’
e’ ≤_M e” e ≤_M e”  The labelling function $l$ respects the function $f$: for
every send event node $e$, we have that $l(e)=p(e)\triangleright p(f(e))!m$
and $l(f(e))=p(f(e))\triangleleft p(e)?m$ for some $m\in\mathcal{V}$.

All MSCs in our work respect FIFO, i.e., there are no
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
such that there are $e_{1},e_{2}\in
p^{-1}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$
with $e_{1}\neq e_{2}$, $l(e_{1})=l(e_{2})$,
$e_{1}\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}e_{2}$
and
$f(e_{2})\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}f(e_{1})$
(also called degenerate) and for every pair of roles
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
and for every two event nodes $e_{1}\leq_{M}e_{2}$ with
$l(e_{i})={\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!\\_$xfor
$i\in\\{1,2\\}$, it holds that
$\mathcal{V}(w_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})=\mathcal{V}(f(w_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}))$
where
$w_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is the (unique) linearisation of
$p^{-1}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$.
A _basic MSC (BMSC)_ has a finite number of nodes $N$ and $\mathcal{M}$
denotes the set of all BMSCs. When unambiguous, we omit the index $M$ for
$\leq_{M}$ and write $\leq$. We define $\lneq$ as expected. The language
$\mathcal{L}(M)$ of an MSC $M$ collects all words $l(w)$ for which $w$ is a
linearisation of $N$ that is compliant with $\leq_{M}$.

If one thinks of a BMSC as straight-line code, a high-level message sequence
chart adds control flow. It embeds BMSCs into a graph structure which allows
for choice and recursion.

######  Definition 4.2 (High-level Message Sequence Charts).

A _high-level message sequence chart (HMSC)_ is a $5$-tuple
$(V,E,v^{I}\negmedspace,V^{T}\negmedspace\\!,\mu)$ where $V$ is a finite set
of vertices, $E\subseteq V\times V$ is a set of directed edges, $v^{I}\in V$
is an initial vertex, $V^{T}\subseteq V$ is a set of terminal vertices, and
$\mu:V\to\mathcal{M}$ is a function mapping every vertex to a BMSC. A path in
an HMSC is a sequence of vertices $v_{1},\ldots$ from $V$ that is connected by
edges, i.e., $(v_{i},v_{i+1})\in E$ for every $i$. A path is _maximal_ if it
is infinite or ends in a vertex from $V^{T}\negmedspace$.

Intuitively, the language of an HMSC is the union of all languages of the
finite and infinite MSCs generated from maximal paths in the HMSC and is
formally defined in Section C.1. Like global types, an HMSC specifies a
protocol. The implementability question was also posed for HMSCs and studied
as _safe realisability_. If the CSM is not required to be deadlock-free, it is
called weak realisability.

######  Definition 4.3 (Safe realisability of HMSCs [4]).

An HMSC $H$ is said to be _safely realisable_ if there exists a deadlock-free
CSM
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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
$\mathcal{L}(H)=\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$.

Encoding Global Types from MSTs as HMSCs

Stutz and Zufferey [57, Sec. 5.2] provide a formal encoding $H(\hbox{-})$ from
global types to HMSCs. We refer to Section C.2 for the definition. We adapt
their correctness result to our setting. In particular, our semantics of
$\mathbf{G}$ use the closure operator $\mathcal{C}^{\sim}(\hbox{-})$ while
they distinguish between a type and execution language. We also omit the
closure operator on the right-hand side because HMSCs are closed with regard
to this operator [57, Lm. 5].

######  Theorem 4.4.

Let $\mathbf{G}$ be a global type. Then, the following holds:
$\mathcal{L}(\mathbf{G})=\mathcal{L}(H(\mathbf{G}))$.

###  4.2 Implementability is Decidable

We introduce a mild assumption for global types. Intuitively, we require that
every run of the protocol can always terminate but does not need to.
Basically, this solely rules out global types that have loops without exit
(cf. Example 4.21). In practice, it is reasonable to assume a mechanism to
terminate a protocol for maintenance for instance. Note that this assumption
constitutes a structural property of a protocol and no fairness condition on
runs of the protocol.

######  Assumption ($0$-Reachable).

We say a global type $\mathbf{G}$ is $0$-reachable if every prefix of a word
in its language can be completed to a finite word in its language.
Equivalently, we require that the vertex for the syntactic subterm $0$ is
reachable from any vertex in $H(\mathbf{G})$.

The MSC approach to safe realisability for HMSCs is different from the
classical projection approach to implementability. Given an HMSC, there is a
canonical candidate implementation which always implements the HMSC if an
implementation exists [3, Thm. 13]. Therefore, approaches center around
checking safe realisability of HMSC languages and establishing conditions on
HMSCs that entail safe realisability.

######  Definition 4.5 (Canonical candidate implementation [3]).

Given an HMSC $H$ and a role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
let
$A^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}=(Q^{\prime},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta^{\prime},q^{\prime}_{0},F^{\prime})$
be a state machine with $Q^{\prime}\coloneq\\{q_{w}\mid
w\in\operatorname{pref}(\mathcal{L}(H){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}})\\}$,
$F^{\prime}\coloneq\\{q_{w}\mid
w\in\mathcal{L}_{\operatorname{fin}}(H){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\\}$,
and $\delta^{\prime}(q_{w},x,q_{wx})$ for $x\in Σ_{\mathit{async}}$. The
resulting state machine
$A^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is not necessarily finite so
$A^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is determinised and minimised which yields the FSM
$A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.
We call
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
the canonical candidate implementation of $H$.

Intuitively, the intermediate state machine
$A^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
constitutes a tree whose maximal finite paths give
$\mathcal{L}(H){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\cap\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}^{*}$.
This set can be infinite and, thus, the construction might not be effective.
We give an effective construction of a deterministic FSM for the same language
which was very briefly hinted at by Alur et al. [4, Proof of Thm. 3].

######  Definition 4.6 (Projection by Erasure).

Let
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be a role and
$M=(N,p,f,l,(\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$
be an MSC. We denote the set of nodes of
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
with
$N_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\coloneq\\{n\mid
p(n)={\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}$
and define a two-ary $\operatorname{next}$-relation on
$N_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$_:_
$\operatorname{next}(n_{1},n_{2})$ iff $n_{1}\lneq n_{2}$ and there is no
$n^{\prime}$ with $n_{1}\lneq n^{\prime}\lneq n_{2}$. We define the projection
by erasure of $M$ on to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$:
$M{\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}=(Q_{M},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta_{M},q_{M,0},\\{q_{M,f}\\})$
with

$\displaystyle Q_{M}$ $\displaystyle\coloneq\\{q_{n}\mid n\in
N_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}\uplus\\{q_{M,0}\\}\uplus\\{q_{M,f}\\}\text{
and }$ $\displaystyle\delta_{M}$
$\displaystyle\coloneq\\{q_{M,0}\xrightarrow{\varepsilon}q_{n_{1}}\mid\forall
n_{2}.\,n_{1}\leq
n_{2}\\}\,\uplus\,\\{q_{n_{1}}\xrightarrow{l(n_{1})}q_{n_{2}}\mid\operatorname{next}(n_{1},n_{2})\\}\,\uplus\,\\{q_{n_{2}}\xrightarrow{l(n_{2})}q_{M,f}\mid\forall
n_{1}.\,n_{1}\leq n_{2}\\}$

where $\uplus$ denotes disjoint union. Let
$H=(V,E,v^{I}\negmedspace,V^{T}\negmedspace\\!,\mu)$ be an HMSC. We construct
the projection by erasure for every vertex and identify them with the vertex,
e.g., $Q_{v}$ instead of $Q_{\mu(v)}$. We construct an auxiliary FSM
$(Q^{\prime}_{H},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta^{\prime}_{H},q^{\prime}_{H,0},F^{\prime}_{H})$
with $Q^{\prime}_{H}=\biguplus_{v\in V}Q_{v}$,
$\delta^{\prime}_{H}=\biguplus_{v\in
V}\delta_{v}\uplus\\{q_{v_{1},f}\xrightarrow{\varepsilon}q_{v_{2},0}\mid(v_{1},v_{2})\in
E\\}$, $q^{\prime}_{H,0}=q_{v^{I}\negmedspace,0}$, and
$F^{\prime}_{H}=\biguplus_{v\in V^{F}}q_{v,f}$. We determinise and minimise
$(Q^{\prime}_{H},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta^{\prime}_{H},q^{\prime}_{H,0},F^{\prime}_{H})$
to obtain
$H{\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\coloneq(Q_{H},\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}},\delta_{H},q_{H,0},F_{H})$,
which we define to be the _projection by erasure of $H$ onto
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$_.
The CSM formed from the projections by erasure
$\\{\\!\\!\\{{H{\Downarrow}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
is called _erasure candidate implementation_.

######  Lemma 4.7 (Correctness of Projection by Erasure).

Let $H$ be an HMSC,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be a role, and
$H{\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be its projection by erasure. Then, the following language equality holds:
$\mathcal{L}(H{\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})=\mathcal{L}(H){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$.

The proof is straightforward and can be found in Section C.3. From this result
and the construction of the canonical candidate implementation, it follows
that the projection by erasure admits the same finite language.

######  Corollary 4.8.

Let $H$ be an HMSC,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be a role,
$H{\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be its projection by erasure, and
$A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
be the canonical candidate implementation. Then, it holds that
$\mathcal{L}_{\operatorname{fin}}(H{\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})=\mathcal{L}_{\operatorname{fin}}(A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$.

The projection by erasure can be computed effectively and is deterministic.
Thus, we use it in place of the canonical candidate implementation. Given a
global type, the erasure candidate implementation for its HMSC encoding
implements it if it is implementable.

######  Theorem 4.9.

Let $\mathbf{G}$ be a global type and
$\\{\\!\\!\\{{H(\mathbf{G}){\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
be its erasure candidate implementation. If
$\mathcal{L}_{\operatorname{fin}}(\mathbf{G})$ is implementable 444
_Implementability_ is lifted to languages as expected., then
$\\{\\!\\!\\{{H(\mathbf{G}){\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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 and
$\mathcal{L}_{\operatorname{fin}}(\\{\\!\\!\\{{H(\mathbf{G}){\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})=\mathcal{L}_{\operatorname{fin}}(\mathbf{G})$.

This result does only account for finite languages so we extend it for
infinite sequences. For both, the proof can be found in Section C.4 and
Section C.5.

######  Lemma 4.10 (”Finite implementation“ generalises to infinite language
for $0$-reachable global types).

Let $\mathbf{G}$ be a $0$-reachable global type and
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
be an implementation for $\mathcal{L}_{\operatorname{fin}}(\mathbf{G})$.Then,
it holds that
$\mathcal{L}_{\inf}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})=\mathcal{L}_{\inf}(\mathbf{G})$,
and, thus,
$\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})=\mathcal{L}(\mathbf{G})$.

######  Corollary 4.11.

Let $\mathbf{G}$ be a $0$-reachable implementable global type. Then, the
erasure candidate implementation
$\\{\\!\\!\\{{H(\mathbf{G}){\Downarrow}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}$.

So far, we have shown that, if $\mathbf{G}$ is implementable, the erasure
candidate implementation for its HMSC encoding $H(\mathbf{G})$ implements
$\mathbf{G}$. For HMSCs, this is undecidable in general [45]. We show that,
because of their syntactic restrictions on choice, global types fall into the
class of globally-cooperative HMSCs for which implementability is decidable.

######  Definition 4.12 (Communication graph [32]).

Let
$M=(N,p,f,l,(\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$
be an MSC. The _communication graph_ of $M$ is a directed graph with node
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
for every role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
that sends or receives a message in $M$ and edges
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
if $M$ contains a message from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
i.e., there is $e\in N$ such that
$p(e)={\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
and
$p(f(e))={\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$.

It is important that the communication graph of $M$ does not have a node for
every role but only the active ones, i.e., the ones that send or receive in
$M$.

######  Definition 4.13 (Globally-cooperative HMSCs [32]).

An HMSC $H=(V,E,v^{I},V^{T}\negmedspace,μ)$ is called _globally-cooperative_
if for every loop, i.e., $v_{1},\ldots,v_{n}$ with $(v_{i},v_{i+1})\in E$ for
every $1\leq i<n$ and $(v_{n},v_{1})\in E$, the communication graph of
$\mu(v_{1})\ldots\mu(v_{n})$ is weakly connected, i.e., all nodes are
connected if every edge is considered undirected.

We can check this directly for a global type $\mathbf{G}$. It is
straightforward to define a communication graph for words from
$Σ_{\mathit{sync}}^{*}$. We check it on $\mathsf{GAut}(\mathbf{G})$: for each
binder state, we check the communication graph for the shortest trace to every
corresponding recursion state.

######  Theorem 4.14 (Thm. 3.7 [45]).

Let $H$ be a globally-cooperative HMSC. Restricted to its finite language
$\mathcal{L}_{\operatorname{fin}}(H)$, safe realisability is
$\operatorname{EXPSPACE}$-complete.

######  Lemma 4.15.

Let $\mathbf{G}$ be an implementable $0$-reachable global type. Then, its HMSC
encoding $H(\mathbf{G})$ is globally-cooperative.

The proof can be found in Section C.6 and is far from trivial. We explain the
main intuition for the proof with the following example where we exemplify why
the same result does not hold for HMSCs in general.

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$
---
$m$
---
$m$
---
$m$
---
$m$
---
(a) HMSC $H_{\operatorname{ing}}$

$q_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$$q_{1,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$$q_{2,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m$$q_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}}$$q_{1,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}}$$q_{2,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m$$q_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$$q_{1,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}!m$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}!m$$q_{0,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}}$$q_{1,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}?m$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}?m$

(b) An implementation for $H_{\operatorname{ing}}$

Figure 6: An implementable HMSC which is not globally-cooperative with its
implementation

######  Example 4.16 (Implementable HMSC but not globally cooperative).

HMSC $H_{\operatorname{ing}}$ in Figure 6(a) is implementable but neither
globally-cooperative nor representable with a global type. In the first loop,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
sends a message $m$ to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
while
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
sends a message $m$ to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$
so the communication graph is not weakly connected. In the second loop, only
the interaction between
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
is specified, while, in the third one, it is only the one between
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$.
For a variant of the protocol without the second loop, any candidate
implementation can always expose an execution with more interactions between
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
than the ones between
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}$,
due to the lack of synchronisation. Here, the second loop can make up for such
executions so any execution has a path in $H_{\operatorname{ing}}$. The CSM in
Figure 6(b) implements $H_{\operatorname{ing}}$. In Section C.7, we explain in
detail why there is a path in $H_{\operatorname{ing}}$ for any trace of the
CSM and how to modify the example not to have final states with outgoing
transitions.

######  Theorem 4.17.

Checking implementability of $0$-reachable global types with sender-driven
choice is in $\operatorname{EXPSPACE}$.

######  Proof 4.18.

Let $\mathbf{G}$ be a $0$-reachable global type with sender-driven choice. We
construct $H(\mathbf{G})$ from $\mathbf{G}$ and check if it is globally-
cooperative. For this, we apply the coNP-algorithm by Genest et al. [32] which
is based on guessing a subgraph and checking its communication graph. If
$H(\mathbf{G})$ is not globally cooperative, we know from Lemma 4.15 that
$\mathbf{G}$ is not implementable. If $H(\mathbf{G})$ is globally cooperative,
we check safe realisability for $H(\mathbf{G})$. By Theorem 4.14, this is in
$\operatorname{EXPSPACE}$. If $H(\mathbf{G})$ is not safely realisable, it
trivially follows that $\mathbf{G}$ is not implementable. If $H(\mathbf{G})$
is safely realisable, $\mathbf{G}$ is implemented by the erasure candidate
implementation with Theorems 4.9 and 4.10.

Thus, the implementability problem for global types with sender-driven choice
is decidable.

######  Corollary 4.19.

Let $\mathbf{G}$ be a $0$-reachable global type with sender-driven choice. It
is decidable whether $\mathbf{G}$ is implementable and there is an algorithm
to obtain its implementation.

######  Remark 4.20 (Progress).

The property deadlock freedom is sometimes also studied as _progress_ — in the
sense that a system should never get stuck. For infinite executions, however,
a role could starve in a non-final state by waiting for a message that is
never sent [17, Sec. 3.2]. Thus, Castagna et al. [17] consider a stronger
notion of progress (Def. 3.3: live session) which requires that every role
could eventually reach a final state. Our results also apply to this stronger
notion of progress, which entails that any sent message can eventually be
received. The notion only requires it to be possible but we can ensure that no
role starves in a non-final state in two ways. First, we can impose a (strong)
fairness assumption — as Castagna et al. [17]. Second, we can require that
every loop branch contains at least all roles that occur in interactions of
any path with which the protocol can finish.

##### The Odd Case of Infinite Loops Without Exits.

In theory, one can think of protocols for which the $0$-Reachability-
Assumption (p.Assumption) does not hold. They would simply recurse
indefinitely and can never terminate. This allows interesting behaviour like
two sets of roles that do not interact with each other as the following
example shows.

######  Example 4.21.

Consider the following global type: $\mathbf{G}=\mu
t.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!m.\,t$.
This is basically the protocol that consists only of the first loop of
$H_{\operatorname{ing}}$ (Example 4.16). It describes an infinite execution
with two pairs of roles that independently send and receive messages. This can
be implemented in an infinite setting but the loop can never be exited due to
the lack of synchronisation, breaking protocol fidelity upon termination.

##### Expressiveness of Local Types.

Local types also have a distinct expression for termination: $0$. Thus, if one
considers the FSM of a local type, every final state has no outgoing
transition. Our proposed algorithm might yield FSMs for which this is not the
case. However, the language of such an FSM cannot be represented as local type
since both our construction and FSMs for local types are deterministic. The
latter are also ancestor-recursive, free of intermediate recursion, non-
merging and dense (Proposition 3.6). For FSMs from our procedure, this is not
the case but the ones without final states with outgoing transitions could
possibly be transformed to local types, making subtyping techniques
applicable. One could also study subtyping for FSMs as local specifications.
We leave both for future work.

##### On Lower Bounds for Implementability.

For general globally-cooperative HMSCs, i.e., that are not necessary the
encoding of a global type, safe realisability is
$\operatorname{EXPSPACE}$-hard [45]. This hardness result does not carry over
for the HMSC encoding $H(\mathbf{G})$ of a global type $\mathbf{G}$. The
construction exploits that HMSCs do not impose any restrictions on choice.
Global types, however, require every branch to be chosen by a single sender.

##  5 MSC Techniques for MST Verification

In the previous section, we generalised results from the MSC literature to
show decidability of the implementability problem for global types from MSTs,
yielding an EXPSPACE-algorithm. In this section, we consider further
restrictions on HMSCs to obtain algorithms with better complexity for global
types. First, we transfer the algorithms for $\mathcal{I}$-closed HMSCs, which
requires an HMSC not to exhibit certain anti-patterns of communication, to
global types. Second, we explain approaches for HMSCs that introduced the idea
of choice to HMSCs and a characterisation of implementable MSC languages.
Third, we present a variant of the implementability problem. It can make
unimplementable global types implementable without changing a protocol’s
structure. From now on, we may use the term implementability for HMSCs instead
of safe realisability.

####  $\boldsymbol{\mathcal{I}}$-closed Global Types

For globally-cooperative HMSCs, the implementability problem is
$\operatorname{EXPSPACE}$-complete. The membership in
$\operatorname{EXPSPACE}$ was shown by reducing the problem to
implementability of $\mathcal{I}$-closed HMSCs [45, Thm. 3.7]. These require
the language of an HMSC to be closed with regard to an independence relation
$\mathcal{I}$, where, intuitively, two interactions are independent if there
is no role which is involved in both. Implementability for
$\mathcal{I}$-closed HMSCs is $\operatorname{PSPACE}$-complete [45, Thm. 3.6].
As for the $\operatorname{EXPSPACE}$-hardness for globally-cooperative HMSCs,
the $\operatorname{PSPACE}$-hardness exploits features that cannot be modelled
with global types and there might be algorithms with better worst-case
complexity.

We adapt the definitions [45] to the MST setting. These consider atomic BMSCs,
which are BMSCs that cannot be split further. With the HMSC encoding for
global types, it is straightforward that atomic BMSCs correspond to individual
interactions for global types. Thus, we define the independence relation
$\mathcal{I}$ on the alphabet $Σ_{\mathit{sync}}$.

######  Definition 5.1 (Independence relation $\mathcal{I}$).

We define the independence relation $\mathcal{I}$ on $Σ_{\mathit{sync}}$_:_

$\mathcal{I}\coloneq\\{({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!m^{\prime})\mid\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\}\cap\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\}=\emptyset)\\}.$

We lift this to words, i.e.
$\\{(u.\,x_{1}.\,x_{2}.\,w,u.\,x_{2}.\,x_{1}.\,w)\mid u,w\in
Σ_{\mathit{sync}}^{*}\text{ and }(x_{1},x_{2})\in\mathcal{I}\\}$, and obtain
an equivalence relation $\equiv_{\mathcal{I}}$ as its transitive and reflexive
closure. We define its closure for language $L\subseteq
Σ_{\mathit{sync}}^{*}$_:_
$\mathcal{C}^{\equiv_{\mathcal{I}}}(L)\coloneq\\{u\in
Σ_{\mathit{sync}}^{*}\mid\exists w\in L\text{ with
}u\equiv_{\mathcal{I}}w\\}$.

######  Definition 5.2 ($\mathcal{I}$-closed global types).

Let $\mathbf{G}$ be a global type $\mathbf{G}$. We say $\mathbf{G}$ is
$\mathcal{I}$-closed if
$\mathcal{L}_{\operatorname{fin}}(\mathsf{GAut}(\mathbf{G}))=\mathcal{C}^{\equiv_{\mathcal{I}}}(\mathcal{L}_{\operatorname{fin}}(\mathsf{GAut}(\mathbf{G})))$.

Note that $\mathcal{I}$-closedness is defined on the state machine
$\mathsf{GAut}(\mathbf{G})$ of $\mathbf{G}$ with alphabet $Σ_{\mathit{sync}}$
and not on its semantics $\mathcal{L}(\mathbf{G})$ with alphabet
$Σ_{\mathit{async}}$.

######  Example 5.3.

The global type $\mathbf{G}_{\operatorname{2BP}}$ is $\mathcal{I}$-closed.
Buyer
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{a}}}}$
is involved in every interaction. Thus, for every two consecutive
interactions, there is a role that is involved in both.

######  Algorithm 1 (Checking if $\mathbf{G}$ is $\mathcal{I}$-closed).

Let $\mathbf{G}$ be a global type $\mathbf{G}$. We construct the state machine
$\mathsf{GAut}(\mathbf{G})$. We need to check every consecutive occurrence of
elements from $Σ_{\mathit{sync}}$ for words from
$\mathcal{L}(\mathsf{GAut}(\mathbf{G}))$. For binder states, incoming and
outgoing transition labels are always $\varepsilon$. This is why we slightly
modify the state machine but preserve its language. We remove all variable
states and rebend their only incoming transition to the state their only
outgoing transition leads to. In addition, we merge binder states with their
only successor. For every state $q$ of this modified state machine, we
consider the labels $x,y\in Σ_{\mathit{sync}}$ of every combination of
incoming and outgoing transition of $q$. We check if $x\equiv_{\mathcal{I}}y$.
If this is true for all $x$ and $y$, we return _true_. If not, we return
_false_.

######  Lemma 5.4.

A global type $\mathbf{G}$ is $\mathcal{I}$-closed iff Algorithm 1 returns
_true_.

The proof can be found in Appendix D. This shows that the presented algorithm
can be used to check $\mathcal{I}$-closedness. The algorithm considers every
state and all combinations of transitions leading to and from it.

######  Proposition 5.5.

For global type $\mathbf{G}$, checking if $\mathbf{G}$ is $\mathcal{I}$-closed
is in $O(\lvert\mathbf{G}\rvert^{2})$.

The tree-like shape of $\mathsf{GAut}(\mathbf{G})$ might suggest that this
check can be done in linear time. However, this example shows that recursion
can lead to a quadratic number of checks.

######  Example 5.6.

Let us consider the following global type for some $n\in\mathbb{N}$.

$\mu
t.\,+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{0}\\!:\\!m_{0}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{0}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{0}\\!:\\!m_{0}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{0}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}_{0}\\!:\\!m_{0}.\,0\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!:\\!m_{1}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{1}\\!:\\!m_{1}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{1}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}_{1}\\!:\\!m_{1}.\,t\\\
\quad{\vdots}\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{n}\\!:\\!m_{n}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{n}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{n}\\!:\\!m_{n}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{n}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}_{n}\\!:\\!m_{n}.\,t\end{cases}$

It is obvious that
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!:\\!m_{i},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{i}\\!:\\!m_{i})\notin\mathcal{I}$
and
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{i}\\!:\\!m_{i},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{i}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}_{i}\\!:\\!m_{i})\notin\mathcal{I}$
for every $i$. Because of the recursion, we need to check if
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}_{i}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}_{i}\\!:\\!m_{i},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{j}\\!:\\!m_{j})$
is in $\mathcal{I}$ for every $0\neq i\neq j$. This might lead to a quadratic
number of checks.

If a global type $\mathbf{G}$ is $\mathcal{I}$-closed, we can apply the
results for its $\mathcal{I}$-closed HMSC encoding $H(\mathbf{G})$, for which
checking implementability is in PSPACE. With Corollary 4.11, the projection by
erasure implements $\mathbf{G}$.

######  Corollary 5.7.

Checking implementability of $0$-reachable, $\mathcal{I}$-closed global types
with sender-driven choice is in PSPACE.

######  Example 5.8.

This implementable global type is not $\mathcal{I}$-closed:
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!m.\,0\;.$

#### Detecting Non-local Choice in HMSCs

For HMSCs, there are no restrictions on branching. Similar to choice for
global types, the idea of imposing restrictions on choice was studied for
HMSCs [9, 51, 49, 35, 32]. We refer to [46] for an overview. Here, we focus on
results that seem most promising for developing algorithms to check
implementability of global types with better worst-case complexity. The work
by Dan et al. [27] centers around the idea of non-local choice. Intuitively,
non-local choice yields scenarios that make it impossible to implement the
language. In fact, if a language is not implementable, there is some non-local
choice. Thus, checking implementability amounts to checking non-local choice
freedom. For this definition, they showed insufficiency of Baker’s condition
[7] and reformulated the closure conditions for safe realisability by Alur et
al. [3]. In particular, they provide a definition that is based on projected
words of a language in contrast to explicit choice. While it is
straightforward to check their definition for finite collections of $k$ BMSCs
with $n$ events in
$O(k^{2}\cdot\lvert\mathcal{P}\rvert+n\cdot\lvert\mathcal{P}\rvert)$, it is
unclear how to check their condition for languages with infinitely many
elements. The design of such a check is far from trivial as their definition
does not give any insight about local behaviour and their algorithm heavily
relies on the finite nature of finite collections of BMSCs.

#### Payload Implementability

A deadlock-free CSM implements a global type if their languages are precisely
the same. In the HMSC domain, a variant of the implementability problem has
been studied. Intuitively, it allows to add fresh data to the payload of an
existing message and protocol fidelity allows to omit the additional payload
data. This allows to add synchronisation messages to existing interactions and
can make unimplementable global types implementable while preserving the
structure of the protocol. It can also be used if a global type is rejected by
a projection operator or the run time of the previous algorithms is not
acceptable.

######  Definition 5.9 (Payload implementability).

Let $L$ be a language with message alphabet $\mathcal{V}_{1}$. We say that $L$
is _payload implementable_ if there is a message alphabet $\mathcal{V}_{2}$
for a deadlock-free CSM
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
with
$A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
over
$\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m\mid{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\in\mathcal{P},\;m\in\mathcal{V}_{1}\times\mathcal{V}_{2}\\}$
such that its language is the same when projecting onto the message alphabet
$\mathcal{V}_{1}$, i.e.,
$\mathcal{C}^{\sim}(L)=\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}){\Downarrow}_{\mathcal{V}_{1}}$,
where
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!(m_{1},m_{2})){\Downarrow}_{\mathcal{V}_{1}}\coloneq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}!m_{1}\text{
and
}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?(m_{1},m_{2})){\Downarrow}_{\mathcal{V}_{1}}\coloneq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m_{1}$
and is lifted to words and languages as expected.

The finite language $\mathcal{L}_{\operatorname{fin}}(H)$ of a _local_ HMSC
$H$ is always payload implementable with a deadlock-free CSM of linear size.

######  Definition 5.10 (Local HMSCs [32]).

Let $H=(V,E,v^{I}\negmedspace,V^{T}\negmedspace\\!,\mu)$ be an HMSC. We call
$H$ _local_ if $\mu(v^{I})$ has a unique minimal event and there is a function
$\operatorname{root}\colon V\to\mathcal{P}$ such that for every $(v,u)\in E$,
it holds that $\mu(u)$ has a unique minimal event $e$ and $e$ belongs to
$\operatorname{root}(v)$, i.e., for
$\mu(u)=(N,p,f,l,(\leq_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$,
we have that $p(e)=\operatorname{root}(v)$ and $e\leq e^{\prime}$ for every
$e^{\prime}\in N$.

######  Proposition 5.11 (Prop. 21 [32]).

For any local HMSC $H\negthinspace$, $\mathcal{L}_{\operatorname{fin}}(H)$ is
payload implementable.

With Lemma 4.10, we can use the implementation of a local $H(\mathbf{G})$ for
a $0$-reachable global type $\mathbf{G}$.

######  Corollary 5.12.

Let $\mathbf{G}$ be a $0$-reachable for which $H(\mathbf{G})$ is local. Then,
$\mathbf{G}$ can be implemented with a CSM of linear size.

The algorithm to construct a deadlock-free CSM [32, Sec. 5.2] suggests that
the BMSCs for such HMSCs need to be maximal – in the sense that any vertex
with a single successor is collapsed with its successor. If this was not the
case, the result would claim that the language of the following global type is
payload implementable: $\mu
t.\,+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!m_{1}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{s}}}}\\!:\\!m_{2}.\,t\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\\!:\\!m_{3}.\,0\end{cases}$.
However, is is easy to see that it is not payload implementable since there is
no interaction between
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
which decides whether to stay in the loop or not, and
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$.
Thus, we cannot simply check whether $H(\mathbf{G})$ is local. In fact, it
would always be. Instead, we first need to minimise it and then check whether
it is local. If we collapse the two consecutive vertices with independent
pairs of roles in this example, the HMSC is not local. The representation of
the HMSC matters which shows that local as property is rather a syntactic than
a semantic notion.

######  Algorithm 2 (Checking if $H(\mathbf{G})$ is local – directly on
$\mathsf{GAut}(\mathbf{G})$).

Let $\mathbf{G}$ be a global type $\mathbf{G}$. We consider the finite trace
$w^{\prime}$ of every longest branch-free, loop-free and non-initial run in
the state machine $\mathsf{GAut}(\mathbf{G})$. We split the (synchronous)
interactions into asynchronous events:
$w=\operatorname{split}(w^{\prime})=w_{1}\ldots w_{n}$. We need to check if
there is $u\sim w$ with $u=u_{1}\ldots u_{n}$ such that $u_{1}\neq w_{1}$. For
this, we can construct an MSC for $w$ [31, Sec. 3.1] and check if there is a
single minimal event. This works because MSCs are closed under $\sim$ [57, Lm.
5]. If the MSC of every trace $w^{\prime}$ has a single minimal event, we
return _true_. If not, we return _false_.

It is straightforward that this mimics the corresponding check for the HMSC
$H(\mathbf{G})$ and, with similar modifications as for Algorithm 1, the check
can be done in $O(\lvert\mathbf{G}\rvert)$.

######  Proposition 5.13.

For a global type $\mathbf{G}$, Algorithm 2 returns _true_ iff $H(\mathbf{G})$
is local.

Ben-Abdallah and Leue [9] introduced local-choice HMSCs, which are as
expressive as local HMSCs. Their condition also uses a
$\operatorname{root}$-function and minimal events but quantifies over paths.
Every local HMSC is a local-choice HMSC and every local-choice HMSC can be
translated to a local HMSC that accepts the same language with a quadratic
blow-up [32]. It is straightforward to adapt the Algorithm 2 to check if a
global type is local-choice. If this is the case, we translate the protocol
and use the implementation for the translated protocol.

##  6 Implementability with Intra-role Reordering

In this section, we introduce a generalisation of the implementability problem
that relaxes the total event order for each role. We prove that this
generalisation is undecidable in general.

#### A Case for More Reordering

From the perspective of a single role, each word in its language consists of a
sequence of send and receive events. Choice in global types happens by sending
(and not by receiving). Because of this, one can argue that a role should be
able to receive messages from different senders in any order between sending
two messages. In practice, receiving a message can induce a task with non-
trivial computation that our model does not account for. Therefore, such a
reordering for a sequence of receive events can have outsized performance
benefits. In addition, there are global types that can be implemented with
regard to this generalised relation even if no (standard) implementation
exists.

######  Example 6.1 (Example for intra-role reordering).

Let us consider a global type where a central coordinator
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
distributes independent tasks to different roles in rounds:

$\mathbf{G}_{\operatorname{TC}}\coloneq\mu
t.\,+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!:\\!\operatorname{task}.\,\ldots\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{n}\\!:\\!\operatorname{task}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!\operatorname{result}.\,\ldots\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{n}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!\operatorname{result}.\,t\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!:\\!\operatorname{done}.\,\ldots\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{n}\\!:\\!\operatorname{done}.\,0\end{cases}.$

Since all tasks in each round are independent,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
can benefit from receiving the results in the order they arrive instead of
busy-waiting.

We generalise the indistinguishability relation $\sim$ accordingly.

######  Definition 6.2 (Intra-role indistinguishability relation $\approx$).

We define a family of _intra-role indistinguishability relations_
${\approx_{i}}\subseteq\Sigma^{*}\times\Sigma^{*}$, for $i\geq 0$ as follows.
For all $w,u\in\Sigma^{*}$, $w\sim_{i}u$ entails $w\approx_{i}u$. For $i=1$,
we define: if
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}?m^{\prime}.u\;\approx_{1}\;w.{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m.u.$
Based on this, we define $\approx$ analogously to $\sim$. Let $w$,
$w^{\prime}$, $w^{\prime\prime}$ be words s.t. $w\approx_{1}w^{\prime}$ and
$w^{\prime}\approx_{i}w^{\prime\prime}$ for some $i$. Then
$w\approx_{i+1}w^{\prime\prime}$. We define $w\approx u$ if $w\approx_{n}u$
for some $n$. It is straightforward that $\approx$ is an equivalence relation.
Define $u\preceq_{\approx}v$ if there is $w\in\Sigma^{*}$ such that
$u.w\approx v$. Observe that $u\sim v$ iff $u\preceq_{\approx}v$ and
$v\preceq_{\approx}u$. We extend $\approx$ to infinite words and languages as
for $\sim$.

######  Definition 6.3 (Implementability w.r.t. $\approx$).

A global type $\mathbf{G}$ is _implementable with regard to $\approx$_ if
there exists a deadlock-free CSM
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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 (i)
$\mathcal{L}(\mathbf{G})\subseteq\mathcal{C}^{\approx}(\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}))$
and (ii)
$\mathcal{C}^{\approx}(\mathcal{L}(\mathbf{G}))=\mathcal{C}^{\approx}(\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}))$.
We say that
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
$\approx$-implements $\mathbf{G}$.

In this section, we emphasise the indistinguishability relation, e.g.,
$\approx$-implementable. We could have also followed the definition of
$\sim$-implementability and required
$\mathcal{C}^{\approx}(\mathcal{L}(\mathbf{G}))=\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}})$.
This, however, requires the CSM to be closed under $\approx$. In general, this
might not be possible with finitely many states. In particular, if there is a
loop without any send events for a role, the labels in the loop would
introduce an infinite closure if we require that
$\mathcal{C}^{\approx}(\mathcal{L}(\mathbf{G})){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}=\mathcal{L}(A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})$.

######  Example 6.4.

We consider a variant of $\mathbf{G}_{\operatorname{TC}}$ from Example 6.1
with $n=2$ where
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}$
send a log message to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
after receiving the task and before sending the result back:

$\mathbf{G}_{\operatorname{TCLog}}\coloneq\mu
t.\,+\begin{cases}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!:\\!\operatorname{task}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}\\!:\\!\operatorname{task}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!\operatorname{log}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!\operatorname{log}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!\operatorname{result}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}\\!\to\\!{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\!:\\!\operatorname{result}.\,t\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{1}\\!:\\!\operatorname{done}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}\\!:\\!\operatorname{done}.\,0\end{cases}.$

There is no FSM for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
that precisely accepts
$\mathcal{C}^{\approx}(\mathcal{L}(\mathbf{G}_{\operatorname{TCLog}})){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}$.
If we rely on the fact that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}$
send the same number of $\operatorname{log}$-messages to
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$,
we can use an FSM
$A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
with a single state (both initial and final) with two transitions: one for the
$\operatorname{log}$-message from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{2}$
each, that lead back to the only state. For this, it holds that
$\mathcal{C}^{\approx}(\mathcal{L}(\mathbf{G}_{\operatorname{TCLog}})){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}}\subseteq\mathcal{L}(A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}})$.
If we cannot rely on this, the FSM would need to keep track of the difference,
which can be unbounded and thus not recognisable by an FSM.

This is why we chose a more permissive definition which is required to cover
at least as much as specified in the global type (i) and the $\approx$-closure
of both are the same (ii).

It is trivial that any $\sim$-implementation for a global type does also
$\approx$-implement it.

######  Proposition 6.5.

Let $\mathbf{G}$ be a global type that is $\sim$-implemented by the CSM
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$.
Then,
$\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\in\mathcal{P}}$
also $\approx$-implements $\mathbf{G}$.

For instance, the erasure candidate implementation is a $\sim$-implementation
as well as a $\approx$-implementation for the task coordination protocol
$\mathbf{G}_{\operatorname{TC}}$ from Example 6.1. Still,
$\approx$-implementability gives more freedom and allows to consider all
possible combinations of arrivals of results. In addition,
$\approx$-implementability renders some global types implementable which would
not be otherwise. For instance, those with a role that would need to receive
different sequences, related by $\approx$ though, in different branches it
cannot distinguish (yet).

######  Example 6.6 ($\approx$-implementable but not $\sim$-implementable).

Let us consider the following global type:
$({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!m.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!m.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\\!:\\!m.\,0)$.
This cannot be $\sim$-implemented because
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
would need to know about the choice to receive the messages from
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
in the correct order. However, it is $\approx$-implementable. The FSMs for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
can be obtained with projection by erasure. For
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$,
we can have an FSM that only accepts
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}?m$
but also an FSM which accepts
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\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}\bm{{\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}\bm{{\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}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}?m$
in addition. Note that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
does not learn the choice in the second FSM even if it branches. Hence, it
would not be implementable if it sent different messages in both branches
later on. However, it could still learn by receiving and, afterwards, send
different messages.

#### Implementability with Intra-role Reordering is Undecidable

Unfortunately, checking implementability with regard to $\approx$ for global
types (with directed choice) is undecidable. Intuitively, the reordering
allows roles to drift arbitrarily far apart as the execution progresses which
makes it hard to learn which choices were made.

We reduce the _Post Correspondence Problem_ (PCP) [54] to the problem of
checking implementability with regard to $\approx$. An instance of PCP over an
alphabet $\Delta$, $\lvert\Delta\rvert>1$, is given by two finite lists
$(u_{1},u_{2},\ldots,u_{n})$ and $(v_{1},v_{2},\ldots,v_{n})$ of finite words
over $\Delta$, also called tile sets. A solution to the instance is a sequence
of indices $(i_{j})_{1\leq j\leq k}$ with $k\geq 1$ and $1\leq i_{j}\leq n$
for all $1\leq j\leq k$, such that $u_{i_{1}}\ldots u_{i_{k}}=v_{i_{1}}\ldots
v_{i_{k}}$. To be precise, we present a reduction from the modified PCP (MPCP)
[56, Sec. 5.2], which is also undecidable. It simply requires that a match
starts with a specific pair — in our case we choose the pair with index $1$.
It is possible to directly reduce from PCP but the reduction from MPCP is more
concise. Intuitively, we require that the solution starts with the first pair
so there exists no trivial solution and choosing a single pair is more concise
than all possible ones. Our encoding is the following global type where
$x\in\\{u,v\\}$, $[x_{i}]$ denotes a sequence of message interactions with
message $x_{i}[1],\ldots,x_{i}[k]$ each for $x_{i}$ of length $k$, message
$\textit{c-}x$ indicates choosing tile set $x$, and message $\textit{ack-}x$
indicates acknowledging the tile set $x$:

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
---
$\textit{c-}u$
---
$[u_{1}]$
---
$1$
---
$1$
---