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

11institutetext: New York University, New York, USA 11email<EMAIL_ADDRESS><EMAIL_ADDRESS>22institutetext: Max Planck Institute for Software Systems,
Kaiserslautern, Germany 22email<EMAIL_ADDRESS>
# Deciding Subtyping for
Asynchronous Multiparty Sessions

Authors withheld  Elaine Li corresponding author11 Felix Stutz 22 Thomas Wies
11

###### Abstract

Multiparty session types (MSTs) are a type-based approach to verifying
communication protocols, represented as global types in the framework. We
present a precise subtyping relation for asynchronous MSTs with communicating
state machines (CSMs) as implementation model. We address two problems: when
can a local implementation safely substitute another, and when does an
arbitrary CSM implement a global type? We define safety with respect to a
given global type, in terms of subprotocol fidelity and deadlock freedom. Our
implementation model subsumes existing work which considers local types with
restricted choice. We exploit the connection between MST subtyping and
refinement to formulate concise conditions that are directly checkable on the
candidate implementations, and use them to show that both problems are
decidable in polynomial time.

###### Keywords:

Protocol verification Multiparty session types Communicating state machines
Subtyping Refinement.

##  1 Introduction

Multiparty session types (MSTs) [31] are a type-based approach to verifying
communication protocols. In MST frameworks, a communication protocol is
expressed as a _global type_ , which describes the interactions of all
protocol participants from a birds-eye view. The key property of interest in
MST frameworks is _implementability_ , which asks whether there exists a
collection of local implementations, one per protocol participant, that is
deadlock-free and produces the same set of behaviors described by the global
type. The latter property is known as _protocol fidelity_. Given an
implementable global type, the _synthesis_ problem asks to compute such a
collection. To solve implementability and synthesis, MST frameworks are often
equipped with a _projection operator_ , which is a partial map from global
types to a collection of local implementations. Projection operators compute a
correct implementation for a given global type if one exists.

However, projection operators only compute one candidate out of many possible
implementations for a given global type, which narrows the usability of MST
frameworks. As we demonstrate below, substituting this candidate can in some
cases achieve an exponential reduction in the size of the local
implementation. Furthermore, applications may sometimes require that an
implementation produce only a subset of the global type’s specified behaviors.
We refer to this property as _subprotocol fidelity_. For example, a general
client-server protocol may customize the set of requests it handles to the
specific devices it runs on. Subtyping reintroduces this flexibility into MST
frameworks, by characterizing when an implementation can replace another while
preserving desirable correctness guarantees.

Formally, a subtyping relation is a reflexive and transitive relation that
respects Liskov and Wing’s substitution principle [38]: $T^{\prime}$ is a
subtype of $T$ when $T^{\prime}$ can be _safely_ used in any context that
expects a term of type $T$. While implementability for MSTs was originally
defined on syntactic local types[29, 31], other implementation models have
since been investigated, including communicating session automata [21] and
behavioral contracts [16]. We motivate our work with the observation that a
subtyping relation is only as powerful as its notion of safety, and the
expressivity of its underlying implementation model. Existing subtyping
relations adopt a notion of safety that is agnostic to a global specification.
For example, [2, 3] define safety as the successful completion of a single
role in binary sessions, [36] defines safety as eventual reception and
progress of all roles in multiparty sessions, and [26] defines safety as the
termination of all roles in multiparty sessions. As a result, these subtyping
relations eagerly reject subtypes that are viable for the specific global type
at hand. In addition, existing implementation models are restricted to local
types with _directed choice_ for branching, or equivalent representations
thereof [9], which prohibit a role from sending messages to or receiving
messages from different participants in a choice. This restrictiveness
undermines the flexibility that subtyping is fundamentally designed to
provide.

We present a subtyping relation that extends prior work along both dimensions.
We define a stronger notion of safety with respect to a given global type: a
substitution is safe if in all _well-behaved_ contexts, the resulting
implementation satisfies both deadlock freedom and subprotocol fidelity. We
assume an implementation model of unrestricted communicating state machines
(CSMs) [4] communicating via FIFO channels, which subsumes implementation
models in prior work [36, 26, 20]. We demonstrate that this generalization
renders existing subtyping relations which are precise for a restrictive
implementation model incomplete. As a result of both extensions, our subtyping
relation requires reasoning about available messages [39] for completeness, a
novel feature that is absent from existing subtyping relations.

Our result applies to global types with _sender-driven_ choice, which
generalize global types from their original formulation with directed choice
[31], and borrows insights from recent work on a sound and complete projection
operator for this class of global types [37].

