Communication is an essential element of modern software, yet
programming and analysing communicating systems are difficult tasks.

A reason for this difficulty is the lack of compositional mechanisms
that preserve relevant communication properties.

This problem has been recently addressed for the well-known model of
communicating systems, that is sets of components consisting
of finite-state machines capable of exchanging messages.

The main idea of this approach is to take two systems, select a
participant from each of them, and derive from those participants a
pair of coupled gateways connecting the two systems.

More precisely, a message directed to one of the gateways is
forwarded to the gateway in the other system, which sends it to the
other system.

It has been shown that, under some suitable compatibility
conditions between gateways, this composition mechanism preserves
deadlock freedom for asynchronous as well as symmetric synchronous
communications (where sender and receiver play the same part in
determining which message to exchange).

This paper considers the case of asymmetric synchronous
communications where senders decide independently which message
should be exchanged.

We show here that preservation of lock freedom requires
sequentiality of gateways, while this is not needed for preservation of
either deadlock freedom or strong lock freedom.

§ INTRODUCTION

Communication is an essential constitutive element of modern software
due to the fact that applications are increasingly developed in
distributed architectures (e.g., service-oriented architectures,
microservices, cloud, etc.).

In practice, APIs and libraries featuring different communication
mechanisms are available for practically any programming language.

Reasoning on and developing communicating systems are difficult

Indeed, several models have been used to study interactions between
systems (e.g., process algebras, transition systems, Petri nets,
logical frameworks, etc.).

The so-called business logic, necessary to determine
what has to be communicated, needs to be complemented with the
so-called application level protocol specifying how
information spreads across a system.

Conceptual and programming errors may occur in the realisation of
application level protocols.

For instance, it may happen that some components in a system are
prevented to communicate because all the expected partners terminated
their execution (deadlock).

Other typical errors occur when a system is not lock-free, that is
when some components cannot progress because all their partners are
perpetually involved in other communications.

These kinds of problems can arise when a system can evolve in
different ways depending on some conditions and components have
inconsistent views of the state of the system.

If this happens, some components may reach a state no longer
compatible with the state of their partners and therefore
communications do not happen as expected.

We illustrate these problems with some simple examples for deadlock
freedom (similar examples may be given for lock freedom).

Suppose we want to model a client-server system where clients'
requests are acknowledged either with an answer or with unknown
from servers.

Due to its popularity, we choose CCS [17] to
introduce this scenario, so take the following agents:

\begin{align}\label{eq:v1}
\ptp[C] = \bar{\msg[r]}. \msg[a] + \bar{\msg[r]}. \msg[u]
\quad\qqand\quad
\ptp[D] = \msg[r]. \bar{\msg[a]} + \msg[r]. \bar{\msg[u]}
\end{align}

where ports $\msg[r]$, $\msg[a]$, and $\msg[u]$ are respectively used
to commmunicate requests, answers, and unknowns.

(Recall that in CCS $\msg[a].\_$ and $\_+\_$ represent respectively
prefix and non-deterministic choice.)

The common interpretation of agents in (<ref>) is that $\msg[x]$
and $\bar{\msg[x]}$ respectively represent an input and an output on
port $\msg[x]$.

It is a simple observation that the system $\ptp[C] \mid \ptp[D]$
where $\ptp[C]$ and $\ptp[D]$ run in parallel can evolve to e.g., the
deadlock state $\msg[a] \mid \bar{\msg[u]}$ where each party is
waiting for the other to progress.

The problem is that the choice of what communication should happen
after a request is taken independently by $\ptp[C]$ and $\ptp[D]$
instead of letting $\ptp[D]$ to take the decision and drive $\ptp[C]$
on the right branch.

This is attempted in the next version:

\begin{align}\label{eq:v2}
\ptp[C] = \bar{\msg[r]}. (\msg[a] + \msg[u])
\quad\qqand\quad
\ptp[D] = \msg[r]. (\bar{\msg[a]} + \bar{\msg[u]})
\end{align}

A key difference with the agents in (<ref>) is that the server
$\ptp[D]$ in (<ref>) decides what to reply to the client
$\ptp[C]$, which becomes aware of the choice through the interaction
with $\ptp[D]$ after the request has been made.

Assume now that $\ptp[D]$ acts as a proxy to another server, say

When $\ptp[D]$ cannot return an answer to the client [c] it interacts with
$\ptp[D]'$ on port $\msg[p]$.

Answers are sent directly to [c] if $\ptp[D]'$ can compute them,
otherwise $\ptp[D]'$ returns an unknown on port $\msg[u]'$ to
$\ptp[D]$ which forwards it to [c].

This is modelled by the agents

\begin{align}\label{eq:v3}
% \ptp[C] = \bar{\msg[r]}. (\msg[a] + \msg[u])
% \quad\qqand\quad
\ptp[D] = \msg[r]. (\bar{\msg[a]} + \bar{\msg[p]}. \msg[u]' . \bar{\msg[u]})
\quad\qqand\quad
\ptp[D]' = \msg[p]. (\bar{\msg[a]} + \bar{\msg[u]'})
\end{align}

Note that this change is completely transparent to agent $\ptp[c]$,
which in fact stays as in (<ref>).

It is now more difficult to ascertain if these choices may lead to a
deadlock since the decision of $\ptp[D]$ may involve also $\ptp[D]'$.

Indeed, the parallel composition of agents in (<ref>) may
deadlock because, when $\ptp[C]$ and $\ptp[D]$ interact on port
$\msg[a]$, $\ptp[D]'$ hangs on port $\msg[p]$ and, likewise, if
$\ptp[C]$ and $\ptp[D']$ interact on port $\msg[a]$ then $\ptp[D]$
hangs on port $\msg[u]'$.

A reason for this difficulty is that it is hard to define
compositional mechanisms that preserve relevant communication
properties such as deadlock or lock freedom.

Recently, an approach to the composition of concurrent and distributed
systems has been proposed in [2, 3] for
the well-known model of systems of communicating finite-state
machines (CFSMs) [12], that is sets of finite-state automata
capable of exchanging messages.

The compositional mechanism is based on the idea that two given
systems, say $\aCS$ and $\aCS'$, are composed by transforming two
CFSMs, say $\HH$ in $\aCS$ and $\KK$ in $\aCS'$, into coupled

Basically, each message that $\HH$ receives from a machine in $\aCS$
is forwarded to $\KK$ and vice versa.

It has been shown that, under suitable compatibility conditions
between $\HH$ and $\KK$, this composition mechanism preserves deadlock
freedom for asynchronous as well as symmetric synchronous
communications (where sender and receiver play the same part in
determining which message to exchange).

The compatibility condition identified
in [2, 3] consists in exhibiting
essentially dual behaviours: gateway $\HH$ is able to receive a
message whenever gateway $\KK$ is willing to send one and vice versa.

As observed in [4], a remarkable feature of such an
approach is that it enables the composition of systems originally
designed as closed systems.

As far as two compatible machines can be found, any two systems can be
composed by transforming as hinted above the compatible machines.

The results in [2, 3] are developed in the
asynchronous semantics of CFSMs.

These results have been transferred in [5] to a setting
where CFSMs communicate synchronously much like as the communication
mechanisms considered for instance in process algebras like CCS, ACP,

This model assumes a perfect symmetry between sender and receiver in
synchronous communications.

Let us again discuss this with an example.

Consider the agents

\begin{align}\label{ex:symmetry}
\ptp[T] = \bar{\msg[a]}.\ptp[P] + \bar{\msg[b]}.\ptp[Q]
\qqand
\ptp[R] = \msg[a].\ptp[P]' + \msg[b].\ptp[Q]'
\end{align}

According to the standard semantics of CCS [17],
system $(\ptp[T] \mid \ptp[R])\setminus\Set{\msg[a],\msg[b]}$ has two
possible evolutions:

\begin{align*}
(\ptp[T] \mid \ptp[R])\setminus\Set{\msg[a],\msg[b]} \trans \tau \ptp[P] \mid \ptp[P]'
\qqand
(\ptp[T] \mid \ptp[R])\setminus\Set{\msg[a],\msg[b]} \trans \tau \ptp[Q] \mid \ptp[Q]'
\end{align*}

namely, either both $\ptp[T]$ and $\ptp[R]$ opt for the leftmost
branch (synchronising on $\msg[a]$) or they both choose the
rightmost one (synchronising on $\msg[b]$).

(Recall that in CCS $\_ \setminus X$ is the hiding of ports in the set
$X$ and that $\tau$ represents an internal action.)

This means that, the resolution of the choice is implicit
in the communication mechanism: a branch is taken as soon as $\ptp[T]$
and $\ptp[R]$ synchronise on the corresponding port.

Intuitively, no distinction is made between sender and receiver
(formally they are indeed interchangeable); this implies that the
communication mechanism is at the very core of choice
resolution [5].

Interestingly, for synchronous communications an alternative
interpretation is actually possible. Indeed, this perfect symmetry is not
assumed so that sender and receiver play different roles in choice
resolution while still relying on synchronous communication.

Let us explain this interpretation using again CCS.

Consider a variant of CCS where outputs must be enabled before
being fired.

One could formally specify that with the following reduction rules:

\begin{align}\label{eq:aCCS}
\bar{\msg[a]}.\ptp[P] + \ptp[P]' \trans \tau \bar{\bar{\msg[a]}}.\ptp[P]
\qqand
\bar{\bar{\msg[a]}}.\ptp[P] \mid (\msg[a].\ptp[Q] + \ptp[Q]') \trans \tau \ptp[P] | \ptp[Q]
\end{align}

whereby the leftmost rule chooses one of the possible outputs
of the sender (the chosen output is marked by the double bar in our
notation) and the rightmost rule actually synchronises sender and

This semantics is an abstract model of asymmetric
communications (used e.g., in [8, 18]), where
silent steps taken using the left rule model some internal computation
of the sender to decide what to communicate to the partner.

In other words, now the choice is entirely resolved on one side
while the communication is a mere interaction of complementary
actions, the output and the input.

This asymmetry, at the core of asynchronous communication,
can therefore also carry for synchronous communication.

It is worth observing that asymmetric communications abstract a rather
common programming pattern where sending components may choose the
output to execute depending on some internal computation.

For instance, elaborating on the proxy scenario in (<ref>),
$\ptp[D]$ could decide to directly send unknowns to normal clients
while reserving the use of $\ptp[D]'$ only for privileged

This paper transfers the composition by gateway mechanism
of [2, 3] to the case of asymmetric
synchronous communication of CFSMs.

The main technical results are that, in the asymmetric case, gateway composition

* preserves deadlock freedom (as well as a strong version of lock
freedom) provided that systems are composable (the relation of compatibility – one of the requirements for systems to be composable – in the present paper is less restrictive than
the one
used in [5]);

* preserves lock freedom if systems are composable and gateways are sequential,
namely each state has at most one outgoing transition.

Interestingly, preservation of deadlock freedom can be guaranteed under
milder conditions than in the
symmetric case.

In fact, sequentiality of gateways is not necessary to preserve
deadlock freedom in the asymmetric case, while it is in the symmetric one.

Structure of the paper. <ref> introduces systems
of (asymmetric synchronous) CFSMs, related notions and
communication properties.

Composition by gateways is introduced and discussed in
<ref> together with the compatibility relation.

<ref> discusses the issues that prevent gateway
composition to preserve communication properties.

<ref> is devoted to the preservation of communication

Conclusions, related and future work are discussed in <ref>.

For space limitation, full proofs are reported in [6].

§ BACKGROUND

Communicating Finite State Machines (CFSMs) [12] are Finite
State Automata (FSAs) where transitions are labelled by

We recall basic notions on FSAs.

A finite state automaton (FSA) is a tuple
$A = \conf{\sset, q_0, \lset, \tset}$ where

* $\sset$ is a finite set of states (ranged over by lowercase
italic Latin letters);

* $q_0 \in \sset$ is the initial state;

* $\lset$ is a finite set of labels

* $\tset \,\subseteq\, \sset \times (\lset \cup \{\tau\}) \times
\sset$ is a set of transitions.

Hereafter, we let $\al$ range over $\lset \cup \{\tau\}$ when it is
immaterial to specify the set of labels or it is understood.

We use the usual notation $q_1 \trans \al q_2$ for the transition
$(q_1,\al,q_2) \in \trans{}$, and $q_1 \trans{} q_2$ when there exists a
label $\al$ such that $q_1 \trans \al q_2$.

Let $\_\cat\_$ be the concatenation operation on labels and write
$p \trans \pi q$ where $\pi = \al_1 \cat \al_2 \cat \ldots \cat \al_n$
$p \trans{\al_1} p_1 \trans{\al_2} \ldots \trans{\al_n} p_n = q$.

We let $\pi,\psi,\ldots$ range over $\lset^\star$ (i.e., sequences of
labels) and define the set of reachable states in $A$ from $q$

\begin{align*}
\RS[A,q] & = \Set{p \sst \text{there is } \pi \in \lset^\star \text{ such that } q \trans \pi p}
\end{align*}

The set of reachable states in $A$ is $\RS[A] = \RS[A,q_0]$.

For succinctness, $q \trans{\al} q' \in A$ means that the transition
belongs to (the set of transitions of) $A$; likewise, $q \in A$ means
that $q$ belongs to the states of $A$.

We say that $q \trans{\al} q'$ is an outgoing
(resp. incoming) transition of $q$ (resp. $q'$).

Since we use FSAs to formalise communicating systems, accepting states
are disregarded (as also done in [12]).

We adapt the definitions in [12] to cast CFSMs in our context.

Let $\mathfrak{P}$ be a set of participants (or roles,
ranged over by $\p$, $\p[B]$, etc.) and $\msgset$ a set of
messages (ranged over by $\msg$, $\msg[n]$, etc.).

We take $\mathfrak{P}$ and $\msgset$ disjoint.

An output label is written as $\aout$ and represents the
willingness of  to send message $\msg$ to ; likewise, an
input label is written as $\ain$ and represents the
willingness of  to receive message $\msg$ from .

The subjects of an output label $\aout$ and of an input label
$\ain$ are  and , respectively.

Let	 $\lact = \{\aout, \ain \mid \p[A] \neq \p[B] \in \mathfrak{P}, \msg \in \msgset\}$.

A communicating finite-state machine (CFSM) is an FSA $\aCM$
with labels $\lact \cup \Set{\tau}$ such that, for any transition
$p \trans \al q$ of $\aCM$,

* if $\al$ is an output label then $p \neq q$ and $p$ has
exactly one incoming transition, and such transition is labelled
by $\tau$;

* if $\al = \tau$ then $p \neq q$ and $q$ has exactly one
outgoing transition, and such transition is labelled by an output

A state of $\aCM$ is

* terminal, if it has no outgoing transition; we define
$\tstates \aCM = \Set{p \in \aCM \sst p \text{ is terminal in }
\aCM}$

* sending, if it is not terminal and all its outgoing
transitions have output labels

* receiving, if it is not terminal and all its outgoing
transitions have input labels

* mixed, if it has a silent outgoing transition and an
outgoing transition with an input label.

A CFSM is -local if all its non $\tau$ transitions have subject .

Unlike in [5], the transitions of our CFSMs can also be
labelled by the silent action $\tau$.

<ref> can be looked at as the CFSM
counterpart of the $\tau C$ contracts described
in [7].

Imposing the no-mixed state condition on our CFSM, turns them into the
communicating automata counterpart of the processes (contracts) called
session behaviours[Actually different variations of
this name are used in the listed references.] in
e.g., [11, 1, 8].

These processes are in turn the process counterpart of (binary) session types [14].

As we shall see below (and also shown in [3]
and [5]), the absence of mixed states is necessary in
order to get the preservation of properties by composition.

As a matter of fact, we could drop the conditions related to
$\tau$-transitions in case a transition like
$\cauttr[p][{\aout[X][Y][@][z]}][q][][]$ is the only outgoing
transition from $p$, namely when no actual choice of output actions is
possible in $p$.

We however prefer to avoid this distinction because
($i$) our uniform treatment of transitions allows us to
immediately adapt definitions in a more abstract setting
and ($ii$)

secondly, uniformity allows us to simplify some technicalities.

Said that, all proofs in the present paper could easily be adapted to
the above mentioned alternative definition of CFSM.

A (communicating) system over $\ptpset$ is a map
$\aCS = (\aCM_{\p})_{\p \in \ptpset}$ assigning an $\p$-local CFSM
$\aCM_{\p}$ to each participant $\p \in \ptpset$ where
$\ptpset \subseteq \mathfrak{P}$ is finite and any participant
occurring in a transition of $\aCM_{\p}$ is in $\ptpset$.

Note that <ref> requires that any input or output label does
refer to participants belonging to the system itself.

In other words, <ref> restricts to closed systems.

We define the synchronous semantics of communicating systems as an FSA
(differently from the asynchronous case, where the set of states can
be infinite).

Hereafter, $\dom f$ denotes the domain of a function $f$ and
$\upd f x y$ denotes the update of $f$ in a point $x \in \dom f$ with
the value $y$.

Let $\aCS$ be a communicating system.

A configuration of  $\aCS$ is a map
$\aConf = (q_{\p})_{\p \in \dom \aCS}$ assigning a local state
$q_{\p}\in \aCS(\p)$ to each $\p \in \dom \aCS$.

The asymmetric synchronisations of $\aCS$ is the FSA
$\ssem{\aCS} = \conf{\sset, \aConf_0, \lint\cup\Set{\tau},\tset}$

* $\sset$ is the set of synchronous configurations of $\aCS$, as
defined above;

* $\aConf_0=(q_{0\p})_{\p \in \dom \aCS} \in
\sset$ is the initial configuration where, for  each $\p \in \dom \aCS$,
$q_{0\p}$ is the initial state of $\aCS(\p)$;

* $\lint \ =\ \{\gint[] \mid \p \neq \q \in \mathfrak{P} \text{ and
} \msg \in \msgset\}$ is a set of interaction labels;

* $\aConf \trans{\gint[]} \upd \aConf \p {q, \q \mapsto q'} \in \ssem{\aCS}$
if $\aConf(\p) \trans{\aout} q \in \aCS(\p)$ and $\aConf(\q)
\trans{\ain} q' \in \aCS(\q)$;

* $\aConf \trans{\tau} \upd \aConf \p {q} \in \ssem{\aCS}$
if $\aConf(\p) \trans{\tau} q \in \aCS(\p)$;

Configuration $\aConf$ enables  in $\aCS$ if $\aConf(\p)$
has at least an outgoing transition.

As expected, an interaction $\gint[]$ occurs when $\p$ performs an
output $\aout$ (which has been previously chosen) and $\q$ the
corresponding input $\ain$.
Let us consider the communicating system
$\aCS= (\aCM_{\ptp[X]})_{\ptp[X] \in
\Set{\ptp[K],\ptp[C],\ptp[D],\ptp[E]}}$, where

\[
<EMAIL_ADDRESS>\cfsmK
\cfsmC
\\
\cfsmD
\cfsmE
\end{array}
\]

A sequence of
transitions of
$\ssem{\aCS}$ out of $\aConf_0$ is, according to <ref>,

\[\begin{array}{cccccr}
\aConf_0 = (0_{\KK},0_{\ptp[C]},0_{\ptp[D]}, 0_{\ptp[E]})
& \trans \tau & (1_{\KK},0_{\ptp[C]},0_{\ptp[D]}, 0_{\ptp[E]})
& \trans{\gint[][K][m][C]} & (3_{\KK},1_{\ptp[C]},0_{\ptp[D]},0_{\ptp[E]})
\\
& \trans \tau & (3_{\KK},2_{\ptp[C]},0_{\ptp[D]},0_{\ptp[E]})
& \trans{\gint[][C][c][E]} & (3_{\KK},3_{\ptp[C]},0_{\ptp[D]},4_{\ptp[E]})
\\
& \trans \tau & (3_{\KK},3_{\ptp[C]},0_{\ptp[D]},5_{\ptp[E]})
& \trans{\gint[][E][s][D]} & (3_{\KK},3_{\ptp[C]}, 3_{\ptp[D]},3_{\ptp[E]})
& \hspace{3.25cm}\mbox{\finex}
\end{array}\]

The symmetric synchronisation in [5] for systems without
$\tau$-transitions can be readily obtained from the above definition
by disregarding the clause for the $\tau$-transitions.

In the following, $\ptpof[\tau] = \emptyset$ and
$\ptpof = \ptpof[\aout] = \ptpof[\ain] = \Set{\p,\q}$ and, for a
sequence $\pi = \al_1 \cat \cdots \cat \al_n$, we let
$\ptpof[\pi] = \cup_{1 \leq i \leq n} \ptpof[\al_i]$.

As discussed in <ref>, we shall study the preservation of
communication properties under composition.

We shall consider the following relevant properties: deadlock freedom, lock
freedom and strong lock freedom.

The definitions below adapt the ones in [13] to a synchronous
setting (as done also in [16, 19, 5]).

Let $\aCS$ be a communicating system on $\ptpset$.

We say that a participant $\p \in \ptpset$ is involved in a
run $\aConf \trans{\al_1} \aConf_1 \ldots \trans{\al_n} \aConf_n$ of
$\aCS$ if there is $1 \leq i \leq n$ such that either
$\p \in \ptpof[\al_i]$ or $\al_i = \tau$,
$\aConf_i(\p) \trans \tau q$ in $\aCS(\p)$, and
$\aConf_{i+1} = \upd{\aConf_i} \p q$.

Deadlock freedom

A configuration $\aConf \in \RS[\ssem \aCS]$ is a deadlock

* $\aConf$ has no outgoing transitions in $\ssem{\aCS}$ and

* there exists $\p \in \ptpset$ such that $\aConf(\p)$ enables  in $\aCS$.

A system is deadlock-free if none of its configurations is a deadlock.

Lock freedom

Let $\p\in\ptpset$.
A configuration $\aConf \in \RS[\ssem
\aCS]$ is a lock for $\p$ if

* $\aConf(\p)$ has outgoing transitions; and

*  is not involved in any run from $\aConf$.

A system is lock-free if none of its configurations is a
lock for any of its participants.

Strong lock freedom System $\aCS$ is strongly lock-free
for $\p \in \ptpset$ if for each $\aConf \in \RS[\ssem \aCS]$
enabling  in $\aCS$ then  is involved in all maximal
sequences from $\aConf$.

A system is strongly lock free if it is strongly lock free
for each of its participants.

* Lock-freedom implies deadlock-freedom;

* Strong lock freedom implies lock freedom.

Let us consider the system $\aCS$ of <ref>. The only other
maximal transition sequence in $\ssem \aCS$ out of $\aConf_0$,
besides the one described in <ref>, is
\aConf_0 = (0_{\KK},0_{\ptp[C]},0_{\ptp[D]}, 0_{\ptp[E]})
& \trans \tau & (2_{\KK},0_{\ptp[C]},0_{\ptp[D]}, 0_{\ptp[E]})
& \trans{\gint[][K][n][D]} & (3_{\KK},0_{\ptp[C]},1_{\ptp[D]},0_{\ptp[E]})
\\
& \trans \tau & (3_{\KK},0_{\ptp[C]},2_{\ptp[D]},0_{\ptp[E]})
& \trans{\gint[][D][d][E]} & (3_{\KK},0_{\ptp[C]},3_{\ptp[D]},1_{\ptp[E]})
\\
& \trans \tau & (3_{\KK},0_{\ptp[C]},3_{\ptp[D]},2_{\ptp[E]})
& \trans{\gint[][E][s][C]} & (3_{\KK},3_{\ptp[C]}, 3_{\ptp[D]},3_{\ptp[E]})
\end{array}$$

These two sequences are both maximal and contain all the elements of $\RS[\ssem \aCS]$.
By the above observations it is possible to check $\aCS$ to be strongly lock free.

§ COMPOSITION VIA GATEWAYS

We now discuss the composition of systems of CFSMs via gateways (cf.
[2, 3]) and study its properties under
asymmetric synchronisation.

The main idea is that two systems of CFSMs, say $\aCS_1$ and $\aCS_2$,
can be composed by transforming one participant in each of them into
gateways connected to each other.

§.§ Building gateways

Hereafter, $\HH$ and $\KK$ denote the selected participant in $\aCS_1$
and $\aCS_2$ respectively selected for the composition.

The gateways for $\HH$ and $\KK$ are connected to each other and act
as forwarders: each message sent to the gateway for $\HH$ by a
participant from the original system $\aCS_1$ is now forwarded to the
gateway for $\KK$, that in turn forwards it to the same participant to
which $\KK$ sent it in the original system $\aCS_2$.

The dual will happen to messages that the gateway for $\KK$ receives
from $\aCS_2$. A main advantage of this approach is that no extension
of the CFSM model is needed to transform systems of CFSMs, which are
normally closed systems, into open systems that can be
composed. Another advantage is that the composition is fully
transparent to all participants different from $\HH$ and $\KK$.

We will now define composition via gateways on systems of CFSMs,
following the intuition above.

Given a $\HH$-local CFSM $\aCM$ and a participant $\KK$, the
gateway of $\aCM$ towards $\KK$ is the CFSM
$\gateway \aCM \KK$ obtained by replacing in $\aCM$

* each pair of consecutive transitions $p \trans{\tau} q
\trans{\aout[H][A]} r$ with

\begin{align}\label{eq:gtwout}
p \trans{\ain[K][H]} p' \trans{\tau} q
\trans{\aout[H][A]} r
\qqand[for some fresh state $p'$]
\end{align}

* each transition $p \trans{\ain[A][H]} r$ with

\begin{align}\label{eq:gtwin}
p \trans{\ain[A][H]} p' \trans{\tau} p'' \trans{\aout[H][K]} r
\qqand[for some fresh states $p'$ and $p''$]
\end{align}

We shall call external the states like $p$ and $r$ and
internal the states like $p'$, $p''$ and $q$.

Note that gateways execute segments of the form
described in (<ref>) and (<ref>) in the above

Also, by very construction, we have the following

Given a $\HH$-local CFSM $\aCM$ and a participant $\KK$,
each state of $\gateway \aCM \KK$
has at most one incoming or outgoing
$\tau$ transition.

We compose systems with disjoint participants taking all the
participants of the original systems but $\HH$ and $\KK$, whereas
$\HH$ and $\KK$ are replaced by their respective gateways.

Given two functions $f$ and $g$ such that
$\dom f \cap \dom g = \emptyset$, we let $f + g$ denote the function
behaving as function $f$ on $\dom f$ and as function $g$ on $\dom g$.

Let $\aCS_1$ and $\aCS_2$ be two systems with disjoint domains.

The composition of $\aCS_1$ and $\aCS_2$ via
$\HH \in \dom{\aCS_1}$ and $\KK \in \dom{\aCS_2}$ is defined as

\[\aCS_1 \connect \HH \KK \aCS_2 = \upd{\aCS_1}{\HH}{\gateway{\aCS_1(\HH)} \KK}
+ \upd{\aCS_2} \KK {\gateway{\aCS_2(\KK)} \HH}
% \p \mapsto \begin{cases}
%   \aCS_1(\p), &  \text{if } \p \in \dom{\aCS_1} \setminus \Set{\HH, \KK}
%   \\
%   \aCS_2(\p), &  \text{if } \p \in \dom{\aCS_2} \setminus \Set{\HH, \KK}
%   \\
%   \gateway{\aCS_1(\HH)} \KK, & \text{if } \p = \HH
%   \\
%   \gateway{\aCS_2(\KK)} \HH, & \text{if } \p = \KK
% \end{cases}
\]

(Note that $\dom{\aCS_1 \connect \HH \KK \aCS_2} = \dom{\aCS_1} \cup \dom{\aCS_2}$.)

We remark that, by the above approach for composition, we do not
actually need to formalise the notion of open system.

In fact any closed system can be looked at as open by choosing two
suitable participants in the to-be-connected systems and
transforming them into two forwarders.

Also, note that the notion of composition above is structural:
corresponding notions of behaviourals composition have been studied
in [4] and in [15] for multiparty session

Let us take the following two communicating systems.

\[
\aCS_1 = \dboxed{
<EMAIL_ADDRESS>\begin{array}{c}
\cfsmA
\\
\cfsmB
\end{array}
\cfsmH
\end{array}
\quad
\aCS_2 = \dboxed{\arraycolsep=1pt\def\arraystretch{3}
\begin{array}{cc}
\cfsmK
\cfsmE
\\[-1em]
\cfsmC
\cfsmD
\end{array}
\]

The system $\aCS_1 \connect{\HH}{\KK} \aCS_2$ is

\[
\csys{\arraycolsep=1.2pt
\begin{array}{ll}
\begin{array}{c}
\cfsmA
\\
\cfsmB
\end{array}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = above, initial distance = .4cm, initial text={$\gateway {\aCM_\HH} \KK$}] (zero) {$0$};
\node[state] (three)  [below left of=zero] {$2$};
\node[state] (four)  [below right  of=zero] {$3$};
\node[state] (five)  [below  of=three] {$4$};
\node[state] (six)  [below   of=four] {$5$};
\node[state] (one)  [below  right of=five] {$1$};
\path (zero) edge [bend right] node[above] {$\ain[A][H][][m]$}
(three) edge [bend left] node[above] {$\ain[B][H][][n]$} (four)
(three) edge  node[below] {$\tau$} (five)
(four) edge node[below] {$\tau$} (six)
(five) edge[bend right]  node[below] {$\aout[H][K][][m]$} (one)
(six) edge[bend left]  node[below] {$\aout[H][K][][n]$} (one)
\end{tikzpicture}
\end{array}
\qquad
\begin{array}{l@{\quad}l}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = above, initial distance = .4cm, initial text={$\gateway {\aCM_\KK} \HH$}] (zero) {$0$};
\node[state] (zero) {$0$};
\node[state] (four) [below right of=zero]   {$4$};
\node[state] (five) [below left of=zero]   {$5$};
\node[state] (one) [below of=five]   {$1$};
\node[state] (two) [below  of=four]   {$2$};
\node[state] (three) [below right of=one]   {$3$};
\path (one) edge[bend right] node[below] {$\aout[K][C][][m]$} (three)
(two) edge[bend left] node[below] {$\aout[K][D][][n]$} (three)
(five) edge node[below] {$\tau$} (one)
(four) edge node[below] {$\tau$} (two)
(zero) edge[bend right] node[above] {$\ain[H][K][][m]$} (five)
(zero) edge[bend left] node[above] {$\ain[H][K][][n]$} (four)
\end{tikzpicture}
\begin{array}{c}
\cfsmC
\\
\cfsmD
\\
\cfsmE
\end{array}
\end{array}
\]

Note that the CFSMs , , $\ptp[C]$, $\ptp[D]$, and $\ptp[E]$
remain unchanged.

Given a configuration of the composition of systems $\aCS_1$ and
$\aCS_2$ we can retrieve the configurations of the two subsystems by
taking only the states of participants in $\aCS_1$ and $\aCS_2$
while avoiding, for the gateways, to take the fresh states
introduced by the gateway construction.

Indeed, we shall prove in <ref> that for each
$\aConf \in \RS[\ssem{\aCS}]$, we have
$\cproj \aConf \HH \in \RS[\ssem{\aCS_1}]$ and
$\cproj \aConf \KK \in \RS[\ssem{\aCS_2}]$.

Let $\aConf$ be a configuration of a composed system
$\aCS_1 \connect \HH \KK \aCS_2$ and
$\aCM = \gateway{\aCS_1(\HH)} \KK$.

The left-projection of $\aConf$ on $\aCS_1$ is the map
$\cproj \aConf \HH$ defined on $\dom{\aCS_1}$ by

\[
\cproj \aConf \HH : \p \mapsto
\begin{cases}
q, & \text{if } \aConf(\p) \not\in \aCS_1(\p)
\text{ and there is } q \trans{\ain[k][h]} \aConf(\p) \in \aCM
\text{ or } q \trans {\ain[k][h]} \trans \tau \aConf(\p) \in \aCM
\\
r, & \text{if } \aConf(\p) \not\in \aCS_1(\p)
\text{ and there is } \aConf(\p) \trans{\aout[h][k]} r \in \aCM
\text{ or } \aConf(\p) \trans \tau \trans{\aout[h][k]} r \in \aCM
\\
\aConf(\p), & \text{otherwise } %\aConf(\p) \in \aCS_1(\p)
\end{cases}
\]

The definition of right-projection $\cproj \aConf \KK$ is analogous.

Left- and right-projections are well-defined.

It is enough to show that $\cproj \cdot \HH$ and $\cproj \cdot
\KK$ uniquely assign a state to fresh states because on non-fresh
stats both functions act as the identify map.

This follows since, by construction, each state introduced by our
gateway construction has unique successor and predecessor.

Intuitively, only $\HH$ is aware of an input from $\KK$ when $\HH$
is in the internal state reached after an input from $\KK$; hence to
have a coherent configuration we take the state of $\HH$ before the

If instead $\HH$ is in an internal state corresponding to an output
to $\KK$, then other participants in $\aCS_1$ know that the message
has been sent; hence to have a coherent configuration we take the
state of $\HH$ after the send.

(A similar intuition applies to $\cproj \aConf \KK$.)

$\aConf =
and $\aCS = \aCS_1 \connect{\HH}{\KK} \aCS_2$ be the system of

Then, $\aConf \in \RS[\ssem{\aCS}]$, namely
$\aConf$ is reachable in $\aCS$.

In fact

\begin{eqnarray*}
\aConf_0 = (0_{\p}, 0_{\q}, 0_{\HH},0_{\KK},0_{\ptp[C]},0_{\ptp[D]}, 0_{\ptp[E]})
& \trans \tau & (1_{\p}, 0_{\q}, 0_{\HH},0_{\KK},0_{\ptp[C]},0_{\ptp[D]}, 0_{\ptp[E]})
\\
& \trans{\gint[][A][m][H]} & (2_{\p}, 0_{\q}, 2_{\HH},0_{\KK},0_{\ptp[C]},0_{\ptp[D]},0_{\ptp[E]})
\\
& \trans \tau & (2_{\p}, 0_{\q}, 4_{\HH},0_{\KK},0_{\ptp[C]},0_{\ptp[D]},0_{\ptp[E]})
\\
& \trans{\gint[][H][m][K]} & (2_{\p}, 0_{\q}, 1_{\HH},5_{\KK},0_{\ptp[C]},0_{\ptp[D]},0_{\ptp[E]})
\end{eqnarray*}

The projections of $\aConf$ on, respectively, $\aCS_1$ and $\aCS_2$
are $\cproj \aConf \HH = (2_{\p},0_{\q}, 1_{\HH})$ and
$\cproj \aConf \KK = (0_{\KK},0_{\ptp[C]},0_{\ptp[D]},0_{\ptp[E]})$.

§.§ Compatibility

A few simple auxiliary notions are useful.

$\lio = \Set{\ain[][][][m], \aout[][][][m] \sst \msg[m]\in\msgset}$
and define the functions $\mathsf{io} : \lact \to \lio$ and
$\Dual{(\cdot)} : \lio \to \lio$ as follows

\[
\begin{array}[c]{c@{\qquad}c@{\qquad}c}
\mathsf{io}(\ain) = \ain[][][][m]
\mathsf{io}(\aout) = \aout[][][][m]
\qqand
\Dual{\ain[][][][m]} = \aout[][][][m]
\Dual{\aout[][][][m]} = \ain[][][][m]
\end{array}
\]

These functions extend to CFSMs
in the obvious way: given a CFSM  $\aCM = \conf{\sset,q_0,\lact,\tset}$ we define
$\mathsf{io}(\aCM) = \conf{\sset,q_0,\lio,\tset'}$ where
$\tset' = \Set{ q \trans[{}]{\mathsf{io}(\al)} q' \sst q
\trans[{}]{\al} q' \in \aCM, \al\in\lact} \cup \Set{q
\trans[{}]{\tau} q' \sst q \trans[{}]{\tau} q' \in \aCM}$ and
likewise for $\Dual{\aCM}$.

Informally, two CFSMs $\aCM_1$ and $\aCM_2$ are compatible if
each output of $\aCM_1$ has a corresponding input in $\aCM_2$ and vice
versa once the identities of communicating partners are blurred away.

Let  $\aCM$ and $\aCM'$ be two FSAs on $\lio$.

An io-correspondence is a relation $R$ between states of
$\aCM$ and those of $\aCM'$ such that whenever $(q, q') \in R$:

* $q \in \tstates{\aCM}$ if, and only if,
$q' \in \tstates{\aCM'}$ (cf. <ref>)

* if $q \trans{\aout[][][]} r \in \aCM$ then there is
$q' \trans{\ain[][][]} r' \in \aCM'$ such that $(r, r') \in R$

* if $q' \trans{\aout[][][]} r' \in \aCM'$ then there is
$q \trans{\ain[][][]} r \in \aCM$ such that $(r, r') \in R$

* if $q \trans \tau r \in \aCM$ then  $(r, q') \in R$

* if $q' \trans \tau r' \in \aCM'$ then  $(q, r') \in R$

Two CFSMs $\aCM$ and $\aCM'$ are compatible (in symbols
$\aCM \comp \aCM'$) if there is an io-correspondence relating the
initial states of $\mathsf{io}(\aCM_1)$ and $\mathsf{io}(\aCM')$.

The machines $\HH$ and $\KK$ of <ref> are compatible.

For a more complex example, consider the following CFSMs

\[
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\HH$}] (zero) {$0$};
\node[state] (one) [above right of=zero]   {$1$};
\node[state] (two) [right  of=one]   {$2$};
\node[state] (three) [right of=two]   {$3$};
\node[state] (four) [right  of=three]   {$4$};
\node[state] (five) [right  of=four]   {$5$};
\node[state] (six) [below right of=five]   {$6$};
\node[state] (seven) [below right of=zero]   {$7$};
\node[state] (eight) [right  of=seven]   {$8$};
\node[state] (nine) [right of=eight]   {$9$};
\node[state] (ten) [right of=nine]   {$10$};
\node[state] (eleven) [right of=ten]   {$11$};
\path
(zero) edge [bend left] node[above] {$\tau$} (one)
(zero) edge   [bend right] node[below] {$\tau$} (seven)
(one) edge node[above] {$\aout[H][A]$} (two)
(two) edge    node[above] {$\tau$} (three)
(three) edge   node[above] {$\aout[H][C][][y]$} (four)
(four) edge    node[above] {$\tau$} (five) %
(five) edge  [bend left]  node[above] {$\aout[H][B]$} (six)
(seven) edge   node[below] {$\aout[H][B]$} (eight)
(eight) edge  node[below] {$\tau$} (nine)
(nine) edge  node[below] {$\aout[H][C][][x]$} (ten)
(ten) edge  node[below] {$\tau$} (eleven)
(eleven) edge   [bend right] node[below] {$\aout[H][A]$} (six)
\end{tikzpicture}
\qquad\qquad
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\KK$}] (zero) {$0$};
\node[state] (one) [above right of=zero]   {$1$};
\node[state] (two) [right  of=one]   {$2$};
\node[state] (three) [below right of=two]   {$3$};
\node[state] (four) [below right of=zero]   {$4$};
\node[state] (five) [right  of=four]   {$5$};
\path
(zero) edge [bend left] node[above] {$\ain[D][K]$} (one)
(one) edge node[above] {$\ain[D][K][][x]$} (two)
(two) edge  [bend left]  node[above] {$\ain[D][K]$} (three)
(zero) edge   [bend right] node[below] {$\ain[E][K]$} (four)
(four) edge  node[below] {$\ain[E][K][][y]$} (five)
(five) edge  [bend right]  node[below] {$\ain[E][K]$} (three)
(zero) edge node[above] {$\ain[E][K][][z]$} (three)
\end{tikzpicture}
\]

The above $\HH$ and $\KK$ are compatible. Apart for $\tau$ actions preceding them,
$\HH$ can only perform output actions, whereas $\KK$ can only perform input actions.
By disregarding the names of the receivers in the actions of  $\HH$, and of the senders in those of
$\KK$, any output action after its corresponding $\tau$ can find a matching input in $\KK$.
The vice versa does not hold, since none of the possible output actions that can occur
after a $\tau$ from $0$ (i.e. the outputs from $1$ and $7$ in $\HH$) can actually
match  the input action $\ain[E][K][][z]$ from $0$ in $\KK$. Such a possibility is in fact allowed
by our definition of compatibility.

<ref> transfers the notion of compatibility given
in [4] for processes in multiparty sessions.

Also, <ref> differs from the notions of
compatibility in [5] and
in [2, 3] which are defined as
bisimulations and do not involve $\tau$-transitions.

An -local CFSM $\aCM$ is:

?-deterministic if $p \trans{\ain[x][a]} q$ and
$p \trans{\ain[y][a]} r \in \aCM$ implies $q = r$;

!-deterministic if $p \trans{\tau}\, \trans{\aout[a][x]} q$ and
$p  \trans{\tau} \, \trans{\aout[a][y]} r \in \aCM$ implies $q = r$;

* ?!-deterministic if it is both ?-deterministic and

A non-terminal state $q \in \aCM$ is asymmetric sending
(resp. receiving) if all its outgoing transitions have $\tau$
(resp. receiving) labels; $q$ is a asymmetric mixed state if it
is neither asymmetric sending nor receiving.

Machines $\HH$ and $\KK$ in <ref> are, respectively
non !-deterministic and non ?-deterministic. In particular, conditions
(<ref>) and  (<ref>) of  <ref>  fail for, respectively,
state $0$ of $\HH$ and state $0$ of $\KK$.

We require a stronger condition then compatibity for two systems to be

Let $\aCS_1$ and $\aCS_2$ be two systems with disjoint domains.  We
say that $\aCS_1$ and $\aCS_2$ are $(\HH,\KK)$-composable if
$\HH \in \dom{\aCS_1}$ and $\KK \in \dom{\aCS_2}$ are two compatible
?!-deterministic machines with no asymmetric mixed states.

§ COMPOSITION RELATED ISSUES

It is known that under symmetric synchronisation composition spoils
deadlock-freedom; this is shown by the example below, borrowed
from [5].

[Symmetric synchronisation spoils deadlock-freedom preservation]
Take the systems

\[
\aCS_1 = \dboxed{
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={\p}] (zero) {$0$};
\node[state] (one) [below of=zero] {$1$};
\path (zero) edge node[above] {$\aout[A][H][][m]$} (one)
\end{tikzpicture}
\qquad\quad
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\HH$}] (zero) {$0$};
\node[state] (one) [below of=zero] {$1$};
\path
(zero) edge[bend left] node[below] {$\ain[A][H][][m]$} (one)
(zero) edge[bend right] node[below] {$\ain[A][H][][x]$} (one)
\end{tikzpicture}
\qqand
\aCS_2 =
\dboxed{
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\KK$}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path
(zero) edge[bend left] node[below] {$\aout[K][B][][m]$} (one)
(zero) edge[bend right] node[below] {$\aout[K][B][][x]$} (one)
\end{tikzpicture}
\qquad\quad
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\q$}] (zero) {$0$};
\node[state] (one) [below of=zero] {$1$};
\path (zero) edge node[above] {$\ain[K][B][][x]$} (one)
\end{tikzpicture}
\]

Clearly, $\aCS_1$ and $\aCS_2$ are $(\HH,\KK)$-composable and
deadlock-free, yet their composition
$\aCS = \aCS_1 \connect \HH \KK \aCS_2$ has a deadlock. In fact,
when the gateway for $\KK$ receives $\msg$, it tries to
synchronise with participant  on message $\msg$ while  is
waiting only for $\msg[x]$.

For $\aCS_2$ in isolation, this is not a deadlock, since  and
$\KK$ synchronise on $\msg[x]$ under the symmetric semantics.

Notice that the counterexample of <ref> does not apply in an
asynchronous setting.

Indeed, $\aCS_2$ could deadlock due to the fact that $\KK$ could send
$\msg$ without synchronising with $\q$.

Likewise, the counterexample of <ref> does not apply in our
asymmetric setting.

Even if communication is still synchronous, the $\tau$-transitions
introduced to resolve internal choices (i.e., those prefixing outputs)
allow $\aCS_2$ to reach a deadlock configuration by choosing the
$\tau$-transition leading to the output $\aout[k][b]$.

Let $\aCM$ be an $\HH$-local CFSM and
$\KK \in \ptpset \setminus \Set{\HH}$ be a participant not occurring
in $\aCM$.

Function $\nof[]{}$ maps the states of $\gateway \aCM \KK$ to the
states of $\aCM$ as follows:

\begin{align*}
\nof q =
\begin{cases}
p, & \text{if } p \trans \al q \in \gateway \aCM \KK \text{ and } \al \text{ input label with }\KK \not\in \ptpof[\al]
\\
p, & \text{if } p \trans \al p' \trans \tau q \in \gateway \aCM \KK \text{ and } \al \text{ input label with }\KK \in \ptpof[\al]
\\
r, & \text{if } q \trans \al r \in \gateway \aCM \KK \text{ and } \al \text{ output label with }\KK \not\in \ptpof[\al]
\\
r, & \text{if } q \trans \tau q' \trans \al r \in \gateway \aCM \KK \text{ and } \al \text{ output label with }\KK \in \ptpof[\al]
\\
q,  & \text{if } q \text{ is a state of } \aCM
\end{cases}
\end{align*}

Note that the first four clause imply that $q$ is a fresh state
of $\gateway \aCM \KK$.

Function $\nof[]{}$ is well-defined.

Let $\aCM$ be an $\HH$-local CFSM and
$\KK \in \ptpset \setminus \Set{\HH}$.

We have to check only internal states as the restriction of $\nof[]{}$
to the states of $\aCM$ is the identity by definition.

If $q$ is an internal state of $\gateway \aCM \KK$, by definition of
$\gateway \aCM \KK$, there is a unique $q'$ such that either
$q' \trans{\ain[A][H][][m]} q \in \gateway \aCM \KK$ or
$q \trans{\aout[H][A][][m]} q' \in \gateway \aCM \KK$.

For $\aCS_1 \connect{\HH}{\KK} \aCS_2$ of <ref>,
$\nof[\HH,\KK][\aCS_1(\HH)] 0 = 0$ and
$\nof[\KK,\HH][{\aCS_2(\KK)}] 2 = 0$.

Function $\nof[]{}$ is similar to configuration projection when
considering CFSMs in isolation, with a main difference: when e.g.,
$\gateway \aCM \KK$ in state $q$ receives from a partner in its own
system going to some fresh state $p'$ with a $\tau$-transition to
$p''$, $\nof[]{}$ maps both $p'$ and $p''$ to $p$ (unlike configuration
projection $\cproj \_ \HH$ which maps $q$ to the successor of $p''$).

This represents the fact that the other system, and $\KK$ in
particular, are oblivious of the transition.

In fact, function $\nof[]{}$ is designed to establish a correspondence
with the other system as shown by the next proposition.

Let $\aCS = \aCS_1 \connect \HH \KK \aCS_2$ be the composition of
two $(\HH,\KK)$-composable systems $\aCS_1$ and $\aCS_2$.

If $\aConf \in \RS[\ssem{\aCS}]$ then
$\cproj \aConf \HH \in \RS[\ssem{\aCS_1}]$,
$\cproj \aConf \KK \in \RS[\ssem{\aCS_2}]$, and
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} \comp
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}$.

Let $\aConf_0$ be the initial configuration of $\aCS$ and

\begin{align}\label{eq:run}
\aConf_0 \trans{\al_1} \aConf_1 \cdots \aConf_{n-1} \trans{\al_n} \aConf_n = \aConf
\end{align}

a run reaching $\aConf$ from $\aConf_0$.

We proceed by induction on $n$.

If $n = 0$ the thesis is immediate by observing that

* $\cproj \aConf \HH \in \RS[\ssem{\aCS_1}]$ and
$\cproj \aConf \KK \in \RS[\ssem{\aCS_2}]$ because left- and
right-projections are the initial configurations of $\aCS_1$ and
$\aCS_2$ respectively, and

* $\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)}$ and
$\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}$ are the initial states
of $\aCS_1(\HH)$ and $\aCS_2(\KK)$ respectively which are
compatible by hypothesis.

Let $n > 0$ and assume that the statement holds for all
configurations reachable from $\aConf_0$ in less the $n$

We have that either none of $\HH$ and $\KK$ are involved in
$\al_n$ or that at least one of them is.

In the former case, without loss of generality, assume that the
interacting participants, say  and   are both in $\aCS_1$.

Then, by construction (cf. <ref>),
$\cproj \aConf \KK = \cproj{\aConf_{n-1}} \KK$ and by inductive
hypothesis $\cproj{\aConf_{n-1}} \KK \in \RS[\ssem{\aCS_2}]$.

Moreover, $\cproj \aConf \HH$ equals $\cproj{\aConf_{n-1}} \HH$ but
for the local states of  and ; hence
$\cproj{\aConf_{n-1}} \HH \in \RS[\ssem{\aCS_1}]$ by the semantics
of communicating systems (cf. <ref>).

\[
\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)}=
(\cproj \aConf \HH)(\HH) = (\cproj{\aConf_{n-1}} \HH)(\HH) \comp
(\cproj{\aConf_{n-1}} \KK)(\KK) =(\cproj \aConf \KK)(\KK)
= \nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}
\]

because the equalities above hold by the definition of asymmetric
synchronisation (cf. <ref>) and the compatibility
relation holds by the inductive hypothesis.

So, let us assume that at least one between $\HH$ and $\KK$ is
involved in the last transition reaching $\aConf$ and proceed by
case analysis on $\al_n$.

$\al_n = \tau$ We consider only the case where $\HH$ is involved since
the case where $\KK$ is involved is symmetric.

By our gateway construction (cf. <ref>) only one of
the following two cases are possible for the transitions in
$\gateway{\aCS_1(\HH)} \KK$:

\begin{align}
\label{eq:fromK}
p \trans{\ain[K][H]} \aConf_{n-1}(\HH) \trans{\tau} q \trans{\aout[H][A]} r
\\
\label{eq:fromA}
q \trans{\ain[A][H]} \aConf_{n-1}(\HH)  \trans{\tau} p \trans{\aout[H][K]} r
\end{align}

for some participant  of $\aCS_1$ and states $p$, $q$, $r$ of
$\gateway{\aCS_1(\HH)} \KK$.

Cases (<ref>) and (<ref>)
respectively correspond to have the transitions

\[
p \trans{\tau} q \trans{\aout[H][A]} r
\qquad\qand\qquad
q \trans{\ain[A][H]} r
\]

in the machine $\aCS_1(\HH)$.

In case (<ref>) the last transition in the
run (<ref>) must therefore be preceded by a transition, say
the $i$-th one, where the machines $\gateway{\aCS_1(\HH)} \KK$ and
$\gateway{\aCS_2(\KK)} \HH$ have exchanged message $\msg$.

Hence, we have that $\gateway{\aCS_2(\KK)} \HH$ has a transition
$\aConf_i(\KK) \trans{\aout[k][h]} \aConf_{i+1}(\KK)$ with
$\aConf_{n-1}(\HH) \comp \aConf_{i+1}(\KK)$ since (by inductive
$\aConf_i(\HH) = p = \nof[\HH,\KK][\aCS_1(\HH)]{\aConf_i(\HH)}
\comp \nof[\KK,\HH][\aCS_2(\KK)]{\aConf_i(\KK)}$ and both gateways
are $?!$-deterministic.

We now observe that either $\aConf(\KK) = \aConf_{i+1}(\KK)$ or
it is a fresh state that $\gateway{\aCS_2(\KK)} \HH$ reaches after
having received a message from a participant of $\aCS_2$ (possibly
followed by a $\tau$ transition) between the $i$-th and the last
interactions in (<ref>).

We have that
$\cproj \aConf \HH = \upd{\cproj {\aConf_{n-1}} \HH}{\HH}{p}$,
hence $\cproj \aConf \HH \in \RS[\ssem{\aCS_1}]$ by inductive
hypothesis; also, $\cproj \aConf \KK \in \RS[\ssem{\aCS_2}]$ by
the inductive hypothesis since
$\cproj \aConf \KK = \cproj {\aConf_{n-1}} \KK$ because $\KK$ is
not involved in $\al_n$.

Finally, in both cases the last part of the thesis immediately
follows by observing that
$\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)} =
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf_i(\KK)}$ by definition and
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} = p$.

In case (<ref>), firstly note that by construction
$\p \neq \HH$ (cf. <ref>).

Then $\gateway{\aCS_1(\HH)} \KK$ has the transition
$\aConf_{n-1}(\HH) \trans{\ain[a][h]} \aConf(\HH)$ which
corresponds to an input transition
$\aConf_{n-1}(\HH) \trans{\ain[a][h]} r$ where
$r = \cproj \aConf \HH (\HH) =
\nof[\HH,\KK][\aCS_1(\HH)]{\aConf_{n-1}(\HH)} =
\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)}$ in $\aCS_1(\HH)$.

Hence, the thesis follows since
$\cproj \aConf \KK = \cproj {\aConf_{n-1}} \KK$ because $\KK$ is
not involved in $\al_n$ and
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} \comp
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)} =
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf_{n-1}(\KK)}$ by inductive

$\al_n = \gint[][h][m][x]$ By construction, either
$\p[x] = \KK$ or $\p[x] \neq \HH$ is a participant of $\aCS_1$.

In the former case, $\gateway{\aCS_1(\HH)} \KK$ has the transition
$\aConf_{n-1}(\HH) \trans{\aout[h][k]} \aConf(\HH)$ which
corresponds to an input transition while $\gateway{\aCS_2(\KK)}
\HH$ has the transition
$\aConf_{n-1}(\KK) \trans{\ain[h][k]} \aConf(\KK)$ which
corresponds to a sequence of transitions
$p \trans \tau \trans{\aout[k][b]} \aConf(\KK)$ in $\aCS_2(\KK)$
for some participant $\q \neq \KK$ in $\aCS_2$.

Then the thesis follows by the fact that
$\cproj \aConf \HH = \upd{\cproj {\aConf_{n-1}} \HH} \HH
{\aConf(\HH)}$ and
$\cproj \aConf \KK = \upd{\cproj {\aConf_{n-1}} \KK} \KK p$ by
construction (cf. <ref>) and that, by inductive
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf_{n-1}(\HH)} = q \comp
\aConf(\KK) = \nof[\KK,\HH][\aCS_2(\KK)]{\aConf_{n-1}(\KK)}$ and
therefore, by ?!-determinism and the compatibility relation
$\aConf(\HH) \comp \aConf(\KK)$.

Suppose now that $\p[x]$ is a participant of $\aCS_1$; note that
by construction $\p[x] \neq \HH$ (cf. <ref>).

Since $\cproj \aConf \KK = \cproj {\aConf_{n-1}} \KK$, the inductive
hypothesis immediately entails that $\cproj \aConf \KK \in \RS[\ssem{\aCS_2}]$.

We first show the reachability of left- and right-projections.

The  transition
$\aConf_{n-1}(\HH) \trans{\aout[h][x]} \aConf(\HH)$ is in
$\gateway{\aCS_1(\HH)} \KK$ by construction and it corresponds to
a pair of transitions
$p \trans \tau \aConf_{n-1}(\HH) \trans{\aout[h][x]} \aConf(\HH)$
in $\aCS_1(\HH)$.

We have that $\cproj {\aConf_{n-1}} \HH \in \RS[\ssem{\aCS_1}]$
(by inductive hypothesis) and since
$\cproj {\aConf_{n-1}} \HH(\HH) = p$ (by <ref>) we have
$\cproj {\aConf_{n-1}} \HH \trans \tau \trans{\gint[][h][m][x]} \cproj \aConf \HH$ (by <ref>).

We now show the compatibility condition.

The last transition in the run (<ref>) must be preceded by
a transition, say the $i$-th one, where the machines
$\gateway{\aCS_1(\HH)} \KK$ and $\gateway{\aCS_2(\KK)} \HH$ have
exchanged message $\msg$.

Hence, we have that $\gateway{\aCS_2(\KK)} \HH$ has a transition
$\aConf_i(\KK) \trans{\aout[k][h]} \aConf_{i+1}(\KK)$ with

\begin{align}\label{eq:nof}
\nof[\HH,\KK][\aCS_1(\HH)]{\aConf_{n-1}(\HH)}  = \aConf(\HH)
= \nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)}
\end{align}

which hold by definition of $\nof[{}][{}]{\_}$.

We now observe that either $\aConf(\KK) = \aConf_{i+1}(\KK)$ or
it is a fresh state that $\gateway{\aCS_2(\KK)} \HH$ reaches after
having received a message from a participant of $\aCS_2$ (possibly
followed by a $\tau$ transition) between the $i$-th and the last
interactions in (<ref>).

In both cases the
$\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)} =
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf_{n-1}(\KK)}$ and, by inductive

\[
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf_{n-1}(\KK)} \comp
\nof[\HH,\KK][\aCS_1(\HH)]{\aConf_{n-1}(\HH)}
\]

hence, by equalities (<ref>),
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} \comp
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)} $.

$\al_n = \gint[][x][m][h]$ The case $\p[x] = \KK$ is
symmetric to the previous case with $\al_n = \gint[][h][m][k]$ and
therefore omitted.

So, assume that $\p[x]$ is a participant of $\aCS_1$; note that by
construction $\p[x] \neq \HH$ (cf. <ref>).

Then $\gateway{\aCS_1(\HH)} \KK$ has the transition
$\aConf_{n-1}(\HH) \trans{\ain[x][h]} \aConf(\HH)$ which
corresponds to an input transition
$\aConf_{n-1}(\HH) \trans{\ain[x][h]} r$.

We have that $\cproj {\aConf_{n-1}} \HH \in RS[\ssem{\aCS_1}]$ by
inductive hypothesis, and so is
$\cproj {\aConf_{n-1}} \HH \trans{\gint[][x][m][h]} \cproj \aConf
\HH$ since, by definition of left-projection,
$\cproj \aConf \HH(\HH) = r$.

The reachability of the right-projection of $\aConf$ immediately
follows by inductive hypothesis, since
$\cproj \aConf \KK = \cproj {\aConf_{n-1}} \KK$.

We now show the compatibility condition.

By definition, we have that
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} =
\nof[\HH,\KK][\aCS_1(\HH)]{\aConf_{n-1}(\HH)}$.

Moreover, we necessarily have that $\aConf(\KK)=
\aConf_{n-1}(\KK)$.

Hence by inductive hypothesis,

$$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} = \nof[\HH,\KK][\aCS_1(\HH)]{\aConf_{n-1}(\HH)} \comp
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf_{n-1}(\KK)}= \nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}$$

The cases $\al_n = \gint[][x][m][k]$ and $\al_n = \gint[][k][m][x]$
are similar to the last two cases above.

Now, one may think that analogously to what happens
in [2, 3], if two systems are
$(\HH,\KK)$-composable and deadlock-free then their composition is
deadlock-free too.

In <ref> we shall prove that in our setting lock-freedom is
preserved by composition, without any further condition beside

Before doing that, we give examples showing the necessity of our conditions for
deadlock freedom preservation.

Let us begin with compatibility.

Properties cannot be preserved under composition without
compatibility, as shown in the next example.
[Lack of compatibility spoils deadlock freedom preservation]
The systems

\[
\aCS_1 =\dboxed{
\begin{array}{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\p$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[H][A][][x]$} (one)
\end{tikzpicture}
\\
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\HH$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\path
(zero) edge node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[H][A][][x]$} (two)
\end{tikzpicture}
\end{array}
\qquad\text{and}\qquad
\aCS_2 =\dboxed{
\begin{array}[c]{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\KK$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[C][K][][y]$} (one)
\end{tikzpicture}
\\
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\ptp[C]$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\path
(zero) edge node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[C][K][][y]$} (two)
\end{tikzpicture}
\end{array}
\]

are trivially deadlock free.

However, $\HH$ and $\KK$ are not compatible, since there is no
corresponding input in $\KK$ for the output from $\HH$.

The composition of $\aCS_1$ and $\aCS_2$  via $\HH$ and $\KK$ yields

\[
\csys[c@{\hspace{1cm}}c]{
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\p$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\path(zero) edge node[above] {$\ain[H][A][][x]$} (one)
\end{tikzpicture}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\gateway {\aCS_2(\KK)} \HH$}] (zero) {$0$};
\node[state] (two) [right of=zero]   {$2$};
\node[state] (three) [right of=two]   {$3$};
\node[state] (one) [right of=three]   {$1$};
\path
(zero) edge node[above] {$\ain[C][K][][y]$} (two)
(two) edge node[above] {$\tau$} (three)
(three) edge node[above] {$\aout[K][H][][y]$} (one)
\end{tikzpicture}
\\[1em]
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\gateway {\aCS_1(\HH)} \KK$}] (zero) {$0$};
\node[state] (three) [right of=zero]   {$3$};
\node[state] (one) [right of=three]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\path
(zero) edge node[above] {$\ain[K][H][][x]$} (three)
(three) edge node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[H][A][][x]$} (two)
\end{tikzpicture}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\ptp[C]$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\path
(zero) edge node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[C][K][][y]$} (two)
\end{tikzpicture}
\]

Starting from the initial configuration of
$\aCS_1 \connect \HH \KK \aCS_2$, the following transitions are
possible in $\ssem{\aCS_1 \connect \HH \KK \aCS_2}$

\[
\trans{\tau} (0_{\p},0_{\HH},0_{\KK},1_{\ptp[C]})
\trans{\gint[][C][y][K]} (0_{\p},0_{\HH},2_{\KK},2_{\ptp[C]})
\trans{\tau} (0_{\p},0_{\HH},3_{\KK},2_{\ptp[C]}) \not\trans{}
\]

where $(0_{\p},0_{\HH},3_{\KK},2_{\ptp[C]})$ is a deadlock
configuration for $\ssem{\aCS_1 \connect \HH \KK \aCS_2}$ since
$\KK$ wishes to send $\msg[y]$ to $\HH$, which is instead waiting
for message $\msg[x]$.

The following example, casting in our setting an example given
in [3] for the asynchronous semantics, illustrates
that asymmetric mixed states must be avoided to preserve properties
under composition.

[Asymmetric mixed-states spoil deadlock freedom preservation]

Let $\aCS_1$ and $\aCS_2$ be

\aCS_1 =\dboxed{
\begin{array}{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\p$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[H][A][][x]$} (one)
\end{tikzpicture}
\\
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\q$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\path
(zero) edge node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[B][H][][y]$} (two)
\end{tikzpicture}
\\
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\HH$}] (zero) {$0$};
\node[state] (one) [above right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\node[state] (three) [below right of=two]   {$3$};
\node[state] (four) [below right of=zero]   {$4$};
\node[state] (five) [right of=four]   {$5$};
\path
(zero) edge [bend left] node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[H][A][][x]$} (two)
(zero) edge [bend right] node[below] {$\ain[B][H][][y]$} (four)
(two) edge [bend left]   node[above] {$\ain[B][H][][y]$} (three)
(four) edge  node[below] {$\tau$} (five)
(five) edge [bend right]  node[below] {$\aout[H][A][][x]$} (three)
\end{tikzpicture}
\end{array}
\qquad
\aCS_2 =\dboxed{
\begin{array}[c]{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\ptp[C]$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[K][C][][y]$} (one)
\end{tikzpicture}
\\
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\ptp[D]$}] (zero) {$0$};
\node[state] (one) [right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\path
(zero) edge node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[K][D][][x]$} (two)
\end{tikzpicture}
\\
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\KK$}] (zero) {$0$};
\node[state] (one) [above right of=zero]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\node[state] (three) [below right of=two]   {$3$};
\node[state] (four) [below right of=zero]   {$4$};
\node[state] (five) [right of=four]   {$5$};
\path
(zero) edge [bend left] node[above] {$\ain[D][K][][x]$} (one)
(one) edge node[above] {$\tau$} (two)
(zero) edge [bend right] node[below] {$\tau$} (four)
(two) edge [bend left]   node[above] {$\aout[K][C][][y]$} (three)
(four) edge  node[below] {$\aout[K][C][][y]$} (five)
(five) edge [bend right]  node[below] {$\ain[D][K][][x]$} (three)
\end{tikzpicture}
\end{array}

Noticeably, the initial states are asymmetric mixed and $\HH$
and $\KK$ are compatible.

The gateways are

\begin{align*}
\begin{tikzpicture}[mycfsm, node distance = 1.2cm]
\node[state, initial, initial where = right, initial distance = .4cm, initial text={$\gateway {\aCS_1(\HH)} \KK$}] (zero) {$0$};
\node[state] (six) [above right of=zero]   {$6$};
\node[state] (nine) [below right of=zero]   {$9$};
\node[state] (ten) [right of=nine]   {$10$};
\node[state] (one) [right of=six]   {$1$};
\node[state] (two) [right of=one]   {$2$};
\node[state] (seven) [right of=two]   {$7$};
\node[state] (eight) [right of=seven]   {$8$};
\node[state] (three) [below right of=eight]   {$3$};
\node[state] (four) [right of=ten]   {$4$};
\node[state] (eleven) [right of=four]   {$11$};
\node[state] (five) [right of=eleven]   {$5$};
\path
(zero) edge [bend left] node[above] {$\ain[K][H][][x]$} (six)
(one) edge node[above] {$\aout[H][A][][x]$} (two)
(zero) edge [bend right] node[below] {$\ain[B][H][][y]$} (nine)
(two) edge   node[above] {$\ain[B][H][][y]$} (seven)
(eleven) edge  node[below] {$\tau$} (five)
(four) edge  node[below] {$\ain[K][H][][x]$} (eleven)
(five) edge [bend right]  node[below] {$\aout[H][A][][x]$} (three)
(six) edge   node[above] {$\tau$} (one)
(seven) edge   node[above] {$\tau$} (eight)
(nine) edge   node[below] {$\tau$} (ten)
(eight) edge [bend left]  node[above] {$\aout[H][K][][y]$} (three)
(ten) edge  node[below] {$\aout[H][K][][y]$} (four)
\end{tikzpicture}
\qquad
\begin{tikzpicture}[mycfsm, node distance = 1.2cm]
\node[state, initial, initial where = right, initial distance = .4cm, initial text={$\gateway {\aCS_2(\KK)} \HH$}] (zero) {$0$};
\node[state] (six) [above right of=zero]   {$6$};
\node[state] (nine) [below right of=zero]   {$9$};
\node[state] (seven) [right of=six]   {$7$};
\node[state] (one) [ right of=seven]   {$1$};
\node[state] (eight) [right of=one]   {$8$};
\node[state] (two) [right of=eight]   {$2$};
\node[state] (three) [below right of=two]   {$3$};
\node[state] (four) [ right of=nine]   {$4$};
\node[state] (five) [right of=four]   {$5$};
\node[state] (ten) [right of=five]   {$10$};
\node[state] (eleven) [right of=ten]   {$11$};
\path
(zero) edge [bend left] node[above] {$\ain[D][K][][x]$} (six)
(zero) edge [bend right] node[below] {$\ain[H][K][][y]$} (nine)
(six) edge node[above] {$\tau$} (seven)
(seven) edge node[above] {$\aout[K][H][][x]$} (one)
(one) edge node[above] {$\ain[H][K][][y]$} (eight)
(eight) edge node[above] {$\tau$} (two)
(nine) edge  node[below] {$\tau$} (four)
(two) edge [bend left]   node[above] {$\aout[K][C][][y]$} (three)
(four) edge  node[below] {$\aout[K][C][][y]$} (five)
(five) edge  node[below] {$\ain[D][K][][x]$} (ten)
(ten) edge node[above] {$\tau$} (eleven)
(eleven) edge [bend right] node[below] {$\aout[K][H][][x]$} (three)
\end{tikzpicture}
\end{align*}

The composed system $\aCS_1 \connect \HH \KK \aCS_2$ deadlocks when
$\gateway {\aCS_1(\HH)} \KK$ receives from  while
$\gateway {\aCS_2(\KK)} \HH$ receives from [d] since both gateways
reach an output state (respectively states $10$ and $7$).

The following example shows that
!?-nondeterminism is problematic too.

Consider the two deadlock-free systems

\begin{align*}
\aCS_1 =
<EMAIL_ADDRESS>\begin{array}[c]{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = above, initial distance = .4cm, initial text={\p}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[H][A][][m]$} (one)
\end{tikzpicture}
\qquad
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = above, initial distance = .4cm, initial text={\q}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[H][B][][m]$} (one)
\end{tikzpicture}
\\[4em]
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = above, initial distance = .4cm, initial text={$\ptp[c]$}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path
(zero) edge   [bend right] node[below] {$\ain[H][C][][x]$} (one)
(zero) edge   [bend left] node[below] {$\ain[H][C][][y]$} (one)
\end{tikzpicture}
\end{array}
\begin{tikzpicture}[mycfsm, node distance = 1.2cm]
\node[state, initial, initial where = below, initial distance = .4cm, initial text={$\HH$}] (zero) {$0$};
\node[state] (one) [below right of=zero]   {$1$};
\node[state] (two) [below  of=one]   {$2$};
\node[state] (three) [below of=two]   {$3$};
\node[state] (four) [below  of=three]   {$4$};
\node[state] (five) [below  of=four]   {$5$};
\node[state] (six) [below left of=five]   {$6$};
\node[state] (seven) [below left of=zero]   {$7$};
\node[state] (eight) [below  of=seven]   {$8$};
\node[state] (nine) [below of=eight]   {$9$};
\node[state] (ten) [below of=nine]   {$10$};
\node[state] (eleven) [below of=ten]   {$11$};
\path
(zero) edge [bend left] node[above] {$\tau$} (one)
(zero) edge   [bend right] node[above] {$\tau$} (seven)
(one) edge node[below] {$\aout[H][A][][m]$} (two)
(two) edge    node[below] {$\tau$} (three)
(three) edge   node[below] {$\aout[H][C][][y]$} (four)
(four) edge    node[below] {$\tau$} (five)
(five) edge  [bend left]  node[below] {$\aout[H][B][][m]$} (six)
(seven) edge   node[below] {$\aout[H][B][][m]$} (eight)
(eight) edge  node[below] {$\tau$} (nine)
(nine) edge  node[below] {$\aout[H][C][][x]$} (ten)
(ten) edge  node[below] {$\tau$} (eleven)
(eleven) edge   [bend right] node[below] {$\aout[H][A][][m]$} (six)
\end{tikzpicture}
\qqand
\aCS_2 =
<EMAIL_ADDRESS>\begin{array}[c]{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = above, initial distance = .4cm, initial text={$\KK$}] (zero) {$0$};
\node[state] (one) [below right of=zero]   {$1$};
\node[state] (two) [below  of=one]   {$2$};
\node[state] (three) [below left of=two]   {$3$};
\node[state] (four) [below left of=zero]   {$4$};
\node[state] (five) [below  of=four]   {$5$};
\path
(zero) edge [bend left] node[above] {$\ain[D][K][][m]$} (one)
(one) edge node[below] {$\ain[D][K][][x]$} (two)
(two) edge  [bend left]  node[below] {$\ain[D][K][][m]$} (three)
(zero) edge   [bend right] node[above] {$\ain[E][K][][m]$} (four)
(four) edge  node[below] {$\ain[E][K][][y]$} (five)
(five) edge  [bend right]  node[below] {$\ain[E][K][][m]$} (three)
(zero) edge node[above] {$\ain[E][K][][z]$} (three)
\end{tikzpicture}
\\[8em]
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\ptp[E]$}] (zero) {$0$};
\end{tikzpicture}
\end{array}
\begin{tikzpicture}[mycfsm, node distance = 1cm]
\node[state, initial, initial where = right, initial distance = .4cm, initial text={$\ptp[D]$}] (zero) {$0$};
\node[state] (one) [below  of=zero]   {$1$};
\node[state] (two) [below  of=one]   {$2$};
\node[state] (three) [below  of=two]   {$3$};
\node[state] (four) [below  of=three]   {$4$};
\node[state] (five) [below  of=four]   {$5$};
\node[state] (six) [below  of=five]   {$6$};
\path
(zero) edge node[above] {$\tau$} (one)
(one) edge node[below] {$\aout[D][K][][m]$} (two)
(two) edge  node[above] {$\tau$} (three)
(three) edge    node[below] {$\aout[D][K][][x]$} (four)
(four) edge    node[above] {$\tau$} (five)
(five) edge  node[below] {$\aout[D][K][][m]$} (six)
\end{tikzpicture}
\end{align*}

The deadlock freedom of $\aCS_1$ follows from the fact that, from
its initial configuration $(0_{\p}, 0_{\q}, 0_{\ptp[C]}, 0_{\HH})$,
$\aCS_1$ can only branch over the two $\tau$-transitions of $\HH$
reaching either of the following configurations
$(0_{\p}, 0_{\q}, 0_{\ptp[C]}, 7_{\HH})$ or
$(0_{\p}, 0_{\q}, 0_{\ptp[C]}, 1_{\HH})$.

From the former (resp. latter) configuration $\aCS_1$ can only reach
configurations where $\HH$ synchronises with $\ptp[c]$ and then with
(resp. ).

In either case $\aCS_1$ reaches the terminal configuration
$(1_{\ptp[A]}, 1_{\ptp[B]}, 1_{\ptp[C]}, 6_{\ptp[H]})$.

Let us take a look at $\aCS_2$.

The only possible transitions of $\aCS_2$ can
involve $\KK$ and $\ptp[d]$ only since $\ptp[e]$ cannot synchronise being it

We therefore have that

\begin{align*}
(0_{\ptp[K]}, 0_{\ptp[D]}, 0_{\ptp[E]})
\trans \tau
(0_{\ptp[K]}, 1_{\ptp[D]}, 0_{\ptp[E]})
\trans{\gint[][d][m][k]}
(1_{\ptp[K]}, 2_{\ptp[D]}, 0_{\ptp[E]})
\trans \tau
(1_{\ptp[K]}, 3_{\ptp[D]}, 0_{\ptp[E]})
\trans{\gint[][d][x][k]}
(2_{\ptp[K]}, 4_{\ptp[D]}, 0_{\ptp[E]})
\\ &
\trans \tau
(2_{\ptp[K]}, 5_{\ptp[D]}, 0_{\ptp[E]})
\trans{\gint[][d][m][k]}
(3_{\ptp[K]}, 6_{\ptp[D]}, 0_{\ptp[E]})
\end{align*}

is the only possible execution from the initial configuration
$(0_{\ptp[K]}, 0_{\ptp[D]}, 0_{\ptp[E]})$ of $\aCS_2$, leading to
the terminal configuration
$(3_{\ptp[K]}, 6_{\ptp[D]}, 0_{\ptp[E]})$.

The next example shows that the compositions of the systems $\aCS_1$
and $\aCS_2$ in <ref> can deadlock.

[$?!$-determinism is necessary]
The CFSMs $\HH$ and $\KK$ in <ref> are compatible as
seen in <ref>.

Hence, we can build the composed system
$\aCS_1 \connect \HH \KK \aCS_2$ through the gateways

\begin{align*}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\gateway{\aCM_\HH}{\KK}$}] (zero) {$0$};
\node[state] (twelve) [below right of=zero]   {$12$};
\node[state] (thirteen) [above right of=zero]   {$13$};
\node[state] (one) [right of=thirteen]   {$1$};
\node[state] (two) [right  of=one]   {$2$};
\node[state] (fifteen) [right  of=two]   {$15$};
\node[state] (three) [right of=fifteen]   {$3$};
\node[state] (four) [right  of=three]   {$4$};
\node[state] (seventeen) [right  of=four]   {$17$};
\node[state] (five) [right  of=seventeen]   {$5$};
\node[state] (six) [below right of=five]   {$6$};
\node[state] (seven) [right of=twelve]   {$7$};
\node[state] (eight) [right  of=seven]   {$8$};
\node[state] (fourteen) [right  of=eight]   {$14$};
\node[state] (nine) [right of=fourteen]   {$9$};
\node[state] (ten) [right of=nine]   {$10$};
\node[state] (sixteen) [right of=ten]   {$16$};
\node[state] (eleven) [right of=sixteen]   {$11$};
\path
(zero) edge [bend right] node[below] {$\ain[K][H][][m]$} (twelve)
(zero) edge   [bend left] node[above] {$\ain[K][H][][m]$} (thirteen)
(twelve) edge  node[below] {$\tau$} (seven)
(thirteen) edge  node[above] {$\tau$} (one)
(one) edge node[above] {$\aout[H][A][][m]$} (two)
(two) edge    node[above] {$\ain[K][H][][y]$} (fifteen)
(fifteen) edge  node[above] {$\tau$} (three)
(three) edge   node[above] {$\aout[H][C][][y]$} (four)
(four) edge    node[above] {$\ain[K][H][][m]$} (seventeen)
(seventeen) edge    node[above] {$\tau$} (five)
(five) edge  [bend left]  node[above] {$\aout[H][B][][m]$} (six)
(seven) edge   node[below] {$\aout[H][B][][m]$} (eight)
(eight) edge  node[below] {$\ain[K][H][][x]$} (fourteen)
(fourteen) edge  node[below] {$\tau$} (nine)
(nine) edge  node[below] {$\aout[H][C][][x]$} (ten)
(ten) edge  node[below] {$\ain[K][H][][m]$} (sixteen)
(sixteen) edge  node[below] {$\tau$} (eleven)
(eleven) edge   [bend right] node[below] {$\aout[H][A][][m]$} (six)
\end{tikzpicture}
\qqand
\\[1em]
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\gateway{\aCM_\KK}{\HH}$}] (zero) {$0$};
\node[state] (eight) [above right of=zero]   {$8$};
\node[state] (nine) [right  of=eight]   {$9$};
\node[state] (one) [right  of=nine]   {$1$};
\node[state] (fourteen) [right  of=one]   {$14$};
\node[state] (fifteen) [right  of=fourteen]   {$15$};
\node[state] (two) [right  of=fifteen]   {$2$};
\node[state] (sixteen) [right  of=two]   {$16$};
\node[state] (seventeen) [right  of=sixteen]   {$17$};
\node[state] (six) [below right of=zero]   {$6$};
\node[state] (seven) [right  of=six]   {$7$};
\node[state] (four) [right  of=seven]   {$4$};
\node[state] (ten) [right  of=four]   {$10$};
\node[state] (eleven) [right  of=ten]   {$11$};
\node[state] (five) [right  of=eleven]   {$5$};
\node[state] (twelve) [right  of=five]   {$12$};
\node[state] (thirteen) [right  of=twelve]   {$13$};
\node[state] (three) [above right of=thirteen]   {$3$};
\node[state] (18) [right of=zero,xshift=3cm]   {$18$};
\node[state] (19) [right of=18]   {$19$};
\path
(zero) edge [bend left] node[above] {$\ain[D][K][][m]$} (eight)
(nine) edge node[above] {$\aout[K][H][][m]$} (one)
(seventeen) edge  [bend left]  node[above] {$\aout[K][H][][m]$} (three)
(zero) edge   [bend right] node[below] {$\ain[E][K][][m]$} (six)
(seven) edge  node[below] {$\aout[K][H][][m]$} (four)
(five) edge   node[above] {$\ain[E][K][][m]$} (twelve)
(four) edge  node[below] {$\ain[E][K][][y]$} (ten)
(six) edge  node[above] {$\tau$} (seven)
(eight) edge  node[above] {$\tau$} (nine)
(ten) edge  node[below] {$\tau$} (eleven)
(one) edge  node[above] {$\ain[D][K][][x]$} (fourteen)
(twelve) edge  node[below] {$\tau$} (thirteen)
(thirteen) edge  [bend right]  node[below] {$\aout[K][H][][m]$} (three)
(eleven) edge  node[below] {$\aout[K][H][][y]$} (five)
(fourteen) edge  node[above] {$\tau$} (fifteen)
(fifteen) edge  node[above] {$\aout[K][H][][x]$} (two)
(two) edge node[above] {$\ain[D][K][][m]$} (sixteen)
(sixteen) edge  node[above] {$\tau$} (seventeen)
(zero) edge node[above]{$\ain[e][k][][z]$} (18)
(18) edge node[above]{$\tau$} (19)
(19) edge node[above]{$\aout[k][h][][z]$} (three)
\end{tikzpicture}
\end{align*}

Now, from the initial configuration
$\aConf_0 = (0_{\p}, 0_{\q}, 0_{\ptp[c]},
0_{\gateway{\aCM_\HH}{\KK}}, 0_{\gateway{\aCM_\KK}{\HH}},
0_{\ptp[D]}, 0_{\ptp[e]})$ of $\aCS_1 \connect \HH \KK \aCS_2$ we have the following run

\begin{align}
\aConf_0
\trans \tau \nonumber
(0_{\p}, 0_{\q}, 0_{\ptp[c]}, 0_{\gateway{\aCM_\HH}{\KK}}, 0_{\gateway{\aCM_\KK}{\HH}}, 1_{\ptp[D]}, 0_{\ptp[e]})
\\ \nonumber
\trans{\gint[][D][m][K]} \trans \tau &
(0_{\p}, 0_{\q}, 0_{\ptp[c]}, 0_{\gateway{\aCM_\HH}{\KK}}, 9_{\gateway{\aCM_\KK}{\HH}}, 2_{\ptp[D]}, 0_{\ptp[e]})
\\\label{eq:gatewaysmove}
\trans{\gint[][k][m][h]} \trans \tau &
(0_{\p}, 0_{\q}, 0_{\ptp[c]}, 13_{\gateway{\aCM_\HH}{\KK}}, 1_{\gateway{\aCM_\KK}{\HH}}, 3_{\ptp[D]}, 0_{\ptp[e]})
\\\nonumber
\trans{\gint[][d][x][k]} &
(0_{\p}, 0_{\q}, 0_{\ptp[c]}, 13_{\gateway{\aCM_\HH}{\KK}}, 14_{\gateway{\aCM_\KK}{\HH}}, 4_{\ptp[D]}, 0_{\ptp[e]})
\\\nonumber
\trans \tau \trans \tau \trans \tau &
(0_{\p}, 0_{\q}, 0_{\ptp[c]}, 1_{\gateway{\aCM_\HH}{\KK}}, 15_{\gateway{\aCM_\KK}{\HH}}, 5_{\ptp[D]}, 0_{\ptp[e]})
\\\label{eq:dl}
\trans{\gint[][h][m][a]} &
(1_{\p}, 0_{\q}, 0_{\ptp[c]}, 2_{\gateway{\aCM_\HH}{\KK}}, 15_{\gateway{\aCM_\KK}{\HH}}, 5_{\ptp[D]}, 0_{\ptp[e]})
\end{align}

where the $\tau$-transition of $\ptp[d]$ enables the synchronisation
of $\gateway{\aCM_\KK}{\HH}$ and $\ptp[d]$ with label
$\gint[][D][m][K]$ that leads the gateway in state $9$ after its
$\tau$-transition from state $8$.

Now, the two gateways can communicate and exchange message

Due to $?!$-nondeterminism of $\aCS_1$, from state $0$
$\gateway{\aCM_\HH}{\KK}$ can move either to state $12$ or to state

Fatally, transition (<ref>) leads to a
deadlock: after $\gateway{\aCM_\KK}{\HH}$ and $\ptp[d]$ synchronise
to exchange message $\msg[x]$ the system goes into a configuration
from where $\gateway{\aCM_\HH}{\KK}$ forwards $\msg[m]$ to  and
reaches the last configuration (<ref>).

This is a deadlock for $\aCS_1 \connect \HH \KK \aCS_2$, since no
CFSM can do a $\tau$-transitions, the only enabled output action is
from $\gateway{\aCM_\KK}{\HH}$ which tries to send message $\msg[x]$
to $\gateway{\aCM_\HH}{\KK}$; however, $\gateway{\aCM_\HH}{\KK}$ can
only receive message $\msg[y]$ from $\KK$ and hence these actions
cannot synchronise.

§ PRESERVING PROPERTIES BY COMPOSITION

Composition via gateways does not ensure the preservation of
communication properties.

We provide below sufficient conditions for this to happen.

Recall that $(\HH, \KK)$-composability requires absence of asymmetric
mixed states and ?!-determinism.

[Deadlock freedom preservation]theoremseqgatthm
Let $\aCS_1$ and $\aCS_2$ be two $(\HH,\KK)$-composable and
deadlock-free systems.

Then the composed system $\aCS_1 \connect \HH \KK \aCS_2$ is

Given an $\HH$-local CFSM $\aCM$ and a participant
$\KK \in \pset \setminus \{\HH\}$, call connecting a fresh
asymmetric sending state of $\gateway \aCM \KK$ whose next outgoing
transition does not have $\KK$ as receiver.

We show that if the composed system $\aCS_1 \connect \HH \KK
\aCS_2$ reaches a deadlock configuration $\aConf$ then at least
one of $\cproj \aConf \HH$ and $\cproj \aConf \KK$ is a deadlock.

Without loss of generality, we assume that the deadlock is the
left-projection; the case where the deadlock is the
right-projection is similar.

First, we show that if a participant $\p$ from $\aCS_1$ has an
enabled transition in $\aConf$ then some participant in $\aCS_1$
has a transition enabled in $\cproj \aConf \HH$.

Note that $\cproj \aConf \HH$ is reachable in $\aCS_1$ by

If $\p \neq \HH$ then any transition of $\p$ enabled in $\aConf$
is also enabled in $\cproj \aConf \HH$ since
$\cproj \aConf \HH(\p) = \aConf(\p)$ by <ref>.

If $\p=\HH$, then either of the following cases occurs

* $\HH$ has enabled an input

Assume that the input is from $\KK$.

Then by construction $\cproj \aConf \HH(\HH)$ has a
$\tau$-transition enabled in $\aCS_1(\HH)$.

If the input of $\HH$ is from a participant  of $\aCS_1$ then
by construction $\cproj \aConf \HH(\HH)$ has an input transition
enabled in $\aCS_1(\HH)$.

* $\HH$ has enabled an output.

Assume that the receiver of such output is $\KK$.

$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)} \comp
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}$ by <ref>.

By definition of $\nof[]{}$ and of gateway,
$\nof[\HH,\KK][\aCS_1(\HH)]{\aConf(\HH)}$ has an input
transition enabled from a participant in $\aCS_1$, hence
$\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}$ has a corresponding
output transition enable towards a participant in $\aCS_2$ by

By construction (<ref>),
$\cproj \aConf \KK(\KK) =
\nof[\KK,\HH][\aCS_2(\KK)]{\aConf(\KK)}$, hence there is a
participant, in particular $\KK$, willing to take a transition.

If the receiver of the output from $\HH$ is a participant of
$\aCS_1$ then, by definition of gateway and configuration
projection, we get that in $\HH$ is willing to perform an output
from $\cproj \aConf \HH(\HH)$ in $\aCS_1$.

* $\HH$ can perform a $\tau$-transition.

Then, there is a sequence of transitions of the form
$\aConf(\HH) \trans \tau \trans{\aout[h][x]}$ in $\aCS(\HH)$
with $\p[x] = \KK$ or $\p[x] \neq \HH$ participant of $\aCS_1$.

If the former case we can reason as in the previous case when
$\HH$ outputs to $\KK$.

Otherwise, $\cproj \aConf \HH(\HH)$ has an enabled
$\tau$-transition in $\aCS_1(\HH)$ by <ref>.

If $\aConf$ is a deadlock, by definition of deadlock freedom
(cf. <ref>), $\aConf \not\trans{}$ but there are
participants in $\aCS$ with enabled transitions in $\aConf$.

Under the assumption that $\cproj \aConf \KK$ is deadlock-free,
such participants must belong to $\aCS_1$.

By the cases shown above, $\cproj \aConf \HH$ enables some
participants in $\aCS_1$; therefore, there is
$\cproj \aConf \HH \trans \al$ because $\aCS_1$ is deadlock free
by hypothesis.

It must be that $\HH$ is involved in all transitions from
$\cproj \aConf \HH$ of $\aCS_1$ otherwise $\aConf \trans \al$
since for all $\p[x] \in \ptpof[\al]$
$\aConf(\p[x]) = \cproj \aConf \HH (\p[x])$ (by <ref>)
contrary to our assumption that $\aConf$ is a deadlock.

We proceed by case analysis on $\al$.

$\al = \gint[][h][m][x]$ If $\p[x] \neq \KK$ then
$\cproj \aConf \HH (\p[x]) = \aConf(\p[x]) \trans{\ain[h][a]}$;
also, $\HH$ would be in a connecting state and, by
$\cproj \aConf \HH (\HH) = \aConf(\HH) \trans{\aout[h][a]}$.

Hence $\aConf \trans \al$ contrary to the hypothesis
that $\aConf$ is a deadlock configuration.

If $\p[x] = \KK$ then we have again a contradiction since
$\aConf \trans{\al}$ by <ref>.

$\al = \gint[][x][m][h]$ If $\p[x] \neq \KK$ then
$\cproj \aConf \HH (\p[x]) = \aConf(\p[x]) \trans{\aout[a][h]}$
and $\cproj \aConf \HH (\p[x]) \trans{\ain[a][h]} = \aConf(\HH)$

Hence $\aConf \trans \al$ contrary to the hypothesis that $\aConf$
is a deadlock configuration.

If $\p[x] = \KK$ then we have again a contradiction since
$\aConf \trans{\al}$ by <ref>.

$\al = \tau$ If $\aConf(\HH) = p''$ is fresh then
$\gateway{\aCS_1(\HH)} \KK$ must have a sequence of transitions

\begin{align} \label{eq:toK}
p \trans{\ain[a][h]} p' \trans \tau p'' \trans{\aout[h][k]} r
\end{align}

with $\p$ participant of $\aCS_1$ and $p'$ fresh.

(Note that it cannot be $\aConf(\HH) = p'$ otherwise
$\aConf(\HH) \trans \tau$ contradicting $\aConf \not\trans{}$.)

By <ref>, $\cproj \aConf \HH(\HH) = r$.

Hence, by <ref> we have $s \trans{\gint[][h][m][k]}$
contradicting $\aConf \not\trans{}$.

If $\aConf(\HH)$ is not fresh then $\HH$ has a $\tau$ transition
enabled at $\aConf$ (because $\aConf(\HH) = \cproj \aConf
\HH(\HH)$ by <ref>) again contradicting
$\aConf \not\trans{}$.

The proof relies on the fact that the reachable configurations of
$\aCS_1 \connect \HH \KK \aCS_2$ can be projected on reachable
configurations of $\aCS_1$ and $\aCS_2$.

This implies that a deadlock in $\aCS_1 \connect \HH \KK \aCS_2$
corresponds to a deadlock in $\aCS_1$ or in $\aCS_2$.

See the appendix for the detailed proof.

We can infer deadlock-freedom of the system
$\aCS = \aCS_1 \connect{\HH}{\KK} \aCS_2$ of <ref> by the
result above, since $\aCS_1$ and $\aCS_1$ are $(\HH,\KK)$-composable
and deadlock-free.

Somehow surprisingly, in the symmetric case preservation of deadlock
freedom requires stricter conditions on gateways than in the
asymmetric case.

In fact, in the asymmetric case, deadlock freedom preservation
requires only absence of asymmetric mixed states and $?!$-determinism
while the symmetric case requires the (stronger) condition of

A CFSM is sequential if each of its states has at most one
outgoing transition.

A participant  of a system $\aCS$ is sequential if $\aCS(\p)$ is

As we will see (cf. <ref>), sequentiality is necessary
to preserve lock-freedom also in the asymmetric case.

We note that sequentiality implies absence of asymmetric mixed states
and $?!$-determinism, while the converse does not hold.

As mentioned before, the property of lock freedom is not preserved in
general by composition, as shown by the following example.

[Composability does not preserve lock-freedom]
Take the communicating systems

\begin{align*}
\aCS_1 = \dboxed{
\begin{array}{c}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\p$}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path
(zero) edge[bend left] node[below] {$\tau$} (one)
(one) edge[bend left]  node[above] {$\aout[A][H][][m]$} (zero)
\end{tikzpicture}
\end{array}
\qquad
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\HH$}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path
(zero) edge [loop right,looseness=40] node[above] {$\ain[A][H][][m]$} (zero)
(zero) edge node[above] {$\ain[A][H][][x]$} (one)
\end{tikzpicture}
\qand
\aCS_2 = \dboxed{
\begin{array}{ccc}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\KK$}] (zero) {$0$};
\node[state] (one) [below left of=zero]   {$1$};
\node[state] (two) [below right of=zero]   {$2$};
\node[state] (three) [below  of=two]   {$3$};
\path
(zero)  edge[bend right] node[above, near end] {$\tau$} (one)
(zero) edge[bend left] node[above] {$\tau$} (two)
(two) edge node[above] {$\aout[K][C][][x]$} (three)
(one) edge[bend right] node[below] {$\aout[K][C][][m]$} (zero)
\end{tikzpicture}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\q$}] (zero) {$0$};
\node[state] (one) [below of=zero]   {$1$};
\path (zero) edge node[above] {$\ain[C][b][][stop]$} (one)
\end{tikzpicture}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\p[c]$}] (zero) {$0$};
\node[state] (one) [below right of=zero]   {$1$};
\node[state] (two) [below left of=one]   {$2$};
\node[state] (three) [above left of=two]   {$3$};
\path
(zero) edge[loop below,looseness=40] node[below] {$\ain[K][C][][m]$} (zero)
(zero) edge [bend left] node[above] {$\ain[K][C][][x]$} (one)
(one) edge [bend left]  node[above] {$\tau$} (two)
(two) edge [bend left]  node[below] {$\aout[C][b][][stop]$} (three)
\end{tikzpicture}
\end{array}
\end{align*}

Note that both $\aCS_1$ and $\aCS_2$ are lock-free and that $\HH$
and $\KK$ are compatible.

The gateways are

\begin{align*}
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\gateway {\aCM_\HH} \KK$}] (zero) {$0$};
\node[state] (one) [above right of=zero]   {$1$};
\node[state] (two) [below right of=zero]   {$2$};
\node[state] (three) [right  of=one]   {$3$};
\node[state] (four) [right  of=two]   {$4$};
\node[state] (five) [right  of=three]   {$5$};
\path
(zero) edge[bend right] node[below] {$\ain[A][H][][m]$} (two)
(zero) edge[bend left] node[above] {$\ain[a][H][][x]$} (one)
(one) edge node[above] {$\tau$} (three)
(two) edge node[below] {$\tau$} (four)
(three) edge node[above] {$\aout[H][K][][x]$} (five)
(four) edge[bend right] node[above] {$\aout[H][K][][m]$} (zero)
\end{tikzpicture}
\qqand
\begin{tikzpicture}[mycfsm]
\node[state, initial, initial where = left, initial distance = .4cm, initial text={$\gateway {\aCM_\KK} \HH$}] (zero) {$0$};
\node[state] (five) [below right of=zero]   {$5$};
\node[state] (four) [above right of=zero]   {$4$};
\node[state] (one) [right  of=five]   {$1$};
\node[state] (two) [right of=four]   {$2$};
\node[state] (three) [right  of=two]   {$3$};
\path
(zero)  edge[bend right] node[below] {$\ain[H][K][][m]$} (five)
(zero) edge[bend left] node[above] {$\ain[H][K][][x]$} (four)
(five)  edge node[below] {$\tau$} (one)
(four) edge node[above] {$\tau$} (two)
(two) edge node[above] {$\aout[K][b][][x]$} (three)
(one) edge[bend right] node[below] {$\aout[K][C][][m]$} (zero)
\end{tikzpicture}
\end{align*}

Hence, the composed system $\aCS_1 \connect \HH \KK \aCS_2$ is non
lock-free because e.g. the configuration

\[
\aConf = (0_{\p},0_{\gateway {\aCM_{\HH}}{ \KK}}, 0_{\gateway {\aCM_{\KK}}{ \HH}}, 0_{\q}, 0_{\ptp[c]})
\]

is a lock for $\q$, since the only outgoing transition from $0_{\q}$
could be fired only in case the transition $\aout[c][b][][stop]$ is

However, this is impossible since $\gateway {\aCM_{\HH}}{ \KK}$
forwards only message $\msg[m]$; hence, the run
$\aConf \trans \tau \trans{\gint[][a][m][h]} (0_{\p},2_{\gateway
{\aCM_{\HH}}{\KK}}, 0_{\gateway{\aCM_{\KK}}{\HH}}, 0_{\q},
0_{\ptp[c]}) \trans \tau \trans{\gint[][a][m][h]} \aConf \cdots$
(which does not involve $\q$) is perpetually executed.

We show that the problem of <ref> cannot happen in case
we restrict to sequential gateways, as done for deadlock freedom in
the symmetric case (cf. [5]).

As usual, $\prestrict f X$ denotes the restriction of a function $f$
on a subset $X$ of its domain.

[Lock-freedom preservation]theoremlfpresthm
Let $\aCS_1$ and $\aCS_2$ be two $(\HH,\KK)$-composable and
lock-free systems with $\HH$ and $\KK$ sequential.

Then the composed system $\aCS_1 \connect \HH \KK \aCS_2$ is

Let $\aCS = \aCS_1 \connect \HH \KK \aCS_2$ where $\aCS_1$ and
$\aCS_2$ are two $(\HH,\KK)$-composable systems with $\HH$ and
$\KK$ sequential.

Given $\aConf \in \RS[\ssem \aCS]$, if

(1) either $\cproj{\aConf} \HH \trans \al \aConf'$
in $\aCS_1$ and
$\al = \tau \implies \cproj \aConf \HH(\HH) = \aConf'(\HH)$

(2) or $\cproj \aConf \HH \trans \tau \hat \aConf$
involving $\HH$ in $\aCS_1(\HH)$ and $\hat \aConf$ reaching a
configuration $\hat \aConf'$ such that
$\hat \aConf' \trans \al \aConf'$ in $\aCS_1$ with
$\al = \gint[][h][m][a]$

then there is a run
$\aConf \trans{\al_1} \cdots \trans{\al_n} \hat\aConf$ in $\aCS$
such that $\al_n = \al$ and $\cproj{\hat \aConf} \HH = \aConf'$.

The same holds for the right-projection of $\aCS$.

We give the proof for each case.

Case (1) By case analysis on $\al$ noticing that the case
$\al = \gint[][h][m][a]$ is not possible since $\cproj \aConf \HH$
cannot enable output transitions from $\HH$ by construction
(cf. <ref>).

$\al = \tau$. Then the $\tau$-transition is executed by
$\p \neq \HH$ in $\aCS_1$; hence there is a transition
$\cproj \aConf \HH(\p) \trans \tau q$ in $\aCS_1(\p)$.

Observing that $\aConf(\p) = \cproj \aConf \HH(\p)$ by
<ref> we have the thesis since
$\aConf \trans \tau \upd \aConf \p q$.

$\al = \gint[][a][m][h]$. We have

\[
\cproj \aConf \HH(\HH) \trans{\ain[a][h]} p
\text{ in } \aCS_1(\HH)
\qqand
\cproj \aConf \HH(\p) \trans{\aout[a][h]} q
\text{ in } \aCS_1(\p)
\]

moreover, $\aConf(\HH) = \cproj \aConf \HH(\HH)$ and
$\aConf(\p) = \cproj \aConf \HH(\p)$.

\[
\aConf \trans{\gint[][a][m][h]} \aConf''
\qqand[with]
\aConf''(\p[x]) =
\begin{cases}
p, & \text{if } \p[x] = \HH
\\
q, & \text{if } \p[x] = \p
\\
\aConf(\p[x]), & \text{otherwise}
\end{cases}
\]

by <ref>.

Therefore $\cproj{\aConf''}\HH = \aConf'$.

Case (2) Note that $\aCS_1(\HH)$ necessarily contains the
$\cproj \aConf \HH(\HH) \trans \tau \hat \aConf'(\HH)
\trans{\aout[h][a]} r$.

Then, by construction, in $\gateway{\aCS_1(\HH)}{\KK}$ we have

\begin{align}\label{eq:taus}
\cproj \aConf \HH(\HH) \trans{\ain[k][h]} p \trans \tau \hat \aConf'(\HH) \trans{\aout[h][a]} r
\end{align}

note that $p$ and $\hat \aConf'(\HH)$ are fresh, that these are
the only transitions from $\cproj \aConf \HH(\HH)$ to $r$ by
sequentiality, and that $\aConf(\HH) \in \{\cproj \aConf \HH(\HH),p, \hat \aConf'(\HH)$ by construction
(cf. <ref>).

If $\aConf(\HH) = \cproj \aConf \HH(\HH)$ then, by
<ref>, we have
$\aConf \trans{\gint[][k][m][h]} \trans \tau \aConf''$ with
$\aConf''(\HH) = \hat \aConf'(\HH)$.

$\cproj{\aConf''} \HH = \upd{\cproj \aConf \HH} \HH r$ and therefore
$\aConf'' \trans{\gint[][h][m][a]} \aConf''[\HH \mapsto r, \p \mapsto
\aConf'(\p)] = \aConf'''$ which yields the thesis noticing that
$\cproj{\aConf'''} \HH = \aConf'$.

If $\aConf(\HH) = p$ then $\aConf \trans \tau \aConf''$ with
$\aConf''(\HH) = \hat \aConf'(\HH)$; hence the thesis follows as in
the previous case.

Finally, if $\aConf(\HH) = \hat\aConf'(\HH)$ then
$\aConf \trans{\gint[][h][m][a]} \aConf''$ with
$\aConf'' = \aConf[\HH \mapsto r, \p \mapsto \aConf'(\p)]$ and therefore
$\cproj{\aConf''}\HH = \aConf'$.

By contradiction, let us assume
$\aCS = \aCS_1 \connect \HH \KK \aCS_2$ not to be lock-free.

Then there is a configuration $\aConf \in \RS[\ssem \aCS]$ and a
participant $\p[x]$ not involved in any run from $\aConf$.

Without any loss of generality, we can assume $\p[x] \in \aCS_1$.

We have $\cproj \aConf \HH \in \RS[\ssem{\aCS_1}]$ by
<ref> and, by lock-freedom of $\aCS_1$,
$\cproj \aConf \HH$ cannot be a lock of $\aCS_1$ for $\p[x]$.

Hence, there exists a run
$\cproj \aConf \HH \trans{\al_0} \aConf_0 \cdots \aConf_{n-1} \trans{\al_n}
\aConf_n$ of $\aCS_1$ with $\p[x]$ involved in $\al_n$.

We show that this induces a run from $\aConf$ in $\aCS$ involving
$\p[x]$ by induction on $n$.

* If $n=0$, by <ref> there is a run
$\aConf \trans{\psi} \trans \al \aConf'$ such that
$\cproj{\aConf'} \HH = \aConf_0$ with $\al_0 = \al$.

* If $n>0$, we assume that the statement holds for all runs with
less than $n$ transitions.

If $\p[x]$ is involved in $\al_i$ with $0 \leq i < n$ then
the thesis follows by inductive hypothesis.

Let us therefore assume that $\p[x]$ is involved in $\al_n$ only.

By repeated application of <ref>, there is a
$\aConf \trans{\psi_1 \cdot \al_1'} \aConf_1' \cdots
\trans{\psi_{n-1} \cdot \al_{n-1}'} \aConf_{n-1}' \trans{\psi_n
\cdot \al_n'} \aConf_n'$ in $\aCS$ such that $\al_i' = \al_i$
and $\cproj{\aConf_i'} \HH = \aConf_i$ for each $1 \leq i \leq n$.

In both cases $\aConf$ reaches a configuration with a run
involving [x], which contradicts our assumption.

The proof goes as the one of <ref> noticing that
we have to reconstruct backward the sequence of interactions.
This exploits sequentiality and lock-freedom of $\aCS_1$ and
$\aCS_2$ in order to guarantee the reconstruction when we
cross the two composed systems through the gateways.

We turn now our attention to strong lock-freedom.

In this case, as for deadlock freedom, $(\HH,\KK)$-composability
suffices for preservation by composition; we shall see that this is
not the case for lock freedom preservation.

[Strong lock freedom preservation]theoremslfpresthm
Let $\aCS_1$ and $\aCS_2$ be two $(\HH,\KK)$-composable and strongly
lock free systems.

Then the composed system $\aCS_1 \connect \HH \KK \aCS_2$ is
strongly lock free.

By contradiction, let us assume $\aCS_1 \connect \HH \KK \aCS_2$
not to be strongly lock free.

This means that there are a reachable configuration $\aConf$, a
participant $\p[x]$, and a maximal run $\psi$ of
$\aCS_1 \connect \HH \KK \aCS_2$ such that $\aConf \trans{\psi}$
and [x] is not involved in any of those transitions.

By the first part of the proof of <ref>, there exist
two run $\cproj \aConf \HH \trans{\psi_1}$ and
$\cproj \aConf \KK \trans{\psi_2}$ of $\aCS_1$ and $\aCS_2$
respectively such that [x] is involve neither in $\psi_1$ nor
in $\psi_2$.

* In case $\psi$ is infinite, we get that either $\psi_1$ or
$\psi_2$ is infinite, and hence maximal.

* In case $\psi$ is finite it is possible to use the second
part of the proof of <ref> to show that either
$\psi_1$ or $\psi_2$ is maximal,

In both cases we get a contradiction of the hypothesis that
$\aCS_1$ and $\aCS_2$ are strong lock free.

The proof is similar to the one of <ref> but for
the use of strong lock freedom of $\aCS_1$ and $\aCS_2$ instead of
their deadlock freedom.

§ CONCLUSIONS AND FUTURE WORK

We introduce an asymmetric synchronous semantics of communicating
systems which breaks the symmetry between senders and receivers.

In fact, our semantics decouples communication from choice resolution
as in standard semantics of communicating systems (and other models).

We then adapted the gateway composition mechanism defined
in [2, 3] to our asymmetric semantics and
gave conditions for the preservation of some communication properties
under this notion of composition.

In contract automata [10, 9] transitions express
requests and offers among participants.

The composition mechanism is based on trimming a product of
contract automata according to relevant agreement properties.

This yields controllers that preserve deadlocks.

Contract automata do not consider asymmetric synchronous semantics.

Our composition mechanism does not introduce orchestrators which,
under some conditions, can be avoided also for contract
automata [10, 9].

Modular approaches to the development of concurrent systems can be
exploited even for systems designed using formalisms intrinsically
dealing with closed systems.

Indeed, given two systems, any two components – one per system –
exhibiting compatible behaviours can be replaced by two coupled
forwarders (gateways) connecting the systems, as investigated
initially in [2, 3] for an asynchronous
interaction model.

The investigation on the composition-by-gateways technique was shifted
in [5] towards synchronous symmetric interactions.

We pushed a step forward such an investigation,
by considering asymmetric synchronous interactions.

Interestingly, deadlock freedom preservation in the synchronous
asymmetric case we consider does not require sequentiality of
gateways, like in the asynchronous case, and differently from the
synchronous symmetric case.

Notably, sequentiality is needed here for lock-freedom preservation,
but not for strong-lock freedom preservation.

While the path of investigation above is quite homogeneous, the
different analyses present some methodological differences.

For instance, [5] considers also another form of
composition, where one single gateway (interacting with both the
composed systems) is used.

On the other side, [5] focused only on deadlocks,
disregarding other properties we consider.

A first item of future research consist in filling the bits missing
due to the mismatches above.

A more challenging direction for future work is looking for refined
composition mechanisms in order to get preservation of relevant
properties under weaker conditions.

[1]
authorF. Barbanera &
authorU. de'Liguoro
(year2015): titleSub-behaviour relations for
session-based client/server systems.
volume25(number6), pp. pages1339–1381,

[2]
authorFranco Barbanera,
authorUgo de'Liguoro &
authorRolf Hennicker
(year2018): titleGlobal Types for Open
In editorMassimo Bartoletti &
editorSophia Knight, editors: booktitleICE, seriesEPTCS
volume279, pp. pages4–20, 10.4204/EPTCS.279.4.

[3]
authorFranco Barbanera,
authorUgo de'Liguoro &
authorRolf Hennicker
(year2019): titleConnecting open systems of
communicating finite state machines.
journalJLAMP volume109,

[4]
authorFranco Barbanera,
authorMariangiola Dezani-Ciancaglini,
authorIvan Lanese &
authorEmilio Tuosto
(year2021): titleComposition and decomposition
of multiparty sessions.
journalJLAMP volume119, p.
pages100620, 10.1016/j.jlamp.2020.100620.

[5]
authorFranco Barbanera,
authorIvan Lanese &
authorEmilio Tuosto
(year2020): titleComposing Communicating
Systems, Synchronously.
In editorTiziana Margaria &
editorBernhard Steffen, editors:
booktitleISoLA 2020, seriesLNCS
volume12476, publisherSpringer, pp.
pages39–59, 10.1007/978-3-030-61362-4_3.

[6]
authorFranco Barbanera,
authorIvan Lanese &
authorEmilio Tuosto
(year2022): titleOn Composing Communicating
Systems. Full Version.
noteAvailable at

[7]
authorMassimo Bartoletti,
authorTiziana Cimoli &
authorRoberto Zunino
(year2015): titleCompliance in Behavioural
Contracts: A Brief Survey.
In editorChiara Bodei,
editorGian Luigi Ferrari &
editorCorrado Priami, editors: booktitleProgramming Languages with Applications to Biology and
Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th
Birthday, seriesLecture Notes in Computer Science
volume9465, publisherSpringer, pp.
pages103–121, 10.1007/978-3-319-25527-9_9.

[8]
authorMassimo Bartoletti,
authorAlceste Scalas &
authorRoberto Zunino
(year2014): titleA Semantic Deconstruction of
Session Types.
In editorPaolo Baldan &
editorDaniele Gorla, editors: booktitleCONCUR 2014, seriesLNCS
volume8704, publisherSpringer, pp.
pages402–418, 10.1007/978-3-662-44584-6_28.

[9]
authorDavide Basile,
authorMaurice H. ter Beek &
authorRosario Pugliese
(year2020): titleSynthesis of Orchestrations and
Choreographies: Bridging the Gap between Supervisory Control and Coordination
of Services.
volume16(number2), 10.23638/LMCS-16(2:9)2020.

[10]
authorDavide Basile,
authorPierpaolo Degano,
authorGian Luigi Ferrari &
authorEmilio Tuosto
(year2016): titlePlaying with Our CAT and
Communication-Centric Applications.
In editorElvira Albert &
editorIvan Lanese, editors: booktitleFORTE, seriesLNCS
volume9688, publisherSpringer, pp.
pages62–73, 10.1007/978-3-319-39570-8_5.

[11]
authorG. Bernardi &
authorM. Hennessy
(year2012): titleModelling session types using
In: booktitleProceedings of the 27th Annual ACM
Symposium on Applied Computing, seriesSAC '12,
publisherACM, addressNew York, NY, USA, pp.
pages1941–1946, 10.1145/2231936.2232097.

[12]
authorDaniel Brand &
authorPitro Zafiropulo
(year1983): titleOn Communicating Finite-State
journalJ. ACM
volume30(number2), pp. pages323–342,

[13]
authorGérard Cécé &
authorAlain Finkel
(year2005): titleVerification of programs with
half-duplex communication.
volume202(number2), pp. pages166–190,

[14]
authorK. Honda, authorV. T.
Vasconcelos & authorM. Kubo (year1998): titleLanguage
Primitives and Type Disciplines for Structured Communication-based
In editorChris Hankin, editor:
booktitleESOP, seriesLNCS
volume1381, publisherSpringer, pp.
pages22–138, 10.1007/BFb0053567.

[15]
authorH. Hüttel et al.
(year2016): titleFoundations of Session Types
and Behavioural Contracts.
journalACM Comput. Surv.
volume49(number1), pp. pages3:1–3:36,

[16]
authorJulien Lange,
authorEmilio Tuosto &
authorNobuko Yoshida
(year2015): titleFrom Communicating Machines to
Graphical Choreographies.
In editorSriram K. Rajamani &
editorDavid Walker, editors: booktitlePOPL, publisherACM, pp.
pages221–232, 10.1145/2676726.2676964.

[17]
authorRobin Milner (year1980):
titleA Calculus of Communicating Systems.
seriesLNCS volume92,
publisherSpringer, addressBerlin,

[18]
authorL. Padovani (year2010):
titleContract-Based Discovery of Web Services Modulo Simple
journalTheoretical Computer Science
volume411, pp. pages3328–3347,

[19]
authorEmilio Tuosto &
authorRoberto Guanciale
(year2018): titleSemantics of global view of
journalJLAMP volume95, pp.
pages17–40, 10.1016/j.jlamp.2017.11.002.