Composition of synchronous communicating systems

Franco Barbanera, Ivan Lanese, Emilio Tuosto

► To cite this version:

Franco Barbanera, Ivan Lanese, Emilio Tuosto. Composition of synchronous communicating systems. Journal of Logical and Algebraic Methods in Programming, 2023, 135, pp.100890. 10.1016/j.jlamp.2023.100890. hal-04343521

HAL Id: hal-04343521

https://inria.hal.science/hal-04343521v1

Submitted on 13 Dec 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Composition of Synchronous Communicating Systems*

Franco Barbaneraª, Ivan Laneseᵇ, Emilio Tuostoᶜ,\*

ªDept. of Mathematics and Computer Science, University of Catania, Catania, Italy

ᵇFocus Team, University of Bologna/INRIA, Bologna, Italy

ᶜGran Sasso Science Institute, L'Aquila, Italy

## Abstract

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. Two communicating systems can be composed by selecting one component per system, and transforming both of them into coupled gateways connecting the two systems. More precisely, a gateway forwards a message received from within its system to the other gateway, which then delivers the message to the other system. Suitable compatibility conditions between gateways have been proved sufficient for this composition mechanism to preserve properties such as 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 present paper gives a comprehensive treatment of the case of synchronous communications. We consider both symmetric synchronous communications and asymmetric synchronous communications (where senders decide independently which message should be exchanged). The composition mechanism preserves different properties under different conditions depending on the considered type of synchronous communication. We show here that preservation of lock freedom requires an additional condition on gateways for asymmetric communication. Such condition is also needed for preservation of deadlock freedom, lock freedom or strong lock freedom for symmetric communications. This is not needed, instead, for preservation of either deadlock freedom or strong lock freedom with asymmetric interactions.

**Keywords:** Communicating Finite State Machines, Communicating Systems, automata, composition of systems, deadlock freedom, lock freedom, synchronous communications.

## 1. Introduction

Nowadays applications are increasingly developed for and executed on distributed architectures (e.g., service-oriented architectures, microservices, cloud, etc.). Communication is therefore an essential constitutive element of modern software. As a matter of fact, APIs, libraries, and languages feature different

<footnote>* Research partly supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233, by the MIUR project PRIN 2017FTXR7S "IT-MaTTerS" (Methods and Tools for Trustworthy Smart Systems) and by the Project "National Center for "HPC, Big Data e Quantum Computing", Programma M4C2 - dalla ricerca all'impresa - Investimento 1.3: Creazione di "Partenariati estesi alle università, ai centri di ricerca, alle aziende per il finanziamento di progetti di ricerca di base" - Next Generation EU. The authors have also been partially supported by INdAM as members of GNCS (Gruppo Nazionale per il Calcolo Scientifico). The authors acknowledge the support of the PRO3 MUR project Software Quality, and PNRR MUR project VITALITY (ECS00000041), Spoke 2 ASTRA - Advanced Space Technologies and Research Alliance. The authors thank the reviewers of the conference and present versions of this paper for their helpful comments. Finally the authors thank Mariangiola Dezani for her support.</footnote>

<footnote>*Corresponding author</footnote>

<footnote>Email addresses: barba@dmi.unict.it (Franco Barbanera), ivan.lanese@gmail.com (Ivan Lanese), emilio.tuosto@gssi.it (Emilio Tuosto)</footnote>
communication mechanisms. Several models, such as process algebras, transition systems, Petri nets, au-
tomata, etc., have been proposed to study interactions between systems. Indeed, developing and reasoning
on communicating systems are difficult endeavours requiring to juggle the what has to be communicated
(a.k.a. business logic) with the how information spreads across a system, sometimes called application level
protocol. In fact, conceptual and programming errors may occur in the realisation of application level
protocols. Typical errors occur when a system is not guaranteed to enjoy some relevant communication
properties, like those we consider in the present paper, namely deadlock-freedom, lock-freedom and strong
lock-freedom. Roughly, deadlock-freedom guarantees a system to get stuck only if all of its components
terminated; lock-freedom guarantees any component willing to communicate to eventually do so in one of
the possible continuations of the system; in a strong lock-free system, instead, each component willing to
communicate will eventually do so in any possible continuation of the system. Such communication proper-
ties may fail when a system makes a choice among different alternatives, and components have inconsistent
"views" of which alternative has been selected. 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 ex-
pected. Let us discuss deadlock freedom through a simple example (similar examples can be given for lock
freedom or strong 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 appeal
to CCS [1] to give possible specifications of this scenario. Let us start with the following CCS<fnref n="1" /> agents:

$$
C = \bar{r}.a + \bar{r}.u \quad \text{and} \quad S = r.\bar{a} + r.\bar{u} \tag{1}
$$

where C and S respectively give the behaviour of clients and servers. It is a simple observation that after
the handshake on r the system C | S, where C and S run in parallel, can evolve to e.g., the deadlock state
a | ū where each party is waiting for the other to progress.

Enforcing correctness of communicating systems is notoriously difficult. A reason for this difficulty is
that it is hard to define composition mechanisms that preserve the communication properties mentioned
above.

*Contributions.* Driven by the motivations in Section 2, we investigate the mechanism of composition by gateways introduced in [2, 3] (for asynchronous communications) in the setting of communicating finite-state machines (CFSMs) [4] with synchronous communications.

Intuitively, composition by gateways transforms two participants **H** and **K**, taken from two separate
systems, into coupled gateways used to connect the two systems. More precisely, when **H** receives a message
from its own system, it forwards it to **K** to be delivered to the other system and vice versa. Our investigation
concerns deadlock-, lock-, and strong lock-freedom preservation under a notion of composability. This notion
combines compatibility, which intuitively prescribes **H** and **K** to exhibit dual behaviour, namely if **H** sends
some message then **K** is willing to receive it and vice versa, with further technical restrictions.

This paper integrates and refines the preliminary results in [5] and some of the ones in [6]. The latter
also considers an additional form of composition, called semi-direct composition, which we do not take
into account here. We consider both the symmetric and asymmetric communication models. Roughly, in
a (one-to-one) symmetric communication model, sender and receiver in an interaction equally concur to
determining the message to be exchanged. In the asymmetric model, instead, such a symmetry is broken by
a bias towards the sender, which autonomously decides the message to be sent and the intended receiver.
Table 1 summarises the results of this paper and refers to their preliminary conference versions (if any). We
show that

<footnote n="1">¹In CCS, agents (or processes) interact by synchronising on communication ports; an output action on a given port ×, is denoted with x̄ while an input action on × is denoted by × itself. Formally, CCS can be defined as an algebra (of agents) whose operators act on ports and agents itself. A fundamental operator is the non-deterministic choice _ + _ which acts on agents: P+Q represents an agent that can non-deterministically behave as P or as Q. Other important operators are prefixes α_._ where α is a communication action: the agent α.P behaves as P after the execution of the communication α.</footnote>
<table><caption>Table 1: Properties preserved by composition</caption><thead><tr><th></th><th></th><th>Deadlock-freedom</th><th>Lock-freedom</th><th>Strong lock-freedom</th></tr></thead><tbody><tr><td rowspan="2">symm. case</td><td>Composability</td><td><span style="color:red;">X</span> [6] and Ex. 6.7</td><td><span style="color:red;">X</span> Ex. 6.7</td><td><span style="color:red;">X</span> Ex. 6.7</td></tr><tr><td>Comp. + Seq.</td><td>✓ [6] and Thm. 8.7</td><td>✓ Thm. 8.4</td><td>✓ Thm. 8.8</td></tr><tr><td rowspan="2">asymm. case</td><td>Composability</td><td>✓ [5] and Thm. 6.2</td><td><span style="color:red;">X</span> Ex. 6.6</td><td>✓ [5] and Thm. 6.4</td></tr><tr><td>Comp. + Seq.</td><td>✓ trivial from above</td><td>✓ [5] and Thm. 8.4</td><td>✓ trivial from above</td></tr></tbody></table>

**in the asymmetric case** composition by gateways (i) preserves deadlock freedom (Theorem 6.2), as well as a strong version of lock freedom (Theorem 6.4), provided that systems are *composable*; and (ii) preserves lock freedom (Theorem 8.4) if systems are *composable* and gateways are *sequential*<fnref n="2" />, namely each state has at most one outgoing transition;

**in the symmetric case** composition by gateways preserves all the communication properties we take into account -i.e., deadlock-, lock- and strong lock-freedom (Theorem 8.7, Theorem 8.4 and Theorem 8.8, respectively)- whenever the compatibility condition is strengthened with the sequentiality requirement.

Interestingly, preservation of deadlock freedom and strong lock-freedom in the asymmetric case can be guaranteed under milder conditions than in the symmetric case. We give counterexamples showing that properties are not preserved under even weaker conditions.

As reported in Table 1, the results concerning lock- and strong lock-freedom in the symmetric case are new. For the others, besides an improved presentation, we provide full and completely revised proofs. The definition of compatibility (Definition 4.6) has been modified with respect to [5] in order to fix some formalisation issues.

*Structure of the paper.* Section 2 discusses our motivations. Section 3 introduces systems of (asymmetric synchronous) CFSMs, their basics, and their communication properties. Composition by gateways is introduced and discussed in Section 4, together with the compatibility relation which is at the basis of properties preservation. Section 5 relates computations in the component systems to computations in the resulting composition, a relation needed for our main results. Section 6 is devoted to the preservation of communication properties if only composability is considered. In Section 7 we show that composability is needed for the results above. By extending composability with the further requirement of sequentiality, in Section 8 we get all the other results of properties preservation. Conclusions, related and future work are discussed in Section 9. For the sake of readability, some auxiliary results needed for proving the preservation results are in Appendix A, in Appendix B, and in Appendix C.

## 2. Motivations

We motivate our interest in asymmetric synchronous communications by considering again the deadlock issue of the client-server example in Section 1. The problem with the agents in (1) is that the choice of what communication should happen after a request is non-deterministically taken independently by C and S instead of letting S to take the decision and drive C “on the right” branch. Let us consider the following alternative agents:

$$C = \bar{r}.(a + u) \quad \text{and} \quad S = r.(\bar{a} + \bar{u}) \qquad (2)$$

In an asynchronous setting the server S in (2) decides what to reply to the client C after the request has been made; C becomes aware of the choice through the signal received on one of the two ports. The situation is

<footnote n="2">²The term ‘sequential’ refers here to the absence of both concurrency and choices.</footnote>
radically different when communication is synchronous and symmetric. In fact, in such case the resolution of the choice hinges on the communication mechanism: a branch is taken as soon as C and S synchronise on port a or on port u. The resolution of the choice is therefore external, in the jargon of [7]. Basically this means that agents cannot decide which branch to take in isolation (as in the asynchronous case): the symmetry in the communication implies that parties equally contribute to the decision on how to continue the computation. As noted in [7], an alternative way to encompass non-determinism in CCS-like languages is to get rid of internal actions from the syntax and “split” the non-deterministic choice operator into two: an operator for internal choices and one for external choices (respectively denoted as ⊕ and □ in [7]). This breaks the symmetry between input and output of synchronous communication; now the choice is entirely resolved on “one side” because the sender must select the branch to fire “before” executing the output action. In [7] this is formally specified by making agents of the form ¯a.P + P' to “internally” reduce to ¯a.P so that the parallel composition of a sender and a receiver, say ¯a.P | (a.Q + Q') can reduce to P|Q. This semantics provides an abstract model of asymmetric synchronous communications, where choices on outputs are “internally” resolved making the sender decide what to communicate and to which partner. Interestingly, internal and external choice operators are at the core of behavioural type systems [8] and behavioural contracts (used, e.g., in [9, 10, 11]).

Besides the theoretical motivation above, asymmetric synchronous communications have also a more practical motivation. In fact, asymmetric synchronous communications abstract a rather common programming pattern where a component chooses the message to send as well as the target of the communication depending on some condition on its own state, e.g., using a conditional.

We now discuss the interplay between communications and compositionality by elaborating on our client-server example. Assume that S acts as a proxy to another server, say S'. If the server S cannot return an answer to C and C is a privileged client, S interacts with S' on port p. Answers are sent directly to C if S' can compute them, otherwise S' returns an unknown on port u' to S which forwards it to C. This is modelled by the agents

$$S = r.(\bar{a} + \bar{p}.u'.\bar{u}) \quad \text{and} \quad S' = p.(\bar{a} + \bar{u}') \quad (3)$$

Note that this change is completely transparent to agent C, which in fact stays as in (2). Here S resolves the choice and then engages in the corresponding communication.

It is interesting to note that it is now more difficult to ascertain if these choices may lead to a deadlock than for the agents in (2). In fact, the decision of S may involve also S'. The parallel composition of the client C from (2) with the agents in (3) may indeed deadlock because, when C and S synchronise on port a, S' hangs on port p and, likewise, if C and S' synchronise on port a then S hangs on port u'.

The above approach has been applied in [2, 3] for the well-known model of systems of communicating finite-state machines (CFSMs) [4], that is sets of finite-state automata capable of exchanging messages. It has been shown that, under suitable compatibility conditions between H and K, 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 dual behaviours: gateway H is able to receive a message whenever gateway K is willing to send one and vice versa.

The results in [2, 3] are developed for the asynchronous semantics of CFSMs. These results have been transferred in [6] to a setting where CFSMs communicate synchronously much like the communication mechanisms considered for instance in process algebras like CCS, ACP, etc. This model assumes a perfect symmetry between sender and receiver in synchronous communications, which, in absence of internal actions, amount to have only external or global non-determinism [12].

### 3. Communicating Finite State Machines with Internal Actions

In this section we define a natural generalisation of Communicating Finite State Machines [4] suitable for formalising the notions of both symmetric and asymmetric synchronous interactions, as well as the composition of systems via gateways.
We begin by recalling a few basic notions on Finite State Automata (FSAs). A finite state automaton (FSA) is a tuple $A = \langle S, q_0, \mathcal{L}, \rightarrow \rangle$ where

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

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

* $\mathcal{L}$ is a finite set of labels

* $\rightarrow \subseteq S \times (\mathcal{L} \cup \{\tau\}) \times S$ is a set of transitions.

Hereafter, we let $\lambda$ range over $\mathcal{L} \cup \{\tau\}$. As usual $q \xrightarrow{\lambda} q'$ abbreviates $(q, \lambda, q') \in \rightarrow$. We say that $q \xrightarrow{\lambda} q'$ is an outgoing (resp. incoming) transition of $q$ (resp. $q'$). Also, $q \rightarrow$ states that $q$ has an outgoing transition, and $q \nrightarrow$ states that there are no transitions from $q$. Let $\rightarrow$ be the concatenation operation on sequences of labels and write $p \xrightarrow{\pi} q$ where $\pi = \lambda_1 \cdot \lambda_2 \cdot \dots \cdot \lambda_n$ (here we identify labels with sequences of labels of length one) whenever $p \xrightarrow{\lambda_1} p_1 \xrightarrow{\lambda_2} \dots \xrightarrow{\lambda_n} p_n = q$. We let $\pi, \psi, \dots$ range over $(\mathcal{L} \cup \{\tau\})^*$ (i.e., sequences of labels) and define the set of states in A reachable from $q$ as

$$ \mathcal{R}(A, q) = \{ p \mid \text{there is } \pi \in (\mathcal{L} \cup \{\tau\})^* \text{ such that } q \xrightarrow{\pi} p \} $$

The set of reachable states in A is $\mathcal{R}(A) = \mathcal{R}(A, q_0)$. For succinctness, $q \xrightarrow{\lambda} 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. As in [4], we formalise communicating systems as FSAs where accepting states are disregarded. The definition of CFSMs in [4] is extended here with $\tau$ labels to account for asymmetric synchronisation. Let $\mathfrak{P}$ be a set of participants (or roles, ranged over by A, B, etc.) and $\mathcal{M}$ a set of messages (ranged over by m, n, etc.). We take $\mathfrak{P}$ and $\mathcal{M}$ disjoint. An action label is either an output or an input label. An output label is written as A B!m and represents the willingness of A to send message m to B; likewise, an input label is written as A B?m and represents the willingness of B to receive message m from A. Interaction labels, instead, have the form A→B: m, which represents the interaction where the message m is sent from A to B, and received from the latter. The subject of an output label A B!m and of an input label B A?m is A. We also say that A (resp. B) is the sender (resp. receiver) in the interaction label A→B: m.

The set of action- and interaction-labels are hence defined by

$$ \mathcal{L}_{\text{act}} = \{ A B!m, A B?m \mid A \neq B \in \mathfrak{P} \text{ and } m \in \mathcal{M} \} $$

$$ \mathcal{L}_{\text{int}} = \{ A \rightarrow B : m \mid A \neq B \in \mathfrak{P} \text{ and } m \in \mathcal{M} \} $$

In the following, we use function ptp($\lambda$) computing the set of participants occurring in a label $\lambda$, and defined as ptp($\tau$) = $\emptyset$ and ptp(A→B: m) = ptp(A B!m) = ptp(A B?m) = {A, B} and, for a sequence $\pi = \lambda_1 \cdot \dots \cdot \lambda_n$, we let ptp($\pi$) = $\cup_{1 \le i \le n} ptp(\lambda_i)$.

**Definition 3.1** ($\tau$-CFSM). A $\tau$-CFSM is an FSA with labels in $\mathcal{L}_{\text{act}} \cup \{\tau\}$. A $\tau$-CFSM is A-local if all its non $\tau$-transitions have subject A.

An output (resp. input) transition is a transition labelled by an output (resp. input) label.

We now define systems of $\tau$-CFSM.

**Definition 3.2** ($\tau$-systems). Let $\mathcal{P} \subseteq \mathfrak{P}$ be finite set of participants. A $\tau$-system over $\mathcal{P}$ is a map $S = (M_A)_{A \in \mathcal{P}}$ assigning an A-local $\tau$-CFSM $M_A$ to each participant $A \in \mathcal{P}$ where any participant occurring in a transition of $M_A$ is in $\mathcal{P}$.

A $\tau$-system consists of named $\tau$-CFSMs, which we formally describe as a function from $\mathcal{P}$ (the names of the participants of the system) to the set of $\tau$-CFSMs. A $\tau$-CFSM with name A (i.e., describing the behaviour of participant A) is naturally requested to be A-local, that is A is the sender of its output actions and the receiver of its input ones. Note that Definition 3.2 requires also that any input or output label
does refer to participants belonging to the system itself. In other words, Definition 3.2 restricts to closed τ-systems.