Contributions. In this paper, we present the first precise subtyping relation
that guarantees deadlock freedom and subprotocol fidelity with respect to a
global type, and that assumes an unrestricted, asynchronous CSM implementation
model. We solve the _Protocol Verification_ problem and the _Protocol
Refinement_ problem with respect to global type $\mathbf{G}$ and a set of
roles $\mathcal{P}$:

  1. 1.

_Protocol Verification_ : Given a CSM $\mathcal{A}$, does $\mathcal{A}$
implement $\mathbf{G}$?

  2. 2.

_Protocol Refinement_ : 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 let $B$ be a safe implementation 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}}}}$
in any well-behaved context for $\mathbf{G}$. Given $A$, can $A$ safely
replace $B$ in any well-behaved context for $\mathbf{G}$?

We exploit the connection between MST subtyping and CSM refinement to
formulate concise conditions that are directly checkable on candidate state
machines. Using this characterization, we show that both problems are
decidable in polynomial time.

##  2 Motivation

We first showcase that sound and complete projection operators can yield local
implementations that are exponential in the size of its global type, but can
be reduced to constant size by subtyping. We then demonstrate the
restrictiveness of existing subtyping relations both in terms of their notion
of safety and their implementation model.

Subset projection with exponentially many states. We first construct a family
of implementable global types $\mathbf{G}_{n}$ for $n\in\mathbb{N}$ such that
$\mathbf{G}_{n}$ has size linear in $n$ and the deterministic finite state
machine 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{q}}}}$
that recognizes the projection of the global language 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{q}}}}$’s
alphabet
$\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{q}}}}$,
denoted
$\mathcal{L}(\mathbf{G}_{n}){\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{q}}}}}$,
has size exponential in $n$.

The construction of the $\mathbf{G}_{n}$’s builds on the regular expression
$(a^{*}(ab^{*})^{n}a)^{*}$, which can only be recognized by a deterministic
finite state machine that grows exponentially with $n$ [23, Thm. 11].

First, we construct the part for $(ab^{*})^{i}a$ recursively. In global types,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern 1.19995ptm$ denotes 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}}}}$
sending a message $m$ to 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{q}}}}$,
$+$ denotes choice, $\mu t$ binds a recursion variable $t$ that can be used in
the continuation, and $0$ denotes termination.

$\small
G_{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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pta.\,μt_{3,i}.+\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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996ptm_{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{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996ptb.\,t_{3,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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996ptn_{3}.\,G_{i-1}\end{cases}\;\text{for
}i>0\quad\text{ and }\quad
G_{0}\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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996pta.\,t_{1}$

Here, each $G_{i}$ for $i>0$ generates $(ab^{*})$ and $G_{0}$ adds the last
$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}}}}$’s
choice to send either $m_{3}$ or $n_{3}$ 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}}}}$
respectively encodes the choice to continue iterating $b$’s or to stop in
$b^{*}$;
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$
however, is not involved in this exchange and thus
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$’s
local language is isomorphic to $(ab^{*})^{i}a$.

Next, we define some scaffolding $G(\hbox{-})$ for the outermost Kleene Star
and the first $a^{*}$:

$\small G(G^{\prime})\coloneq
μt_{1}.\,+\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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996ptm_{1}.\,μt_{2}.+\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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996ptm_{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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996pta.\,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{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996ptn_{2}.\,G^{\prime}\end{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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996ptn_{1}.\,0\end{cases}\enspace.$

We combine both to obtain the family $\mathbf{G}_{n}\coloneq G(G_{n})$.

As $\mathbf{G}_{n}$ is implementable, the subset projection [37] for each role
is defined. One feature of the implementations computed by this projection
operator is _local language preservation_ , meaning that the language
recognized by the local implementation is precisely the projection of the
global language onto its alphabet, e.g.
$\mathcal{L}(\mathbf{G}_{n}){\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{q}}}}}$
for 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{q}}}}$
with alphabet
$\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{q}}}}$.
In this case, because
$\mathcal{L}(\mathbf{G}_{n}){\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{q}}}}}$
can only be recognized by a deterministic finite state machine with size
exponential in $n$, the corresponding local language preserving implementation
also has size exponential in $n$.

