# On the Impact of the Communication Model on Realisability

Cinzia Di Giusto, Etienne Lozes, Pascal Urso

► To cite this version:

Cinzia Di Giusto, Etienne Lozes, Pascal Urso. On the Impact of the Communication Model on Realisability. 2025. hal-05398956

HAL Id: hal-05398956

https://hal.science/hal-05398956v1

Preprint submitted on 4 Dec 2025

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 Attribution 4.0 International License
ON THE IMPACT OF THE COMMUNICATION MODEL ON
REALISABILITY

CINZIA DI GIUSTO Ⓔª, ETIENNE LOZES Ⓔ, AND PASCAL URSO

Université Côte d'Azur, CNRS, I3S, France

*e-mail address:* cinzia.di-giusto, etienne.lozes, pascal.urso@univ-cotedazr.fr

ABSTRACT. Multiparty Session Types (MPST) provide a type-theoretic foundation for specifying and verifying communication protocols in distributed systems. MPST rely on the notion of global type which specifies the global behaviour and local types, which are the projections of the global behaviour onto each local participant. A central notion in MPST is realisability — whether local implementations derived from a global specification correctly realise the intended protocol under a given communication model. While realisability has been extensively studied under peer-to-peer semantics, it remains poorly understood in alternative communication models such as bag-based, causally ordered, or synchronous communications.

In this paper, we develop a unified framework for reasoning about realisability and
subtyping across a spectrum of communication models. We show that the communication
model does not impact the notion of subtyping, but that it impacts the notion of realisability.
We introduce several decision procedures for subtyping checking and realisability checking
with complexities ranging from NLOGSPACE to EXPSPACE depending on the assumptions
made on the global types, in particular depending on their complementability and the size
of a given complement.

# 1. INTRODUCTION

The design and verification of communication protocols in concurrent and distributed systems is a central concern in programming languages. A prominent formalism is Multiparty Session Types (MPST)—a type-theoretic framework that enables specification and static verification of structured interactions among multiple communicating entities [VH93, HYC08, HLV+16, YG20]. MPST define a global communication protocol that can be projected into local types for each participant, ensuring communication safety and deadlock-freedom.

In this work, we focus on the *realisability problem*, a foundational question in the theory of session types, that concerns the soundness of the projection mechanism: the realisability problem asks whether the local types obtained by projecting a global communication specification can be safely used for restricting processes interactions to the original global protocol.

This problem is central to the goal of *correct-by-construction* protocol design, as it ensures
that local implementations derived from a specification do not introduce communication
mismatches, deadlocks, or unintended behaviours. In the literature on MPST, this challenge

*Key words and phrases:* Multiparty session types, deadlock-freedom, synchronizability, message-sequence-charts.
has appeared under various names, including *implementability* and *projectability*, reflecting different on the same core issue. In this work, we adopt the term *realisability*, following the terminology introduced by Alur et al. [AEY05], to emphasise the connection with automata-theoretic approaches.

The goal of this paper is to tackle the realisability problem for a generalised class of global types, where protocols are specified as *sets of message sequence charts (MSCs)* rather than as a single linearised control flow. These sets (in the style of Alur's work) are specified via MSC graphs (deterministic finite set automata over the language of synchronous exchanges of messages). This representation naturally captures concurrency, and partial orderings of events—features common in real-world protocols. Our framework is parametric in the *communication model*, allowing us to reason uniformly across both synchronous and asynchronous settings, from the fully asynchronous model (bag), passing through FIFO models (peer-to-peer, mailbox), to fully synchronous one. Moreover, we integrate a form of semantic *subtyping*, enabling the refinement of global behaviours.

Our main contribution is the identification of a family of communication models, that we call causally-closed for which we can reduce realisability to realisability in the synchronous model, provided that the behaviours of the projection are quasi-synchronous, orphan and deadlock free. Intuitively, a communication model *com* is causally-closed if for each execution in *com* all causally equivalent (up-to permutations of causally independent actions) executions are also contained in *com*. Moreover, an execution is quasi-synchronous if it is causally equivalent to an execution where all sent messages can be immediately received. Now, it is known that realisability in the synchronous model is generally undecidable. A key insight of our work is the connection between *realisability* and a property we call *complementability*: the ability to construct a global type that captures all behaviours that are complementary (i.e., not allowed) with respect to a given global specification. It turns out that if the complement of a global type is given (or can be computed) then realisability in the synchronous model is decidable.

In the rest of the introduction we give three examples to motivate our choices and results.

## 1.1. Global Types as Automata for Real-World Protocols.
As mentioned above, we adopt the view of *global types as automata* where transitions capture exchanges between participants. This automaton-based perspective supports precise reasoning about the evolution of protocol states, accommodating branching, concurrency, and synchronisation. It is more general than the standard process-algebra approach as it admits: 1) mixed choice 2) non sender-driven choice 3) some form of parallel behaviour.

Take for instance a simplified variant of the MQTT publish/subscribe protocol. Two clients, $c_1$ and $c_2$, communicate through a multi-threaded broker. Each client may independently send a publish ($p$) message to their corresponding broker thread ($b$ or $b'$), which forwards to the other client which itself responds with an acknowledgment ($a$). When a client has finished to publish it send an end message to the broker. When all clients have finished, the broker sends a final acknowledgement and the protocol terminates. This global behaviour is depicted in Figure 1. For readability reasons, we borrow for this example a BPMN inspired notation where nodes labelled with $||$ to represent thread creation and thread joins, whereas $+$ nodes represent choices or merge of distinct branches. A similar notation has been used in [LTY15]. We can compile this formalism to finite state automata (when
<figure><img src="image_2.png" /><figcaption>FIGURE 1. The MQTT global type</figcaption></figure>

the Petri net underlying the BPMN-like process is 1-safe, or more generally bounded). We illustrate the compilation to a finite state automaton on Figure 2.

Crucially, the choice of who sends first is not centralised—either client may initiate communication at any time, and the protocol loops accordingly. More precisely, the global type is not sender-driven, as for instance the initial state of the automaton in Figure 2 offers a choice between $c_1 \xrightarrow{p} b$ and $c_2 \xrightarrow{p} b'$. This is a common pattern in real-world protocols, where multiple participants can initiate communication independently<fnref n="1" />. Despite not being *sender-driven*, this global type is *realisable* in our setting.

## 1.2. Beyond P2P Semantics: the Need for General Communication Models.
Historically, research on asynchronous MPST has predominantly focused on peer-to-peer communications. However, in practice, many systems are built on top of different communication models, such as unordered (or bag-based), mailbox-based, causally ordered, or bus-based communications. Moreover, as mentioned above the question of implementability has been generally confined to adding some constraints on the syntax of global types (e.g., sender-driven choice that admits only non-mixed choice where sends are performed from the same participant). Such constraints respond to general properties that may seem arbitrary and loosely connected to the two guarantees mentioned above: session conformance and deadlock freedom.

In this paper, we have a two-fold objective; we aim at:

(1) introducing a theory that is parametric on the communication model,

(2) weakening the constraints on global types that guarantee implementability.

<footnote n="1">¹Another example, that we will not detail here, could come from the WebSocket protocol used by Internet clients for low-latency, full-duplex communication with a server. After the initial HTTP *Upgrade* handshake, the channel becomes a persistent bidirectional byte stream. Either endpoint, the client or the server, may send a frame at any moment. The concurrency is even stronger than in MQTT: messages cross in flight, and neither side knows who will speak next.</footnote>
<figure><img src="image_3.png" /><figcaption>FIGURE 2. A subtype of the MQTT global type and its representation as an automaton.</figcaption></figure>

The communication models mentioned before form a hierarchy (see Figure 4) from more relaxed to more constrained communication models, either in terms of executions [CHNQ19], or in terms of message sequence charts [DFLL23]. Several interesting properties turn out to be monotonic in the communication model in the following sense: if a property is satisfied in a communication model, then it is preserved for more relaxed (resp. more constrained) ones. This is true, for instance, when checking for reachability of a configuration, for unspecified receptions (the first message in a queue cannot be received by its destination process), orphan messages (i.e., messages sent by a peer but never received), etc. Unfortunately, deadlock-freedom, and therefore deadlock-free realisability, are not monotonic. To better understand this, take the following two examples. First, consider an example of a global type (in standard MPST syntax) that is realisable in the peer-to-peer model but not in the mailbox one:

$$G_1 = p \xrightarrow{m_1} q; r \xrightarrow{m_2} q; \text{end.}$$

This global type is realisable in the peer-to-peer model, because the projection $p \parallel q \parallel r = !m_1 \parallel ?m_1. ?m_2 \parallel !m_2$ is deadlock-free and session conformant. However, this global type is not realisable in the mailbox model, where all incoming messages of process $q$ are stored in a unique FIFO queue, because $m_2$ could be sent and hence stored in the queue before $m_1$
<figure><img src="image_4.png" /><figcaption>FIGURE 3. The two interactions specified by G₂, and another unspecified interaction that happens in the projected system in the p2p semantics</figcaption></figure>

and cause a deadlock. Second, consider this example where the converse happens:

$$ 
\begin{aligned}
G_2 = & p \xrightarrow{m_1} q; p \xrightarrow{m_2} r; p \xrightarrow{m_3} q; q \xrightarrow{m_4} r; \text{end} \\
& + p \xrightarrow{m'_1} q; q \xrightarrow{m'_4} r; q \xrightarrow{m'_3} p; p \xrightarrow{m'_2} r; \text{end}
\end{aligned}
$$

This global type G₂ is depicted in Figure 3, it features two possible scenarios, starting either with m₁ or m'₁, (that are depicted on the left). It is not realisable in the peer-to-peer model, because the projection p || q || r also admits the interaction where p and q follow the first scenario, but r follows the second scenario, resulting in a non synchronisable interaction (also depicted in Figure 3). However, this global type is realisable in the mailbox model, because the messages sent to r are stored in a unique FIFO queue, and their order in the queue, is sufficient for r to not confuse the two scenarios. Moreover, this global type, as well as the previous one, are realisable in the synchronous communication model, where ambiguity is resolved by the message ordering.

These two examples show that realisability is not monotonic, and suggest that every new communication model should prompt the development of a new ad hoc theory of realisable global types, with its own syntactic conditions.

### 1.3. Subtyping: Protocol Flexibility and Safe Refinement.
While exact protocol descriptions are useful for specification, real systems often require adaptability—for example, to accommodate extensions, fallback behaviours, or optional features. This motivates the introduction of *subtyping*: a mechanism for safely refining global types without compromising realisability. Returning to the MQTT example, suppose we define a *subtype* of the protocol where only one client is allowed to publish, see Figure 2.

In our setting, we give a semantic definition of subtyping, based on the idea that a global type G denotes a set of executions $\mathcal{L}_{\text{exec}}^{\text{com}}(G)$ that is parameterised by a communication model com. We therefore say that G is a subtype of G' in a communication model com if $\mathcal{L}_{\text{exec}}^{\text{com}}(G) \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(G')$. However, it turns out that the communication model does not impacts our notion of subtyping essentially because global types also admit a MSC-based semantics that is agnostic of the communication model and that defines the same semantic subtyping relation.

### 1.4. Contributions.
Summing up, we make the following contributions.

* Global type subtyping is a notion that is independent of the communication model (Theorem 4.10).

* As mentioned above, deadlock-free realisability is not monotonic in the communication model; however, if a global type is deadlock-free realisable in a communication model that
contains all synchronous executions, then this global is also realisable in the synchronous model (Theorem 5.5).

* It is decidable to verify whether $G$ is a subtype of $G'$ when $G$ and $G'$ are realisable (Corollary 5.3), and more generally when $G'$ is complementable together with few extra assumptions (Theorems 5.1 and 5.2).

* We show that realisability implies complementability (Theorem 5.4), and that existing frameworks in which MPST are realisable by construction hide a complementation procedure (Theorem 4.26).

* We show that it is decidable to verify if $G$ is realisable in a communication model assuming that a complement of $G$ is provided. The problem is decidable in PSPACE for the synchronous communication model, and in EXPSPACE for p2p, bag, causal, and more generally for any causally closed, regular communication model (Theorem 5.12).

*Outline.* The paper is organised as follows: Section 2 introduces the necessary background on executions, Message Sequence Charts, communication models and communicating finite state machines. MPST, realisability and complementability are introduced in Section 3. Finally Section 5 shows our results on the reduction of realisability to the synchronous communication model based on the notion of effectively complementable global types. Section 6 concludes with some final remarks and discusses related works.

This paper extends and revises the work in [DLU25]

## 2. PRELIMINARIES

We assume a finite set of processes, sometimes also called participants $\mathbb{P} = \{p, q, \dots\}$ and a finite set of messages (labels) $\mathbb{M} = \{m, \dots\}$. We consider two kinds of actions: send actions that are of the form $!m^{p \to q}$ and are executed by process $p$ sending message $m$ to $q$; receive actions that are of the form $?m^{p \to q}$ and are executed by $q$ receiving $m$ from $p$. We write Act for the finite set $\mathbb{P} \times \mathbb{P} \times \{!, ?\} \times \mathbb{M}$ of all actions, and Act$_p$ for the set of actions that can be executed by $p$ (i.e., $!m^{p \to q}$ or $?m^{q \to p}$). We omit processes when they are clear from the context and simply write $!m$ or $?m$ for a send or receive action, respectively.

An event $\eta$ of a sequence of actions $w \in \text{Act}^*$, is an index $i$ in $\{1, \dots, \text{length}(w)\}$; $i$ is a send (resp. receive) event of $w$ if $w[i]$ is a send (resp. receive) action. We write $\text{events}_S(w)$ (resp. $\text{events}_R(w)$) for the set of send (resp. receive) events of $w$ and $\text{events}(w) = \text{events}_S(w) \cup \text{events}_R(w)$ for the set of all events of $w$. When all events are labeled with distinct actions, we identify an event with its action.

### 2.1. Automata.
We assume the standard notions of words $w \in \Sigma^*$ over a finite alphabet $\Sigma$, of deterministic finite automata (DFA) and nondeterministic finite automata (NFA); while dealing with NFA, we assume that an NFA may have $\epsilon$ transitions.

A non-deterministic finite automaton (NFA) is a tuple $\mathcal{A} = (Q, \Sigma, \delta, q_0, F)$, where $Q$ is a finite set of states, $\Sigma$ is a finite alphabet, $\delta: Q \times (\Sigma \cup \varepsilon) \times Q$ is the transition relation, $q_0 \in Q$ is the initial state, and $F \subseteq Q$ is the set of accepting states. We write $\delta^*(s, w)$ to denote the set of states $s'$ that are reachable from $s$ following a path labeled with $w$. The language accepted by $\mathcal{A}$, denoted $\mathcal{L}_{\text{words}}(\mathcal{A})$, is the set of words $w \in \Sigma^*$ such that $\delta^*(q_0, w) \cap F \neq \emptyset$.

A deterministic finite automaton (DFA) is a special case of an NFA where the transition relation $\delta$ is a partial function $\delta: Q \times \Sigma \to Q$; it is complete if the function is total.
Every DFA $\mathcal{A} = (Q, \Sigma, \delta, q_0, F)$ accepts the same language as the complete DFA $\mathcal{A}' = (Q \cup \{\perp\}, \Sigma, \delta', q_0, F)$ where $\delta'(q, a) = \perp$ whenever $\delta(q, a)$ is undefined, and $\delta'(\perp, a) = \perp$.

To every NFA $\mathcal{A} = (Q, \Sigma, \delta, q_0, F)$, one can associate a DFA $\det(\mathcal{A}) \stackrel{\text{def}}{=} (Q', \Sigma, \delta', q'_0, F')$ where $Q' = 2^Q, q'_0 = \{q_0\}, F'$ is the set of subsets of $Q$ that contain at least one accepting state, and $\delta'$ is defined such that for all $S \in Q'$ and $a \in \Sigma$, $\delta'(S, a) = \bigcup \{\delta^*(S, a) | s \in S\}$.

Given two NFAs $\mathcal{A}_1 = (Q_1, \Sigma, \delta_1, q_{0,1}, F_1)$ and $\mathcal{A}_2 = (Q_2, \Sigma, \delta_2, q_{0,2}, F_2)$, we define the product NFA

$$ \mathcal{A}_1 \otimes \mathcal{A}_2 \stackrel{\text{def}}{=} (Q_1 \times Q_2, \Sigma, \delta, (q_{0,1}, q_{0,2}), F_1 \times F_2) $$

where the transition relation $\delta$ is defined as follows:

* for all $(s_1, s_2) \in Q_1 \times Q_2$, $a \in \Sigma$, and $(s'_1, s'_2) \in Q_1 \times Q_2$, we have $((s_1, s_2), a, (s'_1, s'_2)) \in \delta$ if and only if $(s_1, a, s'_1) \in \delta_1$ and $(s_2, a, s'_2) \in \delta_2$, and

* for all $(s_1, s_2) \in Q_1 \times Q_2$ and $(s'_1, s'_2) \in Q_1 \times Q_2$, we have $((s_1, s_2), \varepsilon, (s'_1, s'_2)) \in \delta$ if and only if $(s_1, \varepsilon, s'_1) \in \delta_1$ or $(s_2, \varepsilon, s'_2) \in \delta_2$.

It holds that $\mathcal{L}_{\text{words}}(\mathcal{A}_1 \otimes \mathcal{A}_2) = \mathcal{L}_{\text{words}}(\mathcal{A}_1) \cap \mathcal{L}_{\text{words}}(\mathcal{A}_2)$.

Finally, if $\mathcal{A} = (Q, \Sigma, \delta, q_0, F)$ is a DFA, we can define its dual DFA $\text{dual}(\mathcal{A}) \stackrel{\text{def}}{=} (Q, \Sigma, \delta, q_0, Q \setminus F)$. In this case, if $\mathcal{A}$ is complete, we have $\mathcal{L}_{\text{words}}(\text{dual}(\mathcal{A})) = \Sigma^* \setminus \mathcal{L}_{\text{words}}(\mathcal{A})$.

We write $\mathcal{L}_{\text{words}}(\mathcal{A})$ for the language accepted by the NFA $\mathcal{A}$, $\det(\mathcal{A})$ for the DFA obtained by determinising an NFA $\mathcal{A}$, and $\mathcal{A}_1 \otimes \mathcal{A}_2$ for the product of two NFAs $\mathcal{A}_1$ and $\mathcal{A}_2$ such that $\mathcal{L}_{\text{words}}(\mathcal{A}_1 \otimes \mathcal{A}_2) = \mathcal{L}_{\text{words}}(\mathcal{A}_1) \cap \mathcal{L}_{\text{words}}(\mathcal{A}_2)$. We write $\hat{\mathcal{A}}$ for the NFA obtained from $\mathcal{A}$ by setting all states as accepting states. Finally, we write $\text{dual}(\mathcal{A})$ for the dual DFA of $\mathcal{A}$, where accepting states and non-accepting ones are swapped$^2$, such that $\mathcal{L}_{\text{words}}(\text{dual}(\mathcal{A})) = \Sigma^* \setminus \mathcal{L}_{\text{words}}(\mathcal{A})$.

## 2.2. Executions.
An execution is a sequence of actions where a receive action is always preceded by a unique corresponding send action, i.e., this corresponds to the intuition that no message can be received without having being sent.

**Definition 2.1 (Execution).** An execution over $\mathbb{P}$ and $\mathbb{M}$ is a pair $e = (w, \text{src})$ where $w \in \text{Act}^*$ and $\text{src} : \text{events}_R(w) \to \text{events}_S(w)$ is an injective function from receive events to send events such that for all receive event $r$ labeled with $?m^{p \to q}$, $\text{src}(r)$ is labeled with $!m^{p \to q}$ and $\text{src}(r) < r$.

When all send actions of a sequence of actions $w$ are distinct, there is at most one execution $e$ such that $w$ is the sequence of actions of $e$, and we often identify $w$ with $e$ and let $\text{src}$ be implicit.

An execution $e_1 = (w_1, \text{src}_1)$ is a prefix of an execution $e_2 = (w_2, \text{src}_2)$ if $w_1$ is a prefix of $w_2$ and $\text{src}_1$ is the restriction of $\text{src}_2$ to $\text{events}_R(w_1)$. For a set of executions $\mathcal{E}$, we write $\text{Prefixes}(\mathcal{E})$ for the set of all prefixes of the executions in $\mathcal{E}$. We say that an execution $e_2$ is a completion of an execution $e_1$ if $e_1$ is a prefix of $e_2$. The projection $\text{proj}_p(e)$ of an execution $e$ on a process $p$ is the subsequence of actions in $\text{Act}_p$. A send event $s$ is matched if there is a receive event $r$ such that $s = \text{src}(r)$. An execution $e$ is orphan-free if $\text{src}$ is surjective over the send events of $e$, i.e., all sent messages have been received.
<figure><img src="image_5.png" /><figcaption>FIGURE 4. Hierarchy of communication models, both as sets of executions and as sets of MSCs.</figcaption></figure>

**2.3. Communication Models.** A communication model defines which executions conform to some rules. They are sometimes defined operationally, based on implementation of the transport layer (like queues). In this paper, we adopt a more denotational approach, and consider that a communication model is fully determined by the set of executions it allows.

**Definition 2.2 (Communication model).** A communication model $com$ is a set $\mathcal{E}_{com}$ of executions.

The simplest communication model is the *bag communication model (bag)*, where all executions are allowed, i.e., any sent message can overtake another one, and no assumption holds on the order of message delivery. It represents the loosest degree of asynchrony.

**Definition 2.3 (bag).** $\mathcal{E}_{bag}$ is the set of all executions.

On the other side of the spectrum, in the synchronous communication model (synch), message exchanges can be thought as rendez-vous synchronisations. In other words, an execution *e* belongs to $\mathcal{E}_{synch}$ if all send events are immediately followed by their corresponding receive events.

**Definition 2.4 (synch).** An execution $e = (w, src) \in \mathcal{E}_{synch}$ if for all send event $s \in \text{events}_S(e)$, $s+1$ is a receive event of $e$ and $src(s+1) = s$.

Between these two extremes, we can find a number of communication models, with increased levels of synchrony. In the peer-to-peer communication model (p2p), messages sent by a process *p* to *q* transit over a FIFO channel that is specific to the pair (*p*, *q*): if *p* sends first $m_1$ then $m_2$ to *q*, then $m_2$ cannot overtake $m_1$ in the FIFO channel. In particular:

* if $m_1$ is not received, then $m_2$ is not received either;

* if both are received, then $m_1$ is received before $m_2$.

**Definition 2.5 (p2p).** $\mathcal{E}_{p2p}$ is the set of executions *e* such that for any two send events $s_1 =!m_1^{p \to q}$ and $s_2 =!m_2^{p \to q}$ in $\text{events}_S(e)$, with $s_1 < s_2$, one of the two holds:

* $s_2$ is unmatched, or

<footnote n="2">²possibly after introducing a sink state so as to make $\mathcal{A}$ a complete DFA</footnote>
• there exists $r_1, r_2$ such that $r_1 < r_2$, $\text{src}(r_1) = s_1$, and $\text{src}(r_2) = s_2$.

The causal communication model (causal) was introduced by Lamport [Lam78]; unlike other communication models, it is easier to define it denotationally rather than operationally, as the possible implementations of this communication model are rather subtle. Intuitively, an execution is causal (or causally ordered) if a message sent to a process *p* cannot overtake another message sent to the same process *p* causally before, even if the senders are different. We postpone the formal definition of this model as it requires some further notions (see Definition 2.11 later).

The variety of communication models is large, and we do not aim at being exhaustive here. We can mention the other FIFO-based communication models like the *bus communication model* (a single FIFO queue merging all messages), the *mailbox communication model* (a FIFO queue per process merging all incoming messages), bounded variants of these models (the FIFO queues are often bounded), communication models with errors (message loss, message duplication, message corruption), etc. Figure 4 shows a simplified hierarchy of some of these communication models (see also [EMR02, CHNQ19, DFLL23] for more refined hierarchies). Figure 5 exemplifies this hierarchy. Every example from 5b to 5f is in the corresponding communication model, but is also a counter-example for the next one in the hierarchy.

**2.4. Message Sequence Charts.** While executions correspond to a total order view of the events occurring in a system, message sequence charts (MSC) adopt a distributed, a partial order view on the events. For a tuple $M = (w_p)_{p \in \mathbb{P}}$, each $w_p \in \text{Act}_p^*$ is a sequence of actions representing the ones executed by process *p* according to some total, locally observable, order. We write $\text{events}(M)$ for the set $\{(p, i) | p \in \mathbb{P} \text{ and } 0 \le i < \text{length}(w_p)\}$. The label $\text{action}(\eta)$ of the event $\eta = (p, i)$ is the action $w_p[i]$. The event $\eta$ is a send (resp. receive) event if it is labeled with a send (resp. receive) action. We write $\text{events}_S(M)$ (resp. $\text{events}_R(M)$) for the set of send (resp. receive) events of $M$; we also write $\text{msg}(\eta)$ for the message sent or received at event $\eta$, and $\text{proc}(\eta)$ for the process executing $\eta$. Finally, we write $\eta_1 \prec_{\text{proc}} \eta_2$ if there is a process *p* and $i < j$ such that $\eta_1 = (p, i)$ and $\eta_2 = (p, j)$.

**Definition 2.6 (MSC).** An MSC over $\mathbb{P}$ and $\mathbb{M}$ is a tuple $M = ((w_p)_{p \in \mathbb{P}}, \text{src})$ where

(1) for each process $p$, $w_p \in \text{Act}_p^*$ is a finite sequence of actions;

(2) $\text{src} : \text{events}_R(M) \rightarrow \text{events}_S(M)$ is an injective function from receive events to send events such that for all receive event $\eta$ labeled with $?m^{p \rightarrow q}$, $\text{src}(\eta)$ is labeled with $!m^{p \rightarrow q}$.

For an execution $e$, $\text{msc}(e)$ is the MSC $((w_p)_{p \in \mathbb{P}}, \text{src})$ where $w_p$ is the subsequence of $e$ restricted to the actions of $p$, and $\text{src}$ is the lifting of $\text{src}_e$ to the events of $(w_p)_{p \in \mathbb{P}}$.

**Example 2.7.** MSC $M$ in Figure 5a is an MSC over $\mathbb{P} = \{p, q\}$ and $\mathbb{M} = \{m_1, m_2\}$ with $M = ((w_p, w_q), \text{src})$, $w_p = ?m_2!m_1$, $w_q = ?m_1!m_2$, $\text{src}((p, 0)) = (q, 1)$, and $\text{src}((q, 0)) = (p, 1)$. Note that there is no execution $e$ such that $M = \text{msc}(e)$ as all receptions precede the corresponding sends. On the other hand, the MSC in Figure 5c is $\text{msc}(e)$ for the execution $e = (!m_1!m_2?m_2!m_3?m_3?m_1, \text{src})$ where $\text{src}(3) = 2$, $\text{src}(5) = 2$ and $\text{src}(6) = 4$. It is the only execution that induces this MSC, but in general there might exist several executions inducing the same MSC.

For a set of processes $\mathbb{P}$, an MSC $M = ((w_p)_{p \in \mathbb{P}}, \text{src})$ is the *prefix* of another MSC $M' = ((w'_p)_{p \in \mathbb{P}}, \text{src}')$, in short $M \le_{\text{pref}} M'$, if for all $p \in \mathbb{P}$, $w_p$ is a prefix of $w'_p$ and
<figure><img src="image_6.png" /><figcaption>FIGURE 5. Examples of MSCs for various communication models. The sender of a message is at the origin of the arrow and the receiver at the destination. Unmatched send events are depicted with dashed arrows.</figcaption></figure>

$\text{src}'(e) = \text{src}(e)$ for all receive events $e$ of $M$. The concatenation of MSCs $M_1$ and $M_2$ is the MSC $M_1 \cdot M_2$ obtained by gluing vertically $M_1$ before $M_2$: formally, if $M_1 = ((w_p^1)_{p \in \mathbb{P}}, \text{src}_1)$ and $M_2 = ((w_p^2)_{p \in \mathbb{P}}, \text{src}_2)$, then $M_1 \cdot M_2 = ((w_p)_{p \in \mathbb{P}}, \text{src})$ where for all $p$, $w_p = w_p^1 \cdot w_p^2$, and $\text{src}$ is defined by $\text{src}(e) = \text{src}_i(e)$ for all receive events $e$ of $M_i$ ($i = 1, 2$).

**2.5. Happens-before relation and linearisations.** In a given MSC $M$, an event $\eta$ happens before $\eta'$, if (i) $\eta$ and $\eta'$ are events of a same process $p$ and happen in that order on the time line of $p$, or (ii) $\eta$ is send event matched by $\eta'$, or (iii) a sequence of such situations defines a path from $\eta$ to $\eta'$.

**Definition 2.8 (Happens-before relation).** Let $M$ be an MSC. The happens-before relation over $M$ is the binary relation $\prec_M$ defined as the least transitive relation over $\text{events}(M)$ such that:

* for all $p, i, j$, if $i < j$, then $(p, i) \prec_M (p, j)$, and

* for all receive events $\eta$, $\text{src}(\eta) \prec_M \eta$.

The link between executions and MSCs goes through the notion of linearisation:

**Definition 2.9 (Linearisation).** A linearisation of an MSC $M$ is a total order $\ll$ on $\text{events}(M)$ that refines $\prec_M$: for all events $\eta, \eta'$, if $\eta \prec_M \eta'$, then $\eta \ll \eta'$.

We write $\text{lin}(M)$ for the set of all linearisations of $M$. We often identify a linearisation with the execution it induces.

**Example 2.10.** Take the MSC $M$ in Figure 5g. These messages are ordered following the happens before relation: $!m_1 \prec_M ?m_1 \prec_M !m_3$, and both $!m_3$ and $!m_2$ happen before $?m_3$. Moreover, $\prec_M$ is a partial order, and $!m_1?!m_2?!m_1?!m_3?!m_3?!m_2 \in \text{lin}(M_c)$. On the other hand, consider the MSC $M$ in Figure 5a; then $\prec_{M'}$ is not a partial order, because $?m_2 \prec_{M'} !m_1 \prec_{M'} ?m_1 \prec_{M'} !m_2 \prec_{M'} ?m_2$, therefore $\text{lin}(M') = \emptyset$.

We can now formally define the causal communication model.
**Definition 2.11 (causal).** $\mathcal{E}_{\text{causal}}$ is the set of executions $e$, with $M = \text{msc}(e)$, such that for any two send events $s_1 =!m_1^{p \to q}$ and $s_2 =!m_2^{p' \to q'}$ in $\text{events}_S(e)$, if $s_1 \prec_M s_2$ and $q = q'$, then one of the two holds:

* $s_2$ is unmatched, or

* there exist $r_1, r_2$ such that $r_1 \prec_M r_2$, $\text{src}(r_1) = s_1$, and $\text{src}(r_2) = s_2$.

Given an MSC $M$, we write $\text{lin}_{\text{com}}(M)$ to denote $\text{lin}(M) \cap \mathcal{E}_{\text{com}}$; the executions of $\text{lin}_{\text{com}}(M)$ are called the linearisations of $M$ in the communication model com.

**Definition 2.12 (com-linearisable MSC).** An MSC $M$ is linearisable in a communication model com if $\text{lin}_{\text{com}}(M) \neq \emptyset$. We write $\mathcal{M}_{\text{com}}$ for the set of all MSCs linearisable in com.

**Example 2.13.** The MSC $M_b$ in Figure 5c is linearisable in p2p. It admits only one linearisation, and $\text{lin}_{\text{p2p}}(M_b) = \{!m_1!m_2?m_2!m_3?m_3?m_1\}$. However, $M_b$ is not linearisable in synch. Finally, $M_c$ in Figure 5g is linearisable in synch with

$$ \text{lin}_{\text{synch}}(M_c) = \{!m_1?m_1!m_2?m_2!m_3?m_3, !m_2?m_2!m_1?m_1!m_3?m_3\}. $$

Finally, we introduce a property that will be helpful in the next paragraph for giving an alternative characterisation of deadlock-freedom of a system of communicating finite state machines. This property states that for each execution in the communication model, if we consider the corresponding MSC then all the linearisations of such an MSC belong to the same communication model.

**Definition 2.14 (Causally-closed communication model).** A communication model com is causally-closed if for all MSCs $M$, $\text{lin}_{\text{com}}(M) \neq \emptyset$ implies that $\text{lin}_{\text{com}}(M) = \text{lin}(M)$.

Observe that not all communication models are causally closed. It is the case for p2p, but it is immediate to see that the property is not valid for synch. Take for instance MSC $M$ in Figure 5g, its linearisation $!m_1!m_2?m_1?m_2!m_3?m_3$ does not belong to $\text{lin}_{\text{synch}}(M_c)$.

**Lemma 2.15.** Let $e$ be an execution and $M = \text{msc}(e)$. Then $e$ is an execution of p2p if and only if for any two send events $s_1 =!m_1^{p \to q}$ and $s_2 =!m_2^{p \to q}$ in $\text{events}_S(e)$, with $s_1 \preceq_M s_2$, one of the two holds:

* $s_2$ is unmatched, or

* there exists $r_1, r_2$ such that $r_1 \preceq_M r_2$, $\text{src}(r_1) = s_1$, and $\text{src}(r_2) = s_2$.

*Proof.* Assume that $e$ is a p2p execution. Let $s_1 =!m_1^{p \to q}$ and $s_2 =!m_2^{p \to q}$ be two send events in $\text{events}_S(e)$ such that $s_1 \preceq_M s_2$. Then $s_1 < s_2$ in $e$, because $<$ is a linearisation of $\preceq_M$. By definition of p2p, $s_2$ is unmatched or there exists $r_1, r_2$ such that $r_1 < r_2$, $\text{src}(r_1) = s_1$, and $\text{src}(r_2) = s_2$. In the second case, $r_1 < r_2$ implies that $r_1 \preceq_M r_2$, because both $r_1$ and $r_2$ occur on the same process $q$. Conversely, assume that $e$ and $M$ satisfy the above reformulation of the definition of p2p. Let $s_1 =!m_1^{p \to q}$ and $s_2 =!m_2^{p \to q}$ be two send events in $\text{events}_S(e)$ such that $s_1 < s_2$. Then $s_1 \preceq_M s_2$ because $s_1$ and $s_2$ occur on the same process $p$. By the reformulation of the definition of p2p, $s_2$ is unmatched or there exists $r_1, r_2$ such that $r_1 \preceq_M r_2$, $\text{src}(r_1) = s_1$, and $\text{src}(r_2) = s_2$. In the second case, $r_1 \preceq_M r_2$ implies that $r_1 < r_2$ because $<$ is a linearisation of $\preceq_M$. $\square$

The following lemma gives examples of causally-closed communication models.

**Lemma 2.16.** $\mathcal{E}_{\text{p2p}}, \mathcal{E}_{\text{causal}}$, and $\mathcal{E}_{\text{bag}}$ are causally-closed.
<figure><img src="image_7.png" /><figcaption>FIGURE 6. A system of CFSMs with three processes.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>FIGURE 7. A system of CFSMs with orphan messages.</figcaption></figure>

*Proof.* It is obvious for *bag* because $\text{lin}(M) = \text{lin}_{\text{bag}}(M)$. For *causal*, it is enough to observe that the definition of *causal* (Definition 2.11) only depends on the partial order $\preceq_M$ induced by the MSC $M = \text{msc}(e)$. Let $M \in \mathcal{M}_{p2p}$ and $e$ be a linearisation of $M$. We show that $e \in \mathcal{E}_{p2p}$. By definition of $\mathcal{M}_{p2p}$, there is an execution $e' \in \mathcal{E}_{p2p}$ such that $\text{msc}(e') = M$. By Lemma 2.15, $e$ is also a *p2p* execution. $\square$

**2.6. Communicating finite state machines.** Communicating finite state machines [BZ83] are non-deterministic finite state automata (NFA), possibly with $\varepsilon$-transitions, where the alphabet is the set of actions that can be executed by the processes.

**Definition 2.17 (CFSM).** A communicating finite state machine (CFSM) is an NFA with $\varepsilon$-transitions $\mathcal{A}$ over the alphabet $\text{Act}$. A system of CFSMs is a tuple $S = (\mathcal{A}_p)_{p \in \mathbb{P}}$.

**Example 2.18.** Figure 6 depicts a system $(\mathcal{A}_p, \mathcal{A}_q, \mathcal{A}_r)$ with three processes $p, q, r$.

**Example 2.19.** Figure 7 depicts a system $(\mathcal{A}_{c1}, \mathcal{A}_q, \mathcal{A}_{c2})$ with three processes $c1, q, c2$ that models a naive message passing system. In this systems the broker $b$ passes messages that it receives from $c1$ to $c2$ and conversely. In *synch*, the system is orphan-free and deadlock-free since the broker is always able to treat all the incoming messages, whatever their order of emission. However, in *p2p*, the system is still deadlock-free, but their can be orphan messages, since all processes can be in a accepting states with a client unaware of an incoming message, e.g., after the execution $!m^{c1 \to b}?m^{c1 \to b}!m^{b \to c2}$.

**Example 2.20.** Figure 8 depicts a system $(\mathcal{A}_a, \mathcal{A}_b)$ with two processes $a, b$ exchanging messages *msg* and acknowledgements *ack*. In *synch*, the system is orphan-free and deadlock-free since only one process at a time can emit a message. Contrary to previous example 2.19,
<figure><img src="image_9.png" /><figcaption>FIGURE 8. A system of CFSMs with a deadlock.</figcaption></figure>

the acknowledgements prevents orphans, but, in p2p, the system will face a deadlock, since both processes could send msg concurrently, blocking them in acknowledgement waiting.

Given a system of CFSMs $S = (A_p)_{p \in \mathbb{P}}$, we write $\hat{S}$ for the system of CFSMs $\hat{S} = (\hat{A}_p)_{p \in \mathbb{P}}$ where all states are accepting.

**Definition 2.21** (Executions of a CFSMs in com). Given a system $S = (A_p)_{p \in \mathbb{P}}$ of CFSMs, and a communication model com, $\mathcal{L}_{\text{exec}}^{\text{com}}(S)$ is the set of executions $e \in \mathcal{E}_{\text{com}}$ such that for all $p$, $\text{proj}_p(e)$ is in $\mathcal{L}_{\text{words}}(A_p)$. We write $\mathcal{L}_{\text{msc}}^{\text{com}}(S)$ for the set $\{\text{msc}(e) \mid e \in \mathcal{L}_{\text{exec}}^{\text{com}}(S)\}$.

**Example 2.22.** Let $S = (A_p, A_q, A_r)$ be the system of CFSMs in Figure 6. Then

$$ \mathcal{L}_{\text{exec}}^{\text{com}}(S) = (\!\!\neg a\!\!\neg a\!\!\neg c\!\!\neg c+\!\!\neg a\!\!\neg a\!\!\neg b\!\!\neg b\!\!\neg d\!\!\neg d)^* $$

provided $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$.

**Remark 2.23.** Assume com is a communication model, $S$ a system of CFSMs, and $e, e' \in \mathcal{E}_{\text{com}}$ such that $\text{msc}(e) = \text{msc}(e')$. Then $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(S)$ if and only if $e' \in \mathcal{L}_{\text{exec}}^{\text{com}}(S)$. This follows from the fact that $\text{proj}_p(e) = \text{proj}_p(e')$ for all $p$.

A system is orphan-free if, whenever all machines have reached an accepting state, no message remains in transit, i.e., no message is sent but not received. All synchronous executions are orphan-free by definition.

**Definition 2.24** (Orphan-free). A system of CFSMs $S$ is orphan-free for a communication model com if for all $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(S)$, $e$ is orphan-free.

A system is deadlock-free if any partial execution can be completed to an accepting execution.

**Definition 2.25** (Deadlock-free). A system of CFSMS $S$ is deadlock-free for a communication model com if for all $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\hat{S})$, there is an execution $e' \in \mathcal{L}_{\text{exec}}^{\text{com}}(S)$ such that $e \leq_{\text{pref}} e'$.

**Remark 2.26.** A system of CFSMS $S$ is deadlock-free for com if and only if

$$ \mathcal{L}_{\text{exec}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(S)) $$

The following result shows that, for causally-closed communication models and synch, the deadlock-freedom property of a system of CFSMs can be expressed as a property on the MSCs of the system.

**Proposition 2.27** (Deadlock-freedom as an MSC property). Assume com is causally-closed (respectively, com is synch). Then a system of CFSMs $S$ is deadlock-free for com if and only if $\mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(S))$.
*Proof.* We show each implication separately.

⇒: : if $\mathcal{S}$ is deadlock-free: $\mathcal{L}_{\text{exec}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S}))$, then $\mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S}))$. For this implication, com can be any communication model. Let $M \in \mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S})$, we show that $M \in \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S}))$. By definition, there is an execution $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\hat{S})$ such that $M = \text{msc}(e)$. By hypothesis, there is a completion $e' \in \mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S})$ of $e$. By definition, $\text{msc}(e') \in \mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S})$, so $M \in \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S}))$.

⇔: : for com causally-closed: if $\mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S}))$, then $\mathcal{S}$ is deadlock-free. Let $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\hat{S})$ be an execution, we show that $e$ has a completion in $\mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S})$. By definition, $\text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S})$. By hypothesis, there is a MSC $M' \in \mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S})$ such that $\text{msc}(e) \preceq_{\text{pref}}^{\text{msc}} M'$. By definition of $\preceq_{\text{pref}}^{\text{msc}}$ on MSCs, there are two executions $e_1, e'$ such that $e_1 \leq_{\text{pref}}^{\text{msc}} e'$, $\text{msc}(e') = M'$, and $\text{msc}(e_1) = \text{msc}(e)$. Let $< \leq$ be the binary relation on events($M'$) defined as $<_{\text{def}} = <_e \cup <_1 \cup <_2$, where:

* $\eta <_1 < \eta'$ if $\eta \notin \text{events}(M)$, $\eta' \notin \text{events}(M)$ and $\eta <_{e'} \eta'$;

* $\eta <_2 \eta'$ if $\eta \in \text{events}(M)$ and $\eta' \notin \text{events}(M)$.

Note that $<_1$ and $<_2$ are transitive. We claim that $< \leq$ is also transitive. Indeed,

$$ 
\begin{align*}
\leq_e \cdot <_1 &= <_1 \\
<_1 \cdot <_2 &= <_1 \\
\leq_e \cdot <_2 &= \emptyset \\
(<_1 \cup <_2) \cdot \leq_e &= \emptyset \\
(\leq_e \cup <_2) \cdot <_1 &= \emptyset
\end{align*}
$$

Moreover, $< \leq$ is irreflexive, because $\leq_e$ is irreflexive and $<_1$ and $<_2$ are irreflexive. Let $\leq$ denote the reflexive closure of $<$. Then this is a partial order on events($M'$). By construction, $\leq$ is actually a total order on events($M'$). Finally, we claim that $\leq$ is a linearisation of $M'$, i.e., $\preceq_{M'} \leq \leq$. Indeed, assume that $\eta <_{M'} \eta'$, we show that $\eta < \eta'$:

* if $\eta \in \text{events}(M)$ and $\eta' \in \text{events}(M)$, then $\eta <_{M'} \eta'$ (as $M$ is a prefix of $M'$), hence $\eta \leq_e \eta'$ (because $e$ is a linearisation of $M$), and finally $\eta < \eta'$ by definition of $<$.

* if $\eta \notin \text{events}(M)$ and $\eta' \notin \text{events}(M)$, then $\eta \leq_{e'} \eta'$ (because $e'$ is a linearisation of $M'$), therefore $\eta <_1 \eta'$ by definition of $<_1$, and finally $\eta < \eta'$ by definition of $<$.

* if $\eta \in \text{events}(M)$ and $\eta' \notin \text{events}(M')$, then $\eta <_2 \eta'$ by definition of $<_2$, therefore $\eta < \eta'$ by definition of $<$.

Therefore, $\leq$ is a linearisation of $M'$. Let $e''$ be the execution associated to $\leq$. Then

* $e \leq_{\text{pref}} e''$ by definition of $\leq$;

* $\text{msc}(e'') = M'$ as $\leq$ is a linearisation of $M'$;

* $e'' \in \mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S})$ because $e''$ is a linearisation of $M'$, $M' \in \mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S})$, and com is causally closed by hypothesis.

Altogether, we have shown that $e$ has a completion in $\mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S})$, which ends the proof of the reverse implication.

⇔: : for com = synch: the proof is similar to previous case. We define the linearisation $\leq$ of $M'$ in the exactly same way, but we cannot use the fact that com is causally closed. Instead, we use the fact that both $<_e$ and $<_1$ are synchronous linearisations, and therefore $< \leq$ is a synchronous linearisation as the concatenation of two synchronous linearisations. $\square$
<figure><img src="image_10.png" /><figcaption>FIGURE 9. An example of a global type with three processes $p$, $q$, and $r$, and four messages $a$, $b$, $c$, and $d$.</figcaption></figure>

### 3. GLOBAL TYPES

We now introduce global types. Our definition deviates from the standard one as it allows for more liberal behaviours. For instance, we can have mixed choice, and when considering non-mixed choice we allow global types to send messages from different participants (meaning that our global types can be non sender-driven). This relaxation from the standard definitions, gives the possibility to implement some parallelism, see example in the Introduction.

In our setting, global types are automata over an alphabet that represent message exchanges that we call arrows. Such automata describe a language of MSCs. An arrow is a triple $(p, q, m) \in \mathbb{P} \times \mathbb{P} \times \mathbb{M}$ with $p \neq q$; we often write $p \xrightarrow{m} q$ instead of $(p, q, m)$, and write $\text{Arr}$ to denote the finite set of arrows.

**Definition 3.1 (Global Type).** A global type $G$ is a DFA over the alphabet $\text{Arr}$.

**Remark 3.2.** In order to make a connection with common definitions of global types, we can think of a global type as a term defined by the following grammar:

$$ G ::= \text{end} \mid p \xrightarrow{m} q; \quad G \mid G + G \mid X \mid \text{rec } X.G $$

with a few obvious syntactic restrictions to immediately get a deterministic finite state automaton.

**Example 3.3.** The global type in Figure 9 could be defined syntactically as

$$ \text{rec } X. \text{end} + p \xrightarrow{a} q; \quad (q \xrightarrow{c} p; X + q \xrightarrow{b} r; r \xrightarrow{d} p; X). $$

We quickly recall the definition of sender-driven choice.

**Definition 3.4 (Sender-driven choice).** A global type $G$ has sender-driven choices if for all state $s$ of $G$, if $p \xrightarrow{m} q$ and $p' \xrightarrow{m'} q'$ label two transitions outgoing from $s$, then $p = p'$.

**Example 3.5.** The global type in Figure 9 has sender-driven choices, as all choices are made by the sender of the message. However, the global type on Figure 2 does not have sender-driven choices, as the choice between $c_1 \xrightarrow{p} b$ and $c_2 \xrightarrow{p} b$ is made by the receiver $b$ in the initial state.

The projection of a global type $G$ on a process $p$ is the CFSM $G_p$ obtained by replacing each arrow $q \xrightarrow{m} r$ of a transitions of $G$ by the corresponding action of $p$ (either $!m^{p \to r}$ if $p = q$, or $?m^{q \to p}$ if $p = r$, or $\varepsilon$ otherwise).
**Definition 3.6 (Projected system of CFSMs).** The projected system of CFSMs, proj(G), associated to a global type G is the tuple $(G_p)_{p \in \mathbb{P}}$.

**Example 3.7.** Consider the system of CFSMs in Figure 6. This system can be obtained by projecting the global type of Figure 9.

For every system, we can associate a global type by computing its synchronous product. Let $S = (A_p)_{p \in \mathbb{P}}$ be a system of CFSMs, where $A_p = (L_p, \text{Act}_p, \delta_p, l_{0,p}, F_p)$ is the CFSM associated to process $p$. The synchronous product of $S$ is the NFA preprod($S$) = $(L, \text{Arr}, \delta, l_0, F)$, where $(L, \text{Arr}, \delta, l_0, F)$ where $L = \Pi_{p \in \mathbb{P}} L_p, l_0 = (l_{0,p})_{p \in \mathbb{P}}$, $F = \Pi_{p \in \mathbb{P}} F_p$, and $\delta$ is the transition relation defined by

* $(\vec{l}, p \xrightarrow{m} q, \vec{l}') \in \delta$ if $(l_p, !m^{p \to q}, l'_p) \in \delta_p, (l_q, ?m^{p \to q}, l'_q) \in \delta_q$, and $l'_r = l_r$ for all $r \notin \{p, q\}$, and

* $(\vec{l}, \varepsilon, \vec{l}') \in \delta$ if there is $p \in \mathbb{P}$ such that $(l_p, \varepsilon, l'_p) \in \delta_p$, and $l_q = l'_q$ for all $q \neq p$.

Note that, in general, preprod($S$) is not a global type, as it may be non-deterministic. However, one can compute its determinisation prod(G) $\stackrel{\text{def}}{=} \det(\text{preprod}(S))$ by standard powerset construction obtaining a global type.

We write exec($w$) to denote the synchronous execution coded by the sequence of arrows $w$, i.e., the execution obtained by replacing each arrow $p \xrightarrow{m} q$ of $w$ with the execution $!m^{p \to q}$. We write msc($w$) to denote the MSC msc(exec($w$)).

A global type defines a language of MSCs in two different ways, one existential and one universal. Let $\mathcal{L}_{\text{words}}(G)$ be the set of sequences of arrows $w$ accepted by $G$. Note that for $w \in \text{Arr}^*$, the function $w \mapsto \text{msc}(w)$ with $\text{msc}(w) \in \mathcal{M}_{\text{synch}}$ is not injective, as two arrows with disjoint pairs of processes commute. We write $w_1 \sim w_2$ if $\text{msc}(w_1) = \text{msc}(w_2)$, and $[w]$ for the equivalence class of $w$ wrt $\sim$. The existential MSC language $\mathcal{L}_{\text{msc}}^{\exists}(G)$ of a global type $G$ is the set of MSCs that admit at least one representation as a sequence of arrows in $\mathcal{L}_{\text{words}}(G)$, and the universal MSC language $\mathcal{L}_{\text{msc}}^{\forall}(G)$ of a global type $G$ is the set of MSCs whose representations as a sequence of arrows are all in $\mathcal{L}_{\text{words}}(G)$:

$$ \mathcal{L}_{\text{msc}}^{\exists}(G) \stackrel{\text{def}}{=} \{\text{msc}(w) \mid w \in \mathcal{L}_{\text{words}}(G)\} \qquad \mathcal{L}_{\text{msc}}^{\forall}(G) \stackrel{\text{def}}{=} \{\text{msc}(w) \mid [w] \subseteq \mathcal{L}_{\text{words}}(G)\}. $$

**Definition 3.8 (Commutation-closed).** A global type $G$ is commutation-closed if

$$ \mathcal{L}_{\text{msc}}^{\exists}(G) = \mathcal{L}_{\text{msc}}^{\forall}(G). $$

In that case, we write $\mathcal{L}_{\text{msc}}^{\exists/\forall}(G)$ for the common language.

**Example 3.9.** The global type in Figure 1 is commutation-closed. On the other hand, the global type

$$ p_1 \xrightarrow{m_1} q; p_2 \xrightarrow{m_2} q; \text{end} $$

is not commutation-closed, as the two arrows $p_1 \xrightarrow{m_1} q$ and $p_2 \xrightarrow{m_2} q$ commute, and $\mathcal{L}_{\text{msc}}^{\exists}(G) = \{\text{msc}(m_1 m_2)\}$ while $\mathcal{L}_{\text{msc}}^{\forall}(G) = \emptyset$.

**Proposition 3.10.** If $\#\mathbb{P} \le 3$, then $G$ is commutation-closed.

*Proof.* Any two arrows share at least one process and therefore do not commute. $\square$

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

The following properties/lemma will be useful in the rest of the paper. Recall that $\otimes$ is the product of NFAs, or here DFAs, mimicking language intersection over words.

**Proposition 3.11.** For all global type $G$, $\mathcal{L}_{\text{msc}}^{\forall}(G) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G) \subseteq \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G))$.
**Proof.** The first inclusion is immediate from the definitions. For the second inclusion, let $M \in \mathcal{L}_{\text{msc}}^{\exists}(G)$, we show that $M \in \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G))$. By definition of $\mathcal{L}_{\text{msc}}^{\exists}(G)$, there is a word $w \in \mathcal{L}_{\text{words}}(G)$ such that $\text{msc}(w) = M$. Let $\rho$ be an accepting run of $G$ for $w$. For every $p \in \mathbb{P}$, let $\rho_p$ denote the run of $G_p$ (the machine of $p$ in $\text{proj}(G)$) obtained by projecting $\rho$: note that we kept $\varepsilon$ transitions in $G_p$, see Definition 3.6, so $\rho_p$ is obviously defined. Then $\rho_p$ is an accepting run of $G_p$, therefore $M \in \mathcal{L}_{\text{msc}}^{\text{synch}}(G)$ (by Definition 2.21). $\square$

**Lemma 3.12.** Let $G_1$ and $G_2$ be two global types, with $G_2$ commutation-closed. Then

$$ \mathcal{L}_{\text{msc}}^{\exists}(G_1 \otimes G_2) = \mathcal{L}_{\text{msc}}^{\exists}(G_1) \cap \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\forall}}(G_2). $$

**Proof.** We reason by double inclusion.

⇒ Assume that $M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1 \otimes G_2)$. By definition, there is a word $w$ such that $M = \text{msc}(w)$, and $w \in \mathcal{L}_{\text{words}}(G_1 \otimes G_2)$. By the definition of the product of global types, $\mathcal{L}_{\text{words}}(G_1 \otimes G_2) = \mathcal{L}_{\text{words}}(G_1) \cap \mathcal{L}_{\text{words}}(G_2)$. In particular, $w \in \mathcal{L}_{\text{words}}(G_1)$, thus $\text{msc}(w) \in \mathcal{L}_{\text{msc}}^{\exists}(G_1)$. Similarly, $w \in \mathcal{L}_{\text{words}}(G_2)$, thus $\text{msc}(w) \in \mathcal{L}_{\text{msc}}^{\exists}(G_2)$. Since $G_2$ is commutation-closed, $\text{msc}(w) \in \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\forall}}(G_2)$. Therefore, $\text{msc}(w) \in \mathcal{L}_{\text{msc}}^{\exists}(G_1) \cap \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\forall}}(G_2)$.

⇔ Conversely, assume that $M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1) \cap \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\forall}}(G_2)$. In particular, $M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1)$, which means that there is a word $w_1$ such that $M = \text{msc}(w_1)$ and $w_1 \in \mathcal{L}_{\text{words}}(G_1)$. Since $M \in \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\forall}}(G_2)$, there is a word $w_2$ such that $M = \text{msc}(w_2)$ and $w_2 \in \mathcal{L}_{\text{words}}(G_2)$. Since $G_2$ is commutation-closed and $\text{msc}(w_1) = \text{msc}(w_2)$, $w_1 \in \mathcal{L}_{\text{words}}(G_2)$. Therefore, $w_1 \in \mathcal{L}_{\text{words}}(G_1) \cap \mathcal{L}_{\text{words}}(G_2) = \mathcal{L}_{\text{words}}(G_1 \otimes G_2)$, which means that $M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1 \otimes G_2)$. $\square$

**Proposition 3.13.** For all system $S$ of communicating finite state machines, $\text{prod}(S)$ is commutation-closed and $\mathcal{L}_{\text{msc}}^{\text{synch}}(S) = \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\forall}}(\text{prod}(S))$.

**Proof.** It is sufficient to observe that the runs of the synchronous executions

$$ !m_1?m_1...!m_k?m_k $$

of $S$ are in one-to-one correspondence with the runs of the words $m_1...m_k$ of $\text{preprod}(S)$. $\square$

When a global type is implemented in a concrete system, its behaviour obviously depend on the chosen communication model.

**Definition 3.14 (Global Type Semantics).** Let $G$ be a global type and $\text{com}$ a communication model. The language of $G$ in $\text{com}$ is the set $\mathcal{L}_{\text{exec}}^{\text{com}}(G) \stackrel{\text{def}}{=} \bigcup\{\text{lin}_{\text{com}}(M) \mid M \in \mathcal{L}_{\text{msc}}^{\exists}(G)\}$.

**Example 3.15.** For any communication model $\text{com}$ that contains synch, The global type in Figure 9 has the following semantics:

$$ \mathcal{L}_{\text{exec}}^{\text{com}}(G) = (!a?!a?!c?c+!a?!b?b!d?d)^*. $$

**Example 3.16.** Consider the global type

$$ G = \text{rec } X.\text{end} + p \xrightarrow{m_1} q; X + p \xrightarrow{m_2} q; X. $$

The semantics of $G$ in the communication model bag is the set of executions $e$ such that in any prefix of $e$ the number of $!m_1$ is greater or equal to the number of $?m_1$, and the number of $!m_2$ is greater or equal to the number of $?m_2$, and moreover the numbers of $!m_1$ and $?m_1$ are the same in the whole execution, as well as the numbers of $!m_2$ and $?m_2$. On the other hand, the semantics of $G$ in the communication model p2p (resp. causal) is the set
of executions *e* that moreover contain the same word over $m_1$ and $m_2$ when retaining only sends on the one hand and only receives on the other hand. For instance, $!m_1!m_2?m_2?m_1$ is in $\mathcal{L}_{\text{exec}}^{\text{bag}}(G)$ but not in $\mathcal{L}_{\text{exec}}^{\text{p2p}}(G)$.

## 4. REALISABILITY

We have finally collected all the definitions needed to introduce our notion of realisability of global types that is parametric in a given communication model.

**Definition 4.1** (Deadlock-free realisability). A global type $G$ is *deadlock-free realisable*$^3$ in the communication model $\mathit{com}$ if the following two conditions hold:

(CC): $\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) = \mathcal{L}_{\text{exec}}^{\text{com}}(G)$.

(DF): $\text{proj}(G)$ is deadlock-free in $\mathit{com}$.

Condition (CC) of Definition 4.1 corresponds to *session conformance*: the executions of the projected system do not deviate from the ones specified by the global type.

Deadlock-free realisability is equivalent to the notion of *safe realisability* of [AEY05] when $\mathit{com}$ is $\text{p2p}$ or $\text{synch}$. This is not the case for other communication models, our definition better captures the fact that a key factor for realisability is deadlock-freedom and deadlock freedom is strongly dependent on the communication model being causally-closed.

**Example 4.2.** The global type in Figure 9 is deadlock-free realisable in any communication model that contains $\text{synch}$. Indeed, the projected system of CFSMs is the one in Figure 6, which is deadlock-free. Moreover, the executions of the projected system are exactly those of the global type, as shown in Example 3.15.

**Example 4.3.** The global type $p_1 \xrightarrow{m_1} q$; $p_2 \xrightarrow{m_2} q$; end is realisable in $\text{synch}$ and $\text{p2p}$, but its projection is deadlock in $\mathit{mb}$.

**Example 4.4.** The global type $p_1 \xrightarrow{m_1} q_1$; $p_2 \xrightarrow{m_2} q_2$; end is realisable in $\text{synch}$; indeed, it is deadlock-free and $\mathcal{L}_{\text{exec}}^{\text{synch}}(G) = \{!m_1?m_1!m_2?m_2, !m_2?m_2!m_1?m_1\} = \mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G))$.

**Example 4.5.** The global type $G$ in Figure 2 is deadlock-free realisable in $\text{synch}$. Indeed, it can be checked that $\text{prod}(\text{proj}(G))$ accepts the same sequences of arrows as $G$, up to the commutation of the two last arrows $b \xrightarrow{\text{end}} c_1$ and $b' \xrightarrow{\text{end}} c_2$. It therefore holds that $\mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G)) = \mathcal{L}_{\text{exec}}^{\text{synch}}(G)$. Moreover, $G$ contains no sink state (all states are coreachable from the accepting state), therefore the projected system is deadlock-free in $\text{synch}$.

The following proposition reformulates conformance as an MSC property.

**Proposition 4.6.** Assume $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$. Condition (CC) of Definition 4.1 is equivalent to

$$ (\text{CC}') \quad \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G). $$

*Proof.* We establish the equivalence between Condition (CC) of Definition 4.1 and Condition (CC'). We prove the two implications separately.

⇒ Assume that Condition (CC) of Definition 4.1 holds. Let $M \in \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G))$; we prove that $M \in \mathcal{L}_{\text{msc}}^{\exists}(G)$. By definition of $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G))$, there exists an execution $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))$ such that $M = \text{msc}(e)$. By Condition (CC) of Definition 4.1, $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(G)$. By Definition 3.14, $\text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\exists}(G)$, which shows (CC').

<footnote n="3">³We sometimes say simply *realisable* instead of *deadlock-free realisable*.</footnote>
Assume that Condition (CC') holds. We prove that Condition (CC) of Definition 4.1 holds
by showing the two inclusions.
-

- Let $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))$. By Definition 2.21, $\text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G))$. By Condition (CC'), $\text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\exists}(G)$, which means that $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(G)$. Thus, $\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(G)$.

- Let $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(G)$. By Definition 3.14, $\text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\exists}(G)$. By Condition (CC'), $\text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G))$, which means that $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))$. Thus, $\mathcal{L}_{\text{exec}}^{\text{com}}(G) \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))$.

□

**Example 4.7.** The global type G in Figure 2 is deadlock-free realisable in p2p: the communication model does not change the sets of MSCs of the projected system, i.e. $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(G)) = \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G))$, and the projected system is deadlock-free in p2p.

4.1. **Subtyping.** We adopt the following semantic definition of subtyping.

**Definition 4.8 (Subtyping).** A global type $G_1$ is a *subtype* of a global type $G_2$ in the communication model com if $\mathcal{L}_{\text{exec}}^{\text{com}}(G_1) \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(G_2)$.

**Example 4.9.** The global type rec X.end + p $\xrightarrow{a}$ q + q $\xrightarrow{c}$ p; X is a subtype of the global type in Figure 9 Indeed, the semantics of G is the set of executions !a?!c?!c*, which is contained in the semantics of the other type already given in Example 3.15.

Interestingly, we can prove that the communication model does not play a role in the definition of subtyping. This follows from the characterisation of global types as set of MSCs.

**Theorem 4.10.** Let $G_1$ and $G_2$ be two global types, and com a communication model such that $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$. Then $G_1$ is a subtype of $G_2$ in com if and only if $\mathcal{L}_{\text{msc}}^{\exists}(G_1) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G_2)$.

Proof. Assume $G_1$ is a subtype of $G_2$ in com. By Definition 4.8, we have

$$
\mathcal{L}_{\text{exec}}^{\text{com}}(G_1) \cap \mathcal{E}_{\text{synch}} \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(G_2) \cap \mathcal{E}_{\text{synch}}.
$$

Since $\mathcal{E}_{\text{synch}} \subseteq \mathcal{E}_{\text{com}}$,

$$
\mathcal{L}_{\text{exec}}^{\text{com}}(G_i) \cap \mathcal{E}_{\text{synch}} = \mathcal{L}_{\text{exec}}^{\text{synch}}(G_i) = \mathcal{L}_{\text{msc}}^{\exists}(G_i)
$$

by Definition 3.14. We conclude that $\mathcal{L}_{\text{msc}}^{\exists}(G_1) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G_2)$. The converse also follows from
Definitions 4.8 and 3.14.
□

**4.2. Complementability.** Next, we introduce the notion of complementation for global types, which is a key concept for our decidability results.

**Definition 4.11 (Complement of a Global Type).** A global type $\bar{G}$ is a complement of G if $\mathcal{L}_{\text{msc}}^{\exists}(G) = \mathcal{M}_{\text{synch}} \setminus \mathcal{L}_{\text{msc}}^{\exists}(\bar{G})$. We say that G is *complementable* if it admits at least one complement.

Interestingly, not all global types are complementable. Moreover, we can compute the complement of some already known classes of global types such as commutation-closed, synch-realisable and global types with sender-driven choice.

We first give an example of non-complementable global type.

**Lemma 4.12.** *Not all global types are complementable.*
<figure><img src="image_12.png" /><figcaption>FIGURE 10. The shape of the MSCs in $\mathcal{L}_{\text{msc}}^{\exists/\forall}(G_0)$ for the global type $G_0$ in the proof of Theorem 4.12</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>FIGURE 11. A non-complementable global type</figcaption></figure>

*Proof.* Let $\mathbb{P} = \{p, q, r, s\}$, $\mathbb{M} = \{m_1, m_2, m_3\}$, and $\text{Arr} = \{p \xrightarrow{m_1} q, r \xrightarrow{m_2} s, p \xrightarrow{m_3} q\}$. Consider a global type $G_0$ such that $\mathcal{L}_{\text{words}}(G_0) = (m_1 + m_2) * (m_2 + m_3) * $ and take the minimal DFA recognising this language. Note that $G_0$ is commutation-closed and the MSCs of $\mathcal{L}_{\text{msc}}^{\exists}(G_0)$ are of the form depicted in Figure 10.

Now consider the global type $G$ depicted in Figure 11. We claim that for all natural numbers $k_1, k_2, k_3$,

$$ \text{msc}(m_1^{k_1} m_2^{k_2} m_3^{k_3}) \in \mathcal{L}_{\text{msc}}^{\exists}(G) \quad \text{if and only if} \quad k_1 > k_2 \text{ or } k_2 > k_3. $$

The claim follows by analysis on the paths leading to accepting states in $G$, as hinted by Figure 11. For instance, the language of the words accepted by $G$ with state $q_8$ as the last state is of the form $m_1^+(m_2m_1)*m_3^+$, therefore lead to MSCs with $k_1 > k_2$.

We show that $G$ is not complementable. By contradiction, suppose that $G$ is complementable and $G'$ is a complement. Let $G'' = G' \otimes G_0$; by Lemma 3.12, and the fact that $G_0$
is commutation-closed,

$$ \mathcal{L}_{\text{msc}}^{\exists}(G'') = \mathcal{L}_{\text{msc}}^{\exists/\forall}(G_0) \cap \mathcal{L}_{\text{msc}}^{\exists}(G') = \{\text{msc}(m_1^{k_1} m_2^{k_2} m_3^{k_3}) \mid k_1 \le k_2 \le k_3\}. $$

Now, let $\mathcal{A}$ denote the NFA obtained from $G''$ after replacing each $m_2$ transition with an $\varepsilon$ transition. Then $\mathcal{L}_{\text{words}}(\mathcal{A}) = \{m_1^{k_1} m_3^{k_3} \mid k_1 \le k_3\}$, which is not a regular language, and hence the contradiction. □

**Complementation By Duality.** Recall that we write dual($G$) for the dual DFA of a global type $G$, where accepting states and non-accepting ones are swapped (possibly completing first $G$ with a sink state). It follows from the definition of $\mathcal{L}_{\text{msc}}^{\exists}(G)$ and $\mathcal{L}_{\text{msc}}^{\forall}(G)$ that $\mathcal{L}_{\text{msc}}^{\exists}(\text{dual}(G)) = \mathcal{M}_{\text{synch}} \setminus \mathcal{L}_{\text{msc}}^{\forall}(G)$.

In general dual($G$) is not a complement of $G$, still duality can be used to obtain a complement of $G$ in a few cases. The first and most obvious case is the following.

**Lemma 4.13.** If $G$ is commutation-closed, then dual($G$) is a complement of $G$.

As observed before, all global types with less than three participants are commutation closed, hence from Lemma 4.13 we have the following immediate result.

**Corollary 4.14.** If $|\mathbb{P}| \le 3$, then dual($G$) is a complement of $G$.

Now, even if a global type $G$ is not commutation-closed, it may still be completed by commutation-closure and later complemented by duality; this construction yields a complement of $G$ if $G$ is deadlock-free realisable in synch.

**Lemma 4.15.** If a global type $G$ is deadlock-free realisable in synch, then dual($\text{prod}(\text{proj}(G))$) is a complement of $G$.

*Proof.* Let $G$ be a global type that is deadlock-free realisable in synch. By Condition (CC) of Definition 4.1, $\mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G)) = \mathcal{L}_{\text{exec}}^{\text{synch}}(G)$. If two sets of executions are equal, the corresponding sets of their MSCs are also equal, and thus $\mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G)) = \mathcal{L}_{\text{msc}}^{\text{synch}}(G)$. By Proposition 3.13, the synchronous product $\text{prod}(\text{proj}(G))$ is a commutation-closed global type whose runs are exactly the synchronous executions of the projected system, so

$$ \mathcal{L}_{\text{msc}}^{\exists/\forall}(\text{prod}(\text{proj}(G))) = \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G)) = \mathcal{L}_{\text{msc}}^{\exists}(G). $$

Finally, by Proposition 4.13, dual($\text{prod}(\text{proj}(G))$) is a complement of $\text{prod}(\text{proj}(G))$, thus of $G$. □

**Remark 4.16.** In terms of complexity, complementation by duality is a linear in the number of states of the global type $G$ (possibly after adding a sink state). However, $\text{prod}(\text{proj}(G))$ involves in the worst case a doubly exponential blowup. This may be mitigated if we can avoid to explicitly compute $\text{prod}(\text{proj}(G))$.

**Complementation by Renunciation for Sender-Driven Choices.** Next, we introduce another complementation procedure for global types with sender-driven choices, and more generally presenting a form of determinism in commutations; this construction is also linear, although it does not preserve determinism. We first recall the definition of sender-driven choice and commutation-determinism, then define our complementation procedure, and finally establish its correctness.

For a state $s$ of $G$, let choices$_G(s)$ be the set of arrows labelling outgoing transitions of $s$ in $G$.
**Definition 4.17** (Sender-Driven [Stu24a]). A global type G is sender-driven if it is deterministic and for every state s of G,

$$ \mathit{choices}_G(s) = \{p \xrightarrow{m_i} q_i \mid i = 1, \dots, n\} $$

for some process p and some processes $q_i$ and messages $m_i$.

Stutz et al. introduced this assumption on global types in order to prove that p2p-implementability (a notion close to realisability) is decidable [LSWZ23]. We slightly generalise this condition as the complementation procedure we are about to present also works in this larger setting.

**Definition 4.18** (Commutation-deterministic). A global type G is commutation-deterministic if it is deterministic and for every state s of G, for every two arrows $a, b \in \mathit{choices}_G(s)$, a and b do not commute.

We now formally define the complementation procedure for commutation-deterministic global types.

**Definition 4.19** (Complementation by renunciation). Let G be a commutation-deterministic global type. Let S be the set of states of G, $\bar{S} \stackrel{\text{def}}{=} \{\bar{s} \mid s \in S\}$, and $S' = S \uplus \bar{S}$. $\text{renun}(G)$ is the global type with set of states $S' \cup S' \times \text{Arr} \cup \{s_{\text{acc}}\}$ defined as follows:

* the initial state of $\text{renun}(G)$ is the initial state of G;

* let $F \subseteq S$ be the set of accepting states of G; the set of accepting states of $\text{renun}(G)$ is $(S \setminus F) \cup \bar{S} \cup \{s_{\text{acc}}\}$;

* for any states $s, s' \in S$ of G, for any arrow $a \in \text{Arr}$, if $(s, a, s')$ is a transition in G, then $(s, a, s')$ is a transition in $\text{renun}(G)$;

* for any state s of G, for any arrow $a \notin \mathit{choices}_G(s)$, $(s, a, \bar{s})$ (resp. $(\bar{s}, a, \bar{s})$) is a transition in $\text{renun}(G)$;

* for any state s of G, for any arrow $a \in \mathit{choices}_G(s)$, for any arrow $b \notin \mathit{choices}_G(s)$ that commutes with $a$, $(s, b, (s, a))$ (resp. $((s, a), b, (s, a))$) is a transition in $\text{renun}(G)$

* for any state s of G, for any arrow $a \in \mathit{choices}_G(s)$, for any arrow $b \notin \mathit{choices}_G(s)$ that does not commute with $a$, $(s, b, (\bar{s}, a))$ (resp. $((s, a), b, (\bar{s}, a))$) is a transition in $\text{renun}(G)$

* for any state s of G, for any arrow $a \in \mathit{choices}_G(s)$, for any arrow $b \notin \mathit{choices}_G(s)$, $((\bar{s}, a), b, (\bar{s}, a))$ (resp. $((\bar{s}, a), a, s_{\text{acc}})$) is a transition in $\text{renun}(G)$;

* for any arrow $a$, $(s_{\text{acc}}, a, s_{\text{acc}})$ is a transition in $\text{renun}(G)$.

**Example 4.20.** Figure 12 depicts a sender-driven global type and the complement computed according to Definition 4.19.

Note that the number of states of $\text{renun}(G)$ is linear in the number of states of G (assuming the alphabet $\text{Arr}$ is fixed); it can also be observed that, using Boolean expressions to label transitions, the size of $\text{renun}(G)$ can also be kept linear in the size of G.

**Example 4.21.** Let G, $\text{renun}(G)$, $M_1, M_2$ be the global types and MSCs depicted in Figure 12. It is easy to verify that $M_2 \notin \mathcal{L}_{\text{msc}}^{\exists}(\text{renun}(G))$, because the only sequence of arrows $w_2 = a_2$ such that $M_2 = \text{msc}(w_2)$ is not in $\mathcal{L}_{\text{words}}(\text{renun}(G))$. It can also be checked that $M_1 \notin \mathcal{L}_{\text{msc}}^{\exists}(\text{renun}(G))$, because the only two sequences of arrows $w_{1,1} = a_1 a_3$ and $w_{1,2} = a_3 a_1$ such that $\text{msc}(w_{1,1}) = \text{msc}(w_{1,2}) = M_1$ are not in $\mathcal{L}_{\text{words}}(\text{renun}(G))$.

Intuitively, $\text{renun}(G)$ describes a MSC M that starts with a prefix that is in $\mathcal{L}_{\text{msc}}^{\exists}(G)$ up to a certain state s, at which point a renunciation of the choices of G at s occurs. There are
<figure><img src="image_14.png" /><figcaption>FIGURE 12. A sender-driven global type $G$, with $\mathcal{L}_{\text{msc}}^{\exists}(G) = \{M_1, M_2\}$, and its complement $\text{renun}(G)$. For better readability, the states $s_2$ and $s_3$ (that are sink states in $\text{renun}(G)$) have been pruned. $a^\sharp$ denotes the set of arrows that do not commute with $a$.</figcaption></figure>

two kinds of renunciation: definitive renunciation means that none of the arrows available in the choices will ever occur later. Provisory renunciation means that at least one arrow in the choices will occur later, but not immediately: if $a$ is the first arrow of the choice that occurs later, another arrow $b$ occurs before $a$ such that $b$ does not commute with $a$ and is not in the choices that have been renunciated. The first kind of renunciation corresponds to moving to a state of the form $\bar{s}$, while the second kind corresponds to moving to a state of the form $(s, a)$ or $(\bar{s}, a)$.

**Example 4.22.** Consider the MSC $M_3 = \text{msc}(a_1a'_2a_3)$, with $a'_2 = p \stackrel{m'_2}{\longrightarrow} q'$ for some $m'_2 \neq m_2$. Then $M_3$ is accepted by $\text{renun}(G)$ because $w_{3,1} = a_1a'_2a_3$ is accepted in $\bar{s}_1$. However, the other sequence of arrows $w_{3,2} = a_3a_1a'_2$ such that $\text{msc}(w_{3,2}) = M_3$ is not in $\mathcal{L}_{\text{words}}(\text{renun}(G))$. More generally, $\text{renun}(G)$ is not commutation-closed, and for any MSC
$M \notin \mathcal{L}_{\text{msc}}^{\exists}(G)$, the sequence of arrows $w$ such that $M = \text{msc}(w)$ and $w \in \mathcal{L}_{\text{words}}(\text{renun}(G))$ should be carefully constructed. The strategy consists in picking a sequence of arrows $w = w_1 \cdot w_2$ with the longest possible $w_1$ in Prefixes($\mathcal{L}_{\text{words}}(G)$), i.e., renunciating to a choice as late as possible.

In order to formalise this intuition, we introduce a few notions. Given an MSC $M$ and a state $s$ of a commutation-deterministic global type $G$, we write $\text{next}(M, s)$ for the first arrow of choices$_G(s)$ that occurs in a sequence of arrows $w$ such that $\text{msc}(w) = M$. Note that $\text{next}(M, s)$ is not defined if $M$ contains no arrow of choices$_G(s)$; note also that $\text{next}(M, s)$, when defined, does not depend on the choice of the sequence of arrows $w$ such that $\text{msc}(w) = M$ (otherwise two arrows of choices$_G(s)$ would commute, contradicting the commutation-determinism of $G$).

**Example 4.23.** Consider the MSC $M_4 = \text{msc}(a_1a_2a_3) = \text{msc}(a_3a_1a_2)$, and the initial state $s_0$ of $G$ in Figure 12. Then $\text{next}(M_4, s_0) = a_1$.

We also define $\text{resid}(M, s)$ as $\text{msc}(w)$ for some $w$ such that $M = \text{msc}(\text{next}(M, s)w)$; intuitively, we remove the arrow $\text{next}(M, s)$ from $M$, provided it is not blocked by a previous non-commuting arrow. Note that $\text{resid}(M, s)$ is not defined if in all sequences of arrows $w$ such that $\text{msc}(w) = M$, $\text{next}(M, s)$ never occurs first.

**Example 4.24.** Consider the MSC $M_4 = \text{msc}(a_1a_2a_3)$, and the state $s_0$ of $G$ in Figure 12. Then $\text{resid}(M_4, s_0) = \text{msc}(a_2a_3)$. On the other hand, for the MSC $M_5 = \text{msc}(a_4a_1a_2)$, with $a_4 = q \xrightarrow{m_4} q'$, $\text{resid}(M_5, s_0)$ is undefined, because $a_1$ is blocked by $a_4$.

**Lemma 4.25.** Let $G$ be a commutation-deterministic global type with initial state $s_0$, and $M$ a non-empty MSC. Then $M \notin \mathcal{L}_{\text{msc}}^{\exists}(G)$ if and only if one of the following holds:

* $\text{next}(M, s_0)$ is undefined, or

* $\text{resid}(M, s_0)$ is undefined, or

* $a = \text{next}(M, s_0)$, $s$ is the a-successor of $s_0$ in $G$, $M' = \text{resid}(M, s_0)$ and $M' \notin \mathcal{L}_{\text{msc}}^{\exists}(G_s)$, where $G_s$ is the global type obtained from $G$ by setting the initial state to $s$.

*Proof.* If $\text{next}(M, s_0)$ is undefined, then $M$ contains no arrow of choices$_G(s_0)$, so for every sequence of arrows $w$ such that $\text{msc}(w) = M$, $w$ does not start with an arrow of choices$_G(s_0)$, therefore $w \notin \mathcal{L}_{\text{words}}(G)$. Similarly, when $\text{resid}(M, s_0)$ is undefined, every sequence of arrows $w$ such that $\text{msc}(w) = M$ does not start with an arrow of choices$_G(s_0)$, and again $w \notin \mathcal{L}_{\text{words}}(G)$. In the third case, assume by contradiction that $M \in \mathcal{L}_{\text{msc}}^{\exists}(G)$, i.e. there is a sequence of arrows $w$ such that $\text{msc}(w) = M$ and $w \in \mathcal{L}_{\text{words}}(G)$. Then $w = aw'$ for some $a = \text{next}(M, s_0)$ and $w' \in \mathcal{L}_{\text{words}}(G, s)$, with $\text{resid}(M, s_0) = \text{msc}(w')$. It follows that $\text{resid}(M, s_0) \in \mathcal{L}_{\text{msc}}^{\exists}(G_s)$, and the contradiction. $\square$

**Theorem 4.26.** Assume $G$ is a commutation-deterministic global type, and let $\text{renun}(G)$ denote the global type defined as in Def 4.19. Then $\text{renun}(G)$ is a complement of $G$.

*Proof.* It is routine to check that an MSC $M$ is accepted by $\text{renun}(G)$ starting from a state $\bar{s}$ if and only if $\text{next}(M, s)$ is undefined. It is also routine to check that an MSC $M$ is accepted by $\text{renun}(G)$ starting from a state $(s, a)$ if $a = \text{next}(M, s)$ and $\text{resid}(M, s)$ is undefined. It is then also routine, thanks to Lemma 4.25, to show by induction on the size of an MSC $M$ that $M \notin \mathcal{L}_{\text{msc}}^{\exists}(G_s)$ if and only if $M \in \mathcal{L}_{\text{msc}}^{\exists}(\text{renun}(G_s))$. $\square$

Hence summing up:
**Theorem 4.27.** Not all global types are complementable. A global type $G$ is complementable in the following cases:

(1) if $G$ is commutation-closed (in particular with at most 3 processes), then $\text{dual}(G)$ is a complement of $G$ (with a linear increase in the number of states)

(2) if $G$ is deadlock-free realisable in synch, then $\text{dual}(\text{prod}(\text{proj}(G)))$ is a complement of $G$ (with a doubly exponential blowup in the number of states)

(3) if $G$ has sender-driven choice, it admits an effectively computable complement with a linear increase in the number of states

*Proof.* (1) Follows from Lemma 4.12

(2) (a) Follows from Lemma 4.13

(b) Follows from Lemma 4.15

(c) Follows from Lemma 4.26

<figure><img src="image_15.png" /><figcaption>Complexities of construction are summarised in the following table:</figcaption></figure>

<table><thead><tr><td>Class of global types</td><td>Complementation procedure</td><td>Size</td></tr></thead><tbody><tr><td>|P| ≤ 3</td><td>G ↦→ dual(G)</td><td>linear</td></tr><tr><td>commutation-closed</td><td>G ↦→ dual(G)</td><td>linear</td></tr><tr><td>realisable</td><td>G ↦→ dual.prod Understanding of the complement of G' is a subtype of G'. This is a key property of realisability, which ensures that the complement of a global type G is a subtype of G'. The proof of this property is straightforward and follows from the definition of realisability and the properties of the complement of G.</td><td>doubly exponential</td></tr><tr><td>sender-driven choices</td><td>G ↦→ renun(G)</td><td>linear</td></tr></tbody></table>

Notice that apart from the classes mentioned above, deciding whether a complement exists and compute it, is an open problem.

## 5. DECIDABILITY

Deadlock-free realisability in p2p is known to be undecidable for global types [Loh03], and decidable for sender-driven choices [Stu24b]. Here we show that the realisability problem, for global types for which an explicit complement is given, is decidable in PSPACE for the synchronous communication model and in EXPSPACE for RegSC (see Definition 5.7 below), causally-closed, communication models. We show the result for synch, and then extend it to any causally-closed communication model. But first, we consider the decidability of the subtyping problem.

### 5.1. Decidability of Subtyping.

**Theorem 5.1.** Given a global type $G$ and a complementable global type $G'$ with an explicit commutation-closed complement $\overline{G'}$, it is decidable in NLOGSPACE whether $G$ is a subtype of $G'$.

*Proof.* Thanks to Theorem 4.10, $G$ is a subtype of $G'$ if and only if $\mathcal{L}_{\text{msc}}^{\exists}(G) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G')$, i.e., $\mathcal{L}_{\text{msc}}^{\exists}(G) \cap \mathcal{L}_{\text{msc}}^{\exists/\sqrt{\overline{G'}}} = \emptyset$. By Lemma 3.12, this reduces to check whether $\mathcal{L}_{\text{words}}(G \otimes \overline{G'}) = \emptyset$, which is decidable in NLOGSPACE. □

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

It is possible to relax the assumption on the complement of $G'$ to be commutation-closed, as follows.

**Theorem 5.2.** Given a global type $G$ that is realisable in synch, and a complementable global type $G'$ with an explicit complement $\overline{G'}$, it is decidable in EXPSPACE whether $G$ is a subtype of $G'$.
*Proof.* By Theorem 4.27, there is a commutation-closed global type $\overline{\mathbb{G}}$ of double exponential size such that $\mathcal{L}_{\text{msc}}^{\exists}(\mathbb{G}) = \mathcal{L}_{\text{msc}}^{\exists/\forall}(\overline{\mathbb{G}})$. Thanks to Theorem 4.10, $\mathbb{G}$ is a subtype of $\mathbb{G}'$ if and only if $\mathcal{L}_{\text{msc}}^{\exists}(\mathbb{G}) \cap \mathcal{L}_{\text{msc}}^{\exists}(\overline{\mathbb{G}}') = \mathcal{L}_{\text{msc}}^{\exists/\forall}(\overline{\mathbb{G}}) \cap \mathcal{L}_{\text{msc}}^{\exists}(\overline{\mathbb{G}}')\emptyset$. By Lemma 3.12, this reduces to check whether $\mathcal{L}_{\text{words}}(\overline{\mathbb{G}} \otimes \overline{\mathbb{G}}') = \emptyset$. $\square$

**Corollary 5.3.** *Subtyping between two realisable global types is decidable in EXPSPACE.*

## 5.2. Realisability in the Synchronous Model.

**Theorem 5.4.** *Given a global type $\mathbb{G}$ and its complement $\mathbb{G}'$, it is decidable in PSPACE whether $\mathbb{G}$ is deadlock-free realisable in synch.*

*Proof.* Condition (CC) of Definition 4.1 is equivalent to

$$ \mathcal{L}_{\text{msc}}^{\exists/\forall}(\text{prod}(\text{proj}(\mathbb{G}))) \cap \mathcal{L}_{\text{msc}}^{\exists}(\mathbb{G}') = \emptyset. $$

By Lemma 3.12, this reduces to checking the emptiness of $\mathcal{L}_{\text{words}}(\text{prod}(\text{proj}(\mathbb{G})) \otimes \mathbb{G}')$. Recall that $\text{prod}(\mathbb{S}) = \det(\text{preprod}(\mathbb{S}))$, where $\text{preprod}(\mathbb{S})$ denotes the synchronous product of the communicating machines keeping all $\varepsilon$-transitions and non-determinism. It follows that Condition (CC) of Definition 4.1 is equivalent to checking the emptiness of the language of the NFA $\text{preprod}(\text{proj}(\mathbb{G})) \otimes \mathbb{G}'$. The non-emptiness of the language of an NFA can be checked in non-deterministic logarithmic space in the size of the NFA, which yields a PSPACE algorithm in that case, as the exponential size NFA $\text{preprod}(\text{proj}(\mathbb{G}))$ can be lazily constructed while guessing a path to an accepting state.

Assuming that Condition (CC) of Definition 4.1 holds, the second condition of Definition 4.1 is equivalent to whether all control states of $\text{preprod}(\text{proj}(\mathbb{G}))$ that are reachable from the initial state can reach a final state, which again, for the same reason, can be checked in PSPACE. $\square$

## 5.3. Realisability in Causally-Closed Communication Models.
We now show that the realisability problem for complementable global types, given with an explicit complement, is decidable in EXSPACE for bag, p2p, and causal. The proof goes throughout the following steps.

(1) We show that realisability in any communication model that contains synch implies realisability in synch (Theorem 5.5).

(2) We address the contraposite, and identify three necessary and sufficient conditions on the projection of $\mathbb{G}$ in com (Theorem 5.6), namely

(a) $\text{proj}(\mathbb{G})$ is RSC [Ger23]

(b) $\text{proj}(\mathbb{G})$ is orphan-free, and

(c) $\text{proj}(\mathbb{G})$ is deadlock-free.

(3) We show that each of these three conditions is decidable in EXPSPACE.

(4) We conclude with the decidability of the realisability problem in com (Theorem 5.12 thanks to the decidability of the realisability problem in synch (Theorem 5.4).

**Theorem 5.5.** *Assume $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$. If the global type $\mathbb{G}$ is deadlock-free realisable in com, then $\mathbb{G}$ is deadlock-free realisable in synch.*

*Proof.* Assume that $\mathbb{G}$ is deadlock-free realisable in com. We show that $\mathbb{G}$ is deadlock-free realisable in synch by verifying the two conditions of Definition 4.1.
(1) By the hypothesis that $G$ is com-realisable, we have that $\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) = \mathcal{L}_{\text{exec}}^{\text{com}}(G)$, and therefore

$$ \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) \cap \mathcal{E}_{\text{synch}} = \mathcal{L}_{\text{exec}}^{\text{com}}(G) \cap \mathcal{E}_{\text{synch}}. $$

Since $\mathcal{E}_{\text{synch}} \subseteq \mathcal{E}_{\text{com}}$, we have $\mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) \cap \mathcal{E}_{\text{synch}}$. On the other hand, by Definition 3.14, $\mathcal{L}_{\text{exec}}^{\text{com}}(G) \cap \mathcal{E}_{\text{synch}} = \mathcal{L}_{\text{exec}}^{\text{synch}}(G)$. Therefore, we have

$$ \mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{exec}}^{\text{synch}}(G). $$

Conversely, by Property 3.11, $\mathcal{L}_{\text{MSC}}^{\exists}(G) \subseteq \mathcal{L}_{\text{MSC}}^{\text{synch}}(\text{proj}(G))$, and by Definition 3.14, we get $\mathcal{L}_{\text{exec}}^{\text{synch}}(G) \subseteq \mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G))$, which ends the proof of Condition (CC) of Definition 4.1.

(2) By the hypothesis that $G$ is com-realisable and Definition 2.25, we have that

$$ \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))) = \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(G)). $$

and therefore, by $\mathcal{E}_{\text{synch}} \subseteq \mathcal{E}_{\text{com}}$,

$$ \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(\hat{G})) \cap \mathcal{E}_{\text{synch}} \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))) \cap \mathcal{E}_{\text{synch}}. $$

By Definition 2.21, $\mathcal{L}_{\text{exec}}^{\text{com}}(G) \cap \mathcal{E}_{\text{synch}} = \mathcal{L}_{\text{exec}}^{\text{synch}}(G)$, and on the other hand,

$$ \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))) \cap \mathcal{E}_{\text{synch}} \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) \cap \mathcal{E}_{\text{synch}}) = \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G))). $$

Therefore, we have $\mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{synch}}(\text{proj}(G)))$, which ends the proof of Condition (DF) of Definition 4.1.

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

We now establish the converse of Theorem 5.5: we show that the other implication holds under some extra conditions on the projection of $G$ in com, assuming further that com is causally closed.

**Theorem 5.6 (Reduction to synch-implementability).** Assume com is a causally closed communication model such that $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$. The global type $G$ is deadlock-free realisable in com if and only if the following four conditions hold:

(1) $\mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(G)) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$

(2) $\text{proj}(G)$ is orphan-free in com,

(3) $\mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(G)))$, and

(4) $G$ is deadlock-free realisable in synch.

*Proof.* We show both sides in turn:

⇒ : We first show that the four conditions are necessary. Let $G$ be a com-realisable global type.

(1) By Condition (DF) of Definition 4.1, $\text{proj}(G)$ is deadlock-free in com. By Proposition 2.27,

$$ \mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(G))). $$

By Condition (CC) of Definition 4.1,

$$ \mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(G)) = \mathcal{L}_{\text{MSC}}^{\exists}(G) \subseteq \mathcal{M}_{\text{synch}}. $$

Therefore $\mathcal{L}_{\text{MSC}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$.

(2) Let $e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G))$; we show that $e$ is orphan-free. By Condition (CC) of Definition 4.1, $\text{msc}(e) \in \mathcal{L}_{\text{MSC}}^{\exists}(G)$, therefore $\text{msc}(e)$ is synchronous, and in particular orphan-free.
(3) $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)))$ by Condition (DF) of Definition 4.1 and Proposition 2.27.

(4) Follows from Theorem 5.5

⇔ : Next we show that the four conditions are sufficient. Let G be a global type that verifies the four conditions. We prove that G is com-realisable as it satisfies the two conditions of Definition 4.1.

**Condition (CC):** By Proposition 4.6, we show that

$$ \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G). $$

By Condition (CC) of Theorem 5.6,

$$ \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)) = \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G)) $$

and by Condition 4 of Theorem 5.6 and Proposition 4.6, we have that

$$ \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G) $$

which concludes the proof of Condition (CC).

**Condition (DF):** follows from Proposition 2.27 and Condition 3 of Theorem 5.6. □

A system $\mathcal{S}$ such that $\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S}) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$ is called realisable with synchronous communications (RSC) in [Ger23]. Germerie [Ger23] showed that the RSC property is decidable in PSPACE and that whether a RSC system may reach a regular set of configurations is also in PSPACE. As a consequence, conditions 1 and 2 of Theorem 5.6 can be checked in PSPACE. In the remainder, we focus on the decidability of condition 3 of Theorem 5.6.

An execution $e = (w, \text{src})$ is RSC [Ger23] if for all $r \in \text{events}_R(e)$, $\text{src}(r) = r - 1$, i.e., all messages that are sent in $e$ are either orphan or immediately received. An MSC $M$ is RSC if it admits an RSC linearisation. We write $\mathcal{E}_{\text{rsc}}$ and $\mathcal{M}_{\text{rsc}}$ for the sets of RSC executions and MSCs respectively.

**Definition 5.7 (RegSC).** A set $\mathcal{M} \subseteq \mathcal{M}_{\text{rsc}}$ of RSC MSCs is RegSC if there is a NFA $\mathcal{A}_{\mathcal{M}}$ such that $\mathcal{L}_{\text{words}}(\mathcal{A}_{\mathcal{M}}) = \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \mathcal{M}\}$. A communication model com is RegSC if $\mathcal{M}_{\text{com}} \cap \mathcal{M}_{\text{rsc}}$ is RegSC, i.e., there is an NFA $\mathcal{A}_{\text{com}}$ such that $\mathcal{L}_{\text{words}}(\mathcal{A}_{\text{com}}) = \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \mathcal{M}_{\text{com}}\}$.

All communication models mentioned in this paper are RegSC.

**Proposition 5.8.** The following communication models are regular: bag, p2p, causal, and synch.

*Proof.* (Sketch) We only detail the case of com = p2p and com = causal; the other cases are simpler and therefore omitted.

* Case of com = p2p. Intuitively, the automaton $\mathcal{A}_{\text{p2p}}$ guesses for each send action whether it will be followed by its matching receive action or will remain unmatched. It also remembers the set of queues in which unmatched messages are stored, and makes sure that whenever another message is sent in such a queue, it remains unmatched. Formally, the automaton $\mathcal{A}_{\text{p2p}} = (Q, \delta, q_0, F)$ is defined as follows: $Q = 2^{\mathbb{P} \times \mathbb{P}} \times (\varepsilon \cup \text{Act})$, $q_0 = (\emptyset, \varepsilon)$,
$F = 2^{\mathbb{P} \times \mathbb{P}} \times \{\varepsilon\}$, and

$$
\begin{align*}
\delta &\stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left( (S, \varepsilon), !m^{p \to q}, (S, !m^{p \to q}) \right) \mid (p, q) \notin S, p, q \in \mathbb{P}, m \in \mathbb{M} \\ \cup \left( (S, \varepsilon), !m^{p \to q}, (S \cup \{(p, q)\}, \varepsilon) \right) \mid p, q \in \mathbb{P}, m \in \mathbb{M} \\ \cup \left( (S, !m^{p \to q}), ?m^{p \to q}, (S, \varepsilon) \right) \mid p, q \in \mathbb{P}, m \in \mathbb{M} \end{array} \right\}
\end{align*}
$$

* Case of com = causal. We define an NFA $\mathcal{A}$ such that $\mathcal{L}_{\text{words}}(\mathcal{A}) = \mathcal{E}_{\text{rsc}} \setminus \mathcal{E}_{\text{causal}}$; The NFA $\mathcal{A}_{\text{causal}}$, hence, can be defined by complementation. Intuitively, the automaton $\mathcal{A}$ accepts an execution $e$ if and only there is causal path from an unmatched send $s_1 = !m^{p \to q}$ to some reception $r_2 = ?m^{p' \to q}$ for the same process $q$, i.e., if the first condition of Definition 2.11 is not satisfied (note that the other condition is always satisfied for RSC MSCs). Formally, the automaton $\mathcal{A}$ is defined as follows: $Q = S \times (\text{Act} \cup \{\varepsilon\})$, with $S = \{q_{\perp}, q_{\top}\} \cup \mathbb{P} \times \mathbb{P}$, $q_0 = (q_{\perp}, \varepsilon)$, $F = \{q_{\top}\} \times (\text{Act} \cup \{\varepsilon\})$, and

$$
\begin{align*}
\delta &\stackrel{\text{def}}{=} \left\{
\begin{array}{@{}l@{}}
  \left( (s, \varepsilon), !m^{p \to q}, (s, \varepsilon) \right) \mid p, q \in \mathbb{P}, m \in \mathbb{M}, s \in S \\
  \cup \left( (s, \varepsilon), !m^{p \to q}, (s, !m^{p \to q}) \right) \mid p, q \in \mathbb{P}, m \in \mathbb{M}, s \in S \\
  \cup \left( (s, !m^{p \to q}), ?m^{p \to q}, (s, \varepsilon) \right) \mid p, q \in \mathbb{P}, m \in \mathbb{M}, s \in S \\
  \cup \left( (q_{\perp}, \varepsilon), !m^{p \to q}, ((p, q), \varepsilon) \right) \mid p, q \in \mathbb{P}, m \in \mathbb{M} \\
  \cup \left( (((p, q), !m^{p \to r}), ?m^{p \to r}, ((r, q), \varepsilon)) \mid p, q, r \in \mathbb{P}, m \in \mathbb{M} \right) \\
  \cup \left( (((p, q), !m^{p \to q}), ?m^{p \to q}, (q_{\top}, \varepsilon)) \mid p, q \in \mathbb{P}, m \in \mathbb{M} \right).
\end{array}
\right\} \quad \Box
\end{align*}
$$

Next we show that for regular communication models, if a system is RSC then the set of its executions is also regular.

**Lemma 5.9.** Assume com is RegSC and take a system of CFSM S such that $\mathcal{L}_{\text{msc}}^{\text{com}}(S) \subseteq \mathcal{M}_{\text{rsc}}$. Then $\mathcal{L}_{\text{msc}}^{\text{com}}(S)$ is RegSC.

*Proof.* We first show the result for the case where com = bag, and then generalise to all RegSC communication models.

* case of com = bag. Assume $S = (A_p)_{p \in \mathbb{P}}$, with $A_p = (Q_p, q_{0,p}, F_p, \delta_p)$. Let shuffle($S$) denote the shuffle product of all $A_p$'s, i.e., shuffle($S$) = $(Q, q_0, F, \delta)$, where $Q = \Pi_{p \in \mathbb{P}} Q_p$, $q_0 = (q_{0,p})_{p \in \mathbb{P}}$, $F = \Pi_{p \in \mathbb{P}} F_p$, and $\delta$ is defined as follows:

$$
\delta = \bigcup_{a \in \text{Act} \cup \{\varepsilon\}} \left\{ \left( (q_p)_{p \in \mathbb{P}}, a, (q'_p)_{p \in \mathbb{P}} \right) \mid \exists p \in \mathbb{P}, (q_p, a, q'_p) \in \delta_p \text{ and } \forall r \neq p, q_r = q'_r \right\}
$$

The automaton shuffle($S$) accepts a sequence of actions $e$ if and only if for all $p \in \mathbb{P}$, $\text{proj}_p(e) \in \mathcal{L}_{\text{words}}(A_p)$. In particular, if $e \in \mathcal{E}_{\text{rsc}}$, then $e$ is an execution, therefore $e \in \mathcal{L}_{\text{exec}}^{\text{bag}}(S)$ by Definition 2.21. Let $\mathcal{M} = \mathcal{L}_{\text{msc}}^{\text{bag}}(S) \cap \mathcal{M}_{\text{rsc}}$. We have $\mathcal{L}_{\text{words}}(\text{shuffle}(S) \otimes A_{\text{rsc}}) = \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \mathcal{M}\}$, therefore $\mathcal{M}$ is RegSC. By hypothesis, $\mathcal{L}_{\text{msc}}^{\text{bag}}(S) \subseteq \mathcal{M}_{\text{rsc}}$, so $\mathcal{M} = \mathcal{L}_{\text{msc}}^{\text{bag}}(S)$. We conclude that $\mathcal{L}_{\text{msc}}^{\text{bag}}(S)$ is RegSC.

* general case of com being RegSC. Let $\mathcal{M} = \mathcal{L}_{\text{msc}}^{\text{com}}(S) \cap \mathcal{M}_{\text{rsc}}$. By Definition 2.21, $\mathcal{L}_{\text{msc}}^{\text{com}}(S) = \mathcal{L}_{\text{msc}}^{\text{bag}}(S) \cap \mathcal{M}_{\text{com}}$, so $\mathcal{L}_{\text{words}}(\text{shuffle}(S) \otimes A_{\text{rsc}} \otimes A_{\text{com}}) = \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \mathcal{M}\}$, which
shows that $\mathcal{M}$ is RegSC. By hypothesis, $\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S}) \subseteq \mathcal{M}_{\text{rsc}}$, so $\mathcal{M} = \mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S})$. We conclude that $\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S})$ is RegSC.

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

Similarly given a set of regular RSC MSCs, its prefix closure is also regular.

**Lemma 5.10.** Assume $\mathcal{M} \subseteq \mathcal{M}_{\text{rsc}}$ is RegSC. Then Prefixes($\mathcal{M}$) is RegSC.

*Proof.* Let $\mathcal{A} = (Q, q_0, F, \delta)$ be such that $\mathcal{L}_{\text{words}}(\mathcal{A}) = \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \mathcal{M}\}$. We construct an NFA $\mathcal{A}'$ such that $\mathcal{L}_{\text{words}}(\mathcal{A}') = \{e \in \mathcal{E}_{\text{rsc}} | \text{Prefixes}(\mathcal{M})\}$. Intuitively, $\mathcal{A}'$ simulates a run of $\mathcal{A}$ in which for each process $p$ it can stop before reaching the final state. Once it stopped on $p$, all further transitions containing an action of $p$ in $\mathcal{A}$ are replaced with $\epsilon$-transitions. Formally, we define $\mathcal{A}' = (Q', q'_0, F', \delta')$ as follows: $Q' = F' = Q \times 2^{\mathbb{P}} \times (\text{Act} \cup \{\epsilon\})$, $q'_0 = (q_0, \emptyset, \epsilon)$, and

$$ \delta' \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left( (q, S, \varepsilon), !m^{p \to r}, (q', S, !m^{p \to r}) \right) \mid (q, !m^{p \to r}, q') \in \delta, p \notin S \end{array} \right\} \\ \cup \quad \left\{ \left( (q, S, \varepsilon), !m^{p \to r}, (q', S, \varepsilon) \right) \mid (q, !m^{p \to r}, q') \in \delta, p \notin S \right\} \\ \cup \quad \left\{ \left( (q, S, !m^{p \to r}), ?m^{p \to r}, (q', S, \varepsilon) \right) \mid (q, ?m^{p \to r}, q') \in \delta, r \notin S \right\} \\ \cup \quad \left\{ \left( (q, S, \varepsilon), \varepsilon, (q', S \cup \{p\}, \varepsilon) \right) \mid (q, a, q') \in \delta, a \in \text{Act}_p \right\} \quad \square $$

We can now prove that condition 3 of Theorem 5.6 is decidable provided that the considered global type satisfies condition 1 of Theorem 5.6.

**Lemma 5.11.** Assume com is RegSC. Given a global type $G$ such that $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$, it is decidable in EXPSPACE complexity whether

$$ \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G))). $$

*Proof.* Since $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$ (condition 1 of Theorem 5.6), we have that $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$. Thanks to Lemma 5.9, $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(\hat{G}))$ and $\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G))$ are RegSC. Thanks to Lemma 5.10, Prefixes($\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)))$ is RegSC. Let $\mathcal{A}_1, \mathcal{A}_2$ be the NFAs such that

$$ \begin{aligned} \mathcal{L}_{\text{words}}(\mathcal{A}_1) &= \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(\hat{G}))\} \\ \mathcal{L}_{\text{words}}(\mathcal{A}_2) &= \{e \in \mathcal{E}_{\text{rsc}} | \text{msc}(e) \in \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(\text{proj}(G)))\}. \end{aligned} $$

Then condition 3 of Theorem 5.6 holds if and only if $\mathcal{L}_{\text{words}}(\mathcal{A}_1) \subseteq \mathcal{L}_{\text{words}}(\mathcal{A}_2)$. Since $\mathcal{A}_1$ and $\mathcal{A}_2$ are of exponential size in the number of processes, hence in the size $G$, and language inclusion for NFAs is decidable in PSPACE, condition 3 of Theorem 5.6 is decidable in EXPSPACE. $\square$

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

From these results we get an EXPSPACE decision procedure for deadlock-free realisability in asynchronous communication models.

**Theorem 5.12.** Let com = p2p (resp. bag, causal). Given a complementable global type $G$ and a complement $\hat{G}$, it is decidable in EXPSPACE complexity whether $G$ is deadlock-free realisable in com.
## 6. CONCLUDING REMARKS

In this paper, we investigated the realisability of MPSTs across several synchronous and asynchronous communication models, including causally ordered (causal), peer-to-peer ordered (p2p), or unordered (bag). We reduced the realisability in a complex asynchronous communication model to the simpler problem in the synchronous communication model. For a regular, causally-closed communication model com, as well as for com = synch, we showed that realisability in com is decidable in PSPACE for a complementable global type G provided with an explicit complement $\bar{G}$. As a consequence, we established that the realisability problem for sender-drive global types is decidable in PSPACE, because they can be complemented with a linear increase in the size.

Traditionally, the realisability problem is considered only for the peer-to-peer communication model. This paper represents a first step towards a parametric framework for realisability checking, with potential applicability across diverse communication models. Throughout the paper, we have made a deliberate effort to explicitly state the hypotheses (related to the communication model) under which our theorems hold. A particularly critical assumption is that the communication models in question must be causally closed (see Definition 2.14). This is still a bit restrictive, as many communication models, including mailbox, bus, or those based on bounded FIFO channels lack this property. It would be interesting to study realisability for these communication models.

On the complexity side, we showed a PSPACE upper bound on the realisability problem in synch, and an EXPSPACE upper bound in p2p, causal, and bag. We believe that these complexity results can be improved, with more careful constructions (as it has been recently done in the case of sender-driven global types for p2p).

Apart from exploring tighter complexity bounds, as for future work we plan to study the class of complementable global types, possibly setting someun/decidability results. Moreover we plan to extend existing tool ReSCU [DG23] to apply the theoretical insights of this paper.

### 6.1. Related works.
We conclude with a brief excursus on related work. Naturally, the most closely related lines of research are those concerning MPST. Comprehensive surveys on the topic are available in [CDCPY15, YG20]. It is noteworthy that in standard MPST literature, realisability—often referred to as implementability—is typically addressed through syntactic restrictions on global types. In most cases, a global type is implementable if a projection function exists. These syntactic constraints, along with the existence of the projection, imply that the global type is sender-driven, thus placing it within one of the complementable classes discussed in this paper. In contrast, a recent paper by Scalas and Yoshida [SY19] offers a novel perspective. Their approach emphasizes session fidelity and deliberately abandons syntactic restrictions on session types. Instead, they adopt semantic criteria—validated through model checking—to establish implementability, marking a significant shift from the conventional syntactic paradigm or our approach. Although, the comparison is difficult as the underlining models are substantially different, it is worth mentioning [BDCd24] that discusses projectability in the context of synchronous MPST.

The connection between communicating automata and behavioural types were first explored by Villard [Vil11] for the binary case and Deniélou and Yoshida [DY12] for MPSTs. The connection between MPST and HMSCs was initiated by Stutz et al. [Stu23, Stu24b]. In this work, we push these connections much further, in the sense that (1) we view MPST as the subclass of HMSCs restricted to synchronous MSCs, and (2) we provide for the first time
a simple, natural semantics of global types based on languages of MSCs. This MSC-based
semantics of MPST has the appealing property that it is agnostic of the communication
model. This semantics plays a pivotal role in our more traditional execution-based semantics
of MPST (Def 3.14), as it puts the communication model parameter at the right place,
namely the linearisations of MSCs that should be considered.

Our approach also suggest a rather simple and natural way to define a form of semantic
subtyping [CF05] for session types (see Definition 4.8). The boundaries of decidability for
subtyping of MPST have been recently discussed for instance in [BCL+21, LSW24] but
because of the different nature of the definition of subtyping, such work are loosely related
ours.

In [LSWZ23, Stu23], the authors revisited the theory of MPST projections through the
lenses of implementability (a slight variant of realisability), and step by step managed to
improve the complexity of the decision procedure for implementability from EXPSPACE to
PSPACE and more recently NP [LSWZ25]. Although implementability and deadlock-free
realisability are not the same problem, it would be interesting to explore how some of the
ideas behind the optimisations they introduced can be adapted to either global types that
are not sender-driven or communication models beyond p2p. For instance, two criteria,
called *send validity* and *receive validity*, where introduced in [Stu23]; the second criteria,
receive validity, seems strongly justified by the choice of p2p as the communication model,
and is unsound for other communication models, but it might be interesting to identify
variants of these criteria for other communication models beyond p2p.

Deadlock-free realisability was introduced by Alur et al. [AEY05] under the name of safe
realisability. We picked a slightly different name as the two notions only coincide for causally-
closed global types. Indeed, Alur et al. defined deadlock-freedom as an MSC property,
whereas we defined it at the level of executions (see Definition 2.25) and later showed that
it can be lifted to MSCs for causally-closed communication models (see Proposition 2.27).
It is worth noting that, for non-causally-closed communication models (for instance mb),
there are some systems $\mathcal{S}$ that are deadlocked according to Definition 2.25 but for which
$L_{\text{msc}}^{\text{mb}}(\hat{\mathcal{S}}) \subseteq \text{Prefixes}(L_{\text{msc}}^{\text{synch}}(\mathcal{S}))$, i.e., a partial MSC of the system can be extended to an
accepting MSC, possibly reordering some unmatched sends.

Alur et al. [AEY05] showed that weak realisability (i.e., condition 1 of Def 4.1) is
undecidable for HMSCs, and Lohrey [Loh03] extended their result to safe realisability.
The HMSCs they use in their proof are global types (they only describe synchronous MSC
languages), which shows that deadlock-free realisability is undecidable for global types in p2p.
Even more, Lohrey’s proof suggests that deadlock-free realisability might be undecidable even
in synch for 5 processes. It is remarkable that, despite these results are more than 20 years old,
some corners of shadow remain on the exact number of processes needed for undecidability,
or on the extent in which they depend on the asynchrony of the communication model.

Mazurkiewicz traces [DR95] are words over partially commutative alphabets. Synchronous MSCs (but not asynchronous ones) can be seen as Mazurkiewicz traces over the alphabet *Arr* of arrows. Regular trace languages are the ones recognized by commutation-closed finite automata. Zielonka’s asynchronous automata are a model of a distributed implementation of a regular trace language. It differs from realizability of MPSTs and HMSCs in several way: first, processes in this model synchronise by rendez-vous (that may involve more than two processes), second processes may exchange additionnal informations during rendez-vous (not just the message label specified by the choreography), and third, the choreography is commutation-closed. As a consequence, all regular trace languages are implementable,
but the projection operation is highly non-trivial in this setting. Although quite far from
MPSTs at first sight, some old works on Mazurkiewicz traces could possibly shade some
light on a few questions that arise from our work, and which, to the best of our knowledge,
remain open, like the decidability of the complementability of a global type, or concise
complementation procedures for non commutation-closed global types beyond sender-driven
choices.

REFERENCES

[AEY05] Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. Realizability and verification of MSC graphs. *Theor. Comput. Sci.*, 331(1):97–114, 2005. URL: https://doi.org/10.1016/j.tcs.2004.09.034, doi:10.1016/J.TCS.2004.09.034.

[BCL+21] Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping and its implementation. *Log. Methods Comput. Sci.*, 17(1), 2021. URL: https://lmcs.episciences.org/7238.

[BDCd24] Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Un-projectable global types for multiparty sessions. In *Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming*, PPDP '24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3678232.3678245.

[BZ83] Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. *J. ACM*, 30(2):323–342, apr 1983. doi:10.1145/322374.322380.

[CDCPY15] Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. *A Gentle Introduction to Multiparty Asynchronous Session Types*, pages 146–178. Springer International Publishing, Cham, 2015. doi:10.1007/978-3-319-18941-3_4.

[CF05] Giuseppe Castagna and Alain Frisch. A gentle introduction to semantic subtyping. In Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, *Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings*, volume 3580 of *Lecture Notes in Computer Science*, pages 30–34. Springer, 2005. doi:10.1007/11523468\_3.

[CHNQ19] Florent Chevrou, Aurélie Hurault, Shin Nakajima, and Philippe Quéinnec. A map of asynchronous communication models. In Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Creissac Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, and David Delmas, editors, *Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II*, volume 12233 of *Lecture Notes in Computer Science*, pages 307–322. Springer, 2019. doi:10.1007/978-3-030-54997-8\_20.

[DFLL23] Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Étienne Lozes. A partial order view of message-passing communication models. *Proc. ACM Program. Lang.*, 7(POPL):1601–1627, 2023. doi:10.1145/3571248.

[DG23] Loïc Desgeorges and Loïc Germerie Guizouarn. RSC to the rescu: Automated verification of systems of communicating automata. In Sung-Shik Jongmans and Antónia Lopes, editors, *Coordination Models and Languages - 25th IFIP WG 6.1 International Conference, COORDINATION 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings*, volume 13908 of *Lecture Notes in Computer Science*, pages 135–143. Springer, 2023. doi:10.1007/978-3-031-35361-1\_7.

[DLU25] Cinzia Di Giusto, Etienne Lozes, and Pascal Urso. Realisability and complementability of multiparty session types. In *Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming, PPDP 2025, Rende, Italy, September 10-11, 2025*. To appear, 2025.

[DR95] Volker Diekert and Grzegorz Rozenberg, editors. *The Book of Traces*. World Scientific, 1995. doi:10.1142/2563.

[DY12] Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In *Programming Languages and Systems - 21st European Symposium on Programming*,
ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, pages 194-213, 2012. doi:10.1007/978-3-642-28869-2\_10.

[EMR02] A.G. Engels, S. Mauw, and M.A. Reniers. A hierarchy of communication models for message sequence charts. Science of Computer Programming, 44(3):253-292, 2002. URL: https://www.sciencedirect.com/science/article/pii/S0167642302000229, doi:10.1016/S0167-6423(02)00022-9.

[Ger23] Loic Germerie Guizouarn. Communicating automata and quasi-synchronous communications. PhD thesis, Université Côte d'Azur, 2023.

[HLV<sup>+</sup>16] Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1), April 2016. doi:10.1145/2873052.

[HYC08] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. doi:10.1145/1328438.1328472.

[Lam78] Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, July 1978. doi:10.1145/359545.359563.

[Loh03] Markus Lohrey. Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci., 309(1-3):529-554, 2003. URL: https://doi.org/10.1016/j.tcs.2003.08.002, doi:10.1016/J.TCS.2003.08.002.

[LSW24] Elaine Li, Felix Stutz, and Thomas Wies. Deciding subtyping for asynchronous multiparty sessions. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 176-205. Springer, 2024. doi:10.1007/978-3-031-57262-3\_8.

[LSWZ23] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 350-373. Springer, 2023. doi:10.1007/978-3-031-37709-9\_17.

[LSWZ25] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Characterizing implementability of global protocols with infinite states and data. Proc. ACM Program. Lang., 9(OOPSLA1):1434-1463, 2025. doi:10.1145/3720493.

[LTY15] Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 221-232. ACM, 2015. doi:10.1145/2676726.2676964.

[Stu23] Felix Stutz. Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 32:1-32:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.32, doi:10.4230/LIPICS.ECOOP.2023.32.

[Stu24a] Felix Stutz. Implementability of Asynchronous Communication Protocols - The Power of Choice. PhD thesis, Kaiserslautern University of Technology, Germany, 2024. URL: https://kluedo.ub.rptu.de/frontdoor/index/index/docId/8077.

[Stu24b] Felix Stutz. Implementability of Asynchronous Communication Protocols - The Power of Choice. PhD thesis, Kaiserslautern University of Technology, Germany, 2024. URL: https://kluedo.ub.rptu.de/frontdoor/index/index/docId/8077.

[SY19] Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. doi:10.1145/3290343.
[VH93] Vasco Thudichum Vasconcelos and Kohei Honda. Principal typing schemes in a polyadic pi-calculus. In *CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings*, pages 524-538, 1993. doi:10.1007/3-540-57208-2\_36.

[Vil11] Jules Villard. *Heaps and Hops*. PhD thesis, École Normale Supérieure de Cachan, 2011.

[YG20] Nobuko Yoshida and Lorenzo Gheri. A very gentle introduction to multiparty session types. In Dang Van Hung and Meenakshi D'Souza, editors, *Distributed Computing and Internet Technology - 16th International Conference, ICDCIT 2020, Bhubaneswar, India, January 9-12, 2020, Proceedings*, volume 11969 of *Lecture Notes in Computer Science*, pages 73-93. Springer, 2020. doi:10.1007/978-3-030-36987-3\_5.