11institutetext: Université Côte d’Azur, CNRS, I3S, Sophia Antipolis, France

# Guessing the buffer bound for k-synchronizability

Cinzia Di Giusto  11 Laetitia Laversa  11 Etienne Lozes  11

###### Abstract

A communicating system is $k$-synchronizable if all of the message sequence
charts representing the executions can be divided into slices of $k$ sends
followed by $k$ receptions. It was previously shown that, for a fixed given
$k$, one could decide whether a communicating system is $k$-synchronizable.
This result is interesting because the reachability problem can be solved for
$k$-synchronizable systems. However, the decision procedure assumes that the
bound $k$ is fixed. In this paper we improve this result and show that it is
possible to decide if such a bound $k$ exists.

###### Keywords:

communicating automata MSC synchronizability

##  1 Introduction

Communicating finite state machines [4] model distributed systems where
participants exchange messages via FIFO buffers. Due to the unboundedness of
the buffers, the model is Turing powerful as soon as there are two
participants and two queues. In order to recover decidability, several works
introduced restrictions on the model, for instance: lossiness of the channels
[1], specific topologies, or bounded context switching [13]. Another line of
research focused on analyzing the system under the assumption that the
semantics is synchronous [2, 9, 14, 8, 6, 5, 12, 11] or that buffers are
bounded. This assumption is not as restrictive as it may seem at first,
because several systems enjoy the property that their execution, although not
necessarily bounded, can be simulated by a causally equivalent bounded
execution. Existentially $k$-bounded communicating systems [10] are precisely
the systems whose message sequence charts can be generated by $k$-bounded
executions. In particular, the reachability problem is decidable for
existentially $k$-bounded communicating systems. A limitation of this
framework is that the bound $k$ on the buffer size must be fixed. A natural
question is whether the existence of such a bound can be decided. Genest,
Kuske and Muscholl answered this question negatively [10]. Bouajjani et al.
[3]111The results in [3] have then been refined in [7] introduced a variant of
existentially $k$-bounded communicating systems they called $k$-synchronizable
systems. A system is $k$-synchronizable if each of its execution is causally
equivalent to a sequence of communication rounds composed of at most $k$ sends
followed by at most $k$ receptions. In particular, each execution of a
$k$-synchronizable system is causally equivalent to a $k$-bounded execution
(provided all messages are eventually received). Like for existentially
bounded systems, the reachability problem becomes decidable for
$k$-synchronizable systems, and the membership problem - whether a given
system is $k$-synchronizable for a fixed given $k$ is decidable as well.
Bouajjani et al. conjectured that the existence of a bound $k$ on the size of
the communication rounds was undecidable.

Instead, in this paper, we show that this problem is decidable. This result
contrasts with the negative result about the same question for existentially
bounded communicating systems. There is an important difference between
existentially bounded and $k$-synchronizable ones that explains this
situation. Existentially bounded systems deal with peer-to-peer
communications, with one buffer per pair of machines, whereas
$k$-synchronizable systems deal with mailbox communications where one buffer
per machine merges all incoming messages.

The paper is organized as follows: in the next section, we introduce
preliminary definitions on communicating automata and $k$-synchronizable
systems. In Section 3 we explain the general strategy for computing the bound
$k$, which is to compute the automata of two regular languages: the language
of reachable exchanges, and the language of prime exchanges. In Section 4 we
focus on reachable exchanges, and in Section 5 on prime exchanges. Section 6
lastly computes the bound $k$. Finally Section 7 concludes with some final
remarks. An appendix with additional material and proofs is added for the
reviewer convenience.

##  2 Preliminaries

Let $\mathbb{V}$ be a finite set of messages and $\mathbb{P}$ a finite set of
processes exchanging messages. A send action, denoted $send(p,q,v)$,
designates the sending of message $v$ from process $p$ to process $q$, storing
it in the queue of $q$. Similarly, a receive action $rec(q,v)$ expresses that
process $q$ pops message $v$ from its queue of incoming messages. We write $a$
to denote a send or receive action. Let $S~{}=~{}\\{send(p,q,v)\mid
p,q\in\mathbb{P},v\in\mathbb{V}\\}$ be the set of send actions and
$R~{}=~{}\\{rec(q,v)\mid q\in\mathbb{P},v\in\mathbb{V}\\}$ the set of receive
actions. $S_{p}$ and $R_{p}$ stand for the set of sends and receives of
process $p$ respectively.

A _system_ is a tuple $\mathfrak{S}=\left((L_{p},\delta_{p},l^{0}_{p})\mid
p\in\mathbb{P}\right)$ where, for each process $p$, $L_{p}$ is a finite set of
local control states, $\delta_{p}\subseteq(L_{p}\times(S_{p}\cup R_{p})\times
L_{p})$ is the transition relation and $l^{0}_{p}$ is the initial state. In
the rest of the paper, when talking about a system $\mathfrak{S}$, we may also
identify it with the global automaton obtained as the product of the process
automata and denoted $(L_{\mathfrak{S}},\delta_{\mathfrak{S}},\mathbf{l_{0}})$
where $L_{\mathfrak{S}}=\Pi_{p\in\mathbb{P}}L_{p}$ is the set of global
control states, $\mathbf{l_{0}}=(l^{0}_{p})_{p\in\mathbb{P}}$ is the initial
global control state and
$((l_{1},\cdots,l_{q},\cdots,l_{n}),a,(l_{1},\cdots,l^{\prime}_{q},\cdots,l_{n}))\in\delta_{\mathfrak{S}}$
iff $(l_{q},a,l^{\prime}_{q})\in\delta_{q}$ for $q\in\mathbb{P}$. We write
$\mathbf{l}$ in bold to denote the tuple of control states
$(l_{p})_{p\in\mathbb{P}}$, and we sometimes write
$l_{q}\xrightarrow{a}_{q}l^{\prime}_{q}$ (resp.
$\mathbf{l}\xrightarrow{a}\mathbf{l}^{\prime})$ for
$(l_{q},a,l_{q}^{\prime})\in\delta_{q}$ (resp.
$(\mathbf{l},a,\mathbf{l}^{\prime})\in\delta_{\mathfrak{S}}$). We write
$\xRightarrow{a_{1}\cdots a_{n}}$ for
$\xrightarrow{a_{1}}\cdots\xrightarrow{a_{n}}$.

A _configuration_ is a pair $(\mathbf{l},\mathtt{Buf})$ where
$\mathbf{l}=(l_{p})_{p\in\mathbb{P}}\in L_{\mathfrak{S}}$ is a global control
state of $\mathfrak{S}$, and
$\mathtt{Buf}=(b_{p})_{p\in\mathbb{P}}\in(\mathbb{V}^{*})^{\mathbb{P}}$ is a
vector of buffers, each $b_{p}$ being a word over $\mathbb{V}$.
$\mathtt{Buf}_{0}$ stands for the vector of empty buffers. The mailbox
semantics of a system is defined by the two rules below.

[SEND]

$\mathbf{l}\xrightarrow{send(p,q,v)}\mathbf{l^{\prime}}\quad
b_{q}^{\prime}=b_{q}\cdot v$
$(\mathbf{l},\mathtt{Buf})\xmapsto{send(p,q,v)}(\mathbf{l}^{\prime},\mathtt{Buf}[b_{q}^{\prime}/b_{q}])$

[RECEIVE]

$\mathbf{l}\xrightarrow{rec(q,v)}\mathbf{l}^{\prime}\quad b_{q}=v\cdot
b_{q}^{\prime}$
$(\mathbf{l},\mathtt{Buf})\xmapsto{rec(q,v)}(\mathbf{l}^{\prime},\mathtt{Buf}[b_{q}^{\prime}/b_{q}])$

In this paper, we focus on mailbox semantics. An execution $e=a_{1}\cdots
a_{n}$ is a sequence of actions in $S\cup R$ such that
$(\mathbf{l_{0}},\mathtt{Buf}_{0})\xmapsto{a_{1}}\cdots\xmapsto{a_{n}}(\mathbf{l},\mathtt{Buf})$
for some $\mathbf{l}$ and $\mathtt{Buf}$. As usual, $\ext@arrow
0599{\arrowfill@{\Mapstochar\Relbar}\Relbar\Rightarrow}{}{e}$ stands for
$\xmapsto{a_{1}}\cdots\xmapsto{a_{n}}$. We write $asEx(\mathfrak{S})$ to
denote the set of executions of a system $\mathfrak{S}$. Executions impose a
total order over the actions. To stress the causal dependencies between
messages we use message sequence charts (MSCs) that only impose an order
between matched pairs of actions and between the actions of a same process.

######  Definition 1 (Message Sequence Chart)

A message sequence chart $\mu$ is a tuple
$(Ev,\lambda,\prec_{po},\prec_{src})$ such that

  1. 1.

$Ev$ is a finite set of events partially ordered under
$(\prec_{po}\cup\prec_{src})^{*}$,

  2. 2.

$\lambda:Ev\to S\cup R$ tags each event with an action,

  3. 3.

for each process $p$, $\prec_{po}$ induces a total order on the events of $p$,
i.e. on $\lambda^{-1}(S_{p}\cup R_{p})$,

  4. 4.

$(Ev,\prec_{src})$ is the graph of a bijection between a subset of
$\lambda^{-1}(S)$ and the whole of $\lambda^{-1}(R)$

  5. 5.

for all $s\prec_{src}r$, there are $p,q,v$ such that $\lambda(s)=send(p,q,v)$
and $\lambda(r)=rec(q,v)$.

######  Definition 2 (Concatenation of MSCs)

Let $\mu_{1}=(Ev_{1},\lambda_{1},\prec_{po}^{1},\prec_{scr}^{1})$ and
$\mu_{2}=(Ev_{2},\lambda_{2},\prec_{po}^{2},\prec_{scr}^{2})$ be two MSCs.
Their concatenation $\mu_{1}\cdot\mu_{2}$ is the MSC
$\mu=(Ev,\lambda,\prec_{po},\prec_{src})$ such that:

  * •

$Ev=Ev_{1}\cup Ev_{2}$

  * •

$\lambda=\lambda_{1}\cup\lambda_{2}$

  * •

$\prec_{po}=\prec_{po}^{1}\cup\prec_{po}^{2}\cup\bigcup_{p\in\mathbb{P}}\\{(e_{1},e_{2})\mid
e_{1}\in\lambda_{1}^{-1}(S_{p}\cup R_{p}),e_{2}\in\lambda_{2}^{-1}(S_{p}\cup
R_{p})\\}$

  * •

$\prec_{src}=\prec_{src}^{1}\cup\prec_{src}^{2}$.

In a sequence of actions $e=a_{1}\cdots a_{n}$, a send action
$a_{i}=send(p,q,v)$ is _matched_ by a reception
$a_{j}=rec(q^{\prime},v^{\prime})$ (denoted by
$a_{i}\mathrel{\vdash\\!\\!\dashv}a_{j}$) if $i<j$, $p=p^{\prime}$,
$q=q^{\prime}$, $v=v^{\prime}$, and there is $\ell\geq 1$ such that $a_{i}$
and $a_{j}$ are the $\ell$th actions of $e$ with these properties
respectively. A send action $a_{i}$ is _unmatched_ if there is no matching
reception in $e$.

The MSC associated with the execution $e=a_{1}\cdots a_{n}$ is
$(Ev,\lambda,\prec_{po},\prec{src})$ where $Ev=\\{1,\cdots,n\\}$,
$\lambda(i)=a_{i}$, $i\prec_{po}j$ iff $i<j$ and $\\{a_{i},a_{j}\\}\subseteq
S_{p}\cup R_{p}$ for some $p$, and $i\prec_{src}j$ if
$a_{i}\mathrel{\vdash\\!\\!\dashv}a_{j}$.