However, not all implementations need to satisfy local language preservation.
Consider the type $\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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern
1.19995pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern
1.19995pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,0)$.
The projection of the global language 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{q}}}}$
limits
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 only receiving a sequence of
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
messages terminated by a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$
message. However, an implementation 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{q}}}}$
can rely on
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 send correct sequences of messages, and instead accept any message that it
receives. A similar pattern arises in the family $\mathbf{G}_{n}$, where the
exponentially-sized implementation for 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{q}}}}$
can simply be substituted with an automaton that allows to receive any 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}}}}$.

The restrictiveness of existing MST subtyping relations. Consider the two
implementations for 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}}}}$,
represented as finite state machines $A$ and $B$ in Figs. 1(b) and 1(a). State
machine $A$ embodies the idea of input covariance [25] by adding receive
actions, namely
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm$, which denotes 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}}}}$
receiving a message $m$ from 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{q}}}}$.
But is it the case that $A$ is a subtype of $B$? A preliminary answer based on
prior work [34, 26] is _no_ , for the reason that $A$ falls outside of the
implementation models considered in these works: the initial state in $A$
contains outgoing receive transitions from two distinct senders,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 one of the final states contains an outgoing transition. Thus, there
exists no local type representation of $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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm$

(a) $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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm$

(b) $B$

Figure 1: Two state machines for 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{q}}}}$

As a first step, let us generalize the implementation model to machines with
arbitrary finite state control, and revisit the question. It turns out that
the answer now depends on what protocol 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}}}}$,
alongside the other roles in the context, is following. Consider the two
global types

$\small\mathbf{G}_{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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996ptm.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996ptm.\,0\qquad\text{and}\qquad\mathbf{G}_{2}\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}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern 1.07996ptm.\,0\,\enspace.$

We observe that $A$ is a subtype of $B$ under the context of $\mathbf{G}_{2}$,
but not under the context of $\mathbf{G}_{1}$. Suppose that 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{q}}}}$
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}}}}$
are both following $\mathbf{G}_{1}$, and thus both roles send 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{p}}}}$.
Under asynchrony, the two messages can arrive in
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
channel in any order; this holds even in a synchronous setting. Therefore,
there exists an execution trace in which
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$
takes the transition labeled
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm$ in $A$ and first receives 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{r}}}}$.
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}}}}$
then finds itself in a final state with a pending 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}}}}$
that it is unable to receive, thus causing a deadlock in the CSM. On the other
hand, 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}}}}$
were following $\mathbf{G}_{2}$, the addition of the receive transition
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm$ is safe because it is never
enabled, and thus $A$ can safely compose with any context following
$\mathbf{G}_{2}$ without violating protocol fidelity and deadlock freedom.

##  3 Preliminaries

We restate relevant definitions from [37].

##### Words.

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

##### Message Alphabet.

Let $\mathcal{P}$ be a set of roles and $\mathcal{V}$ be a set of messages. We
define the set of _synchronous events_
$Σ_{\mathit{sync}}\coloneq\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern
1.19995ptm\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}}}}∈\mathcal{P}\text{
and }m∈\mathcal{V}\\}$ where
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern 1.19995ptm$ denotes that message $m$ is sent by
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}}$
atomically. This is split for _asynchronous events_. For a role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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 define the alphabet
$\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}}}},!}=\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002ptm\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}\\}$
of _send_ events and the alphabet
$\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm\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}\\}$
of _receive_ events. The 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{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern 0.80002ptm$ denotes 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}}}}$
sending 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}}}}$,
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{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm$ denotes 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}}}}$
receiving a message $m$ 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}}}}$.
We write
$\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}}}}}=\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}}}},!}\cup\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}}}},?}$,
$\Sigma_{!}=\bigcup_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}\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
$\Sigma_{?}=\bigcup_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}\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}}}},?}$.
Finally, $Σ_{\mathit{async}}=\Sigma_{!}\cup\Sigma_{?}$. We say that
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is _active_ in $x\in Σ_{\mathit{async}}$ if
$x\in\Sigma_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$.
For each role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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 define a homomorphism
${\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}}}}}$,
where
$x{\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}}}}}=x$
if
$x\in\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 $\varepsilon$ otherwise. We fix $\mathcal{P}$ and $\mathcal{V}$ in the
rest of the paper.

##### Global Types – Syntax.

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

$\displaystyle G$ $\displaystyle\Coloneqq 0\hskip 3.0pt\mid\hskip
3.0pt\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
1.19995pt{:}\kern 1.19995ptm_{i}.G_{i}\hskip 3.0pt\mid\hskip 3.0pt\mu
t.\;G\hskip 3.0pt\mid\hskip 3.0ptt$