We define the synchronous semantics of τ-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 $f[x \mapsto y]$ denotes the update of f in a point $x \in \text{dom}(f)$ with the value y.

**Definition 3.3 (Synchronous semantics).** Let S be a τ-system. The synchronous semantics of S is the FSA $\llbracket S \rrbracket = \langle S, s_0, \mathcal{L}_{\text{int}} \cup \{\tau\}, \rightarrow \rangle$ where

* S is the set of synchronous configurations of S, where a configuration is a map $s = (q_A)_{A \in \text{dom}(S)}$ assigning a local state $q_A \in S(A)$ to each $A \in \text{dom}(S)$;

* $s_0 = (q_{0A})_{A \in \text{dom}(S)} \in S$ is the initial configuration where, for each $A \in \text{dom}(S)$, $q_{0A}$ is the initial state of $S(A)$;

* $s \xrightarrow{\tau} s[A \mapsto q] \in \llbracket S \rrbracket$ if $s(A) \xrightarrow{\tau} q \in S(A)$;

* $s \xrightarrow{A \to B; m} s[A \mapsto q, B \mapsto q'] \in \llbracket S \rrbracket$ if $s(A) \xrightarrow{AB!m} q \in S(A)$ and $s(B) \xrightarrow{AB?m} q' \in S(B)$.

Configuration s enables A (in S) if $s(A)$ has at least an outgoing transition.

A participant A $\in \mathcal{P}$ is involved in a transition $s \xrightarrow{\lambda} s'$ if either A $\in \text{ptp}(\lambda)$ or $\lambda = \tau$, $s(A) \xrightarrow{\tau} q$ in S(A), and $s' = s[A \mapsto q]$; A is involved in a run if A is involved in one of its transitions.

As expected, an interaction A→B:m occurs when A performs an output AB!m and B the corresponding input AB?m.

A τ-CFSM without τ-transitions is a CFSM in the sense of [4]; following [4], we dub communicating systems those τ-systems consisting of CFSMs only. We simply use system when the type of machines is immaterial. Also, the symmetric synchronous semantics in [6] for systems without τ-transitions can be readily obtained from the above definition by disregarding the clause for τ-transitions. It is worth remarking that the use of τ-transitions in the above definition is not equivalent to that of buffers of size 1 in the model of asynchronous CFSMs [4], since we are modelling (asymmetric) synchronous interactions, which are blocking.

We cast in our framework the usual definition of runs.

**Definition 3.4 (Runs).** A run from s is a (possibly infinite) sequence $\xi = s \xrightarrow{\lambda_1} s_1 \cdots s_{n-1} \xrightarrow{\lambda_n} s_n \cdots$ starting from s. A run is maximal if it is infinite or it reaches a configuration $s'$ such that $s' \nrightarrow$. A run $\xi$ is fair if whenever there is an interaction label $\lambda$ and an index $j \ge 1$ such that $s_i \xrightarrow{\tau^*} \lambda \xrightarrow{\lambda} \in \llbracket S \rrbracket$ for infinitely-many indexes $i \ge j$, we have that for each X involved in $\lambda$ there is $h \ge j$ such that $s_h \xrightarrow{\lambda'} s_{h+1}$ with X involved in $\lambda'$. A run of S is a run from the initial configuration of S.

**Example 3.5 (Runs).** Let us consider the τ-system $S = (M_X)_{X \in \{K,C,D,E\}}$, where

<figure><img src="image_2.png" /></figure>

are the τ-CFSM<fnref n="3" /> $M_K$, $M_C$, $M_D$, and $M_E$ respectively. Then

$$ \begin{array}{lclcl} s_0 = (0_K, 0_C, 0_D, 0_E) & \xrightarrow{\tau} & (1_K, 0_C, 0_D, 0_E) & \xrightarrow{K \to C; m} & (3_K, 1_C, 0_D, 0_E) \\ & \xrightarrow{\tau} & (3_K, 2_C, 0_D, 0_E) & \xrightarrow{C \to E; c} & (3_K, 3_C, 0_D, 4_E) \\ & \xrightarrow{\tau} & (3_K, 3_C, 0_D, 5_E) & \xrightarrow{E \to D; s} & (3_K, 3_C, 3_D, 3_E) \end{array} $$

<footnote n="3">³Hereafter, we specify communicating systems with the graphical notation introduced in Example 3.5.</footnote>
is a sequence of transitions of $[[S]]$ starting from $s_0$ induced by Definition 3.3. Note that this is a maximal run of $S$. ◇

**Example 3.6** (Fair runs). Let us consider the $\tau$-system $S = (M_X)_{X \in \{A,B,C\}}$, where

<figure><img src="image_3.png" /></figure>

Then the following infinite run of $S$ is fair

$$ s_0 = (0_A, 0_B, 0_C) \xrightarrow{\tau} (1_A, 0_B, 0_C) \xrightarrow{A \to B: m} (0_A, 0_B, 0_C) \\ \xrightarrow{\tau} (2_A, 0_B, 0_C) \xrightarrow{A \to C: m} (0_A, 0_B, 0_C) \\ \xrightarrow{\tau} (1_A, 0_B, 0_C) \xrightarrow{A \to B: m} (0_A, 0_B, 0_C) \\ \xrightarrow{\tau} (2_A, 0_B, 0_C) \xrightarrow{A \to C: m} (0_A, 0_B, 0_C) \\ \xrightarrow{\tau} \dots $$

The following infinite run of $S$, instead, is not fair.

$$ s_0 = (0_A, 0_B, 0_C) \xrightarrow{\tau} (1_A, 0_B, 0_C) \xrightarrow{A \to B: m} (0_A, 0_B, 0_C) \\ \xrightarrow{\tau} (1_A, 0_B, 0_C) \xrightarrow{A \to B: m} (0_A, 0_B, 0_C) \\ \xrightarrow{\tau} \dots $$

The run above is not fair for $C$ since there are infinitely many configurations where the transition $A \to C: m$ could be executed (after the $\tau$-transition to state 2 in $A$), however, $A$ keeps choosing the $\tau$-transition to state 1, so preventing $C$ to execute. ◇

### 3.1. Asymmetric Synchronous Interactions

We model asymmetric synchronous communications by restricting the (too liberal) $\tau$-CFSMs formalism.

**Definition 3.7** ($\tau$!-CFSM). A $\tau$!-CFSM (pronounced ‘tau-bang CFSM’) is a $\tau$-CFSM, say $M$, such that

* for all output transitions $p \xrightarrow{\lambda} q$ of $M$, $p$ has exactly one incoming transition in $M$, and such transition is labelled by $\tau$;

* for all $\tau$-transitions $p \xrightarrow{\tau} q$ of $M$, $q$ has exactly one outgoing transition in $M$, and such transition is an output transition.

We call $\tau$!-systems $\tau$-systems consisting of $\tau$!-CFSMs only.

Observe that both conditions in the above definition imply $p \neq q$. All our proofs could easily be adapted to an alternative definition of $\tau$!-CFSM, where the condition of having $\tau$-transitions prefixing output transitions like $p \xrightarrow{X|Y|Z} q$ is dropped if $p \xrightarrow{X|Y|Z} q$ is the only outgoing transition from $p$. Indeed, in this case no actual choice about which output to perform needs to be taken. We however prefer to stick to Definition 3.7 because (i) our uniform treatment of transitions allows us to immediately adapt definitions to more abstract settings and (ii) uniformity allows us to simplify some technicalities.

**Example 3.8.** The $\tau$-CFSMs of Example 3.5 are $\tau$!-CFSMs.
## 3.2. Communication Properties

As discussed in Section 1, we shall study the preservation of communication properties under composition. We shall consider the following 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 [14, 15, 6]).

**Definition 3.9 (Communication properties).** Let $S$ be a system on $\mathcal{P}$.

**Deadlock freedom.** A configuration $s \in \mathcal{R}(\llbracket S \rrbracket)$ is a deadlock if

* there exists $A \in \mathcal{P}$ such that $s$ enables $A$ in $S$ and

* $s$ has no outgoing transitions in $\llbracket S \rrbracket$.

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

**Lock freedom.** A configuration $s \in \mathcal{R}(\llbracket S \rrbracket)$ is a lock for $A \in \mathcal{P}$ if

* $s$ enables $A$ in $S$ and

* there is no run from $s$ involving $A$.

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

**Strong lock freedom.** A configuration $s \in \mathcal{R}(\llbracket S \rrbracket)$ is a weak lock for $A \in \mathcal{P}$ if

* $s$ enables $A$ in $S$ and

* there is at least a maximal fair run from $s$ not involving $A$.

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

**Proposition 3.10.** Strong lock freedom implies lock freedom and lock freedom implies deadlock freedom.

*Proof.* Directly from the definitions. □

**Example 3.11.** Let us consider the system $S$ of Example 3.5. The only other maximal run in $\llbracket S \rrbracket$ starting from $s_0$, besides the one described in Example 3.5, is

$$ s_0 = (0_K, 0_C, 0_D, 0_E) \xrightarrow{\tau} (2_K, 0_C, 0_D, 0_E) \xrightarrow{\substack{K \to D: n \\ D \to E: d}} (3_K, 0_C, 1_D, 0_E) \\ \xrightarrow{\tau} (3_K, 0_C, 2_D, 0_E) \xrightarrow{\substack{D \to E: d \\ E \to C: s}} (3_K, 0_C, 3_D, 1_E) \\ \xrightarrow{\tau} (3_K, 0_C, 3_D, 2_E) \xrightarrow{\substack{E \to C: s \\ C \to A: m}} (3_K, 3_C, 3_D, 3_E) $$

Then $\mathcal{R}(\llbracket S \rrbracket)$ consists of all and only the configurations on these two runs. By inspecting these finitely many configurations we can check that $S$ is strongly lock free.

Let us consider now the system $S = (M_X)_{X \in \{A,B,C,D\}}$, where

<figure><img src="image_4.png" /></figure>

Such a system is both deadlock- and lock-free, but it is not strongly lock-free since its initial configuration $s_0$ is a weak-lock for $D$. In fact it enables $D$, but the following infinite run

$$ s_0 = (0_A, 0_B, 0_C, 0_D) \xrightarrow{\tau} (0_A, 1_B, 0_C, 0_D) \xrightarrow{\substack{B \to A: m \\ C \to A: m}} (2_A, 0_B, 0_C, 0_D) \\ \xrightarrow{\tau} (2_A, 0_B, 1_C, 0_D) \xrightarrow{\substack{C \to A: m \\ A \to B: m}} (0_A, 0_B, 0_C, 0_D) \\ \xrightarrow{\tau} \dots $$

does not involve $D$ but it is fair because there is no interaction involving $D$ which is enabled infinitely many times (possibly after some $\tau$-transitions). Actually, no interaction involving $D$ is ever enabled. ◇
## 4. Composition via Gateways

Recently, an approach to the composition of concurrent and distributed systems has been proposed in [2]. The composition mechanism is based on the idea that two given systems, say $S_1$ and $S_2$, are composed by transforming two participants, one per system, say $H$ in $S_1$ and $K$ in $S_2$, into “coupled forwarders”.

Basically, each message that $H$ receives from a participant in $S_1$ is forwarded to $K$ and vice versa. In order to clarify the underlying idea, let us consider a system $S_1$ made of several communicating participants, among which a participant $H$ (graphically represented on the left) is present. Participant $H$ can receive messages of type $a$ from other participants of $S_1$ and send messages of type $b$, $c$, or $d$. For the purpose of this example, we abstract from the way communications are performed and from the logical order of the exchanged messages. Now let us consider a second system $S_2$, where a participant $K$ is present, and assume that $K$ (graphically represented on the right) can send to other participants messages of type $a$, and receive messages of type $b$, $c$, or $d$.

Participants $H$ and $K$ are compatible in the sense that, if some participant of the system $S_1$ needs a message “produced” by $H$, this message can actually be the one received in system $S_2$ by $K$. Symmetrically, the messages that $H$ receives from other participants of $S_1$ could be forwarded to $S_2$ as if they were messages sent by $K$ to participants of $S_2$. From this point of view, the behaviours of $H$ and $K$ can be looked at as “interfaces” which describe what one system expects from the other in case they interact. As observed in [2, 16, 3], a remarkable feature of such an approach is that it enables the composition of systems originally designed as closed. Provided that two compatible participants can be found, any two systems can be composed by transforming as sketched above the two selected participants.

The composition mechanism consists then in replacing the two participants $H$ and $K$ by two forwarders, $gw(H, K)$ and $gw(K, H)$, respectively, and connecting them as follows:

<figure><img src="image_5.png" /></figure>

Hereafter, $H$ and $K$ denote the participant selected for the composition in, respectively, $S_1$ and $S_2$.

Using gateways, open systems can hence be seen as a special kind of closed ones, satisfying suitable compatibility conditions when composing them into a whole; so exploiting the flexibility of modular development of systems also in case these were not developed as open.

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 $H$ and $K$.

Following the intuition above, we now define composition via gateways for both systems of CFSMs and of $\tau$!-CFSMs. They slightly differ since we have to make sure that a gateway obtained out of a CFSM (resp. a $\tau$!-CFSM) is still a CFSM (resp. a $\tau$!-CFSM).

**Definition 4.1 (Gateways).** Fix two distinct participants $H, K \in \mathcal{P}$.

i) The gateway towards $K$ of an $H$-local CFSM $M$ is the CFSM $gw(M, K)$ obtained by replacing in $M$:

$$ \bullet \text{ each transition } q \xrightarrow{H A! m} r \in M \text{ with} \qquad q \xrightarrow{K H? m} q' \xrightarrow{H A! m} r \quad \text{for some fresh state } q' \qquad (4) $$

$$ \bullet \text{ each transition } q \xrightarrow{A H? m} r \in M \text{ with} \qquad q \xrightarrow{A H? m} q' \xrightarrow{H K! m} r \quad \text{for some fresh state } q' \qquad (5) $$
ii) The gateway towards K of an H-local τ!-CFSM M is the τ!-CFSM gw(M, K) obtained by replacing in M:

$$
\bullet \text{ each pair of consecutive transitions } q \xrightarrow{\tau} q' \xrightarrow{HA!m} r \text{ with} \\
q \xrightarrow{KH?m} q'' \xrightarrow{\tau} q' \xrightarrow{HA!m} r \quad \text{for some fresh state } q'' \qquad (6)
$$

$$
\bullet \text{ each transition } q \xrightarrow{AH?m} r \text{ with}
$$
$$
q \xrightarrow{AH?m} q' \xrightarrow{\tau} q'' \xrightarrow{HK!m} r \quad \text{for some fresh states } q' \text{ and } q'' \qquad (7)
$$

We call the sequences of transitions (4) and (6) q-r importing segments (from K) and the sequences of transitions (5) and (7) q-r exporting segments (to K). Also, we call internal the state q' in (4) and (5) as well as the states q' and q'' in (6) and (7).

Note that a gateway gw(M, -) executes segments of the form described above which are different for CFSMs and τ!-CFSMs; indeed our notation is overloaded, but contexts will clarify which type of machines is involved. Also, by very construction, we have the following

**Fact 4.2.** *Given an H-local τ!-CFSM M and a participant K not occurring in M, each state of gw(M, K) has at most one incoming or outgoing τ transition.*

As a consequence of the above fact, the alternative definition of τ!-CFSMs discussed after Definition 3.7
would make gateways for τ!-CFSM identical to gateways for CFSMs.

We compose systems with disjoint participants taking all the participants of the original systems but H and K, whereas H and K are replaced by their respective gateways.

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

**Definition 4.3 (System composition).** Let $S_1$ and $S_2$ be either communicating systems or $\tau$!-systems with disjoint domains. The composition of $S_1$ and $S_2$ via $H \in \text{dom}(S_1)$ and $K \in \text{dom}(S_2)$ is defined as

$$
S_1^{H \to K} S_2 = S_1[H \mapsto gw(S_1(H), K)] + S_2[K \mapsto gw(S_2(K), H)]
$$