When $v$ is either an unmatched $send(p,q,v)$ or a pair of matched actions
$\\{send(p,q,v),rec(q,v)\\}$, we write $\mathsf{proc}_{S}(v)$ for $p$ and
$\mathsf{proc}_{R}(v)$ for $q$. Note that $\mathsf{proc}_{R}(v)$ is defined
even if $v$ is unmatched. An MSC is depicted with vertical timelines (one for
each process) where time goes from top to bottom. Points on the lines
represent events of this process. We draw an arc between two matched events
and a dashed arc to depict an unmatched send. The concatenation
$\mu_{1}\cdot\mu_{2}$ of two MSCs is the union of the two MSCs where, for each
$p$, all $p$-events of $\mu_{1}$ are considered $\prec_{po}$ smaller than all
$p$-events of $\mu_{2}$. We write $msc(e)$ for the MSC associated with the
execution $e$, and we say that a sequence of actions $e$ is a linearization of
a given MSC if it is the sequence of actions induced by a total order
extending $(\prec_{po}\cup\prec_{src})^{*}$. We write $asTr(\mathfrak{S})$ for
the set $\\{msc(e)\mid e\in asEx(\mathfrak{S})\\}$. We write
$\mathbf{l}\mathrel{\leavevmode\hbox to10.82pt{\vbox
to10.53pt{\pgfpicture\makeatletter\hbox{\hskip 5.41168pt\lower-6.19025pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.10892pt}{-0.8264pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle\mu$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{{ {\pgfsys@beginscope{{}}
\pgfsys@setlinewidth{0.4pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{}
\pgfsys@moveto{-1.005pt}{1.9875pt}\pgfsys@curveto{-0.5175pt}{0.9375pt}{0.795pt}{0.0375pt}{1.545pt}{0.0pt}\pgfsys@curveto{0.795pt}{-0.0375pt}{-0.5175pt}{-0.9375pt}{-1.005pt}{-1.9875pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{2.71669pt}{-4.54025pt}\pgfsys@lineto{0.46169pt}{-4.54025pt}\pgfsys@lineto{-0.39189pt}{-5.24025pt}\pgfsys@lineto{-2.09906pt}{-3.84026pt}\pgfsys@lineto{-4.46169pt}{-4.54025pt}\pgfsys@lineto{-4.46169pt}{-4.54025pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{2.71669pt}{-4.54025pt}\pgfsys@lineto{0.46169pt}{-4.54025pt}\pgfsys@lineto{-0.39189pt}{-5.24025pt}\pgfsys@lineto{-2.09906pt}{-3.84026pt}\pgfsys@lineto{-4.46169pt}{-4.54025pt}\pgfsys@lineto{-4.46169pt}{-4.54025pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{2.71669pt}{-4.54025pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mathbf{l}^{\prime}$
to denote that $\mathbf{l}\xRightarrow{e}\mathbf{l^{\prime}}$ for any
linearization $e$ of $\mu$. Finally, we recall from [7] the definition of
causal delivery that allows to consider only MSCs that correspond to
executions in the mailbox semantics.

######  Definition 3 (Causal delivery)

Let $\mu=(Ev,\lambda,\prec_{po},\prec_{src})$ be an MSC. We say that $\mu$
satisfies causal delivery if it admits a linearization with the total order
$<$ such that for any two events $s_{1},s_{2}\in Ev$, if $s_{1}<s_{2}$,
$\lambda(s_{1})~{}=~{}send(p,q,v)$ and
$\lambda(s_{2})=send(p^{\prime},q,v^{\prime})$ for a same destination process
$q$, then either $s_{2}$ is unmatched, or there are $r_{1},r_{2}$ such that
$s_{1}\prec_{src}r_{1}$, $s_{2}\prec_{src}r_{2}$, and $r_{1}<r_{2}$.

A $k$-exchange (with $k\geq 1$) is an MSC that admits a linearization $e\in
S^{\leq k}R^{\leq k}$ starting with at most $k$ sends and followed by at most
$k$ receives. An MSC is _$k$ -synchronous_ if it can be chopped into a
sequence of _$k$ -exchanges_.

######  Definition 4 ($k$-synchronous)

An MSC $\mu$ is $k$-synchronous if $\mu=\mu_{1}\cdot\mu_{2}\cdots\mu_{n}$
where, for all $i\in[1..n]$, $\mu_{i}$ is a k$-exchange$.

For instance, the MSC $\mu_{1}$ depicted on Fig. 2 is $2$-synchronous, as it
can be split in two $2$-exchanges.

An execution $e$ is $k$-synchronizable if $msc(e)$ is $k$-synchronous. A
system $\mathfrak{S}$ is _$k$ -synchronizable_ if all its executions are
$k$-synchronizable.

$p$$q$$r$ Figure 1: MSC $\mu_{1}$

######  Theorem 2.1 ([3, 7])

It is decidable whether a system $\mathfrak{S}$ is $k$-synchronizable for a
given $k$. Moreover, it is decidable to know whether a control state is
reachable under the assumption that $\mathfrak{S}$ is $k$-synchronizable.

This result is interesting but somehow incomplete as it assumes that a fixed
value of the parameter $k$ has been found. We aim at answering this limitation
by computing the _synchronizability degree_ of a given system.

######  Definition 5 (Synchronizability degree)

The synchronizability degree $\mathsf{sd}(\mathfrak{S})$ of a system
$\mathfrak{S}$ is the smallest $k$ such that $\mathfrak{S}$ is
$k$-synchronizable. In particular, $\mathsf{sd}(\mathfrak{S})=\infty$ if
$\mathfrak{S}$ is not $k$-synchronizable for any $k$.

##  3 Largest prime reachable exchange

In this section, we relate the synchronizability degree of a system to the
size of a “maximal, prime, reachable exchange”. We start with defining these
notions.

An _exchange_ is a $k$-exchange for some arbitrary $k$, and we call $k$ the
size of the exchange. An exchange $\mu$ is _reachable_ if there exist
exchanges $\mu_{1},\cdots,\mu_{n}$ for some $n\geq 0$ and such that
$\mu_{1}\cdots\mu_{n}\cdot\mu\in asTr(\mathfrak{S})$. An exchange $\mu$ is
_prime_ if there does not exist a decomposition $\mu=\mu_{1}\cdot\mu_{2}$ in
two non-empty exchanges. For instance, the 2-exchange (depicted by the MSC
$\mu_{2}$, Fig. 3) with linearization:

$send(p,q,v_{1})\cdot send(r,q,v_{2})\cdot rec(q,v_{1})\cdot rec(q,v_{2})$

is not prime, as it can be factored in two 1-exchanges as follows

$send(p,q,v_{1})\cdot rec(q,v_{1})~{}~{}\cdot~{}~{}send(r,q,v_{2})\cdot
rec(q,v_{2}).$

$p$$q$$r$$v_{1}$$v_{2}$ Figure 2: MSC $\mu_{2}$

The size of the biggest prime reachable exchange is related to the
synchronizability degree $\mathsf{sd}(\mathfrak{S})$ by the following
property.

######  Lemma 1 ()

Let $k\in\mathbb{N}\cup\\{\infty\\}$ be the supremum of the sizes of all prime
reachable exchanges. (1) If $k=\infty$, then
$\mathsf{sd}(\mathfrak{S})=\infty$ (2) if $k<\infty$, then either
$\mathfrak{S}$ is $k$-synchronizable and $\mathsf{sd}(\mathfrak{S})=k$, or
$\mathfrak{S}$ is not $k$-synchronizable and
$\mathsf{sd}(\mathfrak{S})=\infty$.

###### Proof

Let $k\in\mathbb{N}\cup\\{\infty\\}$ be the supremum of the sizes of all prime
reachable exchanges.

Assume that there exists $K$ such that $\mathfrak{S}$ is $K$-synchronizable.
Let us show that $k\leq K$ and $\mathfrak{S}$ is $k$-synchronizable.

  * •

$k\leq K$. Assume by contradiction that $k\geq K+1$. Then there exists
exchanges $\mu_{1},\dots,\mu_{n},\mu$ such that
$\mu_{1}\cdots\mu_{n}\cdot\mu\in asTr(\mathfrak{S})$ and $\mu$ is prime of
size $K+1$. Since $\mu$ is prime, it corresponds to a strongly connected
component of size $K+1$ of the conflict graph of
$\mu_{1}\cdots\mu_{n}\cdot\mu$, so $\mu_{1}\cdots\mu_{n}\cdot\mu$ cannot be
$K$-synchronous: contradiction.

  * •

$\mathfrak{S}$ is $k$-synchronizable. Let $\mu\in asTr(\mathfrak{S})$ be fixed
an let us show that it can be chopped into a sequence of $k$ exchanges. Since
by hypothesis $\mathfrak{S}$ is $K$-synchronizable, there are $K$-exchanges
$\mu_{1},\dots,\mu_{n}$ such that $\mu=\mu_{1}\cdots\mu_{n}$. Up to
decomposing each $\mu_{i}$ as a product of prime exchanges, we can assume that
all $\mu_{i}$ are prime. Moreover, they are all reachable, so their size is
bounded by $k$. As a consequence, $\mu$ can be decomposed in a sequence of
$k$-exchanges.

∎

Since by Theorem 2.1 it is decidable whether $\mathfrak{S}$ is
$k$-synchronizable, it is enough to know $k$ in order to compute
$\mathsf{sd}(\mathfrak{S})$. In order to compute $k$, we have to address two
problems: the number of exchanges is possibly infinite, and one should examine
sequences of arbitrarily many exchanges. To solve these issues, we are going
to reduce to a problem on regular languages. Let
$\Sigma=\\{!?,!\\}\times\mathbb{V}\times\mathbb{P}^{2}$; for better
readability, we write $!?v^{p\to q}$ (resp. $!v^{p\to q}$) for a
$\Sigma$-symbol. To every $\Sigma$-word $w$ we associate an MSC $msc(w)$ as
follows. Consider the substitutions $\sigma_{1}:\Sigma\to S$ and
$\sigma_{2}:\Sigma\to R\cup\\{\epsilon\\}$ such that $\sigma_{1}(!?v^{p\to
q})=\sigma_{1}(!v^{p\to q})=send(p,q,v)$, $\sigma_{2}(!?v^{p\to q})=rec(q,v)$
and $\sigma_{2}(!v^{p\to q})=\epsilon$. Then $msc(w)$ is defined as
$msc(\sigma_{1}(w)\sigma_{2}(w))$. Clearly, it is an exchange (by
construction, it admits a linearization in $S^{*}R^{*}$), but more remarkably
any reachable exchange can be represented by such a word.

######  Lemma 2 ()

For all reachable exchanges $\mu$, there exists $w\in\Sigma^{*}$ s.t.
$\mu=msc(w)$.

###### Proof

Let $\mu$ be a reachable exchange, and let $\mu_{1},\dots\mu_{n}$ be such that
$\mu_{1}\cdot\mu_{2}\cdots\mu_{n}\cdot\mu\in asTr(\mathfrak{S})$. There is a
linearization of $\mu_{1}\cdots\mu_{n}\cdot\mu$ which follows the mailbox
semantics. This linearization induces a linearization $lin(\mu)$ of $\mu$ that
also follows the mailbox semantics. Then $lin(\mu)$ induces an enumeration
$send(p_{1},q_{1},v_{1}),\dots,send(p_{n},q_{n},v_{n})$ of the send events of
$\mu$. Let $w=a_{1}\dots a_{n}$ where $a_{i}$ is either
$!?v_{i}^{p_{i}\rightarrow q_{i}}$ if $send(p_{i},q_{i},v_{i})$ is matched in
$\mu$, or $!v_{i}^{p_{i}\rightarrow q_{i}}$ if it is unmatched. Then, the
claim is that $msc(w)=\mu$, or in other words, $\sigma_{1}(w)\sigma_{2}(w)$ is
a linearization of $\mu$. By contradiction, assume it is not. Then there are
two events $e,e^{\prime}$ such that $e<e^{\prime}$ in the enumeration
$\sigma_{1}(w)\sigma_{2}(w)$ but
$(e^{\prime},e)\in(\prec_{po}\cup\prec_{src})^{*}$.

  * •

if $e,e^{\prime}$ are two send events then $e$ occurs before $e^{\prime}$ in
$\sigma_{1}(w)$, i.e. $e$ occurs before $e^{\prime}$ in $lin(\mu)$, which is a
linearization of $\mu$, and the contradiction with
$(e^{\prime},e)\in(\prec_{po}\cup\prec_{src})^{*}$.

  * •

if $e$ is a send event and $e^{\prime}$ a receive event, then
$(e^{\prime},e)\in(\prec_{po}\cup\prec_{src})^{*}$ contradicts the fact that
$\mu$ is an exchange.

  * •

if $e$ is a receive event and $e^{\prime}$ is a send event, then
$e<e^{\prime}$ wrt $\sigma_{1}(w)\sigma_{2}(w)$ contradicts the definition of
$\sigma_{1},\sigma_{2}$.

  * •

assume finally that $e$ and $e^{\prime}$ are receive events. From
$(e^{\prime},e)\in(\prec_{po}\cup\prec_{src})^{*}$, we deduce that
$e^{\prime}\prec_{po}e$ , because $\mu$ is an exchange. Let $s,s^{\prime}$ be
the matching send events of $e,e^{\prime}$ respectively. Since $e<e^{\prime}$
wrt $\sigma_{1}(w)\sigma_{2}(w)$, $s<s^{\prime}$ wrt
$\sigma_{1}(w)\sigma_{2}(w)$, and therefore $s<s^{\prime}$ wrt $lin(\mu)$. But
$e^{\prime}<e$ wrt $lin(\mu)$ because $e^{\prime}\prec_{po}e$, which violates
the mailbox semantics: contradiction.

∎

The proof follows from the fact that it is always possible to receive messages
in the same global order as they have been sent. Such a property would not
hold for peer-to-peer communications, as we can see in the following counter-
example.

Consider MSC $\mu_{6}$ on the right. This MSC does not satisfy causal delivery
in a mailbox semantics, because the sending of $v_{1}$ happens before the
sending of $v_{4}$, and the reception of $v_{4}$ happens before the reception
of $v_{1}$. For this reason, there is no word $w$ such that $msc(w)$
corresponds to this MSC: such a word would give a linearization that would
correspond to a valid mailbox execution. On the other hand, this MSC satisfies
causal delivery in a peer-to-peer semantics. For instance, the following
linearization is a peer-to-peer execution:

$!v_{3}\cdot!v_{4}\cdot!v_{1}\cdot!v_{2}\cdot?v_{2}\cdot?v_{3}\cdot?v_{4}\cdot?v_{1}$

$p$$q$$r$$s$$v_{1}$$v_{2}$$v_{3}$$v_{4}$ Figure 3: MSC $\mu_{6}$

We can now define two languages over $\Sigma$:

$\mathcal{L}_{\mbox{r}}=\\{w\in\Sigma^{*}\mid msc(w)\mbox{ is
reachable}\\}\text{ and }\mathcal{L}_{\mbox{p}}=\\{w\in\Sigma^{*}\mid
msc(w)\mbox{ is prime}\\}$

Then the bound $k$ we are looking for is the length of the longest word in
$\mathcal{L}_{\mbox{r}}\cap\mathcal{L}_{\mbox{p}}$. It suffices to show that
both $\mathcal{L}_{\mbox{r}}$ and $\mathcal{L}_{\mbox{p}}$ are effective
regular languages to get an algorithm for computing $k$. This is the content
of Sections 4 and 5.

##  4 Regularity of reachable exchanges

In this section, we aim at defining a finite state automaton that accepts a
word $w\in\Sigma^{*}$ iff $msc(w)$ is reachable, that is, iff there exists
$\mu_{1},\mu_{2},\ldots,\mu_{n}$ such that
$\mu_{1}\cdot\mu_{2}\cdots\mu_{n}\cdot msc(w)\in asTr(\mathfrak{S}).$ Now,
observe that the prefix $\mu_{1}\cdot\mu_{2}\cdots\mu_{n}$ brings the system
in a certain global control state that conditions what can be done by
$msc(w)$. Moreover, the presence of unmatched messages in a buffer imposes
that none of the subsequent messages sent to the same buffer can be read.

The construction of the automaton accepting $\mathcal{L}_{\mbox{r}}$ proceeds
in three separate steps. First, we build an automaton that accepts the
language of all words that code an exchange, starting in a certain global
control state $\mathbf{in}$, and ending in another global control state
$\mathbf{fin}$, and possibly not satisfying causal delivery. Secondly, we
consider the set of MSCs that satisfy causal delivery. We define automata that
recognize the words coding MSCs starting from a certain “buffer state” and
ending in another “buffer state”, the “buffer state” characterizing whether or
not the MSC satisfies causal delivery. Finally, we show that
$\mathcal{L}_{\mbox{r}}$ is a boolean combination of the languages of some of
these automata.

###  4.1 Automata of the control states

We consider triples of global states
$(\mathbf{in},\mathbf{mid},\mathbf{fin})$, representing the exchanges such
that $\mathbf{mid}$ can be reached only with sends from $\mathbf{in}$ and
$\mathbf{fin}$ can be reached only with receptions from $\mathbf{mid}$. We
want to define an automaton
$\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})$ that recognizes the words
coding such exchanges. Intuitively,
$\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})$ is a product of on the
one hand the global automaton $\mathfrak{S}$ restricted to send transitions
and on the other hand $\mathfrak{S}$ restricted to receive transitions. For
each send action, either the reception is available and a matched message
possible, or there is no corresponding reception and so we obtain an unmatched
message.

######  Definition 6 (Automaton of control states)

Let $\mathfrak{S}$ be a system and $\mathbf{in},\mathbf{mid},$ $\mathbf{fin}$
global states.
$\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})=(L_{\mathtt{SR}},\delta_{\mathtt{SR}},\mathbf{l^{0}_{\mathtt{SR}}},F_{\mathtt{SR}})$
is the automaton where:

  * •

$L_{\mathtt{SR}}=\\{(\mathbf{l},\mathbf{l^{\prime}})\mid~{}\mathbf{l},\mathbf{l^{\prime}}\in
L_{\mathfrak{S}}\\}$;
$\mathbf{l^{0}_{\mathtt{SR}}}=(\mathbf{in},\mathbf{mid})$;
$F_{\mathtt{SR}}=\\{(\mathbf{mid},\mathbf{fin})\\}$;

  * •

for each
$(\mathbf{l_{s}},send(p,q,v),\mathbf{l^{\prime}_{s}})\in\delta_{\mathfrak{S}}$:

    * –

$((\mathbf{l_{s}},\mathbf{l}),!v^{p\rightarrow
q},(\mathbf{l^{\prime}_{s}},\mathbf{l}))\in\delta_{\mathtt{SR}}$ for
$\mathbf{l}\in L_{\mathfrak{S}}$;

    * –

if $(\mathbf{l_{r}},rec(q,v),\mathbf{l^{\prime}_{r}})\in\delta_{\mathfrak{S}}$
then $((\mathbf{l_{s}},\mathbf{l_{r}}),!?v^{p\rightarrow
q},(\mathbf{l^{\prime}_{s}},\mathbf{l^{\prime}_{r}}))\in\delta_{\mathtt{SR}}$

We denote $\mathcal{L}(\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin}))$
the language of a such automaton. This is an example of the construction.

###### Example 1

Let $\mathfrak{S}_{1}$ be the system whose process automata $p,q$ and $r$ are
depicted in Fig 4. For the triple $(\mathbf{in},\mathbf{mid},\mathbf{fin})$
where $\mathbf{in}=(0,0,0),\mathbf{mid}=(2,0,1)$ and $\mathbf{fin}=(2,1,2)$,
automaton $\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})$ is depicted
below the system and has for language:

$\displaystyle\mathcal{L}(\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin}))=~{}$
$\displaystyle!?a^{p\rightarrow r}(!c^{p\rightarrow q}!?b^{r\rightarrow
q}~{}+~{}!?b^{r\rightarrow q}!c^{p\rightarrow q})$
$\displaystyle+~{}!?b^{r\rightarrow q}!?a^{p\rightarrow r}!c^{p\rightarrow q}$