where
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}}_{i}$
range over $\mathcal{P}$, $m_{i}$ over $\mathcal{V}$, and $t$ over a set of
recursion variables.

We require each branch of a choice to be distinct:
$∀i,j∈I.\,i≠j⇒({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}}_{j},m_{j})$,
the sender and receiver of an event to be distinct:
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}_{i}$
for each $i\in I$, and recursion to be guarded: in $μt.\,G$, there is at least
one message between $μt$ and each $t$ in $G$. We omit $\sum$ for singleton
choices. When working with a protocol described by a global type, we use
$\mathbf{G}$ to refer to the top-level type, and $G$ to refer to its subterms.

We use the extended definition of global types from [39] featuring _sender-
driven choice_. This definition subsumes classical MSTs that only allow
_directed choice_ [31]. We focus on communication primitives and omit features
like delegation or parametrization, and refer the reader to Section 7 for a
discussion of different MST frameworks.

##### Global Types – Semantics.

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

  * •

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

  * •

$δ_{\mathbf{G}}$ consists of the transitions
$(\sum_{i∈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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
1.19995pt{:}\kern
1.19995ptm_{i}.G_{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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
1.19995pt{:}\kern 1.19995ptm_{i},G_{i})$ for each $i∈I$, as well as
$(μt.G^{\prime},ε,G^{\prime})$ and $(t,ε,μt.G^{\prime})$ for each subterm $\mu
t.G^{\prime}$,

  * •

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

We define a homomorphism $\operatorname{\texttt{{split}}}$ onto the
asynchronous alphabet:

$\operatorname{\texttt{{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{p}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern
1.19995ptm)\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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002ptm.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm\enspace.$

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

We call a state $q_{G}\in Q_{\mathbf{G}}$ a _send-originating_ state, denoted
$q_{G}\in Q_{\mathbf{G},!}$ for 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}}}}$
if there exists a transition
$q_{G}\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern 1.19995ptm}q_{G^{\prime}}\in\delta_{\mathbf{G}}$, and a
_receive-originating_ state, denoted $q_{G}\in Q_{\mathbf{G},?}$ 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}}}}$
if there exists a transition
$q_{G}\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{\to}\kern
1.19995pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.19995pt{:}\kern 1.19995ptm}q_{G^{\prime}}\in\delta_{\mathbf{G}}$. We omit
mention of 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}}}}$
when clear from context.

##### Communicating State Machine [4].

$\mathcal{A}=\\{\\!\\!\\{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}}$
is a CSM over $\mathcal{P}$ and $\mathcal{V}$ if
${A}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}=(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{p}}}},\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_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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_{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}}}}},F_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 a deterministic finite state machine over
$\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}}}}$
for every
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$.
Let
$\prod_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}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{p}}}}$
denote the set of global states and
$\mathsf{Chan}=\\{({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}})\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}}}}\in\mathcal{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}}}}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\\}$
denote the set of channels. A  _configuration_ of $\mathcal{A}$ is a pair
$(\vec{s},\xi)$, where $\vec{s}\,$ is a global state and
$\xi:\mathsf{Chan}\rightarrow\mathcal{V}^{*}$ is a mapping from each channel
to a sequence of messages. We use
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
to denote the state of
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
in $\vec{s}$. The CSM transition relation, denoted $\rightarrow$, is defined
as follows.

  * •

$(\vec{s},\xi)\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern 0.80002ptm}(\vec{s}\mkern
2.0mu\vphantom{s}^{\prime},\xi^{\prime})$ if
$(\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern 0.80002ptm,\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}})\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}=\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
for every role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$,
$\xi^{\prime}({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}})=\xi({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}})\cdot
m$ and $\xi^{\prime}(c)=\xi(c)$ for every other channel $c\in\mathsf{Chan}$.

  * •

$(\vec{s},\xi)\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm}(\vec{s}\mkern
2.0mu\vphantom{s}^{\prime},\xi^{\prime})$ if
$(\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern 0.80002ptm,\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}})\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
$\vec{s}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}=\vec{s}\mkern
2.0mu\vphantom{s}^{\prime}_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}$
for every role
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{r}}}}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$,
$\xi({\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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}}}})=m\cdot\xi^{\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}}}},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 $\xi^{\prime}(c)=\xi(c)$ for every other channel $c\in\mathsf{Chan}$.

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

######  Definition 1 (Implementability)