(Note that $\text{dom}(S_1^{H \to K} S_2) = \text{dom}(S_1) \cup \text{dom}(S_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 behavioural composition have been studied in [16] for multiparty session types.

**Example 4.4.** *Take the communicating systems S<sub>1</sub> and S<sub>2</sub> below*

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /><figcaption>The following communicating system</figcaption></figure>

<figure><img src="image_8.png" /></figure>

is the composition $S_1^{H \to K} S_2$.

<figure><img src="image_9.png" /></figure>
**Example 4.5.** Let us take the following two τ!-systems.

<figure><img src="image_10.png" /></figure>

The τ!-system $S_1^{H*K} S_2$ is

<figure><img src="image_11.png" /></figure>

Note that the CFSMs for participants A, B, C, D, and E remain unchanged.

<figure><img src="image_12.png" /></figure>

### 4.1. Compatibility

The notion of compatibility formalises the intuitive requirement that behaviours of the two gateways should match. It is clear that without such a requirement the composition would not behave well. We will see later on that for a successful composition additional technical conditions are needed. Intuitively, two interfaces H and K are compatible if:

* each input of one of them has a corresponding (matching) output in the other one.

Since an input of an interface, say H, is followed in the corresponding gateway by an output towards the gateway for K, this guarantees that each message sent by the gateway for H can be received from the one for K.

* if an output is possible in one of the interfaces, then at least one input (possibly with a message that does not match it) is possible in the other one.

This ensures that if the gateway for H needs to send messages to $S_1$, then at least a message can arrive from the gateway for K. However, if the gateway for H can send more than one message, it may be the case that the gateway for K can send only some of them. What happens in this case is that an internal choice in H is delegated to K, which may decide to never choose some of the available options, while always choosing only available options (this follows from the point above).

To define the compatibility relation it is useful to introduce a few auxiliary notions. More precisely, we let $\mathcal{L}_{i/o} = \{ ?m, !m \mid m \in \mathcal{M} \}$ and borrow from [3] the function $io: \mathcal{L}_{act} \to \mathcal{L}_{i/o}$ defined as follows

$$io(AB?m) = ?m \quad \text{and} \quad io(AB!m) = !m$$
This function straightforwardly extends to $\tau$-CFSMs. In particular, given $M = \langle S, q_0, \mathcal{L}_{\text{act}} \cup \{\tau\}, \rightarrow \rangle$ we define $\text{io}(M) = \langle S, q_0, \mathcal{L}_{i/o} \cup \{\tau\}, \rightarrow' \rangle$ where

$$ \rightarrow' = \{ q \xrightarrow{\text{io}(\lambda)} q' \mid q \xrightarrow{\lambda} q' \in M, \lambda \in \mathcal{L}_{\text{act}} \} \cup \{ q \xrightarrow{\tau} q' \mid q \xrightarrow{\tau} q' \in M \} $$

The function $\text{io}(\cdot)$ captures the fact that our gateway construction blurs away the identities of the participants that actually sent the messages to their gateway.

**Definition 4.6 (Compatibility).** Let $M$ and $M'$ be either two CFSMs or two $\tau$!-CFSMs<fnref n="4" /> whose sets of states are respectively $S$ and $S'$. A relation $R \subseteq S \times S'$ is an io-matching of $M$ and $M'$ if whenever $(q, q') \in R$:

(i) if $q \xrightarrow{?m} r \in \text{io}(M)$ then

* either there is $q' \xrightarrow{1m} r' \in \text{io}(M')$ such that $(r, r') \in R$

* or there is $q' \xrightarrow{\tau} \xrightarrow{1m} r' \in \text{io}(M')$ such that $(r, r') \in R$

(ii) if either $q \xrightarrow{1m} r \in \text{io}(M)$ or $q \xrightarrow{\tau} r \in \text{io}(M)$ then $q'$ has at least one input transition in $\text{io}(M')$.

An io-correspondence between $M$ and $M'$ is an io-matching $R$ between $M$ and $M'$ such that $R^{-1}$ is an io-matching between $M'$ and $M$. We say that two states $q$ and $q'$ are compatible (in symbols $q \asymp q'$) if there is an io-correspondence containing $(q, q')$; $M$ and $M'$ are compatible if their initial states are compatible.

Definition 4.6 transfers the notion of compatibility given in [16] for processes in multiparty sessions. Our compatibility relation is a form of bisimulation with a bias on the input transitions of the interfaces; in fact, we require to match an input transition with an output of the same message while the requirement is weaker for output or $\tau$-transitions. It is worth noticing that such a weaker requirement, namely condition (ii) of Definition 4.6, makes sense only because, when defining $q \asymp q'$, we expect that there exists an io-matching $R$ such that also $R^{-1}$ is so. Such inverse io-matching relation ensures (via condition (i)) that the input transition that should exist matches one of the available outputs. Summarising, the two conditions together ensure that the outputs are a subset of the inputs (see Example 4.7 below). This notion differs from the ones in [6] and in [2, 3] which are defined as bisimulations and do not involve $\tau$-transitions.

**Example 4.7 (Compatibility and CFSMs).** The relation $\{(0,0), (0,1)\}$ is an io-correspondence between the states of the CFSMs in Example 4.4, stating that state 0 of $M_H$ corresponds to both states 0 and 1 of $M_K$. Therefore, $M_H$ and $M_K$ are compatible. A more interesting example is given by the following CFSMs:

<figure><img src="image_13.png" /></figure>

<figure><img src="image_14.png" /></figure>

and it is easy to check that $\{(0,0), (1,1)\}$ is an io-correspondence relating the initial states of $M_H$ and $M_K$. Interestingly, the transition $0 \xrightarrow{1y} 1 \in \text{io}(M_K)$ is not matched by an input of $\text{io}(M_H)$ since Definition 4.6 requires only that the related state has an input transition. ◇

<footnote n="4">⁴The definition can be extended in order to take into account $\tau$-CFSMs in general. We chose not to do so for the sake of simplicity, since our results focus on CFSMs and $\tau$!-CFSMs.</footnote>
**Example 4.8** (Compatibility and τ!-CFSMs). The τ!-CFSMs $M_H$ and $M_K$ of Example 4.5 are compatible, in fact, it is easy to check that the relation { (0, 0), (0, 1), (0, 2), (1, 3) } is an io-correspondence between their states. For a more complex example let us consider the following τ!-CFSMs

<figure><img src="image_15.png" /></figure>

where the states with the same colour are in io-correspondence.

Apart for τ actions preceding them, H can only perform output actions, whereas K can only perform input actions. By disregarding the names of the receivers in the actions of H, and of the senders in those of K, any input action can find a matching output. The vice versa does not hold, since the output from state 12 in $M_H$ is not matched in $M_K$. Such a possibility is in fact allowed by our definition of compatibility. Note that there is no io-correspondence relating state 12 and a state of $M_K$. ◇

Clause (i) in Definition 4.6 ensures that each input of one interface is matched by some output of the other. Clause (ii) requires a milder condition on non-input transitions; in fact, an output or a τ-transition of one interface just force the other interface to be able to execute an input. The latter clause prevents H and K from being compatible in the following systems.

$$S_1 = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, every node/.style={scale=0.7}]
% State 1 (H) interface
% Top-left corner
\node (A) at (0,0) {$A \rightarrow \boxed{0} \xrightarrow{HA?m} \boxed{1}$};
% Top-right corner
\node (H) at (2,0) {$H \rightarrow \boxed{0} \xrightarrow{HA!m} \boxed{1}$};
% Bottom-left corner
\node (L) at (0,-1) {$\boxed{0} \rightarrow A \xrightarrow{HA?m} \boxed{1}$};
% Bottom-right corner
\node (R) at (2,-1) {$H \xrightarrow{HA!m} \boxed{0}$};
% Arrows
\draw[->] (A) -- (L);
\draw[->] (H) -- (R);
\draw[->] (A) -- (R);
\draw[->] (L) -- (R);
\end{tikzpicture} \quad \text{and} \quad S_2 = \boxed{K \rightarrow \boxed{0}}$$

Allowing their compatibility would spoil the deadlock freedom of the composed system:

$$S_1 \overset{H \leftrightarrow K}{=} \boxed{A \rightarrow \boxed{0} \xrightarrow{HA?m} \boxed{1} \quad H \rightarrow \boxed{0} \xrightarrow{KH?m} \boxed{0} \quad \boxed{0} \rightarrow A \xrightarrow{HA!m} \boxed{1}}$$

being its initial configuration immediately stuck. As shown in the next section, the compatibility conditions need to be further strengthened in order to preserve communication properties in the composition operation.

## 4.2. Composability

We require a stronger condition than compatibility for two systems to be composable. Basically, we need to restrict the non-deterministic behaviour of systems.

**Definition 4.9** (Machines' determinism). An A-local CFSM or τ!-CFSMM is

1. ?-deterministic if $p \xrightarrow{XA?m} q$ and $p \xrightarrow{YA?m} r \in M$ implies $q = r$;

2. !-deterministic if either

* $M$ is a τ!-CFSM and ($p \xrightarrow{\tau} \boxed{AX!m} \rightarrow q$ and $p \xrightarrow{\tau} \boxed{AY!m} \rightarrow r \in M$) implies $q = r$; or

* $M$ is a CFSM and ($p \xrightarrow{\overrightarrow{AX!m}} q$ and $p \xrightarrow{\overrightarrow{AY!m}} r \in M$) implies $q = r$.

3. ?!-deterministic if it is both ?-deterministic and !-deterministic;

A state $q \in M$ is mixed if it has both at least an outgoing input transition and an outgoing output or τ transition.

**Example 4.10.** Machines H and K in Example 4.8 are, respectively, non !-deterministic and non ?-deterministic. In particular, conditions (2) and (1) of Definition 4.9 fail for, respectively, state 0 of H and state 0 of K. For an example of mixed state the reader is referred to Example 7.2 where the initial state of machine K is mixed.

We now define composability.

**Definition 4.11** ((H, K)-composability). Let $S_1$ and $S_2$ be either both communicating systems or both τ!-system. Systems $S_1$ and $S_2$ are (H, K)-composable if their domains are disjoint, and $H \in \text{dom}(S_1)$ and $K \in \text{dom}(S_2)$ are two compatible ?!-deterministic machines with no mixed states.
## 5. Composed Systems and Their Projections

The general idea underlying most of the proofs of property preservation will be that of showing that if a property does fail for a composed system, so it does for at least one of its composing systems. We introduce a few technical definitions and results to exploit this general proof scheme.

Given a configuration of a composed system, say $S_1^{H*K} S_2$, we can retrieve the configurations of $S_1$ (resp. $S_2$) by taking only the states of participants in $S_1$ (resp. $S_2$) while mapping fresh states introduced by the gateway construction to states of the original machines. Indeed, we shall prove in Proposition 5.9 that reachable configurations of $S_1^{H*K} S_2$ correspond to reachable configurations of $S_1$ and of $S_2$.

**Definition 5.1** (Configuration projections). Let $S = S_1^{H*K} S_2$ be a composed communicating or $\tau$!-system and $s \in \mathcal{R}(\llbracket S \rrbracket)$ be a reachable configuration of $S$. The left-projection of $s$ on $S_1$ is the map $s|_{K}^{H}$ defined on $\text{dom}(S_1)$ by

$$ s|_{K}^{H} : A \mapsto \begin{cases} q, & \text{if } s(A) \text{ is a fresh state of a } q\text{-r importing segment from } K \text{ in } gw(S_1(H), K) \\ r, & \text{if } s(A) \text{ is a fresh state of a } q\text{-r exporting segment to } K \text{ in } gw(S_1(H), K) \\ s(A), & \text{otherwise} \end{cases} $$

The definition of right-projection $s|_{H}^{K}$ is analogous.

**Proposition 5.2.** Left- and right-projections are well-defined.

*Proof.* It is enough to show that $s|_{K}^{H}$ and $s|_{H}^{K}$ uniquely assign a state to fresh states because both functions leave unchanged non-fresh states. This follows since, by definition, each state introduced by our gateway construction belongs to a unique $q\text{-r}$ (importing or exporting) segment. $\square$

Intuitively, only $H$ is aware of an input from $K$ when $H$ is in the internal state of an importing segment; hence to have a coherent configuration we take the state of $H$ before the input. If instead $H$ is in the internal state of an exporting segment, then other participants in $S_1$ know that the message has been sent; hence to have a coherent configuration we take the state of $H$ after the output. (A similar intuition applies to $s|_{H}^{K}$.) A pictorial description of Definition 5.1 according to this intuition is provided after Fact 5.3 below.

**Fact 5.3.** Let $s$ be a configuration of a system $S_1^{H*K} S_2$.

$$ \text{for all } A \in \text{dom}(S_1) \setminus \{H\} \quad s|_{K}^{H} s(A) = s(A) \quad \text{and} \quad \text{for all } A \in \text{dom}(S_2) \setminus \{K\} \quad s|_{H}^{K}(A) = s(A) $$

This fact does not hold for gateways since, for instance, the local state $s(H)$ can be such that $H$ is engaging in a communication with $K$; in this case the configuration projection yields a local state in $S_1(H)$ which depends on the form of the segment $S(H)$ is on. Notice that in the latter case $S(H)$ is a gateway while $S_1(H)$ is the original interface.

To explain the mapping we appeal to the pictorial representation of Definition 5.1 announced above. Assume first that $S_1$ and $S_2$ are communicating systems. By considering transitions in $S_1(H)$ and their corresponding segment in the gateway, we have

<figure><img src="image_16.png" /></figure>

or

<figure><img src="image_17.png" /></figure>

where the dotted edges mark the state assigned by the “left-projection” of $s$ on $H$. For instance, $s|_{K}^{H} s(H) = q$ if $s(H) = q$ while if $s(H) = q'$ then $s|_{K}^{H} s(H) = r$ on the exporting segment to $K$ and $s|_{K}^{H} s(H) = q$ on the importing segment from $K$. Similarly, assuming that $S_1$ and $S_2$ are $\tau$!-systems, we have

<figure><img src="image_18.png" /></figure>

or

<figure><img src="image_19.png" /></figure>
**Example 5.4.** Consider the communicating systems $S_1, S_2$, and $S_1^{H*}S_2$ of Example 4.4. The next picture shows the projection of a configuration of $S_1^{H*}S_2$ on a configuration of $S_1$ and one of $S_2$, where configurations are represented by filled states. The left-projection $s$ is the one identified by the dashed lines, whereas $s|_H^K$ is identified through the dash-dotted lines.

<figure><img src="image_20.png" /></figure>

The configuration of $S_1^{H*}S_2$, say $s$, is reached from the initial configuration after the following sequence of interactions $A \to H: m \cdot H \to K: m \cdot A \to H: m$. Note that such projected configurations are reachable in $S_1$ and $S_2$ respectively. ◇

**Example 5.5.** Let $s = (2_A, 0_B, 1_H, 3_K, 1_C, 0_D, 0_E)$; and $S = S_1^{H*}S_2$ be the $\tau$-system of Example 4.5. Then, $s \in \mathcal{R}(\llbracket S \rrbracket)$, namely $s$ is reachable in $S$. In fact

$$ \begin{array}{lclcl} s_0 = (0_A, 0_B, 0_H, 0_K, 0_C, 0_D, 0_E) & \xrightarrow{\tau} & s_1 = (1_A, 0_B, 0_H, 0_K, 0_C, 0_D, 0_E) \\ & \xrightarrow{A \to H: m} & s_2 = (2_A, 0_B, 2_H, 0_K, 0_C, 0_D, 0_E) \\ & \xrightarrow{\tau} & s_3 = (2_A, 0_B, 4_H, 0_K, 0_C, 0_D, 0_E) \\ & \xrightarrow{H \to K: m} & s_4 = (2_A, 0_B, 1_H, 5_K, 0_C, 0_D, 0_E) \\ & \xrightarrow{\tau} & s_5 = (2_A, 0_B, 1_H, 1_K, 0_C, 0_D, 0_E) \\ & \xrightarrow{K \to C: m} & s = (2_A, 0_B, 1_H, 3_K, 1_C, 0_D, 0_E) \end{array} $$

The projections of $s$ on, respectively, $S_1$ and $S_2$ are $s|_K^H = (2_A, 0_B, 1_H)$ and $s|_H^K = (3_K, 1_C, 0_D, 0_E)$ and they are both reachable in their respective $\tau$-systems:

$$ \begin{array}{lclcl} s_0|_K^H = (0_A, 0_B, 0_H) & \xrightarrow{\tau} & s_1|_K^H = (1_A, 0_B, 0_H) \\ & \xrightarrow{A \to H: m} & s_2|_K^H = (2_A, 0_B, 1_H) & = & s_3|_K^H = s_4|_K^H = s_5|_K^H \end{array} $$

$$ \begin{array}{lclcl} s_0|_H^K = s_1|_H^K = s_2|_H^K = s_3|_H^K = (0_K, 0_C, 0_D, 0_E) & \xrightarrow{\tau} & s_5|_H^K = (1_K, 0_C, 0_D, 0_E) \\ & \xrightarrow{K \to C: m} & s|_H^K = (3_K, 1_C, 0_D, 0_E) \end{array} $$

◇

By the above examples it is natural to expect that the projections of configurations that are reachable in a composed system are in turn reachable in the respective component systems. Also, from Example 5.5, it is reasonable to expect that one of the two composing systems has a participant with an enabled transition from one of the projected configurations when a transition is enabled in a configuration of the composed system. This is formalised in Proposition B.1 (cf. Appendix B).
Next definition maps states of gateways to states of the original interfaces, with the aim of showing that the gateways always stay “in sync”, mimicking the compatibility relation between the interfaces. To simplify the correspondence, we force the two gateways to change configuration at the same time. Given that the only transition where the two gateways interact is the communication between them, transitions allowing one to change state in an interface correspond to the H-K transition in the gateways. This is clearly visible in the graphical interpretation below.

**Definition 5.6 (Gateway embedding).** Let $M$ be an H-local CFSM or $\tau$!-CFSM and $K \in \mathcal{P}$ be a participant not occurring in $M$. The gateway embedding $\Gamma$ maps the states of $gw(M, K)$ to the states of $M$ as follows:

$$ \Gamma_{H,K}(M, p) = \begin{cases} q, & \text{if } A \neq K \text{ and } p \text{ is an internal state of a } q\text{-r exporting segment to } K \text{ in } gw(M, K) \\ r, & \text{if } A \neq K \text{ and } p \text{ is an internal state of a } q\text{-r importing segment from } K \text{ in } gw(M, K) \\ p, & \text{otherwise} \end{cases} $$

As before we give a pictorial description of the above definition. For CFSMs we have

<figure><img src="image_21.png" /></figure>

<figure><img src="image_22.png" /></figure>

while for $\tau$!-CFSM we have

<figure><img src="image_23.png" /></figure>

<figure><img src="image_24.png" /></figure>

By definition of gateway (Definition 4.1) and the above pictures, it immediately descends the following

**Fact 5.7.** Function $\Gamma$ is well-defined.

**Example 5.8.** Let $M$ and $M'$ be the gateways for, respectively, participants H and K of Example 4.4. The gateway embeddings $\Gamma_{H,K}(M, -)$ and $\Gamma_{K,H}(M', -)$ map, respectively, the states of $M$ and $M'$ as indicated below by the dotted edges.

<figure><img src="image_25.png" /></figure>

<figure><img src="image_26.png" /></figure>

Let $M$ and $M'$ be the gateways for, respectively, participants H and K of Example 4.5. The gateway embeddings $\Gamma_{H,K}(M, -)$ and $\Gamma_{K,H}(M', -)$ map, respectively, the states of $M$ and $M'$ as indicated below by the dotted edges.
<table><caption>Table 2: Main notations</caption><thead><tr><td>Notation</td><td>Meaning</td><td>Introduced in</td></tr></thead><tbody><tr><td>M<sub>A</sub></td><td>A-local τ-CFSM</td><td>Definition 3.1</td></tr><tr><td>p, q, ...</td><td>states of a τ-CFSM</td><td>Intro Section 3</td></tr><tr><td>S, S', ...</td><td>systems of τ-CFSMs</td><td>Definition 3.2</td></tr><tr><td>s, s', ...</td><td>configurations of a system</td><td>Definition 3.3</td></tr><tr><td>[[S]]</td><td>S's op. semantics (an FSA)</td><td>Definition 3.3</td></tr><tr><td>R([S])</td><td>S's reachable configurations</td><td>Intro Section 3</td></tr><tr><td>gw(M, K)</td><td>gateway towards K of the τ-CFSM M</td><td>Definition 4.1</td></tr><tr><td>S<sub>1</sub><sup>H*K</sup>S<sub>2</sub></td><td>composition via H and K of S<sub>1</sub> and S<sub>2</sub></td><td>Definition 4.3</td></tr><tr><td>q&asymp;q'</td><td>compatible states</td><td>Definition 4.6</td></tr><tr><td>H<sub>K</sub>|s (s|<sub>H</sub>)</td><td>left(right)-projection of s</td><td>Definition 5.1</td></tr><tr><td>&Gamma;<sub>H,K</sub>(M, p)</td><td>gateway embedding of the state p of M</td><td>Definition 5.6</td></tr></tbody></table>