$0$$1$$2$$!a^{p\rightarrow r}$$!c^{p\rightarrow q}$$p$$0$$1$$?b^{r\rightarrow
q}$$q$$0$$1$$2$$!b^{r\rightarrow q}$$?a^{p\rightarrow r}$$r$

$\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})$ $((0,0,0),$ $(2,0,1))$
$((1,0,0),$ $(2,0,1))$ $((2,0,0),$ $(2,0,1))$ $((2,0,1),$ $(2,0,1))$
$((1,0,1),$ $(2,0,1))$ $((1,0,1),$ $(2,1,1))$ $((0,0,1),$ $(2,0,1))$
$((1,0,0),$ $(2,0,2))$ $((2,0,0),$ $(2,0,2))$ $((2,0,1),$ $(2,1,1))$
$((2,0,1),$ $(2,0,2))$ $((1,0,1),$ $(2,0,2))$ $((0,0,1),$ $(2,1,1))$
$((1,0,1),$ $(2,1,2))$ $((2,0,1),$ $(2,1,2))$ $!a^{p\rightarrow
r}$$!b^{r\rightarrow q}$$!?a^{p\rightarrow r}$$!?b^{r\rightarrow
q}$$!c^{p\rightarrow q}$$!?b^{r\rightarrow q}$$!b^{r\rightarrow
q}$$!c^{p\rightarrow q}$$!b^{r\rightarrow q}$$!?b^{r\rightarrow
q}$$!b^{r\rightarrow q}$$!b^{r\rightarrow q}$$!c^{p\rightarrow
q}$$!c^{p\rightarrow q}$$!c^{p\rightarrow q}$$!c^{p\rightarrow
q}$$!?a^{p\rightarrow r}$$!a^{p\rightarrow r}$$!a^{p\rightarrow
r}$$!?a^{p\rightarrow r}$$!?b^{r\rightarrow q}$$!?b^{r\rightarrow q}$

Figure 4: System $\mathfrak{S}_{1}$ and Automaton
$\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})$

######  Lemma 3 ()