We say that a 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}}$
implements a global type $\mathbf{G}$ if the following two properties hold:
(i) _protocol fidelity:_
$\mathcal{L}(\\{\\!\\!\\{A_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\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})$,
and  (ii) _deadlock freedom:_
$\\{\\!\\!\\{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}}$is
deadlock-free.  A global type $\mathbf{G}$ is _implementable_ if there exists
a CSM that implements it.

One candidate implementation for global types can be computed directly from
$\mathsf{GAut}(\mathbf{G})$, by removing actions unrelated to each role and
determinizing the result. The following two definitions define this candidate
implementation in two steps.

######  Definition 2 (Projection by Erasure [37])

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

We determinize
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
via a standard subset construction [45] to obtain a deterministic local state
machine for
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.
Note that the construction ensures that
$Q_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
only contains subsets of $Q_{\mathbf{G}}$ whose states are reachable via the
same traces.

######  Definition 3 (Subset Construction [37])

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

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

  * •

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

  * •

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

  * •

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

  * •

$\delta_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{\delta}|_{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{p}}}}}\times\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

  * •

$F_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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\\{s\in
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{p}}}}}\mid
s\cap F_{\mathbf{G}}\neq\emptyset\\}$.

Li et al. [37] showed that if $\mathbf{G}$ is implementable, then
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$ and satisfies the following property:

###### Definition 4

Let $\mathbf{G}$ be a global type. We call an implementation
$\\{\\!\\!\\{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}}$
_local language preserving_ with respect to $\mathbf{G}$ if
$\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}}}})=\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}}}}}$
for all
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}$.

For the remainder of the paper, we fix a global type $\mathbf{G}$ that we
assume is implementable.

##  4 Deciding __Protocol Verification__

_Protocol Verification_ asks: Given a CSM $\mathcal{A}$, does $\mathcal{A}$
implement $\mathbf{G}$? For two CSMs $\mathcal{A}$ and $\mathcal{B}$, we say
that $\mathcal{A}$ refines $\mathcal{B}$ if and only if every trace in
$\mathcal{A}$ is a trace in $\mathcal{B}$, and a trace in $\mathcal{A}$
terminates maximally in $\mathcal{A}$ if and only if it terminates maximally
in $\mathcal{B}$. If $\mathcal{A}$ and $\mathcal{B}$ refine each other, we say
that they are equivalent. Further, in the case that $\mathcal{B}$ is deadlock-
free, one can simplify the condition to the following: every trace in
$\mathcal{A}$ is a trace in $\mathcal{B}$, and if a trace terminates in
$\mathcal{A}$, then it terminates in $\mathcal{B}$ and is maximal in
$\mathcal{A}$.

We can recast _Protocol Verification_ in terms of CSM refinement using the
fact that
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 an implementation for $\mathbf{G}$. Therefore, the question amounts to
asking whether $\mathcal{A}$ and
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
are equivalent.

Our goal is then to present a characterization _$C_{1}$_ that satisfies the
following:

###### Theorem 4.1

Let $\mathbf{G}$ be an implementable global type and $\mathcal{A}$ be a CSM.
Then,
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 $\mathcal{A}$ are equivalent if and only if _$C_{1}$_ is satisfied.

We motivate our characterization for _Protocol Verification_ using a series of
examples. Consider the following simple global type $\mathbf{G}_{1}$:

$\small\mathbf{G}_{1}\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{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,0\,\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,0\,\end{cases}$

This global type is trivially implementable; the subset construction for 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{q}}}}$
obtained by the projection operator in [37] is depicted in Fig. 2(a). Clearly,
in any CSM implementing $\mathbf{G}_{1}$, the subset construction can be
replaced with the more compact state machine $A_{1}$, shown in Fig. 2(b).

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$

(a)
$\mathscr{C}(\mathbf{G}_{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}}}})$

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$

(b) $A_{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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern 1.30005pt\\_\kern
0.80002pt{\operatorname{?}}\kern 0.80002pt\\_$

(c) $A_{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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern 1.30005pt\\_\kern
0.80002pt{\operatorname{?}}\kern 0.80002pt\\_$

(d) $A_{3}$

Figure 2: Subset construction of $\mathbf{G}_{1}$ 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}}}}$
and three alternative implementations