edges.

<figure><img src="image_27.png" /></figure>

<figure><img src="image_28.png" /></figure>

The notion of gateway embedding is similar to configuration projection (but for considering a single state instead of a whole configuration); a main change is that, when gw(M<sub>H</sub>, K) receives a message from its own system S<sub>1</sub> going to some fresh state q'', the gateway embedding Γ<sub>H,K</sub> maps q'' to the previous state since S<sub>2</sub>, and K in particular, are not yet aware of the transition. Instead configuration projection maps it to the next state, since the rest of S<sub>1</sub> is aware of the transition but gw(M<sub>H</sub>, K) will complete the transition only in the next state. Thus, gateway embeddings are designed to establish a correspondence with the other system as shown by the next proposition (whose proof is in Appendix A). Roughly, we show that by left/right-projecting a reachable configuration of a composed system, we get reachable configurations in the component systems. Moreover, these latter are compatible. For convenience Table 2 recaps the main notations introduced so far and used below.
**Proposition 5.9.** Let $S_1$ and $S_2$ be two (H, K)-composable communicating systems or $\tau$!-systems. If $s \in \mathcal{R}(\llbracket S_1^{\mathbf{H}*\mathbf{K}} S_2 \rrbracket)$ then $s \upharpoonright_K \llbracket H \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$, $s \downarrow_H^K \in \mathcal{R}(\llbracket S_2 \rrbracket)$, and $\Gamma_{H,K}(S_1(H), s(H))$ and $\Gamma_{K,H}(S_2(K), s(K))$ are compatible (cf. Definition 4.6).

## 6. What does Composability Buy Us?

Composition via gateways does ensure the preservation of deadlock freedom assuming composability of $\tau$!-systems. This follows since the reachable configurations of $S_1^{\mathbf{H}*\mathbf{K}} S_2$ can be projected on reachable configurations of $S_1$ and $S_2$. This will imply that a deadlock in $S_1^{\mathbf{H}*\mathbf{K}} S_2$ corresponds to a deadlock in $S_1$ or in $S_2$.

This fact in turn will be obtained using the following proposition, whose proof will be provided in Appendix B. Roughly, it states that if a projection of a system composed of deadlock-free subsystems can move then also the composed system moves.

**Proposition 6.1** (Weak lifting of $\tau$!-systems). Let $S_1$ and $S_2$ be two (H, K)-composable and deadlock-free $\tau$!-systems and let $S = S_1^{\mathbf{H}*\mathbf{K}} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$ if $s \upharpoonright_K \llbracket H \rrbracket \to s \downarrow_H^K \to$ then $s \to$.

**Theorem 6.2** (Deadlock freedom preservation for $\tau$!-systems). Let $S_1$ and $S_2$ be two (H, K)-composable and deadlock-free $\tau$!-systems. The composed $\tau$!-system $S_1^{\mathbf{H}*\mathbf{K}} S_2$ is deadlock-free.

*Proof.* We show that if the composed $\tau$!-system $S_1^{\mathbf{H}*\mathbf{K}} S_2$ reaches a deadlock configuration $s$ then at least one of $s \upharpoonright_K \llbracket H \rrbracket$ and $s \downarrow_H^K$ is a deadlock. This descends immediately from the fact that if $s \in \mathcal{R}(\llbracket S_1^{\mathbf{H}*\mathbf{K}} S_2 \rrbracket)$ enables a participant in $S_1^{\mathbf{H}*\mathbf{K}} S_2$ then $s \upharpoonright_K \llbracket H \rrbracket$ or $s \downarrow_H^K$ enable one of their participants (cf. Proposition B.1) once we show that

$$s \not\to \upharpoonright_K \llbracket H \rrbracket s \not\to \text{ and } s \downarrow_H^K \not\to$$

This can be obtained as the contrapositive of Proposition 6.1 □

**Example 6.3.** We can infer deadlock-freedom of the $\tau$!-system $S = S_1^{\mathbf{H}*\mathbf{K}} S_2$ of Example 4.5 by the result above, since $S_1$ and $S_2$ are (H, K)-composable and deadlock-free.

We turn now our attention to strong lock-freedom. In this case, as for deadlock freedom, (H, K)-composability suffices for preservation under composition; we shall see that this is not the case for lock freedom preservation.

**Theorem 6.4** (Strong lock freedom preservation for $\tau$!-systems). Let $S_1$ and $S_2$ be two (H, K)-composable and strongly lock free $\tau$!-systems. The composed $\tau$!-system $S = S_1^{\mathbf{H}*\mathbf{K}} S_2$ is strongly lock free.

*Proof.* Let $X$ be a participant enabled in a reachable configuration $s \in \mathcal{R}(\llbracket S \rrbracket)$ of $S$. Without loss of generality, we can assume $X \in \text{ptp}(S_1)$. By contradiction, let $\psi$ be a maximal fair run starting from $s$ not involving $X$ and let $s(X) \xrightarrow{\lambda} q$ be a transition of $S(X)$. Necessarily, $H, K \in \text{ptp}(\lambda)$ otherwise by strong lock freedom of $S_1$ and fairness there would be transitions on $\psi$ involving the participants of $\lambda$ contrary to our hypothesis. Notice that if $\lambda$ is an output from $H$ towards $S_1$ then the transformation to gateway turns an internal choice of $H$ (due to $\tau$ transitions) to a choice of $K$ due to the $H-K$ interactions. However, in both cases strong lock freedom applies to all the possible options of the choice, hence we can appeal to the strong lock freedom of $S_1$ for each of them.

Hence, either of the following cases is possible:

* $\lambda = H \to K$: m. The gateway $gw(M_K, H)$ has an input enabled from $H$ in $S(K)$; by Proposition 5.9 each input from $S(K)$ is matched by an output of $S(H)$ (possibly after a $\tau$-transition) of $gw(M_H, K)$ and, by fairness of $\psi$, there should be a transition on $\psi$ involving $H$.

* $\lambda = K \to H$: m. By Proposition 5.9 each input from $S(H)$ is matched by an output of $S(K)$ (possibly after a $\tau$-transition) of $gw(M_K, H)$ and, by fairness of $\psi$, there should be a transition on $\psi$ involving $H$.

Both cases contradict the assumption that $H$ is not involved on $\psi$ and we get the thesis. □
Notice that dropping the restriction to fair runs in the definition of strong lock freedom (Definition 3.9) would falsify the above theorem, as shown in the simple following example.

**Example 6.5** (Unfair runs spoil strong lock freedom preservation). The following τ!-systems are trivially (H, K)-composable and strongly lock free.

<figure><img src="image_29.png" /></figure>

The composition of the above τ!-systems is obtained by simply putting them side by side. In such a case, if we did not restrict ourselves to fair runs in the definition of strong lock freedom, the composition would be non strongly lock free. In fact the initial configuration would be a weak lock for A by considering the (unfair) maximal infinite run where C and D keep on exchanging the message m.

The present counterexample immediately adapts to communicating systems by simply taking out the τ transitions. ◇

Turning now our attention to lock freedom, it is possible to show, by the following example, that composability is too weak a property to preserve lock freedom in the case of asymmetric synchronous interactions.

**Example 6.6** (Composability does not preserve lock-freedom for τ!-systems). Let us consider the following τ!-systems.

<figure><img src="image_30.png" /></figure>

Note that both $S_1$ and $S_2$ are lock-free and that H and K are compatible. The gateways are

<figure><img src="image_31.png" /></figure>

The initial configuration of the composed τ!-system, say $s_0$, is a lock for B since the only outgoing transition from $0 \in M_B$ could be fired only in case the transition CB!stop is enabled. However, this is impossible since A always sends message m, which is forwarded by gw($M_H$, K) towards $S_2$; hence, in $[[S_1^{H \leftrightarrow K} S_2]]$ only the following run is present:

$$ \begin{array}{lclcl} s_0 & \xrightarrow{\tau} & (1_A, 0_{gw(M_H,K)}, 0_{gw(M_K,H)}, 0_B, 0_C) \\ \frac{A \to H : m}{\tau} & \xrightarrow{\tau} & (0_A, 2_{gw(M_H,K)}, 0_{gw(M_K,H)}, 0_B, 0_C) \\ \frac{H \to K : m}{\tau} & \xrightarrow{\tau} & (0_A, 4_{gw(M_H,K)}, 0_{gw(M_K,H)}, 0_B, 0_C) \\ \frac{K \to C : m}{\dots} & \xrightarrow{\tau} & (0_A, 0_{gw(M_H,K)}, 5_{gw(M_K,H)}, 0_B, 0_C) \\ & & (0_A, 0_{gw(M_H,K)}, 1_{gw(M_K,H)}, 0_B, 0_C) \\ & & s_0 \end{array} $$
where the above shown transitions (which do not involve B) are perpetually executed, leaving no chance to B of ever firing the only outgoing transition from its initial state. ◇

Somehow surprisingly, in the symmetric case none of the properties of Definition 3.9 is preserved by composition if only composability is required.

**Example 6.7** (Symmetric synchronisation spoils communication properties). *Take the following communicating systems:*

<figure><img src="image_32.png" /></figure>

Clearly, $S_1$ and $S_2$ are $(H, K)$-composable and strongly lock-free (hence also lock- and deadlock-free). However, their composition $S_1^{H*}S_2$ reaches the following configuration (identified by the filled states):

<figure><img src="image_33.png" /></figure>

which is a deadlock (and hence the composition is neither deadlock-, nor lock-, nor strongly lock-free). In fact such configuration is reached when the gateway for K receives m, it tries to synchronise with participant B on message m while B is waiting only for x. For $S_2$ in isolation, this is not a deadlock, since B and K synchronise on x under the symmetric semantics. ◇

This example shows that deadlock freedom would not be preserved even by strengthening the notion of compatibility by disregarding our bias on inputs, like in [6, Def. 3.6]. The example above, instead, is not a counterexample in an asynchronous setting. Indeed, $S_2$ could deadlock due to the fact that K could send m without synchronising with B. Likewise, Example 6.7 does not yield a counterexample in our asymmetric setting. In fact, despite synchronicity, the $\tau$-transitions introduced to resolve internal choices (i.e., those prefixing outputs) allow $S_2$ to reach a deadlock configuration by choosing the $\tau$-transition leading to the output $KB!m$.

The following examples show that the compositionality issue is due to distributed choices, hence it also emerges in slightly different contexts than in Example 6.7.

**Example 6.8** (Distributed choices may spoil communication properties). *The composition of the deadlock-free communicating systems below is the following system:*

<figure><img src="image_34.png" /></figure>

<figure><img src="image_35.png" /></figure>
The system above can reach a deadlock, similarly to what happens in Example 6.7. In particular, the interactions A→H: m·H→K: m lead to the configuration

$$ (1_A, 0_B, 1_H, 2_K, 0_D, 0_C) $$

which is a deadlock since the system is stuck but K and D have not terminated: the former is willing to send m while the latter to receive x. However, in Example 6.7 the choice is resolved by a single participant (i.e., A in S₁ and B in S₂) while here the choices involve communications with different participants (i.e., A and B on the left and C and D on the right). ◇

**Example 6.9** (Concurrency may spoil communication properties). Take the communicating systems below

<figure><img src="image_36.png" /></figure>

Their composition is as follows:

<figure><img src="image_37.png" /></figure>

Similarly to Example 6.7, the composed communicating system deadlocks while the two communicating systems in isolation do not. In particular, after the interactions A→H: m·H→K: m·A→B: go·B→H: x the system reaches the configuration

$$ (2_A, 2_B, 1_H, 4_K, 0_D, 0_C) $$

which is a deadlock. Indeed, A and B force an order in the exchange with the gateway while C and D expect the opposite order. Hence also choices embedded in commuting diamonds are problematic. ◇

The examples above clarify that any property in the symmetric synchronous setting and lock-freedom in the asymmetric case can be preserved only under stricter conditions on interfaces than composability. In Section 8 we shall show that, by recurring to interface participants not containing choices, we can recover the missing preservation properties.

## 7. No Composability, No Party

Violating one of the conditions of Definition 4.11 may compromise the validity of Theorem 6.2 and Theorem 6.4. We first show that dropping the compatibility condition can falsify both theorems.

**Example 7.1** (Compatibility is needed). Let us consider the following τ!-systems:

<figure><img src="image_38.png" /></figure>
These $\tau$-systems trivially enjoy all the communication properties of Definition 3.9. However, H and K are not compatible, since there is no corresponding input in K for the output from H. The composition of $S_1$ and $S_2$ via H and K yields

<figure><img src="image_39.png" /></figure>

Starting from the initial configuration of $S_1^{H*}S_2$, the following transitions are possible in $[[S_1^{H*}S_2]]$

$$ (0_A, 0_H, 0_K, 0_C) \xrightarrow{\tau} (0_A, 0_H, 0_K, 1_C) \underset{C \to K: y}{\longrightarrow} (0_A, 0_H, 2_K, 2_C) \xrightarrow{\tau} (0_A, 0_H, 3_K, 2_C) \not\longrightarrow $$

where $(0_A, 0_H, 3_K, 2_C)$ is a deadlock configuration (hence also a lock and a weak lock) for $S_1^{H*}S_2$ since K wishes to send message y to H, which is instead waiting for message x.

By removing $\tau$-transitions in the above machines we immediately get a counterexample for the case of communicating systems in the symmetric synchronous case. ◇

The following example casts in our setting an example given in [3] for the asynchronous semantics. This example illustrates that Theorem 6.2 and Theorem 6.4 fail in presence of mixed states.

**Example 7.2** (Mixed-states spoil communication properties). Let

<figure><img src="image_40.png" /></figure>

The two $\tau$-systems are strongly lock free (and hence necessarily lock- and deadlock-free). Moreover, notice that the initial states are mixed and that H and K are compatible. The gateways we obtain are

<figure><img src="image_41.png" /></figure>
The composed τ!-system $S_1^{H \to K} S_2$ deadlocks when gw($S_1(H)$, K) receives from B while gw($S_2(K)$, H) receives from D since both gateways reach an output state (respectively states 10 and 7). Recall that this necessarily implies such a τ!-system to be neither lock-, strong lock- nor deadlock-free.

By removing τ-transitions in the above machines we immediately get also a counterexample for the case of communicating systems in the symmetric synchronous case. ◇

Example 7.4 below shows that !?-nondeterminism also spoils Theorems 6.2 and 6.4 by taking the composition of the two τ!-systems in Example 7.3, which features a non !?-deterministic deadlock-free τ!-system.

**Example 7.3** (Two deadlock free τ!-systems). The following two τ!-systems whose participants H and K are from Example 4.8,

<figure><img src="image_42.png" /></figure>

are deadlock free. The deadlock freedom of $S_1$ follows from the fact that, from its initial configuration $(0_A, 0_B, 0_C, 0_H)$, $S_1$ can only branch over the two τ-transitions of H reaching either of the following configurations

$$ (0_A, 0_B, 0_C, 7_H) \quad \text{or} \quad (0_A, 0_B, 0_C, 1_H) $$

From the former (resp. latter) configuration $S_1$ can only reach configurations where H synchronises with C and then with A (resp. B). In either case $S_1$ reaches the terminal configuration $(1_A, 1_B, 1_C, 6_H)$.

Let us now have a look at $S_2$. Since

* K is !?-nondeterministic since from its initial state K can reach two different states (1 and 4) by receiving message m and

* E cannot synchronise since $M_E$ does not have any transition.

the only possible transitions of $S_2$ must involve K and D only. We therefore have that

$$ \begin{align*} (0_K, 0_D, 0_E) &\xrightarrow{\tau} (0_K, 1_D, 0_E) &\xrightarrow{D \to K: m} (1_K, 2_D, 0_E) \\ &\xrightarrow{\tau} (1_K, 3_D, 0_E) &\xrightarrow{D \to K: \times} (2_K, 4_D, 0_E) \\ &\xrightarrow{\tau} (2_K, 5_D, 0_E) &\xrightarrow{D \to K: m} (3_K, 6_D, 0_E) \end{align*} $$
is the only possible execution from the initial configuration $(0_K, 0_D, 0_E)$ of $S_2$, leading to the terminal configuration $(3_K, 6_D, 0_E)$. ◇

The next example shows that the compositions of the $\tau$-systems $S_1$ and $S_2$ in Example 7.3 can reach a deadlock.

**Example 7.4** (!?-Nondeterminism spoils deadlock freedom). The $\tau$-CFSMs H and K in Example 7.3 are compatible as seen in Example 4.8. Hence, we can build the composed $\tau$-system $S_1^{H*K} S_2$ through the gateways

<figure><img src="image_43.png" /></figure>

Now, from the initial configuration of $S_1^{H*K} S_2$, say $s_0$, we have the following run

$$ \begin{array}{rcl} s_0 & \xrightarrow{\tau} & (0_A, 0_B, 0_C, 0_{gw(M_H,K)}, 0_{gw(M_K,H)}, 1_D, 0_E) \\ \xrightarrow{D \to K: m} & \xrightarrow{\tau} & (0_A, 0_B, 0_C, 0_{gw(M_H,K)}, 9_{gw(M_K,H)}, 2_D, 0_E) \\ \xrightarrow{K \to H: m} & \xrightarrow{\tau} & (0_A, 0_B, 0_C, 13_{gw(M_H,K)}, 1_{gw(M_K,H)}, 3_D, 0_E) \end{array} \tag{8} $$

$$ \begin{array}{rcl} \xrightarrow{D \to K: x} & (0_A, 0_B, 0_C, 13_{gw(M_H,K)}, 14_{gw(M_K,H)}, 4_D, 0_E) & \\ \xrightarrow{\tau} \xrightarrow{\tau} & (0_A, 0_B, 0_C, 1_{gw(M_H,K)}, 15_{gw(M_K,H)}, 5_D, 0_E) & \\ \xrightarrow{H \to A: m} & (1_A, 0_B, 0_C, 2_{gw(M_H,K)}, 15_{gw(M_K,H)}, 5_D, 0_E) & \end{array} \tag{9} $$