$w\in\mathcal{L}(\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin}))$ for some
$\mathbf{mid}$ iff $\mathbf{in}\mathrel{\leavevmode\hbox to29.71pt{\vbox
to13.16pt{\pgfpicture\makeatletter\hbox{\hskip 14.85318pt\lower-7.50276pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55042pt}{-1.75pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle
msc(w)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}}{{}}} \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.15819pt}{-5.85277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mathbf{fin}$.

###### Proof

Observe that, by construction of
$\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin})$,
$\mathbf{l^{0}_{\mathtt{SR}}}\xRightarrow{w}(\mathbf{l},\mathbf{l^{\prime}})$
iff $\mathbf{in}\xRightarrow{\sigma_{1}(w)}\mathbf{l}$ and
$\mathbf{mid}\xRightarrow{\sigma_{2}(w)}\mathbf{l^{\prime}}$ (this can be
shown by an easy induction on the length of $w$). In particular, $w$ is
accepted iff $\mathbf{in}\xRightarrow{\sigma_{1}(w)}\mathbf{mid}$ and
$\mathbf{mid}\xRightarrow{\sigma_{2}(w)}\mathbf{fin}$, which is equivalent to
$\mathbf{in}\mathrel{\leavevmode\hbox to29.71pt{\vbox
to13.16pt{\pgfpicture\makeatletter\hbox{\hskip 14.85318pt\lower-7.50276pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55042pt}{-1.75pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle
msc(w)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}}{{}}} \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.15819pt}{-5.85277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
###  4.2 Automata of causal delivery exchanges

Let us now move to the trickier part, namely the recognition of words coding
MSCs that satisfy causal delivery. Let
$\mu=(Ev,\lambda,\prec_{po},\prec_{src})$ be an MSC, and $v\in\lambda^{-1}(S)$
a send event, we write $ev_{S}(v)$ for the event $v$ and, when it exists,
$ev_{R}(v)$ for the event $v^{\prime}\in\lambda^{-1}(R)$ such that
$v\prec_{src}v^{\prime}$. We say that $v$ is unmatched

if $ev_{R}(v)$ is undefined. We recall from [3] the notion of conflict graph.
Intuitively, it captures some (but not all) causal dependencies between
events. The figure on the right represents an MSC and its associated conflict
graph.

$p$$q$$r$$v_{1}$$v_{2}$$v_{3}$$v_{1}$$v_{2}$$v_{3}$RSSRSSSR Figure 5: MSC
$\mu_{3}$ and its conflict graph

######  Definition 7 (Conflict Graph)

The conflict graph $\mathsf{CG}(\mu)$ of an MSC
$\mu=(Ev,\lambda,\prec_{po},\prec_{src})$ is the labeled graph
$(V,\\{\stackrel{{\scriptstyle\footnotesize
XY}}{{\longrightarrow}}\\}_{X,Y\in\\{R,S\\}})$ where $V=\lambda^{-1}(S)$, and
for all $v,v^{\prime}\in V$, there is a $XY$ dependency edge
$v\stackrel{{\scriptstyle\footnotesize XY}}{{\longrightarrow}}v^{\prime}$
between $v$ and $v^{\prime}$ $(X,Y\in\\{S,R\\})$, if $ev_{X}(v)$ and
$ev_{Y}(v^{\prime})$ are defined and $ev_{X}(v)\prec_{po}ev_{Y}(v^{\prime})$.

The _extended conflict graph_ [7] $\mathsf{ECG}(\mu)$ is obtained by adding
all dashed edges $v\stackrel{{\scriptstyle\footnotesize
XY}}{{\dashrightarrow}}v^{\prime}$ satisfying the relation
$\stackrel{{\scriptstyle\footnotesize XY}}{{\dashrightarrow}}$ in Fig. 6.
Intuitively, $v\stackrel{{\scriptstyle\footnotesize
XY}}{{\dashrightarrow}}v^{\prime}$ expresses that the event $X$ of $v$ must
happen before the event $Y$ of $v^{\prime}$ due to: their order on the same
machine (Rule 1), or the fact that a send happens before its matching receive
(Rule 2), or to the mailbox semantics (Rules 3 and 4), or because of a chain
of such dependencies (Rule 5). This captures all constraints induced by the
mailbox communication, and it has been shown that an MSC satisfies causal
delivery if and only if its extended conflict graph is acyclic (Theorem 2 in
[7]).

$v_{1}\stackrel{{\scriptstyle\footnotesize XY}}{{\longrightarrow}}v_{2}$ (Rule
1) $v_{1}\stackrel{{\scriptstyle\footnotesize XY}}{{\dashrightarrow}}v_{2}$

$v$ is matched (Rule 2) $v\stackrel{{\scriptstyle\footnotesize
SR}}{{\dashrightarrow}}v$

$v_{1}\stackrel{{\scriptstyle\footnotesize RR}}{{\longrightarrow}}v_{2}$ (Rule
3) $v_{1}\stackrel{{\scriptstyle\footnotesize SS}}{{\dashrightarrow}}v_{2}$

$v_{1}$ is matched $v_{2}$ is unmatched
$\mathsf{proc}_{R}(v_{1})=\mathsf{proc}_{R}(v_{2})$ (Rule 4)
$v_{1}\stackrel{{\scriptstyle\footnotesize SS}}{{\dashrightarrow}}v_{2}$

$v_{1}\stackrel{{\scriptstyle\footnotesize
XY}}{{\dashrightarrow}}\stackrel{{\scriptstyle\footnotesize
YZ}}{{\dashrightarrow}}v_{2}$ (Rule 5)
$v_{1}\stackrel{{\scriptstyle\footnotesize XZ}}{{\dashrightarrow}}v_{2}$

Figure 6: Deduction rules for extended dependency edges of the conflict graph

We build an automaton that recognizes the words $w$ such that $msc(w)$
satisfies causal delivery. To this aim, we associate to each MSC a “buffer
state” that contains enough information to determine whether its extended
conflict graph is acyclic. We write $\mathbb{B}$ for the set
$(2^{\mathbb{P}}\times 2^{\mathbb{P}})^{\mathbb{P}}$. The _buffer state_
$\mathcal{B}(\mu)\in\mathbb{B}$ of the MSC $\mu$ is the tuple
$\mathcal{B}(\mu)=(\mathcal{C}^{\mu}_{S,p},\mathcal{C}^{\mu}_{R,p})_{p\in\mathbb{P}}$
such that for all $p\in\mathbb{P}$:

$\begin{array}[]{ll}\mathcal{C}^{\mu}_{{S},{p}}=&\\{\mathsf{proc}_{S}(v)\mid
v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v~{}\&~{}v^{\prime}\mbox{ is unmatched
}\&~{}\mathsf{proc}_{R}(v^{\prime})=p\\}~{}\cup\\\
&\\{\mathsf{proc}_{S}(v)\mid v\mbox{ is
unmatched}~{}\&~{}\mathsf{proc}_{R}(v)=p\\}\\\
\mathcal{C}^{\mu}_{{R},{p}}=&\\{\mathsf{proc}_{R}(v)\mid
v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v~{}\&~{}v^{\prime}\mbox{ is unmatched
}\&~{}\mathsf{proc}_{R}(v^{\prime})=p~{}\&~{}v\mbox{ is
matched}\\}\end{array}$

We can show that the $\mathsf{ECG}(\mu)$ is acyclic if for all
$p\in\mathbb{P}$, $p\not\in\mathcal{C}^{\mu}_{{R},{p}}$ (immediate consequence
of Theorem 2 in [7]). Moreover, we write $\mathbb{B}_{good}$ for the subset of
$\mathbb{B}$ formed by the tuples $(C_{S,p},C_{R,p})_{p\in\mathbb{P}}$ such
that $p\not\in C_{R,p}$ for all $p$.

######  Proposition 1 ([7])

For $w\in\Sigma^{*}$, $msc(w)$ satisfies causal delivery if and only if
$\mathcal{B}(\mu(w))\in\mathbb{B}_{good}$.

Noticing that $\mathbb{B}$ is finite, we build an automaton
$\mathcal{A}(B_{0},B_{1})$ with $B_{0},B_{1}\in\mathbb{B}$. The intuition
behind these two buffer states is that $B_{0}$ summarises the conflict graph
derived from previous exchanges and $B_{1}$ summarises the conflict graph
obtained when a new exchange is added.

######  Definition 8 (Automaton of causal exchanges)

The automaton $\mathcal{A}(B_{0},B_{1})$ is defined as follows:

  * •

$\mathbb{B}$ is the set of states,

  * •

$B_{0}$ is the initial state (hereafter, we assume that
$B_{0}=(C^{(0)}_{S,p},C^{(0)}_{R,p})_{p\in\mathbb{P}}$).

  * •

$\\{B_{1}$} is the set of final states

  * •

the transition relation $(\xrightarrow{a})_{a\in\Sigma}$ is defined as
follows:

    * –

$(C_{S,p},C_{R,p})_{p\in\mathbb{P}}\xrightarrow{!?v^{p\to
q}}(C^{\prime}_{S,p},C^{\prime}_{R,p})_{p\in\mathbb{P}}$ holds if for all
$r\in\mathbb{P}$: let the intermediate set $C_{S,r}^{\prime\prime}$ be defined
by

$C_{S,r}^{\prime\prime}=\left\\{\begin{array}[]{l}C_{S,r}\cup\\{p\\}\mbox{ if
}p\in C_{R,r}^{(0)}\mbox{ or }q\in C_{R,r}\\\ C_{S,r}\mbox{
otherwise}\end{array}\right.$

Then

$C_{S,r}^{\prime}=\left\\{\begin{array}[]{l}C_{S,r}^{\prime\prime}\cup
C_{S,q}\mbox{ if }p\in C_{S,r}^{\prime\prime}\\\ C_{S,r}\mbox{
otherwise}\end{array}\right.\quad\mbox{and}\quad
C_{R,r}^{\prime}=\left\\{\begin{array}[]{l}C_{R,r}\cup\\{q\\}\cup
C_{R,q}\mbox{ if }p\in C_{S,r}^{\prime\prime}\\\ C_{R,r}\mbox{
otherwise}\end{array}\right.$

    * –

$(C_{S,p},C_{R,p})_{p\in\mathbb{P}}\xrightarrow{!v^{p\to
q}}(C^{\prime}_{S,p},C^{\prime}_{R,p})_{p\in\mathbb{P}}$ holds if for all
$r\in\mathbb{P}$,

$C_{S,r}^{\prime}=\left\\{\begin{array}[]{l}C_{S,r}\cup\\{p\\}\mbox{ if
}q=r\mbox{ or }q\in C_{R,r}\\\ C_{S,r}\mbox{
otherwise}\end{array}\right.\quad\mbox{and}\quad C_{R,r}^{\prime}=C_{R,r}$

Let $\mathcal{L}(B_{0},B_{1})$ denote the language recognized by
$\mathcal{A}(B_{0},B_{1})$.

###### Example 2

Consider $\mu_{4}=msc(w)$ with $w=!v_{3}^{p_{1}\to p_{2}}!?v_{4}^{p_{3}\to
p_{2}}!?v_{5}^{p_{4}\to p_{6}}!?v_{6}^{p_{6}\to p_{7}}$
and assume we start with $B_{0}$ such that $C_{S,p_{5}}=\\{p_{4}\\}$ and
$C_{R,p_{5}}=\\{p_{3}\\}$. Then the update of $B$ (or, more precisely, of
$C_{S,p_{5}}$, $C_{R,p_{5}}$, and $C_{S,p_{2}}$) after reading each message is
shown below. Note how $v_{6}$ has no effect, despite the fact that $p_{6}\in
C_{R,p_{5}}$ at the time the message is read.
$p_{1}$$p_{2}$$p_{3}$$p_{4}$$p_{5}$$p_{6}$$p_{7}$$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{5}$$v_{6}$
Figure 7: MSC $\mu_{4}$

$C_{S,p_{5}}$ | $\\{p_{4}\\}$ |  | $\\{p_{4}\\}$ |  | $\\{p_{1},p_{3},p_{4}\\}$ |  | $\\{p_{1},p_{3},p_{4}\\}$ |  | $\\{p_{1},p_{3},p_{4}\\}$
---|---|---|---|---|---|---|---|---|---
$C_{R,p_{5}}$ | $\\{p_{3}\\}$ | $\xrightarrow{!v_{3}}$ | $\\{p_{3}\\}$ | $\xrightarrow{!?v_{4}}$ | $\\{p_{2},p_{3}\\}$ | $\xrightarrow{!?v_{5}}$ | $\\{p_{2},p_{3},p_{6}\\}$ | $\xrightarrow{!?v_{6}}$ | $\\{p_{2},p_{3},p_{6}\\}$
$C_{S,p_{2}}$ | $\emptyset$ |  | $\\{p_{1}\\}$ |  | $\\{p_{1}\\}$ |  | $\\{p_{1}\\}$ |  | $\\{p_{1}\\}$

Next lemma states that $\mathcal{A}(B,B^{\prime})$ recognizes the words $w$
such that $msc(w)$, starting with an initial buffer state $B$, ends in final
buffer state $B^{\prime}$.

######  Lemma 4 ()

Let $B,B^{\prime}\in\mathbb{B}$ and $w\in\Sigma^{*}$. Then
$w\in\mathcal{L}(B,B^{\prime})$ if and only if for all MSC $\mu$ such that
$B=\mathcal{B}(\mu)$, $B^{\prime}=\mathcal{B}(\mu\cdot msc(w))$.

###### Proof

Take $w=a_{0}\dots a_{n}\in\Sigma^{*}$. To prove the lemma it is sufficient to
show that if $B=\mathcal{B}(\mu)$ and :

$B=(C^{(0)}_{S,p},C^{(0)}_{R,p})_{p\in\mathbb{P}}\xrightarrow{a_{0}}(C^{(1)}_{S,p},C^{(1)}_{R,p})_{p\in\mathbb{P}}\xrightarrow{a_{1}}\cdots\xrightarrow{a_{n}}(C^{(n+1)}_{S,p},C^{(n+1)}_{R,p})_{p\in\mathbb{P}}=B^{\prime},$

then $B^{\prime}=\mathcal{B}(\mu\cdot msc(w))$.

The proof proceeds by induction on the length of $w$ where the inductive
hypothesis is that
$(C^{(n)}_{S,p},C^{(n)}_{R,p})_{p\in\mathbb{P}}=\mathcal{B}(\mu\cdot
msc(a_{0}\dots a_{n-1}))$.

We start by showing that $\forall r\in\mathbb{P}$,
$C^{(n+1)}_{S,r}=\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$. Suppose that $p\in
C^{(n+1)}_{S,r}$. If $p\in C^{(0)}_{S,r}$ then we can immediately conclude
that $p\in\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$ since
$C^{(0)}_{S,r}=\mathcal{C}^{\mu}_{{S},{r}}\subseteq C^{(n+1)}_{S,r}$ and
function $\mathcal{B}(\cdot)$ is increasing monotone. Instead if $p\notin
C^{(0)}_{S,r}$ then the following can happen (without loss of generality
suppose that $p$ has been added while reading the last symbol of $w$):

  * •

$a_{n}=!?v^{p\to q}$ and $p\in C^{(0)}_{R,r}=\mathcal{C}^{\mu}_{{R},{r}}$

Then there exists a message in $\mu$, $v^{\prime\prime}$ such that
$\mathsf{proc}_{R}(v^{\prime\prime})=p$ and
$v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime}$ with $v^{\prime}$ unmatched. Then it
is easy to see that $v^{\prime\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v$ and therefore $p\in\mathcal{C}^{\mu\cdot
msc(w)}_{{S},{r}}$;

  * •

$a_{n}=!?v^{p\to q}$ and $q\in C^{(n)}_{R,r}=\mathcal{C}^{\mu\cdot
msc(a_{0}\dots a_{n-1})}_{{R},{r}}$

Then there exists a message $v^{\prime\prime}$ in $\mu\cdot msc(a_{0}\dots
a_{n-1})$, such that $\mathsf{proc}_{R}(v^{\prime\prime})=q$ and
$v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime}$ with $v^{\prime}$ unmatched. Then it
is easy to see that $v^{\prime\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v$ and therefore $p\in\mathcal{C}^{\mu\cdot
msc(w)}_{{S},{r}}$;

  * •

$a_{n}=!?v^{p^{\prime}\to q}$ and $p^{\prime}\in C^{\prime\prime(n)}_{S,r}$
and $p\in C^{(n)}_{S,q}=\mathcal{C}^{\mu\cdot msc(a_{0}\dots
a_{n-1})}_{{S},{q}}$

Then there exists a message $v^{\prime\prime}$ in $\mu\cdot msc(a_{0}\dots
a_{n-1})$, such that $\mathsf{proc}_{S}(v^{\prime\prime})=p$ and
$v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime}$ with $v^{\prime}$ unmatched and
$\mathsf{proc}_{R}(v^{\prime})=q$. Then it is easy to see that
$v\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime}$ and since $p^{\prime}\in
C^{\prime\prime(n)}_{S,r}$ and with an analysis similar to the one above we
have $v^{\prime\prime\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v$ with $v^{\prime\prime\prime}$ unmatched and we can
conclude $p\in\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$.

  * •

$a_{n}=!v^{p\to q}$ and $p\in C_{R,r}$

Analogous to case 2 above.

  * •

$a_{n}=!v^{p\to r}$

We can immediately conclude $p\in\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$ as
$v$ is unmatched and $\mathsf{proc}_{R}(v)=r$.

Now suppose that $p\in\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$ (without loss
of generality we can assume $p\notin\mathcal{C}^{\mu\cdot msc(a_{0}\dots
a_{n-1})}_{{S},{r}}$). Then either $a_{n}=!v^{p\to r}$ then it is immediate to
see that $p\in C^{(n+1)}_{S,r}$ or $a_{n}=!?v^{p\to q}$ and
$v^{\prime}\stackrel{{\scriptstyle\footnotesize SS}}{{\dashrightarrow}}v$ for
some $v^{\prime}$ unmatched and $\mathsf{proc}_{R}(v^{\prime})=r$.
$p\notin\mathcal{C}^{\mu\cdot msc(a_{0}\dots a_{n-1})}_{{S},{r}}$ entails that
either $q\in\mathcal{C}^{\mu\cdot msc(a_{0}\dots a_{n-1})}_{{R},{r}}$ or
$p\in\mathcal{C}^{\mu}_{{R},{r}}$ (notice that since $w$ is an exchange,
$p\notin\mathcal{C}^{\mu\cdot msc(a_{0}\dots
a_{n-1})}_{{R},{r}}\setminus\mathcal{C}^{\mu}_{{R},{r}}$ ). In both cases we
can conclude $p\in C^{(n+1)}_{S,r}$.

Next we show that $\forall r\in\mathbb{P}$,
$C^{\prime}_{R,r}=\mathcal{C}^{\mu\cdot msc(w)}_{{R},{r}}$. Suppose that $p\in
C^{(n+1)}_{R,r}$ (without loss of generality we can assume $p\notin
C{(n+1)}_{R,r}$). This entails that:

  * •

either $a_{n}=!?v^{q\to p}$ with $q\in
C^{\prime\prime(n+1)}_{S,r}=\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$:

Then there exists a message $v^{\prime\prime}$ in $\mu\cdot msc(w)$, such that
$\mathsf{proc}_{S}(v^{\prime\prime})=q$ and
$v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime}$ with $v^{\prime}$ unmatched and
$\mathsf{proc}_{R}(v^{\prime})=r$. Then it is easy to see that
$v^{\prime\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v$ and we can conclude $p\in\mathcal{C}^{\mu\cdot
msc(w)}_{{R},{r}}$;

  * •

or $a_{n}=!?v^{q\to p^{\prime}}$ with $q\in
C^{\prime\prime(n+1)}_{S,r}=\mathcal{C}^{\mu\cdot msc(w)}_{{S},{r}}$ and $p\in
C^{(n)}_{R,p^{\prime}}=\mathcal{C}^{\mu\cdot msc(a_{0}\dots
a_{n-1})}_{{R},{p^{\prime}}}$:

Then there exists a message $v^{\prime\prime}$ in $\mu\cdot msc(w)$, such that
$\mathsf{proc}_{S}(v^{\prime\prime})=q$ and
$v^{\prime}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime}$ with $v^{\prime}$ unmatched and
$\mathsf{proc}_{R}(v^{\prime})=r$. Similarly there is $v^{\prime\prime\prime}$
in $\mu\cdot msc(a_{0}\dots a_{n-1})$ such that
$\mathsf{proc}_{R}(v^{\prime\prime\prime})=p$ and
$v^{iv}\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{\prime\prime\prime}$ with $v^{iv}$ unmatched and
$\mathsf{proc}_{R}(v^{iv})=p^{\prime}$. Now when adding $v$ to the conflict
graph we have $v\stackrel{{\scriptstyle\footnotesize
SS}}{{\dashrightarrow}}v^{iv}$. Hence we can conclude
$p\in\mathcal{C}^{\mu\cdot msc(w)}_{{R},{r}}$.

Now suppose that $p\in\mathcal{C}^{\mu\cdot msc(w)}_{{R},{r}}$ (without loss
of generality we can assume $p\notin\mathcal{C}^{\mu\cdot msc(a_{0}\dots
a_{n-1})}_{{R},{r}}$). We know $\mathcal{C}^{\mu\cdot msc(a_{0}\dots
a_{n-1})}_{{R},{r}}=C^{(n)}_{R,r}$ and let $a_{n}=!?v^{q\to p}$. The following
can happen: $q\in\mathcal{C}^{\mu\cdot msc(a_{0}\dots a_{n-1})}_{{S},{r}},$ or
$q\in\mathcal{C}^{\mu\cdot msc(a_{0}\dots a_{n-1})}_{{R},{r}}$, or
$p\in\mathcal{C}^{\mu\cdot msc(a_{0}\dots a_{n-1})}_{{S},{r}}$. The last case
is when $a_{n}=!?v^{q^{\prime}\to p^{\prime}}$ and $p\in\mathcal{C}^{\mu\cdot
msc(a_{0}\dots a_{n-1})}_{{R},{p^{\prime}}}$ and
$q^{\prime}\in\mathcal{C}^{\mu\cdot msc(a_{0}\dots a_{n-1})}_{{S},{r}}$. For
all this cases, by inductive hypothesis and by Definition 8 we can conclude
$p\in C^{n+1}_{R,r}$.∎

###  4.3 Language of reachable exchanges

The only thing that remains to do is to combine the previous automata to
define one that recognizes the (codings of) reachable exchanges. The language
$\mathcal{L}(\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin}))$ contains
arbitrary exchanges which do not necessarily satisfy causal delivery. Here
comes into play the $\mathcal{A}(B,B^{\prime})$ automata, where we take $B$
and $B^{\prime}\in\mathbb{B}_{good}$ in order to ensure causal delivery.

Let

$\mathcal{L}_{\mbox{c}}(\mathbf{in},\mathbf{fin},B,B^{\prime})\stackrel{{\scriptstyle\tiny{\mathsf{def}}}}{{=}}\bigcup_{\mathbf{mid}\in
L_{\mathfrak{S}}}\mathcal{L}(\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin}))\cap\mathcal{L}(B,B^{\prime}).$