For a local state machine in a CSM, control flow is determined by both the
local transition relation and the global channel state. However, in some
cases, the local information is redundant: the role’s channel contents alone
are enough to enforce that it produces the correct behaviors. In the example
above, after
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$
chooses to send
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}$
either
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$
or ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}$
will guarantee that the correct message, i.e. the same one, is sent back 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}}}}$.
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}}}}$’s
state machine can rely on its channel contents to follow the protocol – it
does not need separate control states for each message. In fact, we can
further replace
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
control states after sending with an accepting universal receive state, as
shown in $A_{2}$ in Fig. 2(c). Finally, we can add send transitions from
unreachable states, as shown in $A_{3}$ in Fig. 2(d).

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{?}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$

(a)
$\mathscr{C}(\mathbf{G}_{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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern 1.30005pt\\_\kern
0.80002pt{\operatorname{?}}\kern 0.80002pt\\_$

(b) $A_{4}$

${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern 1.30005pt\\_\kern
0.80002pt{\operatorname{?}}\kern 0.80002pt\\_$

(c) $A_{5}$

Figure 3: Subset construction of $\mathbf{G}_{2}$ 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}}}}$
and two alternative implementations

Similar patterns arise for send actions. Consider the following variation of
the first global type, $\mathbf{G}_{2}$:

$\small\mathbf{G}_{2}\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{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}b}.\,0\,\\\
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}.\,{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}\kern
1.07996pt{\to}\kern
1.07996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.07996pt{:}\kern
1.07996pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}m}.\,0\,\end{cases}$

The subset construction from [37] yields the state machine 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}}}}$
shown in Fig. 3(a).

Our reasoning above shows that $A_{4}$, depicted in Fig. 3(b), is a correct
alternative implementation 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}}}}$.
Now observe that the pre-states of the two
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002pt{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}o}$
transitions can be collapsed because their continuations are identical. This
yields another correct alternative implementation $A_{5}$, shown in Fig. 3(c).

Informally, the subset construction takes a “maximalist” approach, creating as
many distinct states as possible from the global type, and checking whether
they are enough to guarantee that the role behaves correctly. However,
sometimes this maximalism creates redundancy: just because two states are
distinct according to the global type does not mean they need to be. In these
cases, an implementation has the flexibility to merge certain distinct states
together, or add transitions to a state. We wish to precisely characterize
when such modifications to local state machines preserve protocol fidelity and
deadlock freedom.

Our conditions for _$C_{1}$_ are inspired by the Send and Receive Validity
conditions that precisely characterize implementability for global types,
given in [37]. We restate the conditions, in addition to relevant definitions,
for clarity.

######  Definition 5 (Available messages [39])

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

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

$\mathit{get\mu}(\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.95996pt{\to}\kern
0.95996pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.95996pt{:}\kern
0.95996ptm_{i}.G_{i})\coloneq\bigcup_{i∈I}\mathit{get\mu}(G_{i})$

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

$M^{\mathcal{B},T}_{(0\ldots)}\coloneq∅\hfill
M^{\mathcal{B},T}_{(μt.G\ldots)}\coloneq
M^{\mathcal{B},T∪\\{t\\}}_{(G\ldots)}\hfill
M^{\mathcal{B},T}_{(t\ldots)}\coloneq\begin{cases}∅&\text{if}~{}t∈T\\\
M^{\mathcal{B},T∪\\{t\\}}_{(\mathit{get\mu}_{\mathbf{G}}(t)\ldots)}&\text{if}~{}t∉T\end{cases}\\\
M^{\mathcal{B},T}_{(\sum_{i∈I}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.75597pt{\to}\kern
0.75597pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.75597pt{:}\kern
0.75597ptm_{i}.G_{i}\ldots)}\coloneq\begin{cases}\bigcup_{i∈I,m∈\mathcal{V}}(M^{\mathcal{B},T}_{(G_{i}\ldots)}\setminus\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
1.17004pt{\triangleright}\kern
0.72002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.72002pt{\operatorname{!}}\kern
0.72002ptm\\})∪\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.17004pt{\triangleright}\kern
0.72002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.72002pt{\operatorname{!}}\kern
0.72002ptm_{i}\\}\quad\hfill\text{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{p}}}}∉\mathcal{B}\\\
\bigcup_{i∈I}M^{\mathcal{B}∪\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{q}}}}_{i}\\},T}_{(G_{i}\ldots)}\quad\hfill\text{if}~{}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}∈\mathcal{B}\end{cases}$

We write $M^{\mathcal{B}}_{(G\ldots)}$ for
$M^{\mathcal{B},\emptyset}_{(G\ldots)}$. If $\mathcal{B}$ is a singleton set,
we omit set notation and write
$M^{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}_{(G\ldots)}$
for
$M^{\\{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\\}}_{(G\ldots)}$.

