# Realisability and Complementability of Multiparty Session Types

Cinzia Di Giusto, Etienne Lozes, Pascal Urso

► To cite this version:

Cinzia Di Giusto, Etienne Lozes, Pascal Urso. Realisability and Complementability of Multiparty Session Types. 2025. hal-05166255v2

HAL Id: hal-05166255

https://hal.science/hal-05166255v2

Preprint submitted on 8 Aug 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
# Realisability and Complementability of Multiparty Session Types

Cinzia Di Giusto

Etienne Lozes

Pascal Urso

## Abstract

Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type, specifying the global behaviour, and local types, which are the projections of the global behaviour onto each local participant. An essential property of global types is realisability, i.e., whether the composition of the local behaviours conforms to those specified by the global type. We explore how realisability of MPST relates to their complementability, i.e., whether there exists a global type that describes the complementary behaviour of the original global type. First, we show that if a global type is realisable with p2p communications, then it is realisable with synchronous communications. Second, we show that if a global type is realisable in the synchronous model, then it is complementable, in the sense that there exists a global type that describes the complementary behaviour of the original global type. Third, we give an algorithm to decide whether a complementable global type, given with an explicit complement, is realisable in p2p. As a side contribution, we propose a complementation construction for global types with sender-driven choice, and more generally commutation-deterministic global types.

## 1 Introduction

The design of communication protocols for concurrent and distributed systems is a central concern in programming languages research. Modern systems – from microservices to IoT networks – rely on structured sequences of message exchanges between multiple parties. In the family of behavioural types [21], multiparty session types (MPST) were introduced by Honda et al. [14, 15, 23] and have emerged as a powerful methodology to specify and verify such structured interactions. An MPST defines a global type describing the communication protocol as a whole, which can be projected into local types for each participant.

This type-based approach enables static verification of communication safety (no unexpected messages) and liveness properties (no deadlocks) by ensuring each party’s code conforms to its local type. In essence, MPSTs allow protocol designers to treat communication patterns as first-class abstractions that yield a rigorous framework for building correct distributed applications.

In this work, we focus on the realisability problem, i.e., whether the local types projected from a global type can be recomposed into a concrete system that conforms to the intended global protocol. In classical MPST theory, protocols are often formulated under the sender-driven choice assumption: only one designated participant (the sender) decides between alternative message flow branches for all parties. While this assumption simplifies theoretical analysis, it proves too restrictive for many real-world protocols. We lift this assumption and build a theory for unrestricted choice.

Local types are often defined as systems of communicating finite state machines [7], following the works of Villard [22] and Denielou and Yoshida [10]: to every global type $G$, one can associate a system of communicating finite state machines (CFSMs) $\text{proj}(G)$ whose machines are the projections of $G$ onto each participant. In some recent works [19], global types may also be seen as a special case of Higher-order Message Sequence Charts [2] (HMSCs), an automaton model that accepts languages of message sequence charts (MSCs). Adopting such a point of view, every global type $G$ defines a language of MSCs $\mathcal{L}_{\text{msc}}^{\exists}(G)$ which provides a semantics of $G$. In this work, we study two notions on MPSTs coming from these connections with HMSCs and automata theory: deadlock-free realisability, and complementability.

Deadlock-free realisability, introduced by Alur et al. [2] for HMSCs, is central to the goal of *correct-by-construction* protocol design underpinning the MPST approach. Deadlock-free realisability ensures that $\text{proj}(G)$ does not suffer from communication mismatches, deadlocks, and behaviours that are not part of $\mathcal{L}_{\text{msc}}^{\exists}(G)$. In the literature on MPSTs, this property has appeared under various names, including *implementability* and *projectability*, with some slight variations in the formal definition of this notion.
The second notion, complementability, asks whether a global type $G$ admits a complementary one $\bar{G}$ that gives all those behaviours that are not described by $G$, i.e., for all synchronous-like MSCs $M$,

$$M \in \mathcal{L}_{\text{msc}}^{\exists}(\bar{G}) \Leftrightarrow M \notin \mathcal{L}_{\text{msc}}^{\exists}(G).$$

We also study whether some complementation procedure exists that explicitly constructs $\bar{G}$ from $G$, and with which complexity. These problems are popular in automata theory, e.g., it is well known that pushdown automata are not complementable in general, but become complementable adding a visibility condition [3]; Büchi automata are complementable [8], and there has been a long quest for efficient complementation procedures and optimisations for subclasses of Büchi automata.

## Contributions

In this work, we approach the realisability question for two fundamental communication models for implementing MPST protocols: the peer-to-peer (p2p) model, and the synchronous one. In the p2p model, processes communicate via point-to-point message passing over FIFO channels. In the synchronous model, communications are based on rendez-vous (handshakes where send and receive happen simultaneously), representing a globally synchronised message-passing semantics. These two models are widely considered as canonical extremes in analysing distributed protocols.

In this work, we also investigate for the first time the question of the complementability of global types. Our main contribution is to show that realisable global types form a subclass of the complementable ones. More in detail, we establish the following results:

* Every global type realisable in the synchronous communication model is complementable (Theorem 4.2), and the complementation is effective (based on projection and NFA complementation), with a doubly exponential blowup in the size of the global type.

* Realisability is decidable for complementable global types provided an explicit complement is also given as input, both in the synchronous communication model (Theorem 5.1) and in the peer-to-peer model (Theorem 5.4). The latter result is non-trivial and based on recent results on RSC systems [12].

* We also show that if a global type is realisable in the peer-to-peer model, then it is also realisable in the synchronous one (Theorem 5.2), which is not obvious, as deadlock-freedom is not a property that is monotonic in the communication model (a more permissive communication model may both hide some deadlocks and trigger new ones).

* Finally, we show that not all global types are complementable (Theorem 4.1) and we give procedures to find the complement of certain classes: global types with at most three participants are complementable (Corollary 4.1.1), as well as global types with sender-driven choices (Theorem 4.4).

## 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 and realisability are introduced in Section 3. Then Section 4 discusses the issue of complementability, discussing an example of a non-complementable global type as well as several complementation procedures. Finally, Section 5 establishes the decidability of realisability for complementable global types. Section 6 concludes with some final remarks and discusses related works.

# 2 Preliminaries

We assume a finite set of processes $\mathbb{P} = \{p, q, ...\}$ and a finite set of messages (labels) $\mathbb{M} = \{m, ...\}$. 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 \mathbf{Act}^*$, is an index $i$ in $\{1, \dots, \mathrm{length}(w)\}$; $i$ is a send (resp. receive) event of $w$ if $w[i]$ is a send (resp. receive) action. We write $\mathbf{events}_S(w)$ (resp. $\mathbf{events}_R(w)$) for the set of send (resp. receive) events of $w$ and $\mathbf{events}(w) = \mathbf{events}_S(w) \cup \mathbf{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.

**Executions.**

An execution is a well defined sequence of actions $e \in \mathbf{Act}^*$, where a receive action is always preceded by a unique corresponding send action.

**Definition 2.1 (Execution).** An execution over $\mathbb{P}$ and $\mathbb{M}$ is a sequence of actions $e \in \mathbf{Act}^*$ where an injective function from receive events to send events $\mathrm{src}_e: \mathbf{events}_R(w) \to \mathbf{events}_S(w)$ is such that for each receive event $i$ labeled with $?m^{p \to q}$, $\mathrm{src}_e(i)$ is labeled with $!m^{p \to q}$, and $\mathrm{src}_e(i) < i$.

For a set of executions $\mathcal{E}$, we write $\mathbf{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$. A *concatenation* $e_1 \cdot w$ of an execution $e_1$ and a sequence of actions $w$ is the execution $e_2 = e_1 \cdot w_2$ where $e_2$ is a completion of $e_1$ (note that $w$ is not an execution, since it may contain receive events which sources are in $e_1$). The *projection* $\mathrm{proj}_p(e)$ of an execution $e$ on a process $p$ is the subsequence of actions in $\mathbf{Act}_p$. A send event $s$ is *matched* if there is a receive event $r$ such that $s = \mathrm{src}(r)$. An execution $e$ is *orphan-free* if $\mathrm{src}$ is surjective over the send events of $e$, i.e., all send events are matched.

**Communication Models.**

In this paper, we consider two communication models: peer-to-peer (p2p) and synchronous (synch). However, as commented in the conclusions, this work is part of a bigger more general project and a large amount of the results of the paper can be extended to "any" communication model, or only require few assumptions. In this perspective, we introduce here a general definition of a communication model and discuss specific results regarding how it can be extended to the general case.

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

In the synchronous communication model synch, message exchanges can be thought as rendezvous 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.3 (synch).** An execution $e = (w, \mathrm{src}) \in \mathcal{E}_{synch}$ if for all send event $s \in \mathbf{events}_S(e)$, $s+1$ is a receive event of $e$ and $\mathrm{src}(s+1) = s$.

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.4 (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 $\mathbf{events}_S(e)$, with $s_1 < s_2$, one of the two holds:

* $s_2$ is unmatched, or

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

Note that, $\mathcal{E}_{synch} \subset \mathcal{E}_{p2p}$. Moreover, if $e$ is an execution in p2p, then $\mathrm{src}_e$ is defined as follows: the source of the $i$-th receive event of $q$ from $p$ is the $i$-th send event of $p$ to $q$. If $e$ is an execution in synch, then $\mathrm{src}_e$ is defined as follows: for all receive event $i$, $\mathrm{src}_e(i) = i - 1$.
<figure><img src="image_2.png" /><figcaption>Figure 1: Examples of MSCs. 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>

## 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 and 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) \mid p \in \mathbb{P} \text{ and } 0 \le i < \text{length}(w_p)\}$. The label `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.5 (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) \to \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 \to q}$, $\text{src}(\eta)$ is labeled with $!m^{p \to 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.1.** MSC $M$ in Fig. 1a 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 Fig. 1b 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$. This 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 \preceq_{\text{pref}} M'$, if for all $p \in \mathbb{P}$, $w_p$ is a prefix of $w'_p$ and $\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'_1)_{p \in \mathbb{P}}, \text{src}_1)$ and $M_2 = ((w'_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'_1 \cdot w'_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$).

## 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.6 (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$.

**Definition 2.7 (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 $\ln(M)$ for the set of all linearisations of $M$. We often identify a linearisation with the execution it induces.

**Example 2.2.** Let $M$ be the MSC in Fig. 1c. Then $!m_1$ happens before $?m_1$, which happens before $!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 \ln(M_c)$. On the other hand, consider the MSC $M$ in Fig. 1a; 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 $\ln(M') = \emptyset$.

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

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

**Example 2.3.** The MSC $M_b$ in Fig. 1b is linearisable in p2p, with $\ln_{\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 the MSC $M_c$ in Fig. 1c is linearisable in synch with $\ln_{\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.

**Definition 2.9 (Causally-closed communication model).** A communication model com is causally-closed if for all MSCs $M$, $\ln_{\text{com}}(M) \neq \emptyset$ implies that $\ln_{\text{com}}(M) = \ln(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 Fig. 1c, its linearisation $!m_1!m_2?m_1?m_2!m_3?m_3$ does not belong to $\ln_{\text{synch}}(M_c)$. To show that p2p is causally closed, notice that $<$ can be replaced with $\preceq_M$ in Definition 2.4.

**Lemma 2.1.** 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 events$_S(e)$, with $s_1 \preceq_M s_2$, one of the two holds:

* $s_2$ is unmatched, or

* there exist $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 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 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$

**Lemma 2.2.** $\mathcal{E}_{\text{p2p}}$ is causally-closed.

*Proof.* Let $M \in \mathcal{M}_{\text{p2p}}$ and $e$ be a linearisation of $M$. We want to show that $e \in \mathcal{E}_{\text{p2p}}$. By definition of $\mathcal{M}_{\text{p2p}}$, there is an execution $e' \in \mathcal{E}_{\text{p2p}}$ such that $\text{msc}(e') = M$. By Lemma 2.1, $e$ is also a p2p execution. $\square$

## Communicating finite state machines.

We assume standard notations for automata, words and languages. As usual, a non-deterministic finite state automaton (NFA) is a tuple $\mathcal{A} = (Q, \Sigma, \delta, l_0, F)$ where $Q$ is a set of control states, $\Sigma$ is an alphabet, $\delta: Q \times \Sigma \to 2^Q$ is the transition relation, $l_0$ is the initial control state, and $F \subseteq Q$ is the set of accepting states. The language $\mathcal{L}_{\text{words}}(\mathcal{A})$ of an NFA $\mathcal{A}$ and the notion of deterministic finite state automaton (DFA) or $\varepsilon$ transitions are defined as usual. We write $\hat{\mathcal{A}}$ for the automaton obtained from $\mathcal{A}$ by setting $F = Q$. We recall the definition of communicating finite state machines [7].
**Definition 2.10 (CFSM).** A communicating finite state machine (CFSM) is an NFA with $\epsilon$-transitions $\mathcal{A}$ over the alphabet $\mathcal{Act}$. A system of CFSMs is a tuple $\mathcal{S} = (\mathcal{A}_p)_{p \in \mathbb{P}}$.

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

**Definition 2.11 (Executions of a CFSMs in com).** Given a system $\mathcal{S} = (\mathcal{A}_p)_{p \in \mathbb{P}}$ of CFSMs, and a communication model com, $\mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{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}}(\mathcal{A}_p)$.

*Remark 2.1.* Let com be a communication model, $\mathcal{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}}(\mathcal{S})$ if and only if $e' \in \mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S})$. This follows from the fact that $\text{proj}_p(e) = \text{proj}_p(e')$ for all $p$.

We write $\mathcal{L}_{\text{msc}}^{\text{com}}(\mathcal{S})$ for the set $\{\text{msc}(e) | e \in \mathcal{L}_{\text{exec}}^{\text{com}}(\mathcal{S})\}$.

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.

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

All synchronous executions are orphan-free by definition.

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

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

*Remark 2.2.* A system of CFSMs $\mathcal{S}$ is deadlock-free for a communication model com if and only if

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

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

**Proposition 2.1 (Deadlock-freedom as an MSC property).** Assume com is p2p (respectively, com is synch). Then a system of CFSMs $\mathcal{S}$ is deadlock-free for com if and only if

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

# 3 Global Types

In this section, we define global types. We deviate from the standard definition to allow for more liberal behaviours. In our setting, global types are automata that 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. Two arrows $p_1 \xrightarrow{m_1} q_1$ and $p_2 \xrightarrow{m_2} q_2$ commute if $\{p_1, q_1\} \cap \{p_2, q_2\} = \emptyset$.

**Definition 3.1 (Global Type).** A global type $G$ is a non-deterministic finite state automaton over the alphabet $\text{Arr}$.

*Remark 3.1.* Following a more standard approach, we could equally define global types with the following grammar

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

and associate a non-deterministic finite state automaton to each global type.

We also consider deterministic global types that are defined as deterministic finite state automata over the alphabet $\text{Arr}$; we always explicitly stress determinism and otherwise implicitly assume non-determinism.

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 $\epsilon$ otherwise).
**Definition 3.2** (Projected system of CFSMs). The projected system of CFSMs $\text{proj}(G)$ associated to a global type $G$ is the tuple $(G_p)_{p \in \mathbb{P}}$.

Conversely, for every system, we can associate a global type 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 global type $\text{prod}(S) = (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 $(l_p, \varepsilon, l'_p) \in \delta_p$ for some $p \in \mathbb{P}$ and $l'_r = l_r$ for all $r \neq p$.

Projection and synchronous product form a Galois connection. For two NFAs $A, B$ over a same alphabet, let $A \sqsubseteq_{\text{words}} B$ denote that $\mathcal{L}_{\text{words}}(A) \subseteq \mathcal{L}_{\text{words}}(B)$; similarly, for two tuples of NFAs $A = (A_p)_{p \in \mathbb{P}}$ and $B = (B_p)_{p \in \mathbb{P}}$, let $A \sqsubseteq_{\text{words}} B$ denote that $\mathcal{L}_{\text{words}}(A_p) \subseteq \mathcal{L}_{\text{words}}(B_p)$ for all $p \in \mathbb{P}$.

**Proposition 3.1** (Galois connection). Let $S$ be a system of CFSMs and $G$ a global type. Then

$$ \text{proj}(G) \sqsubseteq_{\text{words}} S \quad \text{if and only if} \quad G \sqsubseteq_{\text{words}} \text{prod}(S). $$

*Proof.* We fix $S = (A_p)_{p \in \mathbb{P}}$. We show the two implications separately, starting from the right to left one.

* Assume that $G \sqsubseteq_{\text{words}} \text{prod}(S)$. Let $p \in \mathbb{P}$, and a sequence of actions $w_p \in \mathcal{L}_{\text{words}}(G_p)$; by definition of $G_p$, there is a sequence of arrows $w \in \mathcal{L}_{\text{words}}(G)$ such that $w_p = \text{proj}_p(w)$. By hypothesis, $w \in \mathcal{L}_{\text{words}}(\text{prod}(S))$. By definition of prod($S$), $w_p \in \mathcal{L}_{\text{words}}(A_p)$, which shows that $G_p \sqsubseteq_{\text{words}} A_p$, and more generally $\text{proj}(G) \sqsubseteq_{\text{words}} S$.

* Assume that $\text{proj}(G) \sqsubseteq_{\text{words}} S$. Let $w \in \mathcal{L}_{\text{words}}(G)$. By definition of $G_p$, $w_p \stackrel{\text{def}}{=} \text{proj}_p(w) \in \mathcal{L}_{\text{words}}(G_p)$. From the hypothesis, $w_p \in \mathcal{L}_{\text{words}}(A_p)$ for all $p$. Assume $w = a_1 \dots a_n$ and let $a_{i,p} = \text{proj}_p(a_i) \in \text{Act} \cup \{\varepsilon\}$. Since $w_p$ is accepted by $A_p$, there is a "run"

$$ \rho_p \stackrel{\text{def}}{=} q_{0,p} a_{1,p} q_{1,p} a_{2,p} \dots q_{n-1,p} a_{n,p} q_{n,p} $$

such that

- $q_{0,p}$ is the initial state of $A_p$, $q_{n,p}$ is an accepting state of $A_p$,

- if $a_i = \varepsilon$, then $q_{i,p} = q_{i-1,p}$,

- if $a_i \in \text{Act}$, there is a path from $q_{i-1}$ to $q_i$ labeled with $\varepsilon^* a_{i,p} \varepsilon^*$ that may include some $\varepsilon$ steps of $p$

There is therefore a run of $w$ on prod($S$)

$$ (q_{0,p})_{p \in \mathbb{P}} \quad a_1 \quad (q_{1,p})_{p \in \mathbb{P}} \quad a_2 \quad \dots \quad (q_{n-1,p})_{p \in \mathbb{P}} \quad a_n \quad (q_{n,p})_{p \in \mathbb{P}} $$

defined as a synchronous product of all $\rho_p$ (while reading $a_i$, we schedule first the silent steps, then the synchronised send and receive actions of the two processes involved in $a_i$, then the remaining silent steps). It is accepting by construction, since each $\rho_p$ is accepting, so $w \in \mathcal{L}_{\text{words}}(\text{prod}(S))$, which shows that $G \sqsubseteq_{\text{words}} \text{prod}(S)$. $\square$

We write $\text{exec}(w)$ to denote the execution obtained by replacing each arrow $p \xrightarrow{m} q$ of $w$ with $!m^{p \to q} \cdot ?m^{p \to q}$. We write $\text{msc}(w)$ to denote the MSC $\text{msc}(\text{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$ with respect to $\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)$:

$$ \begin{aligned} \mathcal{L}_{\text{msc}}^{\exists}(G) &\stackrel{\text{def}}{=} \{\text{msc}(w) \mid w \in \mathcal{L}_{\text{words}}(G)\} \\ \mathcal{L}_{\text{msc}}^{\forall}(G) &\stackrel{\text{def}}{=} \{\text{msc}(w) \mid [w] \subseteq \mathcal{L}_{\text{words}}(G)\}. \end{aligned} $$
Remark 3.2. Note that the two languages may differ even for deterministic global types, and do not confuse the existential and universal acceptance condition with the angelic and demoniac branching non-determinism of NFAs. Here $\exists$ and $\forall$ refer to angelic and demoniac commutative non-determinism, but the branching non-determinism is angelic in both cases. In particular, we have

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

**Definition 3.3 (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. As an example, any global type with $|P| \le 3$ is commutation-closed, as any two arrows share at least one process and therefore do not commute.

**Proposition 3.2.** 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.* (Sketch) 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 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.2, 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.11). $\square$

**Lemma 3.1.** 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/\forall}(G_2). $$

**Proposition 3.3.** 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/\forall}(\text{prod}(S)). $$

*Proof.* (Sketch) 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{prod}(S)$. $\square$

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

**Definition 3.4 (Global Type Language).** Let G be a global type and com a communication model. The language of G in com is $\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)\}$.

## 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 3.5 (Deadlock-free realisability).** A global type G is *deadlock-free realisable*<fnref n="1" /> in the communication model com if there is a system S such that the following two conditions hold:

1. $\mathcal{L}_{\text{exec}}^{\text{com}}(S) = \mathcal{L}_{\text{exec}}^{\text{com}}(G)$

2. S is deadlock-free in com.

Condition 1 of Definition 3.5 corresponds to *global type conformance*: the executions of the system do not deviate from the ones specified by the global type.

Deadlock-free realisability is equivalent to the notion of *safe realisability* of [2] when com is p2p or synch. This is not the case for other communication models, like mailbox, for which Proposition 2.1 does not hold. However, even for such communication models, global type conformance can still be characterized in terms of MSCs.

<footnote n="1">¹We sometimes say simply *realisable* instead of *deadlock-free realisable*.</footnote>
**Proposition 3.4** (Global type conformance as an MSC property). Let $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$, Condition 1 of Definition 3.5 is equivalent to $\mathcal{L}_{\text{msc}}^{\text{com}}(S) \subseteq \mathcal{L}_{\text{msc}}^{\exists}(G)$.

We conclude with a classical result, briefly stated in [2], that establishes that $\text{proj}(G)$ is the best system candidate for realising $G$. We say that an NFA is *pruned* if every state belongs to at least one accepting path. Note that we can always prune an NFA without changing its language.

**Proposition 3.5** (Canonicity of projection). Assume that $\mathcal{E}_{\text{com}} \supseteq \mathcal{E}_{\text{synch}}$ and $G$ is a pruned global type. Then $G$ is deadlock-free realisable in $\text{com}$ iff the two conditions of Definition 3.5 hold for $S = \text{proj}(G)$.

*Proof.* The only-if direction is immediate. Assume $S$ satisfies the two conditions of Definition 3.5. As $S$ is deadlock-free, we can assume without loss of generality that all machines of $S$ are pruned. By condition 1, we have $\mathcal{L}_{\text{msc}}^{\exists}(G) \subseteq \mathcal{L}_{\text{msc}}^{\text{com}}(S)$; since moreover $\mathcal{L}_{\text{msc}}^{\exists}(G) \subseteq \mathcal{M}_{\text{synch}}$, we get $\mathcal{L}_{\text{msc}}^{\exists}(G) \subseteq \mathcal{L}_{\text{msc}}^{\text{synch}}(S) = \mathcal{L}_{\text{msc}}^{\exists}(\text{prod}(S))$; since $\text{prod}(S)$ is commutation-closed (Proposition 3.3), we get $G \subseteq_{\text{words}} \text{prod}(S)$, and by Galois connection (Proposition 3.1),

$$ \text{proj}(G) \subseteq_{\text{words}} S. $$

From there, we get $\mathcal{L}_{\text{exec}}^{\text{com}}(\text{proj}(G)) \subseteq \mathcal{L}_{\text{exec}}^{\text{com}}(S) = \mathcal{L}_{\text{exec}}^{\text{com}}(G)$, which shows condition 1. For condition 2, since both $G$ and $S$ are pruned, $\text{proj}(\hat{G}) \subseteq_{\text{words}} \hat{S}$, and we get

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

□

In the remainder, we always implicitly assume that global types are pruned, and that deadlock-free realisability is defined according to Definition 3.5 with $S = \text{proj}(G)$.

# 4 Complementability

In this section, we introduce the notion of complementability for global types and we present some complementation procedures. Our complementation procedures target for some notable subclasses of global types, namely commutation-closed global types, synch-realisable global-types, and global types with sender-driven choice. For the later, we introduce a generalisation of sender-driven choice that we call commutation-determinism. Our complementation procedure naturally fits in this larger framework.

We start with the definition of complement global type:

**Definition 4.1** (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.

Note that $G$ is complementable if and only if $\text{det}(G)$ is complementable, since the determinisation does not change the MSC language (see Remark 3.2).

**Theorem 4.1.** Not all global types are complementable.

*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 $\mathbb{P}^2$ global type $G_0$ such that $\mathcal{L}_{\text{words}}(G_0) = (m_1 + m_2)^*(m_2 + m_3)^*$. Note that $G_0$ is commutation-closed and the MSCs of $\mathcal{L}_{\text{msc}}^{\exists}(G_0)$ are of the form depicted in Fig. 3.

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

$$ \mathbf{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 Fig. 2. 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.1, 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, hence the contradiction. □

<footnote n="2">²for instance take the minimal DFA recognising this language</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 2: A non-complementable global type</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 3: The shape of the MSCs in $\mathcal{L}_{\text{msc}}^{\exists/\forall}(G_0)$ for the global type $G_0$.</figcaption></figure>

## 4.1 Complementation By Duality

We write dual(G) for the dual DFA of a deterministic 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.

**Proposition 4.1.** If G is deterministic and 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.1 we have the following immediate result.

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

Now, even if a global type G is not commutation-closed, it may be "enlarged" as the commutation-closed global type prod Understanding of this concept is often called Cartesian abstraction [4]. This commutation-closed global type can later be complemented by duality to an under-approximation of a complement of G. When G is deadlock-free realisable in synch, this under-approximation is exact.

**Theorem 4.2.** If a global type G is deadlock-free realisable in synch, then dual det.prod Fouling of this process is a complement of G.
*Proof.* Let $G$ be a global type that is deadlock-free realisable in synch. By Condition (CC) of Definition 3.5,

$$ \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.3, the synchronous product prodность 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.1, dual det prod proj G is a complement of prod proj G, thus of G. $\square$

*Remark 4.1.* In terms of complexity, complementation by duality is linear in the number of states of the global type $G$ (possibly after adding a sink state). However, the determined Cartesian abstraction det.prod.Proj(G)) involves in the worst case a doubly exponential blowup.

## 4.2 Complementation by Renunciation

In this section, 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 labeling outgoing transitions of $s$ in $G$.

**Definition 4.2 (Sender-Driven [20]).** A global type $G$ is sender-driven if it is deterministic and for every state $s$ of $G$,

$$ \text{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 [16]. We slightly generalise this condition as the complementation procedure we are about to present also works in this larger setting.

**Definition 4.3 (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 \text{choices}_G(s)$, $a$ and $b$ do not commute.

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

**Definition 4.4 (Complementation by renunciation).** Let $G$ be a commutation-deterministic global type. Let $S$ be the set of states of $G$, $\bar{S} = \{\bar{s} \mid s \in S\}$, and $S' = S \uplus \bar{S}$. 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 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 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 renun(G);

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

* for any state $s$ of G, for any arrow $a \in \text{choices}_G(s)$, for any arrow $b \notin \text{choices}_G(s)$ that commutes with $a$, $(s, b, (s, a))$ (resp. $((s, a), b, (s, a))$) is a transition in renun(G)
<figure><img src="image_5.png" /><figcaption>Figure 4: 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>

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

* for any state $s$ of $G$, for any arrow $a \in \text{choices}_G(s)$, for any arrow $b \notin \text{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.1.** Fig. 4 depicts a sender-driven global type and the complement computed according to Definition 4.4.

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.2.** Let $G$, $\text{renun}(G)$, $M_1, M_2$ be the global types and MSCs depicted in Fig. 4. 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 two kinds of renuncia-
tion: 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.3.** Consider the MSC $M_3 = \mathbf{msc}(a_1a'_2a_3)$, with $a'_2 = p \xrightarrow{m'_2} q'$ for some $m'_2 \neq m_2$. Then $M_3$ is accepted by 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 $\mathbf{msc}(w_{3,2}) = M_3$ is not in $\mathcal{L}_{\text{words}}(\text{renun}(G))$. More generally, 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 = \mathbf{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 $\mathbf{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 $\mathbf{msc}(w) = M$ (otherwise two arrows of choices$_G(s)$ would commute, contradicting the commutation-determinism of $G$).

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

We also define resid$(M, s)$ as $\mathbf{msc}(w)$ for some $w$ such that $M = \mathbf{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 $\mathbf{msc}(w) = M$, $\text{next}(M, s)$ never occurs first.

**Example 4.5.** Consider the MSC $M_4 = \mathbf{msc}(a_1a_2a_3)$, and the state $s_0$ of $G$ in Fig. 4. Then $\text{resid}(M_4, s_0) = \mathbf{msc}(a_2a_3)$. On the other hand, for the MSC $M_5 = \mathbf{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.3.** 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 (sketch).* 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 $\mathbf{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 $\mathbf{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 $\mathbf{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) = \mathbf{msc}(w')$. It follows that $\text{resid}(M, s_0) \in \mathcal{L}_{\text{msc}}^{\exists}(G_s)$, and the contradiction. $\square$

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

*Proof (sketch).* It is routine to check that an MSC $M$ is accepted by 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 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.3, 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$
# 5 Decidability of Realisability

In this section, we show that the realisability problem for complementable global types, given with an explicit complement, is decidable in both the synchronous and the p2p model. We first show the result for the synchronous model, which is simpler, and then extend it to the p2p model using a characterisation of realisability in the p2p model.

## 5.1 Realisability in the synchronous model

**Theorem 5.1.** Given a global types $G$ and a complement $\bar{G}$ of $G$, it is decidable in PSPACE complexity whether $G$ is deadlock-free realisable in synch.

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

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

By Lemma 3.1, this reduces to checking the emptiness of $\mathcal{L}_{\text{words}}(\text{prod}(\text{proj}(G)) \otimes \bar{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 global type $\text{prod}(\text{proj}(G))$ can be lazily constructed while guessing a path to an accepting state.

Assuming that Condition (CC) of Definition 3.5 holds, the second condition of Definition 3.5 is equivalent to whether all control states of $\text{prod}(\text{proj}(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.2 Realisability in the p2p model

We now consider the realisability problem in the p2p model. Note that relaxing the communication model may both remove some deadlock situations, but also introduce some new ones (because new configurations may be reachable). So realisability in the p2p model and realisability in the synch model could be expected to be two different properties, none of which implies the other. Due to the fact that global types enforce a form of synchronous-like behaviour, however, it turns out that every global type that is realisable in the p2p model is also realisable in the synch model.

**Theorem 5.2.** If $G$ is deadlock-free realisable in p2p, then $G$ is deadlock-free realisable in synch.

*Proof.* Assume that $G$ is p2p-realisable. We show that $G$ is synch-realisable by verifying the two conditions of Definition 3.5.

* Since $\mathcal{E}_{\text{synch}} \subseteq \mathcal{E}_{\text{p2p}}$, we have

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

By Proposition 3.4 and the hypothesis that $G$ is p2p-realisable, we have that

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

Therefore, we have

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

and by Proposition 3.4, $G$ satisfies condition 1 of Definition 3.5 for being deadlock-free realisable in synch.

* By Proposition 2.1 and condition 1, the condition 2 of Definition 3.5 is equivalent to

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

when com is either p2p or synch. We can therefore assume that

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

and we show that

$$ \mathcal{L}_{\text{msc}}^{\text{synch}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\exists}(G)) $$
This follows from the fact that

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

because $\mathcal{E}_{\text{synch}} \subseteq \mathcal{E}_{\text{p2p}}$.

□

We now show a "converse" of Theorem 5.2, which precisely states which additional conditions are needed to ensure that a global type that is deadlock-free realisable in the synch model is also deadlock-free realisable in the p2p model.

**Theorem 5.3 (Reduction to realisability in synch).** A global type $G$ is deadlock-free realisable in p2p if and only if the following four conditions hold:

1. $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(G)) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$

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

3. $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{p2p}}(\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 p2p-realisable global type.

1. By Condition 2 of Definition 3.5, $\text{proj}(G)$ is deadlock-free in p2p. By Proposition 2.1,

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

By Condition 1 of Definition 3.5,

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

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

2. Let $e \in \mathcal{L}_{\text{exec}}^{\text{p2p}}(\text{proj}(G))$; we show that $e$ is orphan-free. By Condition 1 of Definition 3.5, $\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{p2p}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(G)))$ by Condition 2 of Definition 3.5 and Proposition 2.1.

4. Follows from Lemma 5.2

⇔ 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 p2p-realisable as it satisfies the two conditions of Definition 3.5.

**Condition 1** By Proposition 3.4, we show that

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

By Condition 1 of Theorem 5.3,

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

and by Condition 4 of Theorem 5.3 and Proposition 3.4, 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 1.

**Condition 2** follows from Proposition 2.1 and Condition 3 of Theorem 5.3.

□
<figure><img src="image_6.png" /><figcaption>Figure 5: Hierarchy of semantic properties of global types</figcaption></figure>

A system $\mathcal{G}$ with $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\mathcal{G}) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$ is called *realisable with synchronous communications (RSC)* after Germerie [12]. Germerie showed that the RSC property is decidable and that whether a RSC system may reach a regular set of configurations is also decidable. As a consequence, conditions 1 and 2 of Theorem 5.3 are decidable. Assuming that $\text{proj}(\mathcal{G})$ is RSC, $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(\hat{\mathcal{G}}))$ can be coded as an effective regular set of executions, as well as Prefixes($\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(\mathcal{G}))$), and Condition 3 of Theorem 5.3 reduces to checking the inclusion of two NFAs, which can be checked in PSPACE using a lazy construction of the NFAs.

From these results we can conclude that it is decidable whether a given complementable global type, together with its complement, is deadlock-free realisable in the p2p model.

**Theorem 5.4.** Given a complementable global type $G$ and a complement $\bar{G}$, it is decidable whether $G$ is deadlock-free realisable in p2p.

# 6 Concluding remarks

In this paper, we investigated the realisability and complementability of MPSTs across two canonical communication models: synchronous and asynchronous (p2p). We reduce the task of checking realisability in the complex asynchronous setting to the simpler synchronous case, as long as the initial system satisfies key properties such as deadlock-freedom, absence of orphan messages, and a form of "synchronisability" (RSC property [12]). Said differently, we showed that global types that are realisable in the p2p model form a recursive subclass of the ones realisable in synch. We also showed that this latter class itself is a subclass of the class of global types that are equivalent (in terms of MSC semantics) to a commutation-closed global type, and these form a subclass of the complementable ones (see Figure 5). Among others, it suggests that any framework enforcing "by construction" the realisability of global types "hides" a complementation procedure for the global types embraced by this framework.

We explored the complementability of global types, looking for complementation procedures. We first observed that the complementation of a global type is not always possible, but we proposed several complementation procedures for various subclasses of global types, among which the one of sender-driven global types. For each of these subclasses, we derive a decision procedure for realisability in synch with PSPACE complexity, and for realisability in p2p with at most EXPSPACE complexity. Figure 6 summarises these results.

We believe that our results not only improve theoretical clarity but also are amenable to generalisation. 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.9). Based on this, we conjecture that our results can be extended to models such as bag and causally ordered systems, both of which satisfy causal closure. In contrast, models like mailbox
<table><caption>Figure 6: Summary of complementation procedures for global types</caption><thead><tr><th>Class of global types</th><th>Complementation procedure</th><th>Size of complement</th><th>synch-realisability</th></tr></thead><tbody><tr><td>|P| ≤ 3</td><td>G : det ↦→ dual(G) : det</td><td>linear</td><td>PSPACE</td></tr><tr><td>commutation-closed</td><td>G : det ↦→ dual(G) : det</td><td>linear</td><td>PSPACE</td></tr><tr><td>com-realisable</td><td>G : ndet ↦→ dual det.prod proj(G) det</td><td>doubly exponential</td><td>constant time</td></tr><tr><td>sender-driven choices</td><td>G : det ↦→ renun(G) : ndet</td><td>linear</td><td>PSPACE</td></tr><tr><td>commutation deterministic</td><td>G : det ↦→ renun(G) : ndet</td><td>linear</td><td>PSPACE</td></tr></tbody></table>

or those based on bounded FIFO channels lack this property and therefore require specialised analysis. We aim to explore these cases further and, ultimately, to develop a more comprehensive framework in future work.

We introduced the notion of commutation-determinism generalising the notion of sender-driven global types. It is unclear whether this generalisation may be immediately useful, like capturing "real" global types. However, we believe it is a valuable idea as it may prompt further generalisations; for instance, a reader influenced by categories may think about "time reversing" transformations, and how global types that are "commutation-codeterministic" (their mirror language is recognized by a commutation-deterministic automaton) may be complemented.

Apart from these generalisations, we aim to extend the framework to cover more expressive classes of global types, including those that go beyond synchronisable MSCs. We also plan to revisit results on the realisability of MSCs, possibly linking criteria such as send-validity and receive-validity [16, 19] to our synchronous realisability conditions. This opens the door to formally investigating whether global types that are realisable in the synchronous model satisfy send-validity, or if this is a weaker or stronger condition—this remains an open and promising question.

## Related works

We conclude with a brief excursus on related works. Naturally, the most closely related lines of research are those concerning MPST. Comprehensive surveys on the topic are available in [9, 23]. 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 [18] 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 underlying models are substantially different, it is worth mentioning [5] that discusses projectability in the context of synchronous MPST.

The connection between communicating automata and behavioural types were first explored by Villedard [22] for the binary case and Deniélou and Yoshida in [10] for MPSTs; the connection between HMSCs and MPST was initiated by Stutz [19, 20]. In this work, we slightly push further this connection explicating the MSC-based semantics of global types that remained somehow implicit in Stutz's work.

In [16, 19], the authors revisited the theory of MPST projections through the lenses of realisability of MSCs, and proposed two criteria, called *send validity* and *receive validity*, that yield the first sound and complete characterisation of MPST implementable in the context of the p2p communication model, provided the global type is sender-driven. In particular, the second criteria, receive validity, is strongly justified by the choice of the communication model and is unsound for other communication models beyond p2p. An important difference, though, is that these works address the *implementability* problem, that defines deadlock-freedom as the absence of situations where all processes are blocked. Unlike deadlock-free realisability, implementability does not guarantee the absence of unspecified receptions
or orphan messages immediately from its definition, but only induces it "as a side effect", at least for sender-driven global types.

Realisability was introduced by Alur et al [2] with early undecidability results, later simplified by Lohrey [17], showing in particular that deadlock-free realisability is decidable for bounded communications (a result recently generalised by Bollig et al [6]), but undecidable with 5 participants. Our results show that realisability is decidable with 3 participants, which leaves a gap, even if Alur et al showed that weak realisability is undecidable for 4 participants with p2p communications. Guanciale and Tuosto [13] studied realisability on pomsets.

Mazurkiewicz traces [11] are words over partially commutative alphabets. Synchronous MSCs (but not asynchronous ones) can be seen as Mazurkiewicz traces over the alphabet Arr of arrows. Consistent regular trace languages [1] are the ones recognized by commutation-closed finite automata. Zielonka's asynchronous automata [24] are a model of a distributed implementation of a regular trace language. It differs from realizability of MPSTs and HMSCs in several ways: first, processes in this model synchronise by rendezvous (that may involve more than two processes), second processes may exchange additional information during rendezvous (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 (the "gossip") is highly non-trivial in this setting. Although quite far from MPSTs at first sight, some old works on Mazurkiewicz traces could possibly shed 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 commutation-determinism.

## References

[1] IJsbrand Jan Aalbersberg and Grzegorz Rozenberg. Theory of traces. *Theoretical Computer Science*, 60(1):1-82, 1988. URL: https://www.sciencedirect.com/science/article/pii/0304397588900515, doi:10.1016/0304-3975(88)90051-5.

[2] 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.

[3] Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In *Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing*, STOC '04, page 202-211, New York, NY, USA, 2004. Association for Computing Machinery. doi:10.1145/1007352.1007390.

[4] Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. Boolean and cartesian abstraction for model checking c programs. In *Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems*, TACAS 2001, page 268-283, Berlin, Heidelberg, 2001. Springer-Verlag.

[5] 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.

[6] Benedikt Bollig, Marie Fortin, and Paul Gastin. High-level message sequence charts: Satisfiability and realizability revisited. In Elvio Gilberto Amparore and Lukasz Mikulski, editors, *Application and Theory of Petri Nets and Concurrency - 46th International Conference, PETRI NETS 2025, Paris, France, June 22-27, 2025, Proceedings*, volume 15714 of Lecture Notes in Computer Science, pages 109-129. Springer, 2025. doi:10.1007/978-3-031-94634-9_6.

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

[8] J.R. Buechi. On a decision method in restricted second-order arithmetic. *Proc. Internat. Congr. Logic, Methodology and Philosophy of Science*, 1:1-12, 1962.
[9] 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.

[10] 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.

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

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

[13] Roberto Guanciale and Emilio Tuosto. Realisability of pomsets. *J. Log. Algebraic Methods Program.*, 108:69–89, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.06.003, doi:10.1016/J.JLAMP.2019.06.003.

[14] 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.

[15] 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 Gi-anluigi Zavattaro. Foundations of session types and behavioural contracts. *ACM Comput. Surv.*, 49(1), April 2016. doi:10.1145/2873052.

[16] 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.

[17] 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.

[18] 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.

[19] 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.

[20] 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.

[21] 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.

[22] Jules Villard. *Heaps and Hops*. PhD thesis, École Normale Supérieure de Cachan, 2011.
[23] 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.

[24] Wiesław Zielonka. Safe executions of recognizable trace languages by asynchronous automata. In Albert R. Meyer and Michael A. Taitslin, editors, *Logic at Botik '89, Symposium on Logical Foundations of Computer Science, Pereslavl-Zalessky, USSR, July 3-8, 1989, Proceedings*, volume 363 of Lecture Notes in Computer Science, pages 278–289. Springer, 1989. doi:10.1007/3-540-51237-3_22.

## A Standard notions on automata

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})$.

## B Proof of Proposition 2.1

**Proposition 2.1** (Deadlock-freedom as an MSC property). Assume com is p2p (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 $S$ is deadlock-free: $\mathcal{L}_{\text{exec}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{exec}}^{\text{com}}(S))$, then $\mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S}) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{com}}(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}}(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}}(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}}(S))$.
⇔: for com = p2p: if $\mathcal{L}_{\text{msc}}^{\text{com}}(\hat{S}) \subseteq$ Prefixes($\mathcal{L}_{\text{msc}}^{\text{com}}(S)$), then 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}}(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}}(S)$ such that $\text{msc}(e) \leq_{\text{pref}}^{\text{msc}} M'$. By definition of $\leq_{\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 $<$ 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 $<$ 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, $<$ 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., $\leq_{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}}(S)$ because $e''$ is a linearisation of $M'$, $M' \in \mathcal{L}_{\text{msc}}^{\text{com}}(S)$, and p2p is causally closed (Lemma 2.2).

Altogether, we have shown that e has a completion in $\mathcal{L}_{\text{exec}}^{\text{com}}(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 $<$ is a synchronous linearisation as the concatenation of two synchronous linearisations. $\square$

## C Proof of Lemma 3.1

**Lemma 3.1.** 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/\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/\forall}(G_2)$. Since $G_2$ is commutation-closed, $\text{msc}(w) \in \mathcal{L}_{\text{msc}}^{\exists/\forall}(G_2)$. Therefore, $\text{msc}(w) \in \mathcal{L}_{\text{msc}}^{\exists}(G_1) \cap \mathcal{L}_{\text{msc}}^{\exists/\forall}(G_2)$.
\Leftrightarrow \text{Conversely, assume that } M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1) \cap \mathcal{L}_{\text{msc}}^{\exists/\forall}(G_2). \text{ In particular, } M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1), \text{ which means that there is a word } w_1 \text{ such that } M = \text{msc}(w_1) \text{ and } w_1 \in \mathcal{L}_{\text{words}}(G_1). \text{ Since } M \in \mathcal{L}_{\text{msc}}^{\exists/\forall}(G_2), \text{ there is a word } w_2 \text{ such that } M = \text{msc}(w_2) \text{ and } w_2 \in \mathcal{L}_{\text{words}}(G_2). \text{ Since } G_2 \text{ is commutation-closed and } \text{msc}(w_1) = \text{msc}(w_2), w_1 \in \mathcal{L}_{\text{words}}(G_2). \text{ 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), \text{ which means that } M \in \mathcal{L}_{\text{msc}}^{\exists}(G_1 \otimes G_2). \hfill \square

D Proof of Theorem 5.3

**Theorem 5.3** (Reduction to realisability in synch). A global type G is deadlock-free realisable in p2p if and only if the following four conditions hold:

1. $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(G)) \subseteq \text{Prefixes}(\mathcal{M}_{\text{synch}})$

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

3. $\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{p2p}}(\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 p2p-realisable global type.

1. By Condition 2 of Definition 3.5, $\text{proj}(G)$ is deadlock-free in p2p. By Proposition 2.1,

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

By Condition 1 of Definition 3.5,

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

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

2. Let $e \in \mathcal{L}_{\text{exec}}^{\text{p2p}}(\text{proj}(G))$; we show that $e$ is orphan-free. By Condition 1 of Definition 3.5, $\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{p2p}}(\text{proj}(\hat{G})) \subseteq \text{Prefixes}(\mathcal{L}_{\text{msc}}^{\text{p2p}}(\text{proj}(G)))$ by Condition 2 of Definition 3.5 and Proposition 2.1.

4. Follows from Lemma 5.2

☐ 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 p2p-realisable as it satisfies the two conditions of Definition 3.5.

**Condition 1** By Proposition 3.4, we show that

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

By Condition 1 of Theorem 5.3,

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

and by Condition 4 of Theorem 5.3 and Proposition 3.4, 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 1.

**Condition 2** follows from Proposition 2.1 and Condition 3 of Theorem 5.3.

☐