Intuitively, $\mathcal{L}_{\mbox{c}}(\mathbf{in},\mathbf{fin},B,B^{\prime})$
is the language of (codings of) exchanges between global states $\mathbf{in}$
and $\mathbf{fin}$ starting with an initial buffer state $B$ and ending in
final buffer state $B^{\prime}$; when moreover
$B,B^{\prime}\in\mathbb{B}_{good}$, these exchanges satisfy causal delivery.

The last step is to combine causal delivery exchanges so that they can be
performed by the system one after the other from the initial state
$\mathbf{l_{0}}$. This motivates the definition of the following set
$\mathcal{R}$ of _reachable languages_. Let
$B_{\emptyset}=(\emptyset,\emptyset)_{p\in\mathbb{P}}$.

######  Definition 9 (Reachable languages)

Given a system
$\mathfrak{S}=(L_{\mathfrak{S}},\delta_{\mathfrak{S}},\mathbf{l_{0}})$, the
set $\mathcal{R}$ of reachable languages is the least set of languages of the
form
$\mathcal{L}_{\mbox{c}}(\mathbf{in},\mathbf{fin},B_{i},B_{f})$ defined as
follows.

  1. 1.

for any $\mathbf{l}\in L_{\mathfrak{S}}$ and $B\in\mathbb{B}_{good}$,
$\mathcal{L}_{\mbox{c}}(\mathbf{l_{0}},\mathbf{l},B_{\emptyset},B)$ is in
$\mathcal{R}$

  2. 2.