Intuitively, the available messages definition captures all of the messages
that can be at the head of their respective channels when a particular role is
blocked from taking further transitions.

For notational convenience, we define the _origin_ and _destination_ of a
transition following [37], but generalized from the subset construction
automaton.

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

Let $\mathbf{G}$ be a global type and let $\delta_{\downarrow}$ be the
transition relation of
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$.
For
$x\in\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 $s,s^{\prime}\subseteq Q_{\mathbf{G}}$, we define the set of _transition
origins_ $\operatorname{tr-orig}(s\xrightarrow{x}s^{\prime})$ and _transition
destinations_ $\operatorname{tr-dest}(s\xrightarrow{x}s^{\prime})$ as follows:

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

Li et al. [37] showed that $\mathbf{G}$ is implementable if and only if the
subset construction CSM
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
satisfies Send and Receive Validity for each
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}})$.

######  Definition 7 (Send Validity)

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

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

######  Definition 8 (Receive Validity)

$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}})$
satisfies _Receive Validity_ iff no receive transition is enabled in an
alternative continuation that originates from the same source state:

$\begin{array}[]{l}\forall
s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm_{1}}s_{1},\,s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm_{2}}s_{2}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}.\\\
\qquad{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\;\implies\;\forall~{}G_{2}\in\operatorname{tr-
dest}(s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm_{2}}s_{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}}}}_{1}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern 0.80002ptm_{1}\notin
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}}}}}_{(G_{2}\ldots)}\enspace.\end{array}$

We wish to adapt these conditions to define _$C_{1}$_. However, unlike Send
and Receive Validity, which are defined on special state machines, namely the
subset construction for each role, the _Protocol Verification_ problem asks
whether arbitrary state machines implement the given $\mathbf{G}$.

We first present a _state decoration_ function which maps local states in an
arbitrary deterministic finite state machine to sets of global states in
$\mathbf{G}$. Intuitively, state decoration captures all global states that
can be reached in the projection by erasure automaton
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\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{q}}}}}$
on the same prefixes that reach the present state in the local state machine.

######  Definition 9 (State decoration with respect to $\mathbf{G}$)

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}}}}\in\mathcal{P}$
be a role and let
$A=(Q,\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}}}},s_{0},\delta,F)$
be a deterministic finite state machine 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}}}}$.
Let
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\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_{\mathbf{G}},\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}}}}\uplus\\{\varepsilon\\},\delta_{\downarrow},q_{0,\mathbf{G}},F_{\mathbf{G}})$
be
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
projection by erasure state machine for $\mathbf{G}$. We define a total
function $d_{\mathbf{G},A}:Q\rightarrow 2^{Q_{\mathbf{G}}}$ that maps each
state in $A$ to a subset of states in
$\mathsf{GAut}(\mathbf{G})\negmedspace\\!\downarrow_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}$
such that:

$d_{\mathbf{G},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}}}}}(s)=\\{q\in
Q_{\mathbf{G}}\mid\exists
u\in\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}}}}.~{}s_{0}\xrightarrow{u}\mathrel{\vphantom{\to}{}^{*}}s\in\delta\land
q_{0,\mathbf{G}}\xrightarrow{u}\mathrel{\vphantom{\to}{}^{*}}q\in\delta_{\downarrow}\\}\enspace.$

We refer to
$d_{\mathbf{G},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}}}}}(s)$
as the _decoration set_ of $s$, and omit the subscripts
$\mathbf{G},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}}}}$
when clear from context.

###### Remark 1

Note that the subset construction can be viewed as a special state machine for
which the state decoration function is the identity function. In other words,
for all $s\in
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{p}}}}$
where
$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{p}}}}$
is the set of states of
$\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}})$,
$d(s)=s$.

We are now equipped to present _$C_{1}$_.

######  Definition 10 (_$C_{1}$_)

Let $\mathbf{G}$ be a global type and $\mathcal{A}$ be a CSM. _$C_{1}$_ is
satisfied when for all
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}=(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{p}}}},\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_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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_{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}}}}},F_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}})$
denoting the state machine 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}}}}$
in $\mathcal{A}$, the following conditions hold:

  * •

_Send Decoration Validity_ : every send transition
$s\xrightarrow{x}s^{\prime}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
is enabled in all states decorating $s$:
$\forall
s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern
0.80002ptm}s^{\prime}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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{tr-
orig}(d(s)\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern 0.80002ptm}d(s^{\prime}))=d(s)$.

  * •