where the $\tau$-transition of D enables the synchronisation of $gw(M_K, H)$ and D with label $D \to K: m$ that leads the gateway in state 9 after its $\tau$-transition from state 8. Now, the two gateways can communicate and exchange message m. Due to ?!-nondeterminism of $S_1$, from state 0 gateway $gw(M_H, K)$ can move either to state 18 or to state 13. Fatally, transition (8) leads to a deadlock: after $gw(M_K, H)$ and D synchronise to exchange message x the $\tau$-system goes into a configuration from where $gw(M_H, K)$ forwards m to A and reaches the last configuration (9). This is a deadlock for $S_1^{H*K} S_2$, since none of the CFSMs can do a $\tau$-transitions, the only enabled output action is from $gw(M_K, H)$ which tries to send message x to $gw(M_H, K)$; however, $gw(M_H, K)$ can only receive message y from K and hence these actions cannot synchronise. Intuitively, the upper path of $gw(M_H, K)$ should be matched by the lower path of $gw(M_K, H)$. However, since the exchanged message is the same, the choice is actually non-deterministic, hence the wrong combination may happen, and this leads to a deadlock. By removing $\tau$-transitions in the above automata we immediately get a counterexample for the case of communicating systems in the symmetric synchronous case.

Observe that by Proposition 3.10 the reached deadlock configuration is also a (weak) lock configuration.

<figure><img src="image_44.png" /></figure>
## 8. Raise the Bet with Sequentiality and Win the Pot

As mentioned at the end of Section 6, it is possible to show that composition by gateways does preserve all the communication properties if we recur to interface participants not containing choices. We dub such participants sequential.

**Definition 8.1** (Sequential $\tau$-CFSM). A $\tau$-CFSM is sequential if each of its states has at most one outgoing transition. A participant A of a $\tau$-system S is sequential if so is S(A).

By adding the requirement of sequentiality of gateways to composability we manage to show that lock-freedom is preserved in the asymmetric case, as well as all the communication properties in the symmetric case. We note that sequentiality implies absence of mixed states and ?!-determinism, while the converse does not hold. Moreover, the problems of Examples 6.6 and 6.7 cannot happen in case we restrict to sequential gateways.

The following proposition (see Appendix C for the proof) is instrumental for the proof of lock-freedom preservation because it allows us to restructure a run by having $\tau$ steps just before the corresponding output.

**Proposition 8.2** ($\tau$ delaying). Given a $\tau$-system S, for all $s \in \mathcal{R}(\llbracket S \rrbracket)$, if $s \xrightarrow{\lambda} s'$ and $\lambda \neq \tau$ then there is $\hat{s} \in \mathcal{R}(\llbracket S \rrbracket)$ such that $\hat{s} \xrightarrow{\lambda} s$ and the sender of $\lambda$ is involved in $\hat{s} \xrightarrow{\tau} s$.

The key point in the proof of lock-freedom preservation is the construction of a run in $S_1^{\lambda*\kappa} S_2$ out of a run in either $S_1$ or $S_2$. This is obtained in Proposition 8.3 below (see Appendix C for the proof) by exploiting sequentiality and lock-freedom of $S_1$ and $S_2$ in order to guarantee the construction when the run “crosses” the gateways.

**Proposition 8.3** (Transitions lifting). Let $S_1$ and $S_2$ be two (H, K)-composable and lock-free communicating or $\tau$-systems with H and K sequential and let $S = S_1^{\lambda*\kappa} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$ and labels $\lambda$, if $\mathbb{H}_K[s \xrightarrow{\lambda} \bar{s}$ in $\llbracket S_1 \rrbracket$] then there is a configuration $\hat{s} \in \mathcal{R}(\llbracket S \rrbracket, s)$ such that $\hat{s} \xrightarrow{\lambda} s'$ and $\mathbb{H}_K[s'] = \bar{s}$.

*The same holds for the right-projection.*

We can now prove lock-freedom preservation by contradiction.

**Theorem 8.4** (Lock-freedom preservation). Let $S_1$ and $S_2$ be two (H, K)-composable and lock-free communicating or $\tau$-systems with H and K sequential. Then the composed system $S_1^{\lambda*\kappa} S_2$ is lock-free.

*Proof.* By contradiction, let us assume $S = S_1^{\lambda*\kappa} S_2$ not to be lock-free. Then there is a configuration $s \in \mathcal{R}(\llbracket S \rrbracket)$ and a participant $X \in S$ not involved in any run from $s$. Without loss of generality, we can assume $X \in S_1$. We have $\mathbb{H}_K[s \in \mathcal{R}(\llbracket S_1 \rrbracket)]$ by Proposition 5.9 and, by lock-freedom of $S_1$, $\mathbb{H}_K[s]$ cannot be a lock of $S_1$ for $X$. Hence, there exists a run

$$ \mathbb{H}_K[s \xrightarrow{\lambda_1} \hat{s}_1 \cdots \hat{s}_{n-1} \xrightarrow{\lambda_n} \hat{s}_n \qquad (10) $$

of $S_1$ with $X$ involved in $\lambda_n$. This induces a run from $s$ in $S$ involving $X$ by repeated applications of Proposition 8.3 (if $S_1$ and $S_2$ are $\tau$-systems, then by Proposition 8.2 we can safely assume run (10) to be such that each output transition is immediately preceded by the corresponding $\tau$-transition; namely the $\tau$-transition involving the sender of the output action). So $s$ reaches a configuration with a run involving $X$, which contradicts our assumption. $\square$

The fact that a composed $\tau$-system $S = S_1^{\lambda*\kappa} S_2$ enabling a participant induces one of the component $\tau$-systems $S_1$ or $S_2$ to enable one of their participants may, at a first glance, be considered trivial. However, proving this property is not completely straightforward since interfaces are transformed into gateways by our composition operation.

**Proposition 8.5** (Weak lifting of communicating systems). Let $S_1$ and $S_2$ be two (H, K)-composable and deadlock-free communicating systems with H and K sequential and let $S = S_1^{\lambda*\kappa} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$, if $\mathbb{H}_K[s] \rightarrow or s[\mathbb{H}_K] \rightarrow then s \rightarrow$.
**Proposition 8.5** together with **Proposition 8.6** below are used in the proofs of our last two theorems. More precisely, given $S = S_1^{H*}S_2$ and one of its reachable configurations, say $s$, **Proposition 8.5** shows that a transition from the left/right projection of $s$ can be lifted to a transition from $s$ itself. **Proposition 8.6** does roughly the opposite, but in a stronger way: a transition from $s$ can be put in correspondence with a transition from its left/right projection. Besides, the left/right projection of the configuration reached from $s$ is the one reached from the left/right projection of $s$. This means that transitions and projections partly commute.

**Proposition 8.6** (Reflecting interactions on sub-systems). Let $S = S_1^{H*}S_2$ be the composition of $S_1$ and $S_2$, two $(H, K)$-composable communicating systems or $\tau$-systems. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$ and $s \xrightarrow{\lambda} s'$,

i) if $\lambda = \tau$ then $(H_K]s \xrightarrow{\tau} H_K]s'$ or $H_K]s = H_K]s'$)

ii) if $\lambda \neq \tau$ then $H_K]s \xrightarrow{\lambda} H_K]s'$, or $H_K]s \xrightarrow{\tau} H_K]s'$, or else $H_K]s = H_K]s'$.

The same holds for the $\lfloor H_K \rfloor$ projection.

**Theorem 8.7** (Deadlock freedom preservation for communicating systems). Let $S_1$ and $S_2$ be two $(H, K)$-composable and deadlock-free communicating systems, where $H$ and $K$ are sequential. Then the composed communicating system $S_1^{H*}S_2$ is deadlock-free.

*Proof.* We show that if the composed communicating system $S = S_1^{H*}S_2$ reaches a deadlock configuration $s$ then at least one of $H_K]s$ and $s \lfloor_H^K$ is a deadlock. This descends immediately from the fact that if $s \in \mathcal{R}(\llbracket S \rrbracket)$ enables a participant in $S$ then $H_K]s$ or $s \lfloor_H^K$ enable one of their participants (cf. **Proposition B.1**) once we show that

$$s \not\rightarrow \Rightarrow \mathbb{H}_K]s \not\rightarrow \text{ and } s \lfloor_H^K \not\rightarrow$$

This can be obtained as the contrapositive of **Proposition 8.5**. $\square$

**Theorem 8.8** (Strong lock freedom preservation for communicating systems). Let $S_1$ and $S_2$ be two $(H, K)$-composable and strongly lock free communicating systems, with $H$ and $K$ sequential. Then the composed communicating system $S_1^{H*}S_2$ is strongly lock free.

*Proof.* By contradiction, let us assume $S = S_1^{H*}S_2$ not to be strongly lock free. This means that there are a reachable configuration $s$, a participant $X$ enabled in $s$, and a maximal run $\xi$ from $s$ not involving $X$. Without loss of generality, we can assume $X$ to be a participant of $S_1$. By repeated application of **Proposition 8.6**, there exists a run of $S_1$

$$H_K]s \xrightarrow{\lambda_1} s_1 \cdots \xrightarrow{\lambda_n} s_n \cdots \qquad (11)$$

with $X$ not involved in $\xi$. If the run (11) is infinite then it is necessarily maximal; otherwise, let $\hat{s}$ be the last configuration in (11). Then it must be $\hat{s} \not\rightarrow$ otherwise, by **Proposition 8.5**, $\xi$ would not be maximal. In both cases we get a contradiction of the hypothesis that $S_1$ is strongly lock free since we found a maximal run (11) in $S_1$ not involving $X$. $\square$

# 9. Conclusion, Related and Future Work

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, that we call gateways, connecting the systems, as investigated initially in [2, 3] for an asynchronous interaction model, namely the one of Communicating Finite State Machines (CFSMs) [4]. Relevant communication properties were shown to be preserved by the “composition-by-gateway” mechanism. The investigation on such composition method and the properties preserved by it was shifted in [6] towards synchronous
symmetric interactions. In the present paper we pushed such an investigation forward in two directions: (i) by considering other communication properties besides deadlock-freedom (the only one taken into account in [6]); (ii) by considering also an asymmetric synchronous semantics of systems, which breaks the symmetry between senders and receivers. In fact, our asymmetric semantics decouples communication from choice resolution as in standard synchronous semantics of communicating systems (and other models). This is (roughly) accomplished by simply inserting internal silent actions before outputs actions, so yielding what we dub τ!-CFSMs. We then adapted the gateway composition mechanism defined in [2, 3] to our asymmetric semantics and gave conditions for the preservation of relevant communication properties under this notion of composition. We also extended the preservation results in [6] for the symmetric synchronous semantics.

While in the symmetric case, composability is too weak a requirement for preserving any of the com-
munication properties we considered, it is enough to ensure deadlock- and lock-freedom preservation in the
asymmetric case. Notably, sequentiality is needed here for lock-freedom preservation, in both the symmetric
and asymmetric cases. Interestingly, deadlock- and strong lock-freedom preservation in the synchronous
asymmetric case do not require sequentiality of gateways, like in the symmetric case.

Intuitively, τ!-CFSMs can be looked at as the communicating automata counterpart of the τC contracts described in [17, 9]. Imposing the no-mixed state condition (roughly, absence of choices between input and output actions) on our τ!-CFSMs, turns them into the communicating automata counterpart of the processes (contracts) called “session behaviours”^5 in, e.g., [18, 19, 10]. These processes are in turn the process counterpart of (binary) session types [20]. As shown in the paper (and in [3] for asynchronous communications), the absence of mixed states is needed in order to get the preservation of properties under composition. An interesting future work is to check if our compatibility notion falls in the family of compliance relation characterised as fixed points in [21, 22].

In *contract automata* [23, 24] 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 [23, 24].

While the path of investigation above is quite homogeneous, the different analyses present some method-
ological differences. For instance, for deadlock-freedom in the case of symmetric synchronous interactions, [6]
considers also another form of composition, dubbed *semi-direct*, where one single gateway (interacting with
both the composed communicating systems) is used. It will be also worth investigating conditions different
from sequentiality guaranteeing properties preservation under composition. An interesting one is the weak
form of liveness (dubbed !-liveness) taken into account in [6], guaranteeing deadlock-freedom preservation
with symmetric synchronous interactions. Any output action of a !-live interface can be fired in some possible
evolution of the communicating system.

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

References

[1] R. Milner, A Calculus of Communicating Systems, Vol. 92 of LNCS, Springer, Berlin, 1980. doi:10.1007/3-540-10235-3

[2] F. Barbanera, U. de'Liguoro, R. Hennicker, Global types for open systems, in: M. Bartoletti, S. Knight (Eds.), ICE, Vol. 279 of EPTCS, 2018, pp. 4–20. doi:10.4204/EPTCS.279.4

[3] F. Barbanera, U. de'Liguoro, R. Hennicker, Connecting open systems of communicating finite state machines, JLAMP 109 (2019). doi:10.1016/j.jlamp.2019.07.004

[4] D. Brand, P. Zafiropulo, On communicating finite-state machines, J. ACM 30 (2) (1983) 323–342. doi:10.1145/322374.322380.

[5] F. Barbanera, I. Lanese, E. Tuosto, *On composing communicating systems*, in: C. Aubert, C. Di Giusto, L. Safina, A. Scalas (Eds.), *Proceedings 15th Interaction and Concurrency Experience, ICE 2022, Lucca, Italy, 17th June 2022*, Vol. 365 of EPTCS, 2022, pp. 53–68. doi:10.4204/EPTCS.365.4
URL https://doi.org/10.4204/EPTCS.365.4

<footnote>^5Actually different variations of this name are used in the listed references.</footnote>
[6] F. Barbanera, I. Lanese, E. Tuosto, Composing communicating systems, synchronously, in: T. Margaria, B. Steffen (Eds.), ISoLA 2020, Vol. 12476 of LNCS, Springer, 2020, pp. 39–59. doi:10.1007/978-3-030-61362-4\_3.

[7] R. De Nicola, M. Hennessy, CCS without τ's, in: TAPSOFT, Vol.1, Vol. 249 of LNCS, Springer, 1987, pp. 138–152.

[8] H. Hüttel, et al., Foundations of session types and behavioural contracts, ACM Comput. Surv. 49 (1) (2016) 3:1–3:36.
doi:10.1145/2873052.

[9] M. Bartoletti, T. Cimoli, R. Zunino, Compliance in behavioural contracts: A brief survey, in: C. Bodei, G. L. Ferrari, C. Priami (Eds.), Programming Languages with Applications to Biology and Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday, Vol. 9465 of Lecture Notes in Computer Science, Springer, 2015, pp. 103–121. doi:10.1007/978-3-319-25527-9\_9.

[10] M. Bartoletti, A. Calas, R. Zunino, A semantic deconstruction of session types, in: P. Baldan, D. Gorla (Eds.), CONCUR 2014, Vol. 8704 of LNCS, Springer, 2014, pp. 402–418. doi:10.1007/978-3-662-44584-6\_28.

[11] L. Padovani, Contract-based discovery of web services modulo simple orchestrators, Theoretical Computer Science 411 (2010) 3328–3347. doi:10.1016/j.tcs.2010.05.002.

[12] N. Francez, C. A. R. Hoare, D. J. Lehmann, W. P. de Roever, Semantics of nondeterminism, concurrency, and communication, J. Comput. Syst. Sci. 19 (3) (1979) 290–308.

[13] G. Cécé, A. Finkel, Verification of programs with half-duplex communication, I&C 202 (2) (2005) 166–190. doi:10.1016/j.ic.2005.05.006.

[14] J. Lange, E. Tuosto, N. Yoshida, From communicating machines to graphical choreographies, in: S. K. Rajamani, D. Walker (Eds.), POPL, ACM, 2015, pp. 221–232. doi:10.1145/2676726.2676964.

[15] E. Tuosto, R. Guanciale, Semantics of global view of choreographies, JLAMP 95 (2018) 17–40. doi:10.1016/j.jlamp.2017.11.002.

[16] F. Barbanera, M. Dezani-Ciancaglini, I. Lanese, E. Tuosto, Composition and decomposition of multiparty sessions, JLAMP 119 (2021) 100620. doi:10.1016/j.jlamp.2020.100620.

[17] M. Bartoletti, M. Murgia, A. Calas, R. Zunino, Verifiable abstractions for contract-oriented systems, J. Log. Algebraic Methods Program. 86 (1) (2017) 159–207. doi:10.1016/j.jlamp.2015.10.005.
URL https://doi.org/10.1016/j.jlamp.2015.10.005

[18] G. Bernardi, M. Hennessy, Modelling session types using contracts, in: Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC ’12, ACM, New York, NY, USA, 2012, pp. 1941–1946. doi:10.1145/2231936.2232097.

[19] F. Barbanera, U. de'Liguoro, Sub-behaviour relations for session-based client/server systems, MSCS 25 (6) (2015) 1339–1381. doi:10.1017/S096012951400005X.

[20] K. Honda, V. T. Vasconcelos, M. Kubo, Language primitives and type disciplines for structured communication-based programming, in: C. Hankin (Ed.), ESOP, Vol. 1381 of LNCS, Springer, 1998, pp. 22–138. doi:10.1007/BFb0053567.

[21] M. Murgia, A fixed-points based framework for compliance of behavioural contracts, J. Log. Algebraic Methods Program. 120 (2021) 100641. doi:10.1016/j.jlamp.2021.100641.
URL https://doi.org/10.1016/j.jlamp.2021.100641

[22] M. Murgia, A note on compliance relations and fixed points, in: M. Bartoletti, L. Henrio, A. Mavridou, A. Calas (Eds.), Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019, Vol. 304 of EPTCS, 2019, pp. 38–47. doi:10.4204/EPTCS.304.3.
URL https://doi.org/10.4204/EPTCS.304.3

[23] D. Basile, P. Degano, G. L. Ferrari, E. Tuosto, Playing with our CAT and communication-centric applications, in: E. Alber, I. Lanese (Eds.), FORTE, Vol. 9688 of LNCS, Springer, 2016, pp. 62–73. doi:10.1007/978-3-319-39570-8\_5.

[24] D. Basile, M. H. ter Beek, R. Pugliese, Synthesis of orchestrations and choreographies: Bridging the gap between supervisory control and coordination of services, LMCS 16 (2) (2020). doi:10.23638/LMCS-16(2:9)2020.
Appendix A. Proofs for Section 5 (Composed Systems and Their Projections)

**Proposition 5.9.** Let $S_1$ and $S_2$ be two (H,K)-composable communicating systems or $\tau$!-systems. If $s \in \mathcal{R}(\llbracket S_1^{H*K} S_2 \rrbracket)$ then $s \llbracket_H^K \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$, $s \llbracket_H^K \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$, and $\Gamma_{H,K}(S_1(H), s(H))$ and $\Gamma_{K,H}(S_2(K), s(K))$ are compatible (cf. Definition 4.6).

*Proof.* We consider the case of $\tau$!-CFSMs. The proof for CFSMs can be obtained by following the same schema, disregarding $\tau$ transitions.