for any $\mathbf{l_{1}},\mathbf{l_{2}},\mathbf{l_{3}}\in L_{\mathfrak{S}}$ and
any $B_{1},B_{2},B_{3}\in\mathbb{B}_{good}$, if
$\mathcal{L}_{\mbox{c}}(\mathbf{l_{1}},\mathbf{l_{2}},B_{1},B_{2})\in\mathcal{R}$
and
$\mathcal{L}_{\mbox{c}}(\mathbf{l_{1}},\mathbf{l_{2}},B_{1},B_{2})\neq\emptyset$
then
$\mathcal{L}_{\mbox{c}}(\mathbf{l_{2}},\mathbf{l_{3}},B_{2},B_{3})\in\mathcal{R}$.

Then the union $\bigcup\mathcal{R}$ of all reachable languages is equal to the
language $\mathcal{L}_{\mbox{r}}=\\{w\in\Sigma^{*}\mid msc(w)\mbox{ is
reachable}\\}$. As a consequence, we get the following result.

######  Theorem 4.1 ()

$\mathcal{L}_{\mbox{r}}$ is a regular language and is accepted by an effective
finite state automaton.

###### Proof

$\Rightarrow$ $w\in\bigcup\mathcal{R}$ so there is a sequence of words
$w_{1},\cdots,w_{n}\in\Sigma^{*}$ such that $\forall 1\leq j\leq
n,w_{j}\in\mathcal{L}_{\mbox{c}}(\mathbf{l_{j-1}},\mathbf{l_{j}},B_{j-1},B_{j})\neq\emptyset$
with $B_{j}\in\mathbb{B}_{good}$, and there is also $\mathbf{fin}\in
L_{\mathfrak{S}},B_{f}\in\mathbb{B}_{good}$ such that
$w\in\mathcal{L}_{\mbox{c}}(\mathbf{l_{n}},\mathbf{fin},B_{n},B_{f})$.

So,
$w_{j}\in\mathcal{L}(\mathtt{SR}(\mathbf{l_{j-1}},\mathbf{l^{\prime}_{j}},\mathbf{l_{j}}))$
for $\mathbf{l^{\prime}_{j}}\in L_{\mathfrak{S}}$, and, by Lemma 3,
$\mathbf{l_{j-1}}\mathrel{\leavevmode\hbox to31.58pt{\vbox
to13.5pt{\pgfpicture\makeatletter\hbox{\hskip 15.79128pt\lower-7.67616pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.48851pt}{-1.5766pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle
msc(w_{j})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{13.09628pt}{-6.02617pt}\pgfsys@lineto{10.84128pt}{-6.02617pt}\pgfsys@lineto{9.9877pt}{-6.72617pt}\pgfsys@lineto{8.28053pt}{-5.32617pt}\pgfsys@lineto{6.57336pt}{-6.72617pt}\pgfsys@lineto{4.8662pt}{-5.32617pt}\pgfsys@lineto{3.15903pt}{-6.72617pt}\pgfsys@lineto{1.45186pt}{-5.32617pt}\pgfsys@lineto{-0.25531pt}{-6.72617pt}\pgfsys@lineto{-1.96248pt}{-5.32617pt}\pgfsys@lineto{-3.66965pt}{-6.72617pt}\pgfsys@lineto{-5.37682pt}{-5.32617pt}\pgfsys@lineto{-7.08398pt}{-6.72617pt}\pgfsys@lineto{-8.79115pt}{-5.32617pt}\pgfsys@lineto{-10.49832pt}{-6.72617pt}\pgfsys@lineto{-12.20549pt}{-5.32617pt}\pgfsys@lineto{-13.91266pt}{-6.72617pt}\pgfsys@lineto{-14.84128pt}{-6.02617pt}\pgfsys@lineto{-14.84128pt}{-6.02617pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{13.09628pt}{-6.02617pt}\pgfsys@lineto{10.84128pt}{-6.02617pt}\pgfsys@lineto{9.9877pt}{-6.72617pt}\pgfsys@lineto{8.28053pt}{-5.32617pt}\pgfsys@lineto{6.57336pt}{-6.72617pt}\pgfsys@lineto{4.8662pt}{-5.32617pt}\pgfsys@lineto{3.15903pt}{-6.72617pt}\pgfsys@lineto{1.45186pt}{-5.32617pt}\pgfsys@lineto{-0.25531pt}{-6.72617pt}\pgfsys@lineto{-1.96248pt}{-5.32617pt}\pgfsys@lineto{-3.66965pt}{-6.72617pt}\pgfsys@lineto{-5.37682pt}{-5.32617pt}\pgfsys@lineto{-7.08398pt}{-6.72617pt}\pgfsys@lineto{-8.79115pt}{-5.32617pt}\pgfsys@lineto{-10.49832pt}{-6.72617pt}\pgfsys@lineto{-12.20549pt}{-5.32617pt}\pgfsys@lineto{-13.91266pt}{-6.72617pt}\pgfsys@lineto{-14.84128pt}{-6.02617pt}\pgfsys@lineto{-14.84128pt}{-6.02617pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.09628pt}{-6.02617pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mathbf{l_{j}}$, and
$\mathbf{l_{n}}\mathrel{\leavevmode\hbox to29.71pt{\vbox
to13.16pt{\pgfpicture\makeatletter\hbox{\hskip 14.85318pt\lower-7.50276pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55042pt}{-1.75pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle
msc(w)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}}{{}}} \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.15819pt}{-5.85277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mathbf{fin}$.

Moreover, for all $1\leq j\leq n$, $w_{j}\in\mathcal{L}(B_{j-1},B_{j})$ and
$B_{j}\in\mathbb{B}_{good}$. So, each $msc(w_{j})$ verifies causal delivery,
and, we can easily show by induction that $msc(w_{1})\cdots msc(w_{n})\cdot
msc(w)$ verifies causal delivery too. Finally, by Proposition
LABEL:proposition:msc_trace_state, $msc(w_{1})\cdots msc(w_{n})\cdot msc(w)\in
asTr(\mathfrak{S})$ and so, $msc(w)$ is reachable.

$\Leftarrow$ $msc(w)$ is reachable so there is $\mu_{1}\cdots\mu_{n}$ a
sequence of MSCs such that $\mu_{1}\cdots\mu_{n}\cdot msc(w)\in
asTr(\mathfrak{S})$. Suppose that $\mu_{1}\cdots\mu_{n}=\varepsilon$, then,
$\mathbf{l_{0}}\mathrel{\leavevmode\hbox to29.71pt{\vbox
to13.16pt{\pgfpicture\makeatletter\hbox{\hskip 14.85318pt\lower-7.50276pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55042pt}{-1.75pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle
msc(w)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}}{{}}} \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.15819pt}{-5.85277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mathbf{fin}$ for
some $\mathbf{fin}$. Therefore,
$w\in\mathcal{L}(\mathtt{SR}(\mathbf{l_{0}},\mathbf{l},\mathbf{fin}))$ for
some $\mathbf{l}\in L_{\mathfrak{S}}$. As $msc(w)\in asTr(\mathfrak{S})$,
$msc(w)$ verifies causal delivery and so there is $B$ such that
$w\in\mathcal{L}(B_{0},B^{\prime})$ with $B^{\prime}\in\mathbb{B}_{good}$.
Finally, we have that
$w\in\mathcal{L}_{\mbox{c}}(\mathbf{l_{0}},\mathbf{fin},B_{0},B)$ and so
$w\in\bigcup\mathcal{R}$.

Now, suppose that $\mu_{1}\cdots\mu_{n}\neq\varepsilon$. Then, there is a
sequence $w_{1},\cdots,w_{n}\in\Sigma^{*}$ such that $msc(w_{i})=\mu_{i}$,
$1\leq i\leq n$, and we can suppose that
$w_{1},\cdots,w_{n}\in\mathcal{L}_{\mbox{r}}$. By Lemma 4, there is
$B=\mathcal{B}(\mu_{1}\cdots\mu_{n}),B^{\prime}=\mathcal{B}(\mu_{1}\cdots\mu_{n}\cdot
msc(w))\in\mathbb{B}_{good}$ such that $w\in\mathcal{L}(B,B^{\prime})$.
Moreover, there is $\mathbf{in},\mathbf{fin}$ such that
$\mathbf{in}\mathrel{\leavevmode\hbox to29.71pt{\vbox
to13.16pt{\pgfpicture\makeatletter\hbox{\hskip 14.85318pt\lower-7.50276pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55042pt}{-1.75pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\scriptstyle
msc(w)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
{{{{}{}{{}} }}{{}}{{}}} \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.9pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{1.1pt}\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@moveto{12.15819pt}{-5.85277pt}\pgfsys@lineto{9.90318pt}{-5.85277pt}\pgfsys@lineto{9.0496pt}{-6.55276pt}\pgfsys@lineto{7.34244pt}{-5.15277pt}\pgfsys@lineto{5.63527pt}{-6.55276pt}\pgfsys@lineto{3.9281pt}{-5.15277pt}\pgfsys@lineto{2.22093pt}{-6.55276pt}\pgfsys@lineto{0.51376pt}{-5.15277pt}\pgfsys@lineto{-1.1934pt}{-6.55276pt}\pgfsys@lineto{-2.90057pt}{-5.15277pt}\pgfsys@lineto{-4.60774pt}{-6.55276pt}\pgfsys@lineto{-6.31491pt}{-5.15277pt}\pgfsys@lineto{-8.02208pt}{-6.55276pt}\pgfsys@lineto{-9.72925pt}{-5.15277pt}\pgfsys@lineto{-11.43642pt}{-6.55276pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@lineto{-13.90318pt}{-5.85277pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.15819pt}{-5.85277pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mathbf{fin}$, so
$w\in\mathcal{L}(\mathtt{SR}(\mathbf{in},\mathbf{mid},\mathbf{fin}))$ for some
$\mathbf{mid}$. Finally, we have
$w\in\mathcal{L}_{\mbox{c}}(\mathbf{in},\mathbf{fin},B,B^{\prime})$ and then
$w\in\mathcal{L}_{\mbox{r}}$.∎

##  5 Prime exchanges

We reformulate the primality of an exchange in terms of its conflict graph. We
say that the conflict graph $\mathsf{CG}(\mu)$ associated with the MSC $\mu$
is strongly connected if for all $v,v^{\prime}\in V$ it holds that
$v\to^{*}v^{\prime}$, where $\to^{*}$ is the reflexive transitive closure of
$\to=\bigcup_{X,Y\in\\{S,R\\}}\stackrel{{\scriptstyle\footnotesize
XY}}{{\longrightarrow}}$.

######  Lemma 5 ()

An exchange $\mu$ is prime iff $\mathsf{CG}(\mu)$ is strongly connected.

###### Proof

Let $\mu=\mu_{1}\cdots\mu_{n}$ be an MSC formed with a sequence of exchanges.
Let $e,e^{\prime}$ be two events of $\mu$, and let
$i,i^{\prime}\in\\{1,\ldots,n\\}$ be such that $e$ appears in $\mu_{i}$ and
$e^{\prime}$ appears in $\mu_{i^{\prime}}$. If there is an edge
$e\xrightarrow{XY}e^{\prime}$ in the conflict graph of $\mu$, then $i\leq
i^{\prime}$. As a consequence, if $e$ and $e^{\prime}$ are on a same strongly
connected component, then $i=i^{\prime}$, and if the conflict graph of $\mu$
is strongly connected, then $n=1$ and $\mu$ is a prime exchange. ∎

Next we discuss the construction of the automaton that recognizes
$\\{w\in\Sigma^{*}\mid msc(w)\mbox{ is prime}\\}$. Since there are infinitely
many $\mathsf{CG}(msc(w))$, in order to have a finite state automaton, we
compute a finite abstractions of $\mathsf{CG}(msc(w))$ that is sound in the
sense that $\mathsf{CG}(msc(w))$ is strongly connected if and only if its
abstraction is of a certain shape. Let us now define this abstraction.

We need to define some graph transformations. The graphs we are going to
manipulate are oriented graphs labeled with a pair of set of processes on each
vertex. We call such objects P-graphs. Formally, a P-graph is a tuple
$(V,E,\lambda_{S},\lambda_{R})$ with $E\subseteq V\times V$ and
$\lambda_{X}:V\to 2^{\mathbb{P}}$ for $X\in\\{S,R\\}$. The P-graph
$\mathsf{pgr}(\mu)$ associated with the conflict graph
$\mathsf{CG}(\mu)=(V,\\{\stackrel{{\scriptstyle\footnotesize
XY}}{{\longrightarrow}}\\}_{X,Y\in\\{S,R\\}})$ is
$(V,E,\lambda_{S},\lambda_{R})$ where (1) $(v,v^{\prime})\in E$ if
$v\stackrel{{\scriptstyle\footnotesize XY}}{{\longrightarrow}}v^{\prime}$ for
some $X,Y$, (2) $\lambda_{S}(v)=\\{\mathsf{proc}_{S}(v)\\}$, and (3) if $v$ is
matched, then $\lambda_{R}(v)=\\{\mathsf{proc}_{R}(v)\\}$, and if $v$ is
unmatched $\lambda_{R}(v)=\emptyset$.

The first graph transformation we consider consists in merging the vertices
that belong to a same strongly connected component (SCC). Formally, let
$G=(V,E,\lambda_{S},\lambda_{R})$ be a P-graph, and let
$\mathsf{merge}(G)=(V^{\prime},E^{\prime},\lambda_{S},\lambda_{R})$ be defined
by (1) $V^{\prime}$ is the set of maximal SCCs of $G$, (2) for two distinct
maximal SCCs $U,U^{\prime}$, $(U,U^{\prime})\in E^{\prime}$ if there are $v\in
U$ and $v^{\prime}\in U^{\prime}$ such that $(v,v^{\prime})\in E^{+}$ (the
transitive closure of $E$), (3) for $X=S,R$, $\lambda_{X}(U)=\bigcup_{v\in
U}\lambda_{X}(v)$.

The second graph transformation we consider consists in erasing some of the
processes that appear in the labels. Let $G=(V,E,\lambda_{S},\lambda_{R})$ be
a fixed P-graph, and let $v\in V$, $X\in\\{S,R\\}$, and $p\in\lambda_{X}(v)$
be fixed. We say that $p$ is X-redundant in $v$ if there are $v_{1},v_{2}$
such that (1) $(v_{1},v)\in E^{+}$ and $(v,v_{2})\in E^{+}$, and (2)
$p\in\lambda_{X}(v_{1})\cap\lambda_{X}(v_{2})$. Intuitively, $p$ is redundant
in $v$ if it also appears in the label of an ancestor and a descendant of $v$.
We define the P-graph $\mathsf{erase}(G)$ as
$(V,E,\lambda_{S}^{\prime},\lambda_{R}^{\prime})$ where for all
$X\in\\{S,R\\}$, for all $v\in V$, $\lambda_{X}^{\prime}(v)$ is the set of
processes $p\in\lambda_{X}(v)$ such that $p$ is not X-redundant at $v$.

The last graph transformation we consider consists in sweeping out the
vertices labeled with empty sets of processes. Formally, for
$G=(V,E,\lambda_{S},\lambda_{R})$, the P-graph $\mathsf{sweep}(G)$ is
$(V^{\prime},E^{\prime},\lambda_{S},\lambda_{R})$ where $V^{\prime}=\\{v\in
V\mid\lambda_{S}(v)\cup\lambda_{R}(v)\neq\emptyset\\}$ and $E^{\prime}=E\cap
V^{\prime}\times V^{\prime}$. The abstraction $\alpha(G)$ of a P-graph $G$ is
defined as $\mathsf{sweep}(\mathsf{erase}(\mathsf{merge}(G)))$. An example of
the construction is in Fig 8.

$p$$q$$r$$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{5}$$v_{6}$$\lambda_{S}$$\lambda_{R}$
$v_{1}$ $\\{q\\}$$\\{r\\}$ $v_{2}$ $\\{q\\}$$\\{r\\}$ $v_{3}$
$\\{q\\}$$\\{r\\}$ $v_{4}$ $\\{q\\}$$\\{p\\}$ $v_{5}$
$\\{p\\}$$\\{q\\}$$\lambda_{S}$$\lambda_{R}$ $\hskip 1.9919pt\\{v_{1}\\}$
$\\{q\\}$$\\{r\\}$ $\hskip 1.9919pt\\{v_{3}\\}$ $\emptyset$$\\{r\\}$
$\\{v_{4},v_{5}\\}$ $\\{p,q\\}$$\\{p,q\\}$ Figure 8: MSC $\mu_{5}$, its
associated P-graph $\mathsf{pgr}(\mu_{5})$, and the abstraction
$\alpha(\mathsf{pgr}(\mu_{5}))$.

######  Lemma 6 ()

$\mathsf{CG}(\mu)$ is strongly connected iff $\alpha(\mathsf{pgr}(\mu))$ is a
single vertex graph.

###### Proof

By definition of $\alpha$, and in particular of function $\mathsf{merge}(.)$,
a vertex of $\alpha(\mathsf{pgr}(\mu))$ corresponds to a strongly connected
component of $\mathsf{CG}(\mu)$.∎

By construction, for any process $p$, and for any $X\in\\{S,R\\}$, there are
at most two vertices $v$ of $\alpha(\mathsf{pgr}(\mu))$ such that
$p\in\lambda_{X}(v)$. From this, we deduce that $\alpha(\mathsf{pgr}(\mu))$
has at most $2|\mathbb{P}|$ vertices, and as a consequence:

######  Lemma 7 ()

$\sharp\\{\alpha(\mathsf{pgr}(\mu))\mid\mu\mbox{ is an exchange}\\}\leq
2^{6|\mathbb{P}|^{2}}$.

###### Proof

Let $n\geq 0$ be fixed and let us give an upper bound on the number of
P-graphs with $n$ vertices. First, there are $2^{n(n-1)}$ different possible
choices for the edge relation. By construction (in particular, by definition
of function $\mathsf{erase}(.)$), it holds that

$(1)\qquad\forall p\in\mathbb{P},\forall X\in\\{S,R\\},\sharp\\{v\mid
p\in\lambda_{X}(v)\\}\leq 2.$

A choice for the $\lambda$ function is therefore the choice, for each $p$, of
at most two vertices $v$ such that $p\in\lambda_{S}(v)$ and at most two other
vertices $v$ such that $p\in\lambda_{R}(v)$. So there are at most $n^{4}$
different choices for each $p$, and at most $n^{4|\mathbb{P}|}$ different
choices for $\lambda$. To sum up, there are less than
$2^{n^{2}}n^{4|\mathbb{P}|}$ P-graphs with $n$ vertices.

Now, again from (1), there are at most $2|\mathbb{P}|$ vertices in a P-graph,
so the number of P-graph is bounded by

$\sum_{n=1}^{2|\mathbb{P}|}2^{n^{2}}n^{4|\mathbb{P}|}\leq
2|\mathbb{P}|2^{|\mathbb{P}|^{2}}(2|\mathbb{P}|)^{4|\mathbb{P}|}\leq
2^{|\mathbb{P}|^{2}}2^{|\mathbb{P}|^{2}}(2^{|\mathbb{P}|})^{4|\mathbb{P}|}=2^{6|\mathbb{P}|^{2}}.$

∎

There are therefore finitely many $\alpha(\mathsf{pgr}(\mu))$. This allows us
to define the automaton that computes $\alpha(\mathsf{pgr}(msc(w)))$ for any
$w\in\Sigma^{*}$ and accepts $w$ in the language of this new automaton when
this P-graph is a single vertex graph. Let $G=(V,E,\lambda_{S},\lambda_{R})$
and a letter ${\dagger}v^{p\to q}\in\Sigma$ be fixed. We want to define the
transition function $\delta_{g}$ of our automaton, or in other words, the
P-graph $\delta_{g}(G,{\dagger}v^{p\to q})$ reached after adding the message
${\dagger}v^{p\to q}$ to the MSC. We let $\delta_{g}(G,{\dagger}v_{0}^{p\to
q})=\alpha(G^{\prime})$.
$G^{\prime}=(V^{\prime},E^{\prime},\lambda_{S}^{\prime},\lambda_{R}^{\prime})$
is defined as follows: (1) $V^{\prime}=V\uplus\\{v_{0}\\}$, (2)
$\lambda_{S}^{\prime}(v_{0})=\\{p\\}$, (3) if ${\dagger}=!?$, then
$\lambda_{R}^{\prime}(v_{0})=\\{q\\}$, and if ${\dagger}=!$, then
$\lambda_{R}^{\prime}(v_{0})=\emptyset$, (4) for all $v\in V$, for all
$X\in\\{S,R\\}$, $\lambda_{X}^{\prime}(v)=\lambda_{X}(v)$, and (5) the set of
edges $E^{\prime}$ is defined as

$\begin{array}[]{lll}\quad E^{\prime}&=&E\cup\\{(v,v_{0})\mid
p\in\lambda_{S}(v)\\}\cup\\{(v_{0},v)\mid p\in\lambda_{R}(v)\\}\\\
&\cup&\left\\{\begin{array}[]{ll}\\{(v,v_{0})\mid
q\in\lambda_{S}(v)\cup\lambda_{R}(v)\\}&\mbox{if }{\dagger}=!?\\\
\emptyset&\mbox{if }{\dagger}=!\end{array}\right.\end{array}$ For example,
consider the MSC $\mu$ of Fig. 8 and let $G=\alpha(\mathsf{pgr}(\mu))$ be its
associated abstracted P-graph. Let $G^{\prime}$ be defined as above while
reading $!?v_{6}^{r\to q}$. Then $G^{\prime}$ is the graph on the right, and
$\delta_{g}(G,v_{6}^{r\to q})$ is a single vertex graph.

$\hskip 1.42271pt\\{v_{1}\\}$ $\hskip 1.42271pt\\{v_{6}\\}$ $\hskip
1.42271pt\\{v_{3}\\}$ $\\{v_{4},v_{5}\\}$ Figure 9: Graph $G^{\prime}$

######  Lemma 8 ()

$\delta_{g}(\alpha(\mathsf{pgr}(msc(w))),{\dagger}v^{p\to
q})=\alpha(\mathsf{pgr}(msc(w\cdot{\dagger}v^{p\to q})))$.

Before we prove Lemma 8, we need to introduce a few notions and observations.
Let $G=(V,E,\lambda_{S},\lambda_{R})$ be a P-graph. A vertex $v\in V$ is
X-covered if for all $p\in\lambda_{X}(v)$ $p$ is X-redundant. We also say that
$v\in V$ is covered if it is both S-covered and R-covered. A partial
abstraction of $G$ is a graph
$G^{\prime}=(V^{\prime},E^{\prime},\lambda_{S},\lambda_{R})$ such that

  * •

$V^{\prime}=\\{V_{1},\dots,V_{n}\\}$ where each $V_{i}$ is a (not necessarily
maximal) strongly connected component of $G$, all $V_{i}$ are disjoints, and
for all $v\in V\setminus\bigcup_{i=1}^{n}V_{i}$ $v$ is covered.

  * •

for all $i,j$, $(V_{i},V_{j})\in E^{\prime}$ iff $(v,v^{\prime})\in E$ for
some $v\in V_{i}$ and some $v^{\prime}\in V_{j}$.

  * •

for all $i,X$, $\lambda_{X}(V_{i})=\bigcup_{v\in V_{i}}\lambda_{X}(v)$

Intuitively, $G^{\prime}$ is a partial abstraction of $G$ if it results from a
“partial application” of the functions $\mathsf{merge}(.)$,
$\mathsf{erase}(.)$, and $\mathsf{sweep}(.)$: some vertices of a same SCC are
merged, but not necessarily all, some labels are erased, but not necessarily
all, and some vertices are sweeped, but not necessarily all. From this
observation, it follows the following: if $G^{\prime}$ is a partial
abstraction of $G$, then $\alpha(G^{\prime})=\alpha(G)$.

###### Proof

Let $w\in\Sigma^{*}$ and ${\dagger}v^{p\rightarrow q}$ be fixed. Let
$G_{1}=\mathsf{pgr}(msc(w))$ and
$G_{2}=\mathsf{pgr}(msc(w\cdot{\dagger}v^{p\rightarrow q}))$ and let us
compare $G_{1}$ and $G_{2}$. First, there is an extra vertex $v_{0}$ in
$G_{2}$ that represents ${\dagger}v^{p\rightarrow q}$, with
$\lambda_{S}(v_{0})=\\{p\\}$ and either $\lambda_{R}(v_{0})=\\{q\\}$ (if
${\dagger}=!?$) or $\lambda_{R}(v_{0})=\emptyset$ (if ${\dagger}=?$). Now,
consider the extra edges. Obviously, these extra edges have $v_{0}$ either as
source or as destination. First consider the edges with $v_{0}$ as
destination. The send event of $v_{0}$ happens after all send events of $p$,
so for all $v\neq v_{0}$ such that $p\in\lambda_{S}(v)$, $(v,v_{0})\in E_{2}$.
In the case where ${\dagger}=!?$, the receive event of $v_{0}$ also happens
after all send and receive events of $q$, so for all $v\neq v_{0}$ such that
$q\in\lambda_{S}(v)\cup\lambda_{R}(v)$, $(v,v_{0})\in E_{2}$. There are no
other incoming edges in $v_{0}$ Now, consider the outgoing edges of $v_{0}$.
The send event of $v_{0}$ happens before all receive events of $p$, so for all
$v\neq v_{0}$ such that $p\in\lambda_{R}(v)$, $(v_{0},v)\in E_{2}$. To sum up,
we have:

$\begin{array}[]{lll}E_{2}&=&E_{1}\cup\\{(v,v_{0})\mid
p\in\lambda_{S}(v)\\}\\\ &\cup&\\{(v_{0},v)\mid p\in\lambda_{R}(v)\\}\\\
&\cup&\left\\{\begin{array}[]{ll}\\{(v,v_{0})\mid
q\in\lambda_{S}(v)\cup\lambda_{R}(v)\\}&\mbox{if }{\dagger}=!?\\\
\emptyset&\mbox{if }{\dagger}=!\end{array}\right.\end{array}$

Observe now that the rules to add vertices and edges to go from $G_{1}$ to
$G_{2}$ are exactly the same as the rules to go from $G$ to $G^{\prime}$ in
the definition of $\delta_{g}(G,{\dagger}v^{p\rightarrow q})$. Assume that
$G=\alpha(G_{1})=\alpha(\mathsf{pgr}(msc(w))$. Then $G^{\prime}$ is a partial
abstraction of $G_{2}$. So by the discussion above,

$\alpha(G^{\prime})=\alpha(G_{2}).$

Now, by definition of $\delta_{g}$, $\delta_{g}(G,{\dagger}v^{p\rightarrow
q}))=\alpha(G^{\prime})$. To sum up

$\delta_{g}(G,{\dagger}v^{p\rightarrow
q})=\alpha(G_{2})=\alpha(\mathsf{pgr}(msc(w\cdot{\dagger}v^{p\rightarrow
q}))).$

∎

######  Theorem 5.1 ()

There is an effective deterministic finite state automaton $\mathcal{A}$ with
less than $2^{6|\mathbb{P}|^{2}}$ states such that
$\mathcal{L}(\mathcal{A})=\\{w\in\Sigma^{*}\mid msc(w)\mbox{ is prime}\\}$.

###### Proof

Let $\mathcal{A}=(Q,\Sigma,\delta_{q},q_{0},F)$ be defined by

  * •

$Q=\\{\alpha(\mathsf{pgr}(\mu))\mid\mu\mbox{ is an exchange}\\}$;

  * •

$\delta_{q}$ as defined in Section 5;

  * •

$q_{0}=\alpha(\mathsf{pgr}(\epsilon))$ where $\epsilon$ denotes the empty MSC

  * •

$F=\\{G\in Q\mid|G|=1\\}$

Then by Lemma 7, $\mathcal{A}$ is a deterministic finite state automaton with
at most $2^{6|\mathbb{P}|^{2}}$ states. Moreover, by Lemma 8, for all $w$,
$\delta_{q}^{*}(q_{0},w)=\mathsf{pgr}(msc(w))$, so $w$ is accepted iff
$\mathsf{pgr}(msc(w))$ is a single vertex graph. By Lemma 6, this is
equivalent to the fact that $msc(w)$ is prime. ∎

##  6 Computation of $k$

So far we have shown: in Lemma 1, we established that a way to compute
$\mathsf{sd}(\mathfrak{S})$ was to compute the length $k$ of the largest prime
reachable exchange. To every word $w\in\Sigma^{*}$, we associated an MSC
$msc(w)$, and we showed that for every reachable MSC $\mu$, there exists a
word $w\in\Sigma^{*}$ such that $\mu=msc(w)$ (Lemma 2). We deduced that $k$
corresponds to the length of the longest word of
$\mathcal{L}_{\mbox{r}}\cap\mathcal{L}_{\mbox{p}}$ , if
$\mathcal{L}_{\mbox{r}}\cap\mathcal{L}_{\mbox{p}}$ is finite, otherwise
$k=\infty$. In Section 4, we showed that $\mathcal{L}_{\mbox{r}}$ is an
effective regular language, and, in Section 5, we showed that
$\mathcal{L}_{\mbox{p}}$ is also an effective regular language. We deduce that
$\mathcal{L}_{\mbox{r}}\cap\mathcal{L}_{\mbox{p}}$ is therefore an effective
regular language, and that $k$ is computable (since the finiteness and the
length of the longest word of a regular language are computable). With a
careful analysis of the automata that come into play, we can give an upper
bound on $k$.

######  Theorem 6.1 ()

$\mathsf{sd}(\mathfrak{S})$ is computable, and if
$\mathsf{sd}(\mathfrak{S})<\infty$ then
$\mathsf{sd}(\mathfrak{S})<|\mathfrak{S}|^{2}2^{8|\mathbb{P}|^{2}}$, where
$|\mathfrak{S}|$ is the number of global control states and $|\mathbb{P}|$ the
number of processes.

###### Proof

The fact that $\mathsf{sd}(\mathfrak{S})$ is computable is explained at the
beginning of Section 6. We therefore only prove the claim that, when
$k<\infty$ it holds that $k<|\mathfrak{S}|^{2}2^{8|\mathbb{P}|^{2}}$. $k$ is
the length of the longest word in
$\mathcal{L}_{\mbox{r}}\cap\mathcal{L}_{\mbox{p}}$. By Theorem 4.1,

$\mathcal{L}_{\mbox{r}}=\bigcup\mathcal{R}$

and by Theorem 5.1 there is an automaton $\mathcal{A}$ such that
$\mathcal{L}(\mathcal{A})=\mathcal{L}_{\mbox{p}}$. So we need to bound the
length of the longest word of

$\mathcal{L}(\mathtt{SR}(\mathbf{l},\mathbf{mid},\mathbf{l^{\prime}}))\cap\mathcal{L}(\mathcal{A}(B,B^{\prime}))\cap\mathcal{L}(\mathcal{A})$

assuming that this language is finite, for any
$\mathbf{l},\mathbf{mid},\mathbf{l^{\prime}},B,B^{\prime}$. This bound is
given by the number of states of any automaton that accepts this language
(since any longer word would require the automaton to feature a loop, and the
language would not be finite). This language is recognized by an automaton
that is the product of the automata
$\mathtt{SR}(\mathbf{l},\mathbf{mid},\mathbf{fin})$,
$\mathcal{A}(B,B^{\prime})$, and $\mathcal{A}$, so its number of states is
bounded by

$|\mathtt{SR}(\mathbf{l},\mathbf{mid},\mathbf{l^{\prime}})|\times|\mathcal{A}(B,B^{\prime}))|\times|\mathcal{A}|$

By definition of $\mathtt{SR}$, $L_{\mathtt{SR}}=L_{\mathfrak{S}}^{2}$, so
$|\mathtt{SR}|\leq|L_{\mathfrak{S}}|^{2}$ (which we can also write
$|\mathfrak{S}|^{2}$). By definition of $\mathcal{A}(B,B^{\prime})$,
$L_{(B,B^{\prime})}=\mathbb{B}=(2^{\mathbb{P}}\times
2^{\mathbb{P}})^{\mathbb{P}}$, so $|\mathcal{A}(B,B^{\prime})|\leq
2^{2|\mathbb{P}|^{2}}$. Finally, by Theorem 5.1, $|\mathcal{A}|\leq
2^{6|\mathbb{P}|^{2}}$. All toghether,

$\begin{array}[]{ll}k&\leq|\mathfrak{S}|^{2}2^{2|\mathbb{P}|^{2}}2^{6|\mathbb{P}|^{2}}\\\
&\leq|\mathfrak{S}|^{2}2^{8|\mathbb{P}|^{2}}\end{array}$

∎

As an immediate consequence of Theorems 2.1 and 6.1, we get the following.

######  Theorem 6.2 ()

The following problem is decidable : given a system $\mathfrak{S}$, does there
exists a $k$ such that $\mathfrak{S}$ is $k$-synchronizable.

##  7 Conclusion

We established that it is possible to determine whether there exists a bound
$k$ such that a given communicating system is $k$-synchronizable. For this, we
showed how the set of sequences of actions that compose an exchange of
arbitrary size can be represented as a regular language, which was possible
thanks to the mailbox semantics of communications. We leave for future work to
decide whether it would be possible to extend our result to peer-to-peer
semantics.

## References

  * [1] Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91–101 (1996)
  * [2] Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. 656, 60–75 (2016)
  * [3] Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: CAV 2018. pp. 372–391 (2018)
  * [4] Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
  * [5] Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: RP 2009. vol. 5797, pp. 93–106. Springer (2009)
  * [6] Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, 1988. pp. 44–65. ACM (1988)
  * [7] Di Giusto, C., Laversa, L., Lozes, É.: On the k-synchronizability of systems. In: Goubault-Larrecq, J., König, B. (eds.) FOSSACS 2020, ETAPS 2020. vol. 12077, pp. 157–176. Springer (2020)
  * [8] Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)
  * [9] Finkel, A., Lozes, É.: Synchronizability of communicating finite state machines is not decidable. In: ICALP 2017. pp. 122:1–122:14 (2017)
  * [10] Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007)
  * [11] von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3(POPL), 59:1–59:30 (2019)
  * [12] Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR 2018. vol. 118, pp. 21:1–21:17 (2018)
  * [13] La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: TACAS 2008, ETAPS 2008. pp. 299–314 (2008)
  * [14] Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)