_Receive Decoration Validity_ : no receive transition is enabled in an
alternative continuation originating from the same state:
$\begin{array}[]{l}\forall
s\xrightarrow{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.80002pt{\operatorname{?}}\kern
0.80002ptm_{1}}s_{1},~{}s\xrightarrow{x}s_{2}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}.~{}x\neq{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\triangleleft}\kern
1.30005pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}\kern
0.80002pt{\operatorname{?}}\kern 0.80002pt\\_\implies\\\ \qquad\forall
G^{\prime}\in\operatorname{tr-
dest}(d(s)\xrightarrow{x}d(s_{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}}}}_{1}\kern
1.30005pt{\triangleright}\kern
0.80002pt{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}}\kern
0.80002pt{\operatorname{!}}\kern 0.80002ptm_{1}\notin
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}}}}}_{(G^{\prime}\ldots)}.\end{array}$

  * •

_Transition Exhaustivity_ : every transition that is enabled in some global
state decorating $s$ must be an outgoing transition from $s$:
$\forall s\in Q.~{}\forall
G\xrightarrow{x}\mathrel{\vphantom{\to}{}^{*}}G^{\prime}\in\delta_{\downarrow}.~{}G\in
d(s)\implies\exists s^{\prime}\in
Q.~{}s\xrightarrow{x}s^{\prime}\in\delta_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$.

  * •

_Final State Validity_ : a reachable state with a non-empty decorating set is
final if its decorating set contains a final global state:
$\forall s\in Q.~{}d(s)\neq\emptyset\implies(d(s)\cap
F_{\mathbf{G}}\neq\emptyset\implies s\in
F_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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 want to show the following equivalence to prove Theorem 4.1:

_$C_{1}$_ $\Leftrightarrow\mathcal{A}$ refines
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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
$\\{\\!\\!\\{{\mathscr{C}(\mathbf{G},{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}$
refines $\mathcal{A}$.

We address soundness (the forward direction) and completeness (the backward
direction) in turn. Soundness states that _$C_{1}$_ is sufficient to show that
$\mathcal{A}$ preserves all behaviors of the subset construction, and does not
introduce new behaviors.

We say that a state machine $A$ for 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}}}}$
satisfies _Local Language Inclusion_ if it satisfies
$\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}}}}}}\subseteq\mathcal{L}(A)$.
The following lemma, proven in Section 0.A.2, establishes that _Local Language
Inclusion_ follows from _Transition Exhaustivity_ and _Final State Validity_.
lemmaimpliesLocalLangIncl Let
$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}}}}=(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{p}}}},\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_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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_{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}}}}},F_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,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}}}})$
denote the state machine 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}}}}$
in $\mathcal{A}$. Then, _Transition Exhaustivity_ and _Final State Validity_
imply
$\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}}}}}}\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{p}}}})$.

The fact that $\mathcal{A}$ preserves behaviors follows immediately from
_Local Language Inclusion_. The fact that $\mathcal{A}$ does not introduce new
behaviors, on the other hand, is enforced by _Send Decoration Validity_ and
_Receive Decoration Validity_.

In the soundness proof for each of our conditions, we prove refinement via
structural induction on traces. We show refinement in two steps, first showing
that any trace in one CSM is a trace in the other, and then showing that any
terminated trace in one CSM is terminated in the other and maximal.

We recall two definitions from [37] used in the soundness proof.

######  Definition 11 (Intersection sets)

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

$\operatorname{R}^{\mathbf{G}}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}(w)\coloneq\\{\rho\text{
is a maximal run of }\mathsf{GAut}(\mathbf{G})\mid
w{\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\leq\operatorname{\texttt{{split}}}(\texttt{{trace}}(\rho)){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\\}\enspace.$

We denote the intersection of the possible run sets for all roles as

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

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

Let $\mathbf{G}$ be a global type,
${\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}$
a role, and $w\in Σ_{\mathit{async}}^{*}$ a word. Let $\rho$ be a possible run
in
$\operatorname{R}^{\mathbf{G}}_{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}(w)$.
We define the longest prefix of $\rho$ matching $w$:

$\alpha^{\prime}\coloneq\max\\{\rho^{\prime}\mid\rho^{\prime}\leq\rho~{}\wedge~{}\operatorname{\texttt{{split}}}(\texttt{{trace}}(\rho^{\prime})){\Downarrow}_{\Sigma_{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\bm{{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\mathtt{p}}}}}\leq