Let $s_0$ be the initial configuration of $S = S_1^{H*K} S_2$ and

$$s_0 \xrightarrow{\lambda_1} s_1 \cdots s_{n-1} \xrightarrow{\lambda_n} s_n = s \qquad (A.1)$$

a run reaching $s$ from $s_0$. We proceed by induction on $n$.

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

* $s \llbracket_H^K \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$ and $s \llbracket_H^K \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$ because left- and right-projections are the initial configurations of $S_1$ and $S_2$ respectively, and

* $\Gamma_{H,K}(S_1(H), s(H))$ and $\Gamma_{K,H}(S_2(K), s(K))$ are the initial states of $S_1(H)$ and $S_2(K)$ respectively, which are compatible by hypothesis.

Let $n > 0$ and assume that the statement holds for all configurations reachable from $s_0$ in less the $n$ transitions. We have that either none of $H$ and $K$ are involved in $\lambda_n$ or that at least one of them is. In the former case, without loss of generality, assume that the involved participants are in $S_1$. Then, by construction (cf. Definition 5.1), $s \llbracket_H^K = s_{n-1} \llbracket_H^K$ and by the inductive hypothesis $s_{n-1} \llbracket_H^K \in \mathcal{R}(\llbracket S_2 \rrbracket)$. Moreover, $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$; moreover there is a transition from $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$ to $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$. Hence $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$. Besides,

$$\begin{align*}
\Gamma_{H,K}(S_1(H), s(H)) &= \Gamma_{H,K}(S_1(H), s_{n-1}(H)) && \text{because } s(H) = s_{n-1}(H) \\
&\asymp \Gamma_{K,H}(S_2(K), s_{n-1}(K)) && \text{(by the induction hypothesis)} \\
&= \Gamma_{K,H}(S_2(K), s(K)) && \text{because } s(K) = s_{n-1}(K)
\end{align*}$$

We now consider the case when at least one between $H$ and $K$ is involved in the last transition reaching $s$ and proceed by case analysis on $\lambda_n$.

$\lambda_n = \tau$ We consider only the case where $H$ is involved since the case where $K$ is involved is symmetric. By our gateway construction (cf. Definition 4.1) only one of the following two cases is possible for the transitions in $gw(S_1(H), K)$:

$$q \xrightarrow{A H? m} s_{n-1}(H) \xrightarrow{\tau} p \xrightarrow{H K! m} r \qquad (A.2)$$

$$p \xrightarrow{K H? m} s_{n-1}(H) \xrightarrow{\tau} q \xrightarrow{H A! m} r \qquad (A.3)$$

for some participant $A \neq H$ of $S_1$ and states $p, q, r$ of $gw(S_1(H), K)$. Cases (A.3) and (A.2) respectively correspond to have the transitions

$$p \xrightarrow{\tau} q \xrightarrow{H A? m} r \quad \text{and} \quad q \xrightarrow{A H? m} r$$

in the machine $S_1(H)$.

We consider the case (A.2) first since it is simpler than the other. Since $K$ is not involved in $\lambda_n$, we have that $s \llbracket_H^K = s_{n-1} \llbracket_H^K$ and hence $s \llbracket_H^K \in \mathcal{R}(\llbracket S_2 \rrbracket)$. Moreover, $s$ and $s_{n-1}$ coincide, but for the local state of $H$ and $s(H) = p$. Now, by definition of projection, $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket) = r \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$. By induction hypothesis $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_1 \rrbracket)$. So, we get $s \llbracket_K^H \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$.
Let us show compatibility. First, observe that $\Gamma_{H,K}(S_1(H), s_{n-1}(H)) \asymp \Gamma_{K,H}(S_2(K), s_{n-1}(K))$ (by the induction hypothesis). The thesis then follows by $s_{\lfloor H \rfloor} = s_{n-1} \lfloor H \rfloor$ (as observed previously), and by $\Gamma_{H,K}(S_1(H), s_{n-1}(H)) = \Gamma_{H,K}(S_1(H), s(H))$ (by definition of $\Gamma$).

Let us now consider case (A.3). By the induction hypothesis, $s_{\lfloor H \rfloor} = s_{n-1} \lfloor H \rfloor$ and $s_{n-1} \lfloor H \rfloor \in \mathcal{R}(\llbracket S_1 \rrbracket)$. Since $K$ is not involved in $\lambda_n$, we have that $s_{\lfloor H \rfloor} = s_{n-1} \lfloor H \rfloor$ and hence $s_{\lfloor H \rfloor} \in \mathcal{R}(\llbracket S_2 \rrbracket)$. Moreover, $s$ and $s_{n-1}$ do coincide, but for the local state of $H$ in $s_{n-1}$, which becomes $s(H) = q$ in $s$. By definition of projections (Definition 5.1), it immediately follows that $s_{\lfloor H \rfloor} \in \mathcal{R}(\llbracket S_1 \rrbracket)$.

To show the compatibility of the states, we first notice that the last transition in the run (A.1) must be preceded by a transition, say the $i$-th one, where the $\tau$!-CFSMs $gw(S_1(H), K)$ and $gw(S_2(K), H)$ have exchanged message $m$. We have hence that $s_i(H) = p$ and $gw(S_2(K), H)$ has a transition $s_i(K) \xrightarrow{K H^! m} s_{i+1}(K)$. By definition of gateway and $\Gamma$, there is a participant $C \in S_2$ such that $\Gamma_{K,H}(S_2(K), s_i(K)) \xrightarrow{C K^? m} s_{i+1}(K) = \Gamma_{K,H}(S_2(K), s_{i+1}(K))$. Besides, $p \asymp \Gamma_{K,H}(S_2(K), s_i(K))$ since

$$ \begin{array}{l} \Gamma_{H,K}(S_1(H), s_i(H)) \asymp \Gamma_{K,H}(S_2(K), s_i(K)) \quad \text{by the induction hypothesis} \\ \text{and } \Gamma_{H,K}(S_1(H), s_i(H)) = \Gamma_{H,K}(S_1(H), p) = p \quad \text{by definition of } \Gamma. \end{array} $$

So, from $p \xrightarrow{\tau} q \xrightarrow{H^! m} r$ and $\Gamma_{K,H}(S_2(K), s_i(K)) \xrightarrow{C H^? m} \Gamma_{K,H}(S_2(K), s_{i+1}(K))$ and the fact that $r$ is unique by ?!-determinism, $r \asymp \Gamma_{K,H}(S_2(K), s_{i+1}(K))$ by compatibility. Also, since $\Gamma_{H,K}(S_1(H), s(H)) = r$ (by definition of $\Gamma$), we have

$$ \Gamma_{H,K}(S_1(H), s(H)) \asymp \Gamma_{K,H}(S_2(K), s_{i+1}(K)) $$

We now observe that either $s(K) = s_{i+1}(K)$ or $s(K)$ is an internal state that $gw(S_2(K), H)$ reaches starting from $s_{i+1}(K)$ after having received a message from a participant of $S_2$ between the $(i+1)$-th and the last interactions in (A.1). The thesis is immediate in the first case, while in the second case, the thesis follows by observing $\Gamma_{H,K}(S_2(H), s_{i+1}(K)) = \Gamma_{K,H}(S_2(K), s(K))$ (by definition of $\Gamma$, cf. Definition 5.6).

$\lambda_n = H \to X$; m By construction, either $X = K$ or $X \neq H$ is a participant of $S_1$.

**Case X = K.** In the former case, there are participants $A \in S_1$ and $B \in S_2$ such that $gw(S_1(H), K)$ and $gw(S_2(K), H)$ respectively have the sequences of transitions

$$ p \xrightarrow{A H^? m} \tau \xrightarrow{s_{n-1}(H)} \underline{H K^! m} \xrightarrow{s(H)} \text{ and } s_{n-1}(K) \xrightarrow{H K^? m} \underline{s(K)} \xrightarrow{\tau} \underline{K B^! m} \xrightarrow{r} $$

respectively obtained through our gateway construction on the following sequences of $S_1(H)$ and $S_2(K)$

$$ p \xrightarrow{A H^? m} \tau \xrightarrow{s(H)} \text{ and } s_{n-1}(K) \xrightarrow{K B^! m} r $$

We also notice that $s_{\lfloor H \rfloor} = s_{n-1}$ but for the local states of $H$ and $K$. Now, by the induction hypothesis we have $s_{\lfloor H \rfloor} \in \mathcal{R}(\llbracket S_1 \rrbracket)$ and $s_{n-1} \lfloor H \rfloor \in \mathcal{R}(\llbracket S_2 \rrbracket)$. Also, by definition of projection (cf. Definition 5.1) $s_{\lfloor H \rfloor} = s_{n-1}(H) = s(H) = s(H)$ and $s_{n-1} \lfloor H \rfloor = s_{\lfloor H \rfloor}(K)$. This implies that $s_{\lfloor H \rfloor} \in \mathcal{R}(\llbracket S_1 \rrbracket)$ and $s_{\lfloor H \rfloor} \in \mathcal{R}(\llbracket S_2 \rrbracket)$.

To show the compatibility part, we first observe that

$$ p = \Gamma_{H,K}(S_1(H), s_{n-1}(H)) \quad \text{and} \quad \Gamma_{K,H}(S_2(K), s_{n-1}(K)) = s_{n-1}(K) $$

by definition of $\Gamma$ (cf. Definition 5.6). Therefore, $p \asymp s_{n-1}(K)$ by the inductive hypothesis. Necessarily, we have $s(H) \asymp r$ by ?!-determinism and definition of compatibility. Finally, by definition of $\Gamma$ (cf. Definition 5.6), $\Gamma_{H,K}(S_1(H), s(H)) = s(H)$ and $r = \Gamma_{K,H}(S_2(K), s(K))$ we get the thesis.

**Case X $\in S_1$.** We have $X \neq H$ by construction (cf. Definition 3.3) hence the inductive hypothesis immediately entails $s_{\lfloor H \rfloor} \in \mathcal{R}(\llbracket S_2 \rrbracket)$ since $s_{\lfloor H \rfloor} = s_{n-1} \lfloor H \rfloor$ because $K$ is not involved in $\lambda_n$. We now show the reachability of the left-projection.
By construction (cf. Definition 4.1), there is a sequence $p \xrightarrow{\tau} s_{n-1}(H) \xrightarrow{H \times !m} s(H)$ in $S_1(H)$ which yields the importing sequence

$$p \xrightarrow{K H?m} q \xrightarrow{\tau} s_{n-1}(H) \xrightarrow{H \times !m} s(H) \qquad (A.4)$$

in $gw(S_1(H), K)$. We have that $\mathbb{H}_K[s_{n-1} \in \mathcal{R}(\llbracket S_1 \rrbracket)]$ (by the inductive hypothesis). Also, since $\mathbb{H}_K[s_{n-1}(X) = s_{n-1}(X)$, necessarily $s_{n-1}(X) \xrightarrow{H \times ?m} s(X) = \mathbb{H}_K[s_{n-1}(X) \in S_1$ where the equalities hold by Definition 5.1. Hence, $\mathbb{H}_K[s_{n-1} \xrightarrow{H \to X: m} \mathbb{H}_K[s_{n-1} = \mathbb{H}_K]s$ (by Definition 3.3) shows that $\mathbb{H}_K[s \in \mathcal{R}(\llbracket S_1 \rrbracket)]$.

We now show the compatibility part. The last transition in the run (A.1) must be preceded by a transition where the gateway machines $gw(S_1(H), K)$ and $gw(S_2(K), H)$ have exchanged message $m$; let $i$ be the index of the last such transition in the run (A.4). Then, by (A.4) and !?-determinism, we also have

$$s_i(H) = p \xrightarrow{K H?m} s_{i+1}(H) = q \in gw(S_1(H), K) \quad \text{and} \quad s_i(K) \xrightarrow{K H!m} s_{i+1}(K) \in gw(S_2(K), H)$$

with $\Gamma_{H,K}(S_1(H), s_{i+1}(H)) \asymp \Gamma_{K,H}(S_2(K), s_{i+1}(K))$ by the inductive hypothesis, definition of compatibility, and !?-determinism. We now observe that, by definition of $\Gamma$,

$$\Gamma_{H,K}(S_1(H), s_{n-1}(H)) = s(H) = \Gamma_{H,K}(S_1(H), s(H))$$

Moreover, $s(K) = s_{n-1}(K)$ because $K$ is not involved in $\lambda_n$; also, either $s(K) = s_{i+1}(K)$ or it is a fresh state that $gw(S_2(K), H)$ reaches after having received a message from a participant of $S_2$ (possibly followed by a $\tau$ transition) between the $i$-th and the last interactions in (A.1). In both cases, by definition of $\Gamma$, we have that $\Gamma_{K,H}(S_2(K), s(K)) = \Gamma_{K,H}(S_2(K), s_{n-1}(K)) = s_{i+1}(K)$. Then by the induction hypothesis

$$\Gamma_{H,K}(S_1(H), s_{n-1}(H)) \asymp \Gamma_{K,H}(S_2(K), s_{n-1}(K))$$

and the equalities above imply

$$\Gamma_{H,K}(S_1(H), s(H)) = \Gamma_{H,K}(S_1(H), s_{n-1}(H)) \asymp \Gamma_{K,H}(S_2(K), s_{n-1}(K)) = \Gamma_{K,H}(S_2(K), s(K))$$

### Appendix B. Proofs for Section 6 (What does Composability Buy Us?)

The case $X = K$, that is $\lambda_n = K \to H: m$, is symmetric to the previous case and therefore omitted. So, assume that $X$ is a participant of $S_1$; note that by construction $X \neq H$ (cf. Definition 3.3). Then in $gw(S_1(H), K)$ there exists an exporting sequence $s_{n-1}(H) \xrightarrow{X \times ?m} s(H) \xrightarrow{\tau} q \xrightarrow{H K!m} r$ corresponding to a transition $s_{n-1}(H) \xrightarrow{X \times ?m} r \in S_1$. We have that $\mathbb{H}_K[s_{n-1} \in \mathcal{R}(\llbracket S_1 \rrbracket)]$ by inductive hypothesis, and so is $\mathbb{H}_K[s_{n-1} \xrightarrow{X \to H: m} \mathbb{H}_K]s$ since, by definition of left-projection, $\mathbb{H}_K[s(H) = r$. The reachability of the right-projection of $s$ immediately follows by the inductive hypothesis, since $s|_{\mathbb{H}} = s_{n-1}|_{\mathbb{H}}$.

We now show the compatibility condition. By definition, we have that

$$\Gamma_{H,K}(S_1(H), s(H)) = \Gamma_{H,K}(S_1(H), s_{n-1}(H))$$

Moreover, we necessarily have that $s(K) = s_{n-1}(K)$. Hence by the induction hypothesis,

$$\Gamma_{H,K}(S_1(H), s(H)) = \Gamma_{H,K}(S_1(H), s_{n-1}(H)) \asymp \Gamma_{K,H}(S_2(K), s_{n-1}(K)) = \Gamma_{K,H}(S_2(K), s(K))$$

The cases $\lambda_n = X \to K: m$ and $\lambda_n = K \to X: m$ are similar to the last two cases above. We conclude by noticing that the condition of absence of mixed states is actually not needed for the present proof to work. $\square$

## Appendix B. Proofs for Section 6 (What does Composability Buy Us?)

**Proposition 6.1** (Weak lifting of $\tau$?-systems). Let $S_1$ and $S_2$ be two $(H,K)$-composable and deadlock-free $\tau$?-systems and let $S = S_1 \overset{K \to K}{\rightleftharpoons} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$ if $\mathbb{H}_K[s \to s]$ or $s|_{\mathbb{H}} \to s$.
*Proof.* Without loss of generality, we show that if $\mathbb{H}_K^\lambda s \xrightarrow{\lambda}$ for a certain $\lambda$ then $s \xrightarrow{\lambda}$. We proceed by case analysis on $\lambda$ noticing that any participant involved in $\lambda$ belongs to $S_1$. Recall that, by Proposition 5.9, $\mathbb{H}_K^\lambda s \in \mathcal{R}(\llbracket S_1 \rrbracket)$.

$\lambda = \mathbf{Y} \to \mathbf{X}: m$ with $\mathbf{H} \notin \{\mathbf{X}, \mathbf{Y}\}$ Then, by Definition 5.1, we immediately get $s \xrightarrow{\lambda}$.

$\lambda = \mathbf{H} \to \mathbf{X}: m$ By the definition of the projection operation (cf. Definition 5.1), $\mathbb{H}_K^\lambda s(\mathbf{H})$ has an outgoing output transition with label $\mathbf{H}\mathbf{X}!m$ and $\mathbb{H}_K^\lambda s(\mathbf{X}) = s(\mathbf{X})$ has a corresponding input transition by hypothesis. Hence, $s \xrightarrow{\lambda}$ by Definition 3.3.

$\lambda = \mathbf{X} \to \mathbf{H}: m$ This means, by definition of synchronisation (Definition 3.3), that $\mathbb{H}_K^\lambda s(\mathbf{X}) \xrightarrow{\mathbf{X}\mathbf{H}!m} \mathbb{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m}$. Since necessarily $\mathbf{X} \neq \mathbf{K}$, we have $\mathbb{H}_K^\lambda s(\mathbf{X}) = s(\mathbf{X})$. Now, from $\mathbb{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m} \mathbb{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m}$. and Definition 5.1, we can infer that one of the following cases are possible in $S_1^{\mathbf{H}*\mathbf{K}} S_2$ for what concerns the state $s(\mathbf{H})$:

$$ (i) \mathbb{H}_K^\lambda s(\mathbf{H}) = s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m} $$

$$ (ii) s(\mathbf{H}) \xrightarrow{\tau} \mathbb{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m} \text{(since } s(\mathbf{H}) \text{ is the "pre-}\tau\text{" internal state of an exporting segment)} $$

$$ (iii) s(\mathbf{H}) \xrightarrow{\mathbb{H}_K^\lambda} \mathbb{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m} \text{(since } s(\mathbf{H}) \text{ is the "post-}\tau\text{" internal state of an importing segment)} $$

**Case (i)** We get easily the thesis. In fact, from $s(\mathbf{X}) = \mathbb{H}_K^\lambda s(\mathbf{X}) \xrightarrow{\mathbf{X}\mathbf{H}!m} \mathbf{H} \to \mathbf{X}: m$ we get $s \xrightarrow{\mathbf{X}\mathbf{H}?!m} \mathbf{H} \to \mathbf{X}: m$.

**Case (ii)** This is trivial, since, by definition of synchronous semantics (cf. Definition 3.3), we have that $s \xrightarrow{\tau} \mathbf{H} \to \mathbf{X}: m$.

**Case (iii)** In this case we have in particular that

$$ p \xrightarrow{\mathbf{Y}\mathbf{H}?!n} p' \xrightarrow{\tau} s(\mathbf{H}) \xrightarrow{\mathbb{H}_K^\lambda} \mathbb{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{X}\mathbf{H}?!m} $$

where $p = \Gamma_{\mathbf{H},\mathbf{K}}(S_1(\mathbf{H}), s(\mathbf{H}))$. Now, by Proposition 5.9, we obtain $p \asymp \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K}))$. Since in $S_1(\mathbf{H})$ we have

$$ p \xrightarrow{\mathbf{Y}\mathbf{H}?!n} \mathbb{H}_K^\lambda s(\mathbf{H}) $$

we can use the definition of compatibility to get that either

$$ \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K})) \xrightarrow{\mathbb{K}\mathbf{B}!n} \text{ or } \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K})) \xrightarrow{\tau} q \xrightarrow{\mathbb{K}\mathbf{B}!n} $$

with $p \asymp q$ for certain $\mathbf{B}$ and $q$. The former case cannot ever occur by the definition of $\Gamma$. So, let us consider the latter possibility. By definition of $\Gamma$ one of the following cases is possible

$$ \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K})) = s(\mathbf{K}) \xrightarrow{\mathbb{H}\mathbf{K}?!n} p' \xrightarrow{\tau} q \xrightarrow{\mathbb{K}\mathbf{B}!n} \qquad (\text{B.1}) $$

$$ s(\mathbf{K}) \xrightarrow{\tau} \mathbb{K}\mathbf{C}!z \xrightarrow{\mathbb{K}\mathbf{C}!z} \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K})) \qquad (\text{B.2}) $$

$$ s(\mathbf{K}) \xrightarrow{\mathbb{K}\mathbf{C}!z} \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K})) \qquad (\text{B.3}) $$

**Case (B.1)** This case is easy: we had $s(\mathbf{H}) \xrightarrow{\mathbb{H}\mathbf{K}?!n} \mathbf{H} \to \mathbf{K}: n$ by definition of synchronisation (Definition 3.3).

**Case (B.2)** The thesis descends easily since $s \xrightarrow{\tau} \mathbf{H} \to \mathbf{K}: n$ by definition of synchronisation.

**Case (B.3)** We observe that, by definition of projections, we have in particular that in $(S_1^{\mathbf{H}*\mathbf{K}} S_2)(\mathbf{K})$

$$ s_{\mathbf{H}}^{\mathbb{K}}(\mathbf{K}) \xrightarrow{\mathbb{H}\mathbf{K}?!z} p'_{2} \xrightarrow{\tau} s(\mathbf{K}) \xrightarrow{\mathbb{K}\mathbf{C}!z} $$

for a certain $p'_2$. Moreover, we observe that, again by definition of projection, in $S_2(\mathbf{K})$ we have

$$ s_{\mathbf{H}}^{\mathbb{K}}(\mathbf{K}) \xrightarrow{\tau} s(\mathbf{K}) \xrightarrow{\mathbb{K}\mathbf{C}!z} $$

We now have the following cases to consider, noticing that, by the absence of mixed states, a transition of the form $s_{\mathbf{H}}^{\mathbb{K}}(\mathbf{K}) \xrightarrow{-\mathbb{K}?!} \mathbf{K} \to \mathbf{H}$ cannot occur in $S_2(\mathbf{K})$.
$s(D)|_H^K \xrightarrow{\tau} s_2$ for some participant $D \neq K$. This means that, by definition of projection, $s(D)|_H^K = s(D)$. So, by definition of synchronisation we get the thesis, namely $s \xrightarrow{\tau} $.

$s|_H^K(C) \xrightarrow{K C?z} s_2$. We easily get the thesis since, being $C \neq K$, we have $s|_H^K(C) = s(K)$ and hence $s \xrightarrow{K \to C:z} $.

Otherwise, let $\hat{s}$ be the configuration of $S_2$ such that $\hat{s}(K) = s(K)$ and $\hat{s}(X) = s|_H^K(X)$ for any $X \neq K$. So, by definition of synchronisation, $s|_H^K \xrightarrow{\tau} \hat{s}$ and hence $\hat{s} \in \mathcal{R}(\llbracket S_2 \rrbracket)$. We observe that $\hat{s}(K) \xrightarrow{K C!z} $ is the unique transition out of $\hat{s}(K)$ by definition of $\tau$!-CFSMs.<fnref n="6" /> Now, we can recur to deadlock-freedom<fnref n="7" /> of $S_2$ in order to infer that necessarily either

$\hat{s} \xrightarrow{\tau} \text{ or } \hat{s} \xrightarrow{E \to F: y} $

for some $E, F \neq K$, otherwise $\hat{s}$ would be a deadlock for $S_2$. In the first case, we have necessarily that $\hat{s}(D) \xrightarrow{\tau} $ for some $D \neq K$. So, since $\hat{s}(D) = s|_H^K(D) = s(D)$, we get $s \xrightarrow{\tau} $ and we are done. In the second case, we could have

* $E, F \neq K$. Hence, from $\hat{s}(X) = s|_H^K(X) = s(X)$ for any $X \neq K$, we get that $s \xrightarrow{E \to F: y} $ and we are done.

* $E = K, F = C$ and $y = z$. In this case, since $\hat{s}(K) = s(K)$ and $\hat{s}(X) = s|_H^K(X)$ for any $X \neq K$, we get $s \xrightarrow{K \to C: z} $ and we are done.

We conclude by observing that the two above are the only possibilities for $E, F$ and $y$, since, as previously mentioned, there is only one outgoing transition from $\hat{s}(K)$, namely $\hat{s}(K) \xrightarrow{K C!z} $.

$\lambda = \tau$ Let $X$ be the participant of $S_1$ involved in such transition.

If $X \neq H$ then $s(X) =_K^H s(X)$ by definition of projection (cf. Definition 5.1); hence $s \xrightarrow{\tau} $ by definition of synchronisation (cf. Definition 3.3).

If $X = H$ then we proceed by case analysis on the state $s(H)$ of the gateway $gw(S_1(H), K)$ in $s$. If $s(H)$ is a fresh state of an exporting or importing segment in the gateway $gw(S_1(H), K)$ with an enabled $\tau$-transition then $s \xrightarrow{\tau} $. Otherwise, one of the following cases holds:

(a) $q \xrightarrow{K H?m} q'' \xrightarrow{\tau} q' \xrightarrow{H A!m} r$ in $gw(S_1(H), K)$ for some fresh state $q''$ and $K^H s(H) \in \{q, q', r\}$

(b) $q \xrightarrow{A H?m} q' \xrightarrow{\tau} q'' \xrightarrow{H K!m} r$ in $gw(S_1(H), K)$ for some fresh states $q'$ and $q''$ and $K^H s(H) \in \{q, r\}$

where the segment in (a) is induced by the transitions $q \xrightarrow{\tau} q'$ $\xrightarrow{H A!m} r$ in $S_1(H)$ and the segment in (b) is induced by the transition $q \xrightarrow{A H?m} r$ in $S_1(H)$. Necessarily, we are either in case (a) and $^H_K s(H) = q$ or in case (b) and $^H_K s(H) = r$ otherwise $^H_K s(H) \xrightarrow{\tau} $ contrary to the hypothesis that $H$ is involved in $^H_K s$ $\xrightarrow{\tau} $. In the former case the thesis follows because $\Gamma_{H,K}(S_1(H), s(H)) \asymp \Gamma_{K,H}(S_2(K), s(K))$ (by Proposition 5.9) and therefore $s \xrightarrow{K \to H: m} $. In the other case either $s(H) = q''$ or $s(H) = r$ by definition of projection. If $s(H) = q''$ then $s \xrightarrow{H \to K: m} $ since $\Gamma_{H,K}(S_1(H), s(H)) \asymp \Gamma_{K,H}(S_2(K), s(K))$ (by Proposition 5.9). If $s(H) = r$ then the proof proceeds as in the case (a).

<figure><img src="image_45.png" /></figure>

Recall that $(H, K)$-composability requires absence of mixed states and ?!-determinism.

<footnote n="6">⁶This is essentially why we do not need the sequentiality condition that will instead be needed in Proposition 8.5, the CFSMs version of present proposition.</footnote>

<footnote n="7">⁷Notice that in the present proposition we are only expecting to find a transition out of $s$. If we had needed, instead, to use this proposition to “construct” a run of $S_1$ out of a run of $S_1 \llcorner K S_2$, we should have been able to get a transition $H \to A: m$ after the $\tau$ transition, whereas here we can only go on with a transition $H \to B: b$. Only sequentiality could guarantee that. In fact such a requirement is needed in Proposition 8.3.</footnote>
**Proposition B.1** (Enabledness in composed system implies enabledness in projections). Let $S = S_1^{H+K} S_2$ be the composition of $S_1$ and $S_2$, two $(H, K)$-composable $\tau$-systems. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$, if $s$ enables a participant $A \in S$, then $s|_K^H$ enables a participant in $S_1$ or $s|_H^K$ enables a participant in $S_2$.

*Proof.* Without loss of generality, we can assume $A \in S_1$, the case $A \in S_2$ being similar. Note that both $s|_K^H$ and $s|_H^K$ are reachable in, respectively, $S_1$ and $S_2$ by Proposition 5.9.

If $A \neq H$ then any transition of $A$ enabled in $s$ is also enabled in $s|_K^H$ since $s|_K^H(s(A)) = s(A)$ by Definition 5.1. If $A = H$, then either of the following three cases occurs:

**H has enabled an input.** Assume that the input is from $K$.

Then, by construction (Definition 5.1), $s|_K^H(s(H))$ has a $\tau$-transition enabled in $S_1(H)$.

If the input of $H$ is from a participant $B$ of $S_1$ then by construction $s|_K^H(s(H))$ has an input transition enabled in $S_1(H)$.

**H has enabled an output.** If the receiver of the output from $H$ is a participant of $S_1$ then $s$ is the internal state of an importing sequence in $s(H)$ by definition of gateway. Therefore, by configuration projection, $s|_K^H(s(H))$ either has an outgoing output or a $\tau$-transition.

If the receiver of the output from $H$ is $K$ necessarily $s(H)$ has an importing sequence

$$p \xrightarrow{B H^? m} p' \xrightarrow{\tau} s(H) \xrightarrow{H K! m} r$$

corresponding to a transition $p \xrightarrow{B H^? m} r$ where $r = s|_K^H(s(H))$. We can now appeal to Proposition 5.9 and definition of $\Gamma$ in order to get

$$p = \Gamma_{H,K}(S_1(H), s(H)) \asymp \Gamma_{K,H}(S_2(K), s(K))$$

By definition of compatibility (Definition 4.6), from $p \xrightarrow{B H^? m} r$ there is a transition in $S_2$ of the form

$$\Gamma_{K,H}(S_2(K), s(K)) \xrightarrow{K C! m} q$$

We hence get what we needed by observing that $\Gamma_{K,H}(S_2(K), s(K)) = s(K)$, in fact, $K$ is enabled in $s|_H^K$ since it has an outgoing $\tau$-transition.

**H can perform a $\tau$-transition.** Then, there is a sequence of transitions of the form $s(H) \xrightarrow{\tau} s|_K^H$ in $S$ with $X = K$ or $X \neq H$ participant of $S_1$. In the former case we can reason as in the previous case when $H$ outputs to $K$. Otherwise, $s|_K^H(s(H))$ has an enabled $\tau$-transition in $S_1(H)$ by Definition 5.1. $\square$

## Appendix C. Proofs for Section 8 (Raise the Bet with Sequentiality and Win the Pot)

**Proposition 8.2** ($\tau$ delaying). Given a $\tau$-system $S$, for all $s \in \mathcal{R}(\llbracket S \rrbracket)$, if $s \xrightarrow{\lambda} s'$ and $\lambda \neq \tau$ then there is $\hat{s} \in \mathcal{R}(\llbracket S \rrbracket)$ such that $\hat{s} \xrightarrow{\tau} s \xrightarrow{\lambda} s'$ and the sender of $\lambda$ is involved in $\hat{s} \xrightarrow{\tau} s$.

*Proof.* Let $\lambda = A \to B$: m and

$$s_0 \xrightarrow{\lambda_1} s_1 \cdots s_{n-1} \xrightarrow{\lambda_n} s_n = s \xrightarrow{\lambda} s' \qquad (C.1)$$

be a run from the initial configuration of $S$ to $s'$ passing through $s$. By the semantics of $\tau$-systems (cf. Definition 3.3) there is an index $0 \le h < n$ such that $s_h \xrightarrow{\tau} s_{h+1}$ is a $\tau$-transition involving $A$; let $i$ be the largest of such indexes. Necessarily, $s_i(A) \xrightarrow{\tau} s_{i+1}(A) \xrightarrow{A B! m} s'(A) \in S(A)$ and, for all $i+1 \le h < n$, $s_h(A) = s_{i+1}(A)$ since $A$ cannot be involved in transitions other than the last one in (C.1). Therefore, the following run exists in $\llbracket S \rrbracket$:

$$s_i \xrightarrow{\lambda_{i+1}} s'_{i+1} \cdots s'_{n-1} \xrightarrow{\lambda_n} s'_n$$

where $s'_h = s_h[A \mapsto s_i(A)]$ for all $i+1 \le h \le n$. Hence, the thesis follows by observing that $s'_n \xrightarrow{\tau} s$ with $A$ involved in the $\tau$-transition. $\square$
**Lemma C.1** (Interaction lifting). Let $S_1$ and $S_2$ be two (H, K)-composable and lock-free communicating or $\tau$-systems with H and K sequential and let $S = S_1^{\text{H}*\text{K}} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$ and interaction labels $\lambda \neq \tau$, if $\mathbb{H}_K \rfloor s \xrightarrow{\lambda} \bar{s}$ in $\llbracket S_1 \rrbracket$ then there is a configuration $\hat{s} \in \mathcal{R}(\llbracket S \rrbracket, s)$ such that $\hat{s} \xrightarrow{\lambda} s'$ and $\mathbb{H}_K \rfloor s' = \bar{s}$.

*The same holds for the right-projection.*

*Proof.* Let $\lambda = X \to Y: m$ with $X, Y \in \text{ptp}(S_1)$. For some states $q$ and $q'$,

$$ \mathbb{H}_K \rfloor s(X) \xrightarrow{X Y! m} q \in S_1(X) \quad \text{and} \quad \mathbb{H}_K \rfloor s(Y) \xrightarrow{X Y? m} q' \in S_1(Y) $$

and necessarily $\bar{s} = (\mathbb{H}_K \rfloor s)[X \mapsto q, Y \mapsto q']$ by the definition of synchronous semantics (cf. Definition 3.3). We have the following three cases depending on whether H is not or is involved in $\lambda$.

**$H \not\in \text{ptp}(\lambda)$** The left-projection operation leaves unchanged the states of non-interface machines (cf. Definition 5.1), hence $s(X) = \mathbb{H}_K \rfloor s(X)$ and $s(Y) = \mathbb{H}_K \rfloor s(Y)$. Hence $s \xrightarrow{\lambda} s'$ and we have the thesis.

**$H = X$** If the state $s(H)$ is the internal non-fresh state of an importing segment of the gateway $gw(S_1(H), K)$. Hence we have $s(H) = \mathbb{H}_K \rfloor s(H)$ and, as before, $s(Y) = \mathbb{H}_K \rfloor s(Y)$ since the left-projection operation leaves unchanged non-fresh states. The thesis follows by observing that $s \xrightarrow{\lambda} s'$ with $s' = s[X \mapsto q, Y \mapsto q']$ and, since $q$ and $q'$ are non-fresh states, we have $\mathbb{H}_K \rfloor s' = (\mathbb{H}_K \rfloor s)[X \mapsto q, Y \mapsto q'] = \bar{s}$.

For communicating systems we have to consider also the case that $s(H)$ is the starting state of an importing segment; that is $s(H) \xrightarrow{\mathbb{H} H? m} q' \in S_1(H)$. In this case, by Proposition 5.9 we have

$$ s(H) = \Gamma_{H,K}(S_1(H), s(H)) \approx \Gamma_{K,H}(S_2(K), s(K)) $$

and, by lock-freedom of $S_2$, $s$ can reach a transition $s''$ such that

$$ s'' \xrightarrow{K \to H: m} s''', \quad \mathbb{H}_K \rfloor s'' = \mathbb{H}_K \rfloor s, \quad \text{and} \quad \mathbb{H}_K \rfloor s''' = (\mathbb{H}_K \rfloor s)[H \mapsto q'] $$

Hence, $s''' \xrightarrow{\lambda} s'$ with $\mathbb{H}_K \rfloor s' = \bar{s}$.

**$H = Y$** If gateway $s(H)$ is in the starting state of an exporting segment then

$$ s(H) = \mathbb{H}_K \rfloor s(H) \quad \text{and} \quad s(X) = \mathbb{H}_K \rfloor s(X) $$

which imply $s \xrightarrow{\lambda} s'$ with $s'(H)$ the first fresh state of the exporting transition corresponding to $\mathbb{H}_K \rfloor s(H) \xrightarrow{X H? m} q \in S_1(H)$. The thesis then follows since $\mathbb{H}_K \rfloor s' = (\mathbb{H}_K \rfloor s)[H \mapsto q', X \mapsto q]$ by the definition of left-projection.

Suppose now that $s(H)$ is an internal state of an exporting segment. Then

(a) either $s(H) \xrightarrow{\tau} q'' \xrightarrow{\mathbb{H}_K! m} r$ (for $\tau$-systems only)

(b) or $s(H) \xrightarrow{\mathbb{H}_K! m} r$ (for communicating and $\tau$-systems)

In case (a), $s \xrightarrow{\tau} s[H \mapsto q'']$ and by Proposition 5.9

$$ (s[H \mapsto q'']) (K) = \Gamma_{K,H}(S_2(K), s(K)) \asymp \Gamma_{H,K}(S_1(H), q'') = \mathbb{H}_K \rfloor s(H) $$

Hence, by lock freedom of $S_2$ and the sequentiality of $S_2(K)$ we have

$$ s[H \mapsto q''] \xrightarrow{K \to H: m} \hat{s} \quad \text{with} \quad \mathbb{H}_K \rfloor \hat{s} = \mathbb{H}_K \rfloor s $$

by the definition of left-projection. This yields the thesis since $\mathbb{H}_K \rfloor s(H) \xrightarrow{X H? m} q \in S_1(H)$.

The proof in case (b) is similar to case (a) but for the fact that $s$ does not do a $\tau$-transition. $\square$

**Proposition 8.3** (Transitions lifting). Let $S_1$ and $S_2$ be two (H, K)-composable and lock-free communicating or $\tau$-systems with H and K sequential and let $S = S_1^{\text{H}*\text{K}} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$ and labels $\lambda$, if $\mathbb{H}_K \rfloor s \xrightarrow{\lambda} \bar{s}$ in $\llbracket S_1 \rrbracket$ then there is a configuration $\hat{s} \in \mathcal{R}(\llbracket S \rrbracket, s)$ such that $\hat{s} \xrightarrow{\lambda} s'$ and $\mathbb{H}_K \rfloor s' = \bar{s}$.

*The same holds for the right-projection.*
*Proof.* If $\lambda \neq \tau$ the thesis follows by Lemma C.1, hence we only have to consider $\tau$-transitions of $\tau$-systems. Let $\mathbb{H}_K[s] \xrightarrow{\tau} \bar{s}$ and $\mathbf{X}$ be the participant of $S_1$ involved in this $\tau$-transition.

If $\mathbf{X} \neq \mathbf{H}$ then there is a transition $\mathbb{H}_K[s](\mathbf{X}) = s(\mathbf{X}) \xrightarrow{\tau} q'$ in the machine $S_1(\mathbf{X})$ and $\bar{s} = (\mathbb{H}_K[s]) [\mathbf{X} \mapsto q']$; hence, $s \xrightarrow{\tau} s[\mathbf{X} \mapsto q']$ and $\mathbb{H}_K[s](s[\mathbf{X} \mapsto q']) = \bar{s}$.

When $\mathbf{X} = \mathbf{H}$ the proof is more complex. We proceed by case analysis depending on whether $s(\mathbf{H})$ is or is not an internal state of an exporting or an importing segment in $gw(S_1(\mathbf{H}), \mathbf{K})$.

**Case s(H) internal** By our gateway construction (cf. Definition 4.1), we have

<figure><img src="image_46.png" /></figure>

where the highlighted states on the left (resp. right) are those internal on an exporting (resp. importing) segment. Let us consider each possibility.

$s(\mathbf{H}) = q_1$ By definition of $\tau$-CFSMs, there are a participant $\mathbf{B} \neq \mathbf{H}$ of $S_1$ and a message $\mathbf{n}$ such that

$$r \xrightarrow{\tau} r_1 \xrightarrow{\mathbb{H}B!\mathbf{n}} r_2 \quad \text{are transitions in } S_1(\mathbf{H}).$$

and we have

$$\mathbb{H}_K[s](\mathbf{H}) = r, \quad \text{and} \quad \bar{s} = (\mathbb{H}_K[s]) [\mathbf{H} \mapsto r_1] \qquad (C.2)$$

Again by our gateway construction,

$$r \xrightarrow{\mathbb{K}H?\mathbf{n}} r'_1 \xrightarrow{\tau} r_1 \xrightarrow{\mathbb{H}B!\mathbf{n}} r_2 \quad \text{are transitions in } gw(S_1(\mathbf{H}), \mathbf{K}).} \qquad (C.3)$$

By Proposition 5.9 and the definition of gateway embedding (cf. Definition 5.6)

$$\Gamma_{\mathbb{H},\mathbb{K}}(S_1(\mathbf{H}), s(\mathbf{H})) = q \asymp \Gamma_{\mathbb{K},\mathbb{H}}(S_2(\mathbf{K}), s(\mathbf{K}))$$

Therefore, by the sequentiality of $\mathbb{K}$ and the lock freedom of $S_2$ there is a configuration $s_1 \in \mathcal{R}(\llbracket S \rrbracket, s)$ reachable from $s$ such that

$$s_1 \xrightarrow{\tau} \xrightarrow{\mathbb{H} \to \mathbb{K}: m} s'' \quad \text{where } \mathbb{H} \text{ is involved in the } \tau \text{ transition} \qquad (C.4)$$

and $\mathbb{H}_K[s''] = (\mathbb{H}_K[s]) [\mathbf{H} \mapsto r]$. Also, $\Gamma_{\mathbb{H},\mathbb{K}}(S_1(\mathbf{H}), r) \asymp \Gamma_{\mathbb{K},\mathbb{H}}(S_2(\mathbf{K}), s''(\mathbf{K}))$ (by Proposition 5.9, Equation (C.3) above and Proposition 8.2) imply

$$s'' \xrightarrow{\tau} \xrightarrow{\mathbb{K} \to \mathbb{H}: n} \hat{s} \xrightarrow{\tau} s' \quad \text{with } \mathbb{K} \text{ (resp. } \mathbb{H}) \text{ is involved in the first (resp. second) } \tau \text{ transition}$$

where $\mathbb{H}_K[s'] = \mathbb{H}_K[s''] [\mathbf{H} \mapsto r_1] = (\mathbb{H}_K[s]) [\mathbf{H} \mapsto r_1]$.

$s(\mathbf{H}) = q_2$ The proof is similar to the previous case except that, instead of Equation (C.4) above. We have $s \xrightarrow{\mathbb{H} \to \mathbb{K}: m} s''$.

$s(\mathbf{H}) = q'_1$ The thesis is immediate by the fact that $s \xrightarrow{\tau} s[\mathbf{H} \mapsto q']$ and $\mathbb{H}_K[s[\mathbf{H} \mapsto q')] = \mathbb{H}_K[s]$ since

$$\mathbb{H}_K[s](\mathbf{H}) = q, \quad \text{and} \quad \bar{s} = (\mathbb{H}_K[s]) [\mathbf{H} \mapsto q']$$

$s(\mathbf{H}) = q'$ The thesis follows vacuously because $\mathbb{H}_K[s](\mathbf{H}) = q'$ hence $\mathbb{H}_K[s]$ cannot have $\tau$-transitions involving $\mathbb{H}$.
**Case s(H) external** By our gateway construction (cf. Definition 4.1), we have

<figure><img src="image_47.png" /></figure>

where the highlighted states on the left (resp. right) are those non-internal on an exporting (resp. importing) segment. Let us consider each possibility.

**s(H) = q (exporting)** The thesis follows vacuously because $^H_K s(H) = q$ hence $^H_K s$ cannot have $\tau$-transitions involving H.

**s(H) = q (importing)** By Proposition 5.9 and the definition of gateway embedding (cf. Definition 5.6) $\Gamma_{H,K}(S_1(H), s(H)) = q \bowtie \Gamma_{K,H}(S_2(K), s(K))$. Therefore, by the sequentiality of K and the lock freedom of $S_2$ there is a reachable configuration $s'' \in \mathcal{R}(\llbracket S \rrbracket, s)$ such that

$$s'' \xrightarrow{K \to H: m} \hat{s} \xrightarrow{\tau} s'$$

where H is involved in the $\tau$ transition and $^H_K \hat{s} = (^H_K s)[H \mapsto q'] = \bar{s}$.

**s(H) = r (exporting)** By definition of $\tau$-CFSMs, there are a participant B $\neq$ H of $S_1$ and a message n such that

$$r \xrightarrow{\tau} r_1 \xrightarrow{HB!n} r_2 \quad \text{are transitions in } S_1(H)$$

and we have

$$^H_K s(H) = r, \quad \text{and} \quad \bar{s} = (^H_K s)[H \mapsto r_1] \qquad (C.5)$$

Again by our gateway construction,

$$r \xrightarrow{KH?n} r'_1 \xrightarrow{\tau} r_1 \xrightarrow{HB!n} r_2 \quad \text{are transitions in } \mathrm{gw}(S_1(H), K). \qquad (C.6)$$

By Proposition 5.9 and the definition of gateway embedding (cf. Definition 5.6)

$$\Gamma_{H,K}(S_1(H), s(H)) = r \bowtie \Gamma_{K,H}(S_2(K), s(K))$$

Therefore, by the sequentiality of K and the lock freedom of $S_2$ there is a reachable configuration $s''$ of S such that

$$s'' \xrightarrow{K \to H: n} \hat{s} \xrightarrow{\tau} s'$$

where H is involved in the $\tau$ transition and $^H_K \hat{s} = (^H_K s)[H \mapsto r'_1]$. Hence, $^H_K s' = (^H_K s)[H \mapsto r_1] = \bar{s}$.

**s(H) = r (importing)** In this case the state s(H) in the gateway $\mathrm{gw}(S_1(H), K)$ is the starting state of an importing segment and the proof goes as in the corresponding case above. $\square$

**Proposition 8.5** (Weak lifting of communicating systems). Let $S_1$ and $S_2$ be two (H,K)-composable and deadlock-free communicating systems with H and K sequential and let $S = S_1^{H*} S_2$. For all $s \in \mathcal{R}(\llbracket S \rrbracket)$, if $^H_K s \to or s^K \to then s \to$.

*Proof.* We show that for all $\lambda$, $^H_K s \xrightarrow{\lambda} s$ in $\llbracket S_1 \rrbracket$ implies $s \to s$ in $\llbracket S \rrbracket$. (The case of the right-projection is symmetric and therefore omitted.) Note that all participants involved in $\lambda$ are in $S_1$.

If H is not involved in $\lambda$ then $s \xrightarrow{\lambda} s$ since $^H_K s(X) = s(X)$ for all $X \in \mathrm{ptp}(\lambda)$ by left-projection (cf. Definition 5.1). Otherwise, H is either the sender or the receiver of $\lambda$. Recall that exporting and importing
segments correspond to input and output transitions of the interface machine $\mathbf{H}$; pictorially

<figure><img src="image_48.png" /></figure>

or

where the fresh states are highlighted and dashed arrows represent the left-projection mapping.

$s(\mathbf{H}) = q$. Since $s(\mathbf{H}) =_K^{\mathbf{H}} s(\mathbf{H})$ then $s \xrightarrow{\lambda} s(\mathbf{A}) =_K^{\mathbf{H}} s(\mathbf{A})$ by Definition 5.1.

$s(\mathbf{H}) = q'$. By Proposition 5.9, $\Gamma_{\mathbf{H},\mathbf{K}}(S_1(\mathbf{H}), s(\mathbf{H})) = q \asymp \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K}))$ therefore the current state $\mathbf{S}(\mathbf{K})$ of the gateway $\text{gw}(S_2(\mathbf{K}), \mathbf{H})$ is the starting state of an importing segment with an enabled input transition of message $\mathbf{m}$ from $\mathbf{K}$. Hence, $s \xrightarrow{\mathbf{H} \to \mathbf{K}: \mathbf{m}}$.

$s(\mathbf{H}) = r$. The proof is like in the cases $s(\mathbf{H}) = q$ or $s(\mathbf{H}) = \hat{q}$ since $r$ is the starting state of an exporting or exporting segment of the gateway $\text{gw}(S_1(\mathbf{H}), \mathbf{K})$.

$s(\mathbf{H}) = \hat{q}$. By Proposition 5.9, $\Gamma_{\mathbf{H},\mathbf{K}}(S_1(\mathbf{H}), s(\mathbf{H})) = \hat{q} \asymp \Gamma_{\mathbf{K},\mathbf{H}}(S_2(\mathbf{K}), s(\mathbf{K}))$ therefore the current state $\mathbf{S}(\mathbf{K})$ of the gateway $\text{gw}(S_2(\mathbf{K}), \mathbf{H})$ is in a state $s(\mathbf{K})$, with enabled output transitions to $\mathbf{H}$. Note that $s(\mathbf{K})$ is also a state of the interface CFSM $S_2(\mathbf{K})$ (since $s(\mathbf{K}) = s|_{\mathbf{H}}^{\mathbf{K}}(\mathbf{K})$) and that for each output transition from $s(\mathbf{K})$ in the gateway there is a corresponding input transition from $s(\mathbf{K})$ in the CFSM interface $S_2(\mathbf{K})$. By compatibility, one of such inputs should match an output from the state $\hat{q}$ of the interface CFSM $S_1(\mathbf{H})$. Correspondingly, an input from $\hat{q}$ in the gateway $\text{gw}(S_1(\mathbf{H}), \mathbf{K})$ matches an output of $s(\mathbf{K})$ in $\text{gw}(S_2(\mathbf{K}), \mathbf{H})$. By Definition 3.3, $s \xrightarrow{\mathbf{K} \to \mathbf{H}: \mathbf{n}}$ for some message $\mathbf{n}$.

$s(\mathbf{H}) = \hat{q}'$. We have $s \xrightarrow{\lambda} s(\mathbf{A}) =_K^{\mathbf{H}} s(\mathbf{A})$ by Definition 5.1.

$s(\mathbf{H}) = \hat{r}$. The proof is like in the cases $s(\mathbf{H}) = q$ or $s(\mathbf{H}) = \hat{q}$ since $r$ is the starting state of an exporting or exporting segment of the gateway $\text{gw}(S_1(\mathbf{H}), \mathbf{K})$. $\square$

**Proposition 8.6** (Reflecting interactions on sub-systems). Let $\mathbf{S} = S_1^{\mathbf{H}*\mathbf{K}} S_2$ be the composition of $S_1$ and $S_2$, two $(\mathbf{H}, \mathbf{K})$-composable communicating systems or $\tau$!-systems. For all $\mathbf{s} \in \mathcal{R}(\llbracket \mathbf{S} \rrbracket)$ and $\mathbf{s} \xrightarrow{\lambda} \mathbf{s}'$,

i) if $\lambda = \tau$ then $(\mathbf{H}_K^\lambda \mathbf{s} \xrightarrow{\tau} \mathbf{H}_K^\lambda \mathbf{s}'$ or $\mathbf{H}_K^\lambda \mathbf{s} =_K^{\mathbf{H}} \mathbf{s}'$)

ii) if $\lambda \neq \tau$ then $\mathbf{H}_K^\lambda \mathbf{s} \xrightarrow{\lambda} \mathbf{H}_K^\lambda \mathbf{s}'$, or $\mathbf{H}_K^\lambda \mathbf{s} \xrightarrow{\tau} \mathbf{H}_K^\lambda \mathbf{s}'$, or else $\mathbf{H}_K^\lambda \mathbf{s} =_K^{\mathbf{H}} \mathbf{s}'$.

The same holds for the $-\mathbf{H}_K^\lambda$ projection.

*Proof.* $\lambda = \tau$. Implication (i) applies only to $\tau$!-systems. Either $\mathbf{H}$ is not involved in the $\tau$-transition or it is. In the former case the transition occurs because, for a participant $\mathbf{A} \neq \mathbf{H}$, $s(\mathbf{A}) \xrightarrow{\tau} $ hence we get $\mathbf{H}_K^\lambda \mathbf{s} \xrightarrow{\tau} \mathbf{H}_K^\lambda \mathbf{s}'$, by definition of projection.

If $\mathbf{H}$ is involved in the $\tau$-transition, by definition of gateway (cf. Definition 4.1) and left-projection (cf. Definition 5.1), we have that

$$ \bullet q \xrightarrow{\mathbf{A}\mathbf{H}^?\mathbf{m}} s(\mathbf{H}) \xrightarrow{\tau} s'(\mathbf{H}) \xrightarrow{\mathbf{H}\mathbf{K}!\mathbf{m}} r $$

$$ \bullet \mathbf{H}_K^\lambda s(\mathbf{H}) \xrightarrow{\mathbf{K}\mathbf{H}^?\mathbf{m}} s(\mathbf{H}) \xrightarrow{\tau} s'(\mathbf{H}) \xrightarrow{\mathbf{H}\mathbf{A}!\mathbf{m}} r $$

are the only possible sequences of transitions in the gateway $\mathbf{S}(\mathbf{H})$ for some $q, r$ which are also states of the interface participant $\mathbf{H}$.
In the first case $^H_K s =^H_K s'$ because for any $X \neq H \in S_1$, $s(X) = s'(X)$. Also, by definition of projection, $^H_K s'(H) =^H_K s(H)$. In the second case we have $^H_K s'(H) = s'(H)$ which implies $^H_K s(H) \xrightarrow{\tau} ^H_K s'(H) \in S_1(H)$ which, by the synchronous semantics given in Definition 3.3, yields $^H_K s \xrightarrow{\tau} ^H_K s'$.

Assume $\lambda = Y \to X: m$. We have the following cases:

1. neither X nor Y are an interface,

2. only one between X and Y is an interface,

3. both X and Y are an interface.

In case (1) by Definition 5.1, we immediately get $^H_K s \xrightarrow{\lambda} ^H_K s'$ since the projection operation leaves unchanged the states of non-interface participants. In the other cases we can assume without loss of generality that $Y = H$; the cases where $Y = K$ are symmetric and therefore omitted.

In case (2), by our gateway construction and by the left-projection operation we have

$$ \begin{gathered} ^H_K s(H) \xrightarrow{KH?m} \tau \xrightarrow{s(H)} ^H_{X!m} \xrightarrow{s'(H)} ^H_K s'(H) \in S(H) \qquad \text{for } \tau\!\text{-systems} \\ ^H_K s(H) \xrightarrow{KH?m} ^H_{X!m} \xrightarrow{s'(H)} ^H_K s'(H) \in S(H) \qquad \text{for communicating systems} \end{gathered} $$

respectively obtained from $^H_K s(H) \xrightarrow{\tau} s(H) \xrightarrow{^H_{X!m}} ^H_K s'(H) \in S_1(H)$ or $^H_K s(H) = s(H) \xrightarrow{^H_{X!m}} ^H_K s'(H) \in S_1(H)$. Hence we get $^H_K s \xrightarrow{\tau} ^H_{X:m} \xrightarrow{^H_{X:m}} ^H_K s'$ in the former case and $^H_K s \xrightarrow{^H_{X:m}} ^H_K s'$ in the latter case.

In case (3) we have that, for a state $q \in S_1(H)$,

$$ \begin{gathered} q \xrightarrow{XH?m} \tau \xrightarrow{s(H)} ^H_{K!m} \xrightarrow{s'(H)} ^H_K s(H) = ^H_K s'(H) \in s(H) \qquad \text{for } \tau\!\text{-systems} \\ q \xrightarrow{XH?m} \tau \xrightarrow{s(H)} ^H_{K!m} \xrightarrow{s'(H)} ^H_K s(H) = ^H_K s'(H) \in s(H) \qquad \text{for communicating systems} \end{gathered} $$

Hence, in either case we get $s|_H^K = s'|_H^K$ because the projection operation leaves unchanged the states of participants $X \neq H \in S_1$. $\square$