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

HAL
open science

# Global Types and Event Structure Semantics for Asynchronous Multiparty Sessions

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini

► To cite this version:

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini. Global Types and Event Structure Semantics for Asynchronous Multiparty Sessions. Fundamenta Informaticae, 2024, 192 (1), pp.1-75. 10.3233/FI-242188. hal-04895576

HAL Id: hal-04895576

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

Submitted on 18 Jan 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Global Types and Event Structure Semantics
for Asynchronous Multiparty Sessions

Ilaria Castellani*

INRIA, Université Côte d'Azur, France
ilaria.castellani@inria.fr

Mariangiola Dezani-Ciancaglini

Dipartimento di Informatica, Università di Torino, Italy
dezani@di.unito.it

Paola Giannini†

DiSSTE, Università del Piemonte Orientale, Italy
paola.giannini@uniupo.it

**Abstract.** We propose an interpretation of multiparty sessions with asynchronous communication as *Flow Event Structures*. We introduce a new notion of asynchronous type for such sessions, ensuring the expected properties for multiparty sessions, including progress. Our asynchronous types, which reflect asynchrony more directly and more precisely than standard global types and are more permissive, are themselves interpreted as *Prime Event Structures*. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its asynchronous type, namely their domains of configurations are isomorphic.

**Keywords:** Communication-centric Systems, Communication-based Programming, Process Calculi, Event Structures, Multiparty Session Types.

<footnote>Address for correspondence: Paola Giannini, Computer Science Institute, DiSSTE, Pz. S. Eusebio 5 - 13100 Vercelli, Italy
*This research has been supported by the ANR17-CE25-0014-01 CISC project.</footnote>

<footnote>†This original research has the financial support of the Università del Piemonte Orientale. This work was partially funded by the MIUR project "T-LADIES" (PRIN 2020TL3X8X).</footnote>
# 1. Introduction

Session types describe interactions among a number of participants, which proceed according to a given protocol. They extend classical data types by specifying, in addition to the type of exchanged data, also the interactive behaviour of participants, namely the sequence of their input/output actions towards other participants. The aim of session types is to ensure safety properties for sessions, such as the absence of communication errors (no type mismatch in exchanged data) and deadlock-freedom (no standstill until every participant is terminated). Sometimes, a stronger property is targeted, called progress (no participant waits forever).

Initially conceived for describing binary protocols in the π-calculus [1, 2], session types have been later extended to multiparty protocols [3, 4] and embedded into a range of functional, concurrent, and object-oriented programming languages [5]. While binary sessions can be described by a single session type, multiparty sessions require two kinds of types: a global type that describes the whole session protocol, and local types that describe the contributions of the individual participants to the protocol. The key requirement in order to achieve the expected safety properties is that all local types be obtained as projections from the same global type.

Communication in sessions is always directed from a given sender to a given receiver. It can be synchronous or asynchronous. In the first case, sender and receiver need to synchronise in order to exchange a message. In the second case, messages may be sent at any time, hence a sender is never blocked. The sent messages are stored in a queue, where they may be fetched by the intended receiver. Asynchronous communication is often favoured for multiparty sessions, since such sessions may be used to model web services or distributed applications, where the participants are spread over different sites.

Session types have been shown to bear a strong connection with models of concurrency such as communicating automata [6], as well as with message-sequence charts [4], graphical choreographies [7, 8], and various brands of linear logics [9, 10, 11, 12, 13].

In a companion paper [14], we investigated the relationship between synchronous multiparty sessions and Event Structures (ESs) [15], a well-known model of concurrency which is grounded on the notions of causality and conflict between events. We considered a simple calculus, where sessions are described as networks of sequential processes [16], equipped with standard global types [3]. We proposed an interpretation of sessions as Flow Event Structures (FESs) [17, 18], as well as an interpretation of global types as Prime Event Structures (PESs) [19, 20]. We showed that for typed sessions these two interpretations yield isomorphic domains of configurations.

In the present paper, we undertake a similar endeavour in the asynchronous setting. This involves devising a new notion of asynchronous type for asynchronous networks. We start by considering a core session calculus as in the synchronous case, where processes are only able to exchange labels, not values, hence local types coincide with processes. Moreover, networks are now endowed with a queue and they act on this queue by performing outputs or inputs: an output stores a message in the queue, while an input fetches a message from the queue. The present paper differs from [14] not only for the operational semantics, but also for the typing rules and more essentially for the event structure semantics of sessions and types.

To illustrate the difference between synchronous and asynchronous sessions and motivate the introduction of new types for the latter, let us discuss a simple example. Consider the network:

$$N = p[\text{q}\!\text{l}; \text{q}\?\text{l}'] \parallel \text{q}[\text{p}\!\text{l}'; \text{p}\?\text{l}]$$

where each of the participants p and q wishes to first send a message to the other one and then receive a message from the other one.
In a synchronous setting this network is stuck, because a network communication arises from the synchronisation of an output with a matching input, and here the output $q!l$ of p cannot synchronise with the input $p?l$ of q, since the latter is guarded by the output $p!l'$. Similarly, the output $p!l'$ of q cannot synchronise with the input $q?l'$ of p. Indeed, this network is not typable because any global type for it should have one of the two forms:

$$G_1 = p \to q : l; q \to p : l'$$

$$G_2 = q \to p : l'; p \to q : l$$

However, neither of the $G_i$ projects down to the correct processes for both p and q in N. For instance, $G_1$ projects to the correct process $q!l \cdot q?l'$ for p, but its projection on q is $p?l \cdot p!l'$, which is not the correct process for q.

In an asynchronous setting, on the other hand, this network is run in parallel with a queue $M$, which we indicate by $N \parallel M$, and it can always move for whatever choice of $M$. Indeed, the moves of an asynchronous network are not complete communications but rather “communication halves”, namely outputs or inputs. For instance, if the queue is empty, then $N \parallel \emptyset$ can move by first performing the two outputs in any order, and then the two inputs in any order. If instead the queue contains a message from p to q with label $l_1$, followed by a message from q to p with label $l_2$, which we indicate by $M = \langle p, l_1, q \rangle \cdot \langle q, l_2, p \rangle$, then, assuming $l_1 \neq l$ and $l_2 \neq l'$, the network will be stuck after performing the two outputs. Indeed, the two inputs will not be able to occur, since the two messages on top of the queue are not those expected by p and q. Hence we look for a notion of type that accepts the network $N \parallel \emptyset$ but rejects the network $N \parallel \langle p, l_1, q \rangle \cdot \langle q, l_2, p \rangle$.

The idea for our new asynchronous types is quite simple: to split communications into outputs and inputs, and to add a queue to the type, thus mimicking very closely the behaviour of asynchronous networks. Hence, our asynchronous types have the form $G \parallel M$. Clearly, we must impose some well formedness conditions on such types, taking into account also the content of the queue. Essentially, this amounts to requiring that each input appearing in the type be justified by a preceding output in the type or by a message in the queue, and vice versa, that each output in the type or message in the queue be matched by a corresponding input in the type.

Having introduced this new notion of type, it becomes now possible to type the network $N \parallel \emptyset$ with the asynchronous type $G \parallel \emptyset$, where $G = pq!l; qp!l'; pq?l; qp?l'$, or with the other asynchronous types obtained from it by swapping the outputs and/or the inputs. Instead, the network $N \parallel \langle p, l_1, q \rangle \cdot \langle q, l_2, p \rangle$ will be rejected, because the asynchronous type $G \parallel \langle p, l_1, q \rangle \cdot \langle q, l_2, p \rangle$ is not well formed, since its two inputs do not match the first two messages in the queue.

A different solution was proposed in [21] by means of an asynchronous subtyping relation on local types which allows outputs to be brought forward. In our setting this boils down to a subtyping relation on processes yielding both $q!l; q?l' \leq q?l'; q!l$ and $p!l'; p?l \leq p?l; p!l'$. With the help of this subtyping, both $G_1$ and $G_2$ become types for the network $N \parallel \emptyset$ above. Unfortunately, however, this subtyping turned out to be undecidable [22, 23].

To define our interpretations of asynchronous networks and types into FESs and PESs respectively, we follow the same schema as for their synchronous counterparts in our previous work [14]. In particular, the events of the ESs are defined syntactically and they record the “history” of the particular communication occurrence they represent. More specifically, the events of the FES associated with a network – which we call *network events* – record the local history of their communication. By contrast, the events of the PES associated with an asynchronous type – which we call *type events* – record the global history of their communication, namely the whole sequence of past communications that caused it, which is extracted from the computation trace using a permutation equivalence. However, while in [14] an event represented a communication between two participants, here it represents an output or an input pertaining to a single participant. Hence,
some care must be taken in defining the flow relation between network events<fnref n="1" />, and in particular the “cross-flow” between an output event and the matching input event, since input events may also be justified by a message in the queue. For type events, queues appear inside events and affect the permutation equivalence. Therefore, our ES semantics for the asynchronous setting is far from being a trivial adaptation of that given in [14] for the synchronous setting.

To sum up, the contribution of this paper is twofold:

1) We propose an original syntax for asynchronous types, which, in our view, models asynchronous communication in a more natural and precise way than existing approaches. Our type system is more permissive than the standard one [4] – in particular, it allows outputs to take precedence over inputs as in [21], a characteristics of asynchronous communication – but it remains decidable. We show that our asynchronous types ensure classical safety properties as well as progress.

2) We present an Event Structure semantics for asynchronous networks and asynchronous types. Networks are interpreted as FESs and asynchronous types are interpreted as PESs. Our main result here is an isomorphism between the configuration domains of the FES of a typed network and the PES of its asynchronous type.

The paper is organised as follows. Section 2 introduces our calculus for asynchronous multiparty sessions. Section 3 introduces asynchronous types and the associated type system, establishing its main properties. Section 4 recaps some necessary background on Event Structures. In Section 5 we recall our interpretation of processes as PESs, taken from our companion paper [14]. In Section 6 we present our interpretation of asynchronous networks as FESs. In Section 7 we define our interpretation of asynchronous types as PESs. Finally, in Section 8 we prove the equivalence between the FES semantics of a network and the PES semantics of its asynchronous type. We conclude with a discussion on related work and future research directions in Section 9. All results are given with full proofs. When not appearing in the main text, the proofs may be found in the Appendix, which contains also the glossary of symbols.

## 2. A Core Calculus for Multiparty Sessions

We now formally introduce our calculus, where asynchronous multiparty sessions are represented as networks of sequential processes with queues.

We assume the following base sets: *participants*, ranged over by p, q, r and forming the set Part, and *labels*, ranged over by *l*, *l'*, ... and forming the set Lab.

Let $\pi \in \{p!l, p?l | p \in \text{Part}, l \in \text{Lab}\}$ denote an *atomic action*. The action $p!l$ represents an output of label $l$ to participant p, while the action $p?l$ represents an input of label $l$ from participant p.

**Definition 2.1. (Processes)**

Processes are defined by:

$$ P ::=^{coind} \bigoplus_{i \in I} p!l_i; P_i \mid \sum_{i \in I} p?l_i; P_i \mid 0 $$

where $I$ is non-empty and $l_h \neq l_k$ for all $h, k \in I$, $h \neq k$, i.e. labels in choices are all different.

<footnote n="1">¹In FESs, the flow relation represents a direct causality between events.</footnote>
The symbol ::=coind, in the definition above and in later definitions, indicates that the productions should be interpreted *coinductively*. Namely, they define possibly infinite processes. However, we assume such processes to be *regular*, that is, with finitely many distinct subprocesses. In this way, we only obtain processes which are solutions of finite sets of equations, see [24]. So, when writing processes, we shall use (mutually) recursive equations.

In the following, trailing 0's will be omitted. Processes of the shape $\bigoplus_{i \in I} p!l_i; P_i$ and $\sum_{i \in I} p?l_i; P_i$ are called *output* and *input processes*, respectively. We will write $p!l; P$ or $p?l; P$ for choices with just one branch, and use the infix notation $\oplus$ and $+$ in the examples.

Processes can be seen as trees where internal nodes are decorated by $p!$ or $p?$, leaves by 0, and edges by labels $l$.

In a full-fledged calculus, labels would carry values, namely they would be of the form $l(v)$. For simplicity, we consider only simple labels $l$ here. This will allow us to project global types directly to processes, without having to explicitly introduce local types, see Section 3.

In our calculus, asynchronous communication is modelled in the usual way, by storing sent messages in a queue. We define messages to be triples $(p, l, q)$, where $p$ is the sender and $q$ is the receiver, and message queues (or simply queues) to be possibly empty sequences of messages:

$$ \mathcal{M} ::= \emptyset | \langle p, l, q \rangle \cdot \mathcal{M} $$

The order of messages in the queue is the order in which they will be read. Since the only reading order that matters is that between messages with the same sender and the same receiver, we consider message queues modulo the structural equivalence given by:

$$ \mathcal{M} \cdot \langle p, l, q \rangle \cdot \langle r, l', s \rangle \cdot \mathcal{M}' \equiv \mathcal{M} \cdot \langle r, l', s \rangle \cdot \langle p, l, q \rangle \cdot \mathcal{M}' \quad \text{if } p \neq r \text{ or } q \neq s $$

Note in particular that $\langle p, l, q \rangle \cdot \langle q, l', p \rangle \equiv \langle q, l', p \rangle \cdot \langle p, l, q \rangle$. These two equivalent queues represent a situation in which both participants $p$ and $q$ have sent a label to the other one, and neither of them has read the label sent by the other one. Since the two sends occur in parallel, the order of the corresponding messages in the queue should be irrelevant. This point will be further illustrated by Examples 2.4 and 2.5.

In the following we will always consider queues modulo structural equivalence.

Networks are comprised of located processes of the form $p\llbracket P \rrbracket$ composed in parallel, each with a different participant $p$, and by a message queue.

**Definition 2.2. (Networks)**

Networks are defined by:

$$ N \parallel \mathcal{M} $$

where $N = p_1\llbracket P_1 \rrbracket \parallel \cdots \parallel p_n\llbracket P_n \rrbracket$ with $p_h \neq p_k$ for any $h \neq k$, and $\mathcal{M}$ is a message queue.

We assume the standard laws for parallel composition, stating that $\parallel$ is associative, commutative, and has neutral element $p\llbracket 0 \rrbracket$ for any fresh $p$. These laws, together with the structural equivalence on queues, give rise to the structural congruence on networks, also denoted by the symbol $\equiv$.

If $P \neq 0$ we write $p\llbracket P \rrbracket \in N$ as short for $N \equiv p\llbracket P \rrbracket \parallel N'$ for some $N'$. This abbreviation is justified by the associativity and commutativity of parallel composition.

To define the *operational semantics* of networks, we use an LTS whose transitions are decorated by outputs or inputs. We define the set of *input/output communications* (communications for short), ranged over by $\beta, \beta'$, to be $\{pq!l, pq?l | p, q \in \text{Part}, l \in \text{Lab}\}$, where $pq!l$ represents the send of a label $l$ from participant $p$ to participant $q$, and $pq?l$ the read by participant $q$ of the label
$$ p[\bigoplus_{i \in I} q!l_i; P_i] \parallel N \parallel \mathcal{M} \xrightarrow{pq!l_k} p[P_k] \parallel N \parallel \mathcal{M} \cdot \langle p, l_k, q \rangle \quad \text{where } k \in I \quad [\text{SEND}] $$

$$ q[\Sigma_{j \in J} p?l_j; Q_j] \parallel N \parallel \langle p, l_k, q \rangle \cdot \mathcal{M} \xrightarrow{pq?l_k} q[Q_k] \parallel N \parallel \mathcal{M} \quad \text{where } k \in J \quad [\text{RCV}] $$

<caption>Figure 1. LTS for networks.</caption>

l sent by participant p. To memorise this notation, it is helpful to view pq as the channel from p to q and the exclamation/question mark as the mode (write/read) in which the channel is used. The LTS semantics of networks, defined modulo ≡, is specified by the two Rules [SEND] and [RCV] given in Figure 1. Rule [SEND] allows a participant p with an internal choice (a sender) to send to a participant q one of its possible labels $l_k$ by adding it to the queue. Symmetrically, Rule [RCV] allows a participant q with an external choice (a receiver) to read the first label $l_k$ sent to it by participant p, provided this label is among the $l_j$'s specified in the choice. Using structural equivalence, the first message from p to q, if any, can always be moved to the top of the queue.

A key role will be played by (possibly empty) sequences of communications, defined as traces.

**Definition 2.3. (Traces)**

(Finite) traces are defined by:

$$ \tau ::= \epsilon \mid \beta \cdot \tau $$

We use $|\tau|$ to denote the length of the trace $\tau$.

When $\tau = \beta_1 \cdots \beta_n (n \ge 1)$ we write $N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}'$ as short for

$$ N \parallel \mathcal{M} \xrightarrow{\beta_1} N_1 \parallel \mathcal{M}_1 \cdots \xrightarrow{\beta_n} N_n \parallel \mathcal{M}_n = N' \parallel \mathcal{M}' $$

Let us now consider the semantics of the network $N \parallel \emptyset$ discussed in the introduction.

**Example 2.4.** Let $N = p[q!l; q?l'] \parallel q[p!l'; p?l]$. Then $N \parallel \emptyset$ can move by first performing the two sends, in any order, and then the two reads, in any order. A possible execution of $N \parallel \emptyset$, where the use of ≡ on the queue is explicitly shown, is:

$$ \begin{align*} N \parallel \emptyset &\xrightarrow{pq!l} p[q?l'] \parallel q[p!l'; p?l] \parallel \langle p, l, q \rangle \\ \xrightarrow{qp!l'} & p[q?l'] \parallel q[p?l] \parallel \langle p, l, q \rangle \cdot \langle q, l', p \rangle \\ &\equiv p[q?l'] \parallel q[p?l] \parallel \langle q, l', p \rangle \cdot \langle p, l, q \rangle \\ \xrightarrow{qp?l'} & p[\mathbf{0}] \parallel q[p?l] \parallel \langle p, l, q \rangle \\ \xrightarrow{pq?l} & p[\mathbf{0}] \parallel q[\mathbf{0}] \parallel \emptyset \end{align*} $$

The following example illustrates a simple case in which both participants need to do outputs before inputs.

**Example 2.5.** Alice and Bob play heads and tails as follows: they each write their prediction on a piece of paper and then they exchange their papers. If the predictions are the same they start again, otherwise they flip the coin and the winner is the one whose prediction was correct. The initial interaction in this scenario may be represented by the network $p[P] \parallel q[Q] \parallel \emptyset$ where p, q incarnate Alice and Bob, h, t stand for head and tail, and P, Q are defined as follows:

$$ P = q!h; (q?h; P + q?t) \oplus q!t; (q?h + q?t; P) $$

$$ Q = p!h; (p?h; Q + p?t) \oplus p!t; (p?h + p?t; Q) $$
We now introduce the notion of player, which will be extensively used in the rest of the paper. The player of a communication $\beta$ is the participant who is active in $\beta$.

**Definition 2.6. (Players of communications and traces)**

We denote by $\text{play}(\beta)$ the set of players of communication $\beta$ defined by

$$ \text{play}(pq!\ell) = \{p\} \quad \text{play}(pq?\ell) = \{q\} $$

The function play is extended to traces in the obvious way:

$$ \text{play}(\epsilon) = \emptyset \quad \text{play}(\beta \cdot \tau) = \text{play}(\beta) \cup \text{play}(\tau) $$

Notice that the notion of player is characteristic of asynchronous communications, where only one of the involved participants is active, namely the sender for an output communication and the receiver for an input communication. Instead, in synchronous communications both participants (also called roles in the literature) are active.

## 3. Asynchronous Types

In this section we introduce our new types for asynchronous communication. The underlying idea is quite simple: to split the communication constructor of standard global types into an output constructor and an input constructor. This will allow us to type networks in which all participants make all their outputs before their inputs, like the networks of Examples 2.4 and 2.5, whose asynchronous types will be presented in Example 3.9.

**Definition 3.1. (Global and asynchronous types)**

1. Global types are defined by:

$$ G ::=^{\text{coind}} \bigoplus_{i \in I} pq!\ell_i; G_i \mid pq?\ell; G \mid \text{End} $$

where $I$ is non-empty and $p \neq q$ and $\ell_h \neq \ell_k$ for all $h, k \in I, h \neq k$.

2. Asynchronous types are pairs made of a global type and a queue, written $G \parallel M$.

As for processes, $::=^{\text{coind}}$ indicates that global types are coinductively defined regular terms. The global type $\bigoplus_{i \in I} pq!\ell_i; G_i$ specifies that $p$ sends a label $\ell_k$ with $k \in I$ to $q$ and then the interaction described by the global type $G_k$ takes place. Dually, the global type $pq?\ell; G$ specifies that $q$ receives label $\ell$ from $p$ and then the interaction described by the global type $G$ takes place. We will omit trailing End's.

Global types can be naturally seen as trees where internal nodes are decorated by $pq!$ or $pq?$, leaves by End, and edges by labels $\ell$. The sequences of decorations of nodes and edges on the path from the root to an edge of the tree are traces, in the sense of Definition 2.3. We denote by $\text{Tr}^+(G)$ the set of such traces in the tree of $G$. By definition, $\text{Tr}^+(\text{End}) = \emptyset$ and each trace in $\text{Tr}^+(G)$ is non-empty.

In Definition 2.6 we introduced the notion of player for communications and traces. It is useful to extend this notion to global types, by defining the set of players of a global type $G$, $\text{play}(G)$, to be the union of the sets of players of all its traces, namely

$$ \text{play}(G) = \bigcup_{\tau \in \text{Tr}^+(G)} \text{play}(\tau) $$

The regularity assumption ensures that the set of players of a global type is finite.

Asynchronous types will be used to type networks, see Figure 4. A standard guarantee they should ensure is that each participant whose behaviour is not terminated can do some action. Moreover,
since communications are split into outputs and inputs in global types, we must make sure that each input is balanced by an output in the type or by a message in the queue, and vice versa. These requirements will be formulated as well-formedness conditions on asynchronous types.

The remainder of this section is divided in two subsections: the first focusses on well-formedness of asynchronous types, and the second presents the type system and shows that it enjoys the properties of subject reduction and session fidelity and that moreover it ensures progress.

## 3.1. Well-formed Asynchronous Types

We start by defining the projection of global types onto participants (Figure 2). We proceed by defining the boundedness predicate for global types (Definition 3.3) and the balancing predicate for asynchronous types (Figure 3).

$$ G \upharpoonright r = 0 \quad \text{if } r \notin \text{play}(G) \\ \left( \bigoplus_{i \in I} pq!l_i; G_i \upharpoonright p \right) \upharpoonright r = \left\{ \begin{array}{ll} \bigoplus_{i \in I} q!l_i; G_i \upharpoonright p & \text{if } r = p, \\ G_1 \upharpoonright q & \text{if } r = q \text{ and } I = \{1\} \\ \bar{\pi}; \sum_{i \in I} p?l_i; P_i & \text{if } r = q \text{ and } |I| > 1 \text{ and } G_i \upharpoonright q = \bar{\pi}; p?l_i; P_i, \\ G_1 \upharpoonright r & \text{if } r \notin \{p, q\} \text{ and } r \in \text{play}(G_1) \\ & \text{and } G_i \upharpoonright r = G_1 \upharpoonright r \text{ for all } i \in I \end{array} \right. $$

$$ (pq?l; G) \upharpoonright r = \begin{cases} p?l; G \upharpoonright r & \text{if } r = q \\ G \upharpoonright r & \text{if } r \neq q \text{ and } r \in \text{play}(G) \end{cases} $$

<caption>Figure 2. Projection of global types onto participants.</caption>

As mentioned earlier, the projection of global types on participants yields processes. Its coinductive definition is given in Figure 2, where we use $\bar{\pi}$ to denote any sequence, possibly empty, of input/output actions separated by “;”. We write $|I|$ for the cardinality of $I$.

The projection of a global type on a participant which is not a player of the type is the inactive process 0. In particular, the projection of End is 0 on all participants.

The projection of an output choice type on the sender yields an output process sending one of its labels to the receiver and then acting according to the projection of the corresponding branch.

The projection of an output choice type on the receiver $q$ has two clauses: one for the case where the choice has a single branch, and one for the case where the choice has more than one branch.

In the first case, the projection is simply the projection of the continuation of the single branch on $q$. In the second case, the projection is defined if the projection of the continuation of each branch on $q$ starts with the same sequence of actions $\bar{\pi}$, followed by an input of the label sent by $p$ on that branch and then by a possibly different process in each branch. In fact, participant $q$ must receive the label chosen by participant $p$ before behaving differently in different branches.

The projection on $q$ is then the initial sequence of actions $\bar{\pi}$ followed by an external choice on the different sent labels. The sequence $\bar{\pi}$ is allowed to contain another input of a (possibly equal) label from $p$, for example:

$$ (pq!l_1; pq!l; pq?l; pq?l_1; pq?l \boxplus pq!l_2; pq!l'; pq?l; pq?l_2; pq?l') \upharpoonright q = \\ p?l; (p?l_1; p?l + p?l_2; p?l') $$
In Example 3.12 we will show why we need to distinguish these two cases.

The projection of an output choice type on the other participants is defined only if it produces the same process for all branches of the choice.

The projection of an input type on the receiver is an input action followed by the projection of the rest of the type. For the other participants, the projection is simply the projection of the rest of the type.

Note that our projection adopts the strict requirement of [3] for participants not involved in a choice, namely it requires their behaviours to be the same in all branches of a choice. A more permissive projection (in line with [25]) for the same global types is given in [26]. Our choice here is motivated by simplicity, in order to focus on the event structure semantics.

To guarantee the property of progress, our types for networks must ensure that each network player occurs in every computation, whether finite or infinite. To this end, each type player should occur in every path of the tree of the type. Now, projectability already ensures that each player of a choice type occurs in all its branches. This implies that if one branch of the choice gives rise to an infinite path, either the player occurs at some finite depth in this path, or this path crosses infinitely many branching points in which the player occurs in all branches. In the latter case, since the depth of the player increases when crossing each branching point, there is no bound on the depth of the player over all paths of the type. Hence, to ensure that all type players occur in all paths, it is enough to require the existence of such bounds. This motivates the following definitions of depth and boundedness.

We first define the depth of a participant p in a global type G, depth(G, p), which uses the length function $|\cdot|$ of Definition 2.3 as well as the functions play($\beta$) and play($\tau$) of Definition 2.6 and the function play(G) defined earlier in this section. Intuitively, depth(G, p) is the limit, computed over all paths of the tree of G, of the depth of the first occurrence of the player p in the path.

**Definition 3.2. (Depth)**

Let the two functions depth($\tau$, p) and depth(G, p) be defined by:

$$ 
\begin{array}{ll}
\text{depth}(\tau, p) = \begin{cases} n & \text{if } \tau = \tau_1 \cdot \beta \cdot \tau_2 \text{ and } |\tau_1| = n-1 \text{ and } p \notin \text{play}(\tau_1) \text{ and } p \in \text{play}(\beta) \\ 0 & \text{otherwise} \end{cases} & \\
\text{depth}(G, p) = \sup\{\text{depth}(\tau, p) \mid \tau \in \text{Tr}^+(G)\} &
\end{array}
$$

**Definition 3.3. (Boundedness)**

We say that a global type G is *bounded* if depth(G', p) is finite for all subtrees G' of G and for all players p.

To show that G is bounded it is enough to check depth(G', p) for all subtrees G' of G and p ∈ play(G'), since for any other p we have depth(G', p) = 0.

Note that the depth of a participant which is a player of G does not necessarily decrease in the subtrees of G. As a matter of fact, this depth can be finite in G but infinite in one of its subtrees, as shown by the following example.

**Example 3.4.** Consider $G = rq!l; rq?l; G'$ where

$$ G' = pq!l_1; pq?l_1; pr!l_3; pr?l_3 \boxplus pq!l_2; pq?l_2; G' $$

Then we have:

$$ \text{depth}(G, r) = 1 \quad \text{depth}(G, p) = 3 \quad \text{depth}(G, q) = 2 $$

whereas
$$ \frac{\begin{array}{l} \vdash^b G_i \parallel \mathcal{M} \cdot \langle \mathbf{p}, \ell_i, \mathbf{q} \rangle \text{ for all } i \in I \quad \text{if } \coprod_{i \in I} \mathbf{pq}!\ell_i; G_i \text{ is cyclic then } \mathcal{M} = \emptyset \\ \hline \quad \vdash^b \coprod_{i \in I} \mathbf{pq}!\ell_i; G_i \parallel \mathcal{M} \end{array}}{\begin{array}{l} \vdash^b G \parallel \mathcal{M} \\ \hline \quad \vdash^b \mathbf{pq}?!\ell; G \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M} \end{array}} \quad \text{[OUT]} \quad \begin{array}{l} \vdash^b \text{End} \parallel \emptyset \quad \text{[End]} \end{array} $$

<caption>Figure 3. Balancing predicate.</caption>

$$ \text{depth}(G', r) = \infty \quad \text{depth}(G', p) = 1 \quad \text{depth}(G', q) = 2 $$
since $\underbrace{\mathbf{pq}!\ell_2 \cdot \mathbf{pq}?!\ell_2 \cdot \dots \cdot \mathbf{pq}!\ell_2 \cdot \mathbf{pq}?!\ell_2}_{n} \cdot \mathbf{pq}!\ell_1 \cdot \mathbf{pq}?!\ell_1 \cdot \text{pr}!\ell_3 \cdot \text{pr}?!\ell_3 \in \text{Tr}^+(G') \text{ for all } n \ge 0 \text{ and} \\ \sup\{4 + 2n \mid n \ge 0\} = \infty.$$

However, the finite depth of a participant which is a player of G but not the player of its root communication decreases in the immediate subtrees of G, as stated in the following lemma.

**Lemma 3.5.** 1. If $G = \coprod_{i \in I} \mathbf{pq}!\ell_i; G_i$ and $r \in \text{play}(G)$ and $r \neq p$, then $\text{depth}(G, r) > \text{depth}(G_i, r)$ for all $i \in I$.

2. If $G = \mathbf{pq}?!\ell; G'$ and $r \in \text{play}(G)$ and $r \neq q$, then $\text{depth}(G, r) > \text{depth}(G', r)$.

The definition of projection given in Figure 2 is sound for bounded global types.

**Lemma 3.6.** If G is bounded, then $G \upharpoonright r$ is a partial function for all r.

To ensure the correspondence between outputs and inputs, in Figure 3 we define the balancing predicate $\vdash^b$ on asynchronous types, and we say that $G \parallel \mathcal{M}$ is balanced if $\vdash^b G \parallel \mathcal{M}$. The intuition is that every initial input should come with a corresponding message in the queue (Rule [IN]), ensuring that the input can take place. Then, each message in the queue can be exchanged for a corresponding output that will prefix the type (Rule [OUT]): this output will then precede the previously inserted input and thus ensure again that the input can take place. In short, balancing holds if the messages in the queue and the outputs in the global type are matched by inputs in the global type and vice versa. We say that a global type is cyclic if its tree contains itself as proper subtree. So the condition “if the global type is cyclic then the queue is empty” in Rule [OUT] ensures that there is no message left in the queue at the beginning of a new cycle, namely that all messages put in the queue by cyclic global types have matching inputs in the same cycle. For instance we can apply Rule [OUT] to the asynchronous type $G' \parallel \emptyset$ of Example 3.7(3), but not to the asynchronous type $G \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle$ of Example 3.7(2). Similarly, in Example 3.7(4), Rule [OUT] can be used for $G_2 \parallel \emptyset$ but not for $G_2 \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle$.

The double line indicates that the rules are interpreted coinductively [27] (Chapter 21). The condition in Rule [OUT] guarantees that we get only regular proof derivations, therefore the judgement $\vdash^b G \parallel \emptyset$ is decidable. If we derive $\vdash^b G \parallel \emptyset$ we can ensure that in $G \parallel \emptyset$ all outputs are matched
by corresponding inputs and vice versa, see the Progress Theorem (Theorem 3.20). The progress property holds also for standard global types [28, 29].

The next example illustrates the use of the balancing predicate on several asynchronous types.

**Example 3.7.** 1. The asynchronous type $qp?\ell; pq!\ell'; pq?\ell' \parallel \langle q, \ell, p \rangle$ is balanced, as shown by the following derivation:

$$ \frac{\vdash^b \mathrm{End} \parallel \emptyset}{\vdash^b pq?\ell' \parallel \langle p, \ell', q \rangle} \qquad \frac{\vdash^b pq!\ell'; pq?\ell' \parallel \emptyset}{\vdash^b qp?\ell; pq!\ell'; pq?\ell' \parallel \langle q, \ell, p \rangle} $$

2. Let $G = pq!\ell; pq!\ell; pq?\ell; G$. Then $G \parallel \emptyset$ is not balanced. Indeed, we cannot complete the proof tree for $\vdash^b G \parallel \emptyset$ because, since $G$ is cyclic, we cannot apply Rule [OUT] to infer the premise $\vdash^b G \parallel \langle p, \ell, q \rangle$ in the following deduction:

$$ \frac{\vdash^b G \parallel \langle p, \ell, q \rangle}{\vdash^b pq?\ell; G \parallel \langle p, \ell, q \rangle \cdot \langle p, \ell, q \rangle} \qquad \frac{\vdash^b pq!\ell; pq?\ell; G \parallel \langle p, \ell, q \rangle}{\vdash^b G \parallel \emptyset} $$

3. Let $G' = (pq!\ell_1; pq?\ell_1; G' \boxtimes pq!\ell_2; pq?\ell_2)$. Then $G' \parallel \emptyset$ is balanced, as we can see from the infinite (but regular) proof tree that follows:

$$ \frac{\vdots}{\frac{\vdash^b G' \parallel \emptyset}{\vdash^b pq?\ell_1; G' \parallel \langle p, \ell_1, q \rangle}} \qquad \frac{\vdash^b \mathrm{End} \parallel \emptyset}{\vdash^b pq?\ell_2 \parallel \langle p, \ell_2, q \rangle} $$

4. Let $G_1 = pq!\ell; pq!\ell; pq?\ell; G_2$ and $G_2 = pr!\ell; pr?\ell; G_2$. Then $G_1 \parallel \emptyset$ is not balanced. Indeed, we cannot complete the proof tree for $\vdash^b G_1 \parallel \emptyset$, since $G_2$ is cyclic, so we cannot apply Rule [OUT] to infer the premise $\vdash^b G_2 \parallel \langle p, \ell, q \rangle$ in the following deduction:

$$ \frac{\vdash^b G_2 \parallel \langle p, \ell, q \rangle}{\vdash^b pq?\ell; G_2 \parallel \langle p, \ell, q \rangle \cdot \langle p, \ell, q \rangle} \qquad \frac{\vdash^b pq!\ell; pq?\ell; G_2 \parallel \langle p, \ell, q \rangle}{\vdash^b G_1 \parallel \langle p, \ell, q \rangle} $$

Instead, $G_2 \parallel \emptyset$ is balanced:

$$ \frac{\vdots}{\frac{\vdash^b G_2 \parallel \emptyset}{\vdash^b pr?\ell; G_2 \parallel \langle p, \ell, r \rangle}} \qquad \frac{\vdash^b G_2 \parallel \emptyset}{\vdash^b G_2 \parallel \emptyset} $$

It is interesting to notice that balancing of asynchronous types does not imply projectability of their global types. For example, the type $G \parallel \emptyset$ where
$$G = pq!l_1; pq?l_1; rq!l_1; rq?l_1 \boxplus pq!l_2; pq?l_2; rq!l_2; rq?l_2$$

is balanced, but G is not projectable on participant r for any of the projection definitions in the literature. Notably, type G prescribes that r should behave differently according to the message exchanged between p and q, an unreasonable requirement.

Projectability, boundedness and balancing are the three properties that single out the asynchronous types we want to use in our type system.

**Definition 3.8. (Well-formed asynchronous types)**

We say that the asynchronous type $G \parallel \mathcal{M}$ is *well formed* if it is balanced, $G \upharpoonright p$ is defined for all p and G is bounded.

Clearly, it is sufficient to check that $G \upharpoonright p$ is defined for all $p \in \text{play}(G)$, since $G \upharpoonright p = \mathbf{0}$ otherwise.

## 3.2. Type System

In this subsection we present our type system. For establishing its expected properties, we then introduce an LTS for asynchronous types (Figure 5) and show that well-formedness of asynchronous types is preserved by transitions (Lemma 3.15).

$$ \frac{P_i \le Q_i \quad \text{for all } i \in I}{\bigoplus_{i \in I} p!l_i; P_i \le \bigoplus_{i \in I} p!l_i; Q_i} \quad [\le \text{-OUT}] \quad \frac{P_i \le Q_i \quad \text{for all } i \in I}{\sum_{i \in I \cup J} p?l_i; P_i \le \sum_{i \in I} p?l_i; Q_i} \quad [\le \text{-IN}] \\ 0 \le 0 \quad [\le \text{-OUT}] $$

$$ \frac{P_i \le G \upharpoonright p_i \quad \text{for all } i \in I}{\vdash \prod_{i \in I} p_i [P_i] \parallel \mathcal{M} : G \parallel \mathcal{M}} \quad [\text{NET}] $$

<caption>Figure 4. Preorder on processes and network typing rule.</caption>

The typing rules are given in Figure 4. In the unique typing rule for networks, Rule [NET], we assume the asynchronous type to be well formed.

We first define a preorder on processes, $P \le Q$, meaning that *process P can be used where we expect process Q*. More precisely, $P \le Q$ if either P is equal to Q, or we are in one of two situations: either both P and Q are output processes, sending the same labels to the same participant, and after the send P continues with a process that can be used when we expect the corresponding one in Q; or they are both input processes receiving labels from the same participant, and P may receive more labels than Q (and thus have more behaviours) but whenever it receives the same label as Q it continues with a process that can be used when we expect the corresponding one in Q. The rules are interpreted coinductively, since the processes may be infinite. However, derivability is decidable, since processes have finitely many distinct subprocesses.

Clearly, our preorder on processes plays the same role as the subtyping relation on local types in other works. In the original standard subtyping of [30] a better type has more outputs and less inputs, while in the subtyping of [31] a better type has less outputs and more inputs. The subtyping of [30] allows channel substitution, while the subtyping of [31] allows process substitution, as observed in [32]. This justifies our structural preorder on processes, which is akin to a restriction
of the subtyping of [31]. The advantage of this restriction is a strong version of Session Fidelity, see Theorem 3.19. On the other hand, as shown in [33], such a restriction does not change the class of networks that can be typed by standard global types (but may change the types assigned to them). The proof in [33] easily adapts to our asynchronous types.

A network $N \parallel \mathcal{M}$ is typed by the asynchronous type $G \parallel \mathcal{M}$ if for every participant $p$ such that $p\llbracket P \rrbracket \in N$ the process $P$ behaves as specified by the projection of $G$ on $p$. In Rule [NET], the condition play($G$) $\subseteq \{p_i \mid i \in I\}$ ensures that all players of $G$ appear in the network. Moreover it permits additional participants that do not appear in $G$, allowing the typing of sessions containing $p\llbracket 0 \rrbracket$ for a fresh $p$ – a property required to guarantee invariance of types under structural congruence of networks.

**Example 3.9.** The network of Example 2.4 can be typed by $G \parallel \emptyset$ for four possible choices of $G$:

$$pq!\ell; pq!\ell'; pq?\ell; pq?\ell' \qquad pq!\ell; pq!\ell'; pq?\ell'; pq?\ell$$

$$qp!\ell'; pq!\ell; pq?\ell; qp?\ell' \qquad qp!\ell'; pq!\ell; qp?\ell'; pq?\ell$$

since each participant only needs to do the output before the input. Notice that this network cannot be typed with the standard global types of [4].

The network of Example 2.5 can be typed by $G \parallel \emptyset$ where

$$G = pq!h; (qp!h; pq?h; qp?h; G \boxplus qp!t; pq?h; qp?t)\boxplus \\ pq!t; (qp!h; pq?t; qp?h \boxplus qp!t; pq?t; qp?t; G) \parallel \emptyset$$

Again, this network cannot be typed with the standard global types of [4]. On the other hand, both these networks can be typed by adding the semantic subtyping as defined in [21] to the type system with the standard global types. However, the resulting system is less precise than ours, although it can type more networks. As an example, consider the standard global type

$$G' = p \to q : h; (q \to p : h; G' \boxplus q \to p : t) \boxplus p \to q : t; (q \to p : h \boxplus q \to p : t; G')$$

and its projections $G' \upharpoonright p = P'$ and $G' \upharpoonright q = Q'$ defined by

$$P' = q!h; (q?h; P' + q?t) \oplus q!t; (q?h + q?t; P')$$

$$Q' = p?h; (p!h; Q' \oplus p!t) + p?t; (p!h \oplus p!t; Q')$$

Then $G'$ is a type for the network $p\llbracket P \rrbracket \parallel q\llbracket Q \rrbracket \parallel \emptyset$ of Example 2.5, since $Q$ can be obtained from $Q'$ using asynchronous subtyping, by anticipating the outputs towards $p$. Clearly, the global type $G'$ also types the network $p\llbracket P' \rrbracket \parallel q\llbracket Q' \rrbracket \parallel \emptyset$. However, this network does not follow the rules of the game given in Example 2.5.

Figure 5 gives the LTS for asynchronous types. It shows that a communication can be performed also under a choice or an input guard, provided it is independent from it. Actually, we are interested only in the transitions of balanced asynchronous types, see Figure 3. This justifies the shape of the message queues in Rules [ICOMM-OUT] and [ICOMM-IN]. The conditions $p \notin \text{play}(\beta)$ and $q \notin \text{play}(\beta)$ in these rules ensure that $\beta$ does not depend on the enclosing communications.

We say that $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$ is a *top transition* if it is derived using either Rule [EXT-OUT] or Rule [EXT-IN]. Top transitions preserve well-formedness of asynchronous types:

**Lemma 3.10.** If $G \parallel \mathcal{M} \xrightarrow{\beta} G'$ is a top transition and $G \parallel \mathcal{M}$ is well formed, then $G' \parallel \mathcal{M}'$ is well formed too.

The following lemma detects the immediate transitions of an asynchronous type from the projections of its global type.
$$ \boxplus_{i \in I} \mathbf{pq}! \ell_i; G_i \parallel \mathcal{M} \xrightarrow{\mathbf{pq}! \ell_k} G_k \parallel \mathcal{M} \cdot \langle \mathbf{p}, \ell_k, \mathbf{q} \rangle \quad \text{where } k \in I \quad [\text{EXT-OUT}] $$

$$ \mathbf{pq}?!\ell; G \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M} \xrightarrow{\mathbf{pq}?!\ell} G \parallel \mathcal{M} \quad [\text{EXT-IN}] $$

$$ G_i \parallel \mathcal{M} \cdot \langle \mathbf{p}, \ell_i, \mathbf{q} \rangle \xrightarrow{\beta} G'_i \parallel \mathcal{M}' \cdot \langle \mathbf{p}, \ell_i, \mathbf{q} \rangle \quad \text{for all } i \in I \quad \mathbf{p} \notin \text{play}(\beta) \quad [\text{ICOMM-OUT}] $$

$$ \boxplus_{i \in I} \mathbf{pq}! \ell_i; G_i \parallel \mathcal{M} \xrightarrow{\beta} \boxplus_{i \in I} \mathbf{pq}! \ell_i; G'_i \parallel \mathcal{M}' $$

$$ \frac{G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}' \qquad \mathbf{q} \notin \text{play}(\beta)}{\mathbf{pq}?!\ell; G \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M} \xrightarrow{\beta} \mathbf{pq}?!\ell; G' \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M}'} \quad [\text{ICOMM-IN}] $$

<caption>Figure 5. LTS for asynchronous types.</caption>

**Lemma 3.11.** Let $G \parallel \mathcal{M}$ be well formed.

1. If $G \vdash \mathbf{p} = \bigoplus_{i \in I} \mathbf{q}! \ell_i; P_i$, then $G \parallel \mathcal{M} \xrightarrow{\mathbf{pq}! \ell_i} G_i \parallel \mathcal{M} \cdot \langle \mathbf{p}, \ell_i, \mathbf{q} \rangle$ and $G_i \vdash \mathbf{p} = P_i$ for all $i \in I$.

2. If $G \vdash \mathbf{q} = \sum_{i \in I} \mathbf{p}?! \ell_i; P_i$ and $\mathcal{M} \equiv \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M}'$ for some $\ell$, then $I = \{k\}$ and $\ell = \ell_k$ and $G \parallel \mathcal{M} \xrightarrow{\mathbf{pq}?! \ell_k} G' \parallel \mathcal{M}'$ and $G' \vdash \mathbf{q} = P_k$.

The next lemma shows how to retrieve the projections of a global type from the immediate transitions of the asynchronous type obtained by combining the global type with a compliant queue. It also shows that transitions of asynchronous types preserve projectability of their global types. For this purpose, one needs the two clauses in the projection of an output choice on the receiver, see Figure 2, as illustrated by the following example.

**Example 3.12.** Let $G = \mathbf{pq}?!\ell; \mathbf{pq}?!\ell; G'$, where $G' = \mathbf{qr}?!\ell_1; \mathbf{qr}?!\ell_1; \mathbf{pq}?!\ell \boxplus \mathbf{qr}?!\ell_2; \mathbf{qr}?!\ell_2; \mathbf{pq}?!\ell$. The asynchronous type $G \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle$ is well formed. Assume we modify the definition of projection of an output choice on the receiver by removing its first clause and the restriction of the second to $|I| > 1$. Then $G \vdash \mathbf{q}$ is defined since $(\mathbf{pq}?!\ell; G') \vdash \mathbf{q} = \mathbf{p}?!\ell; (\mathbf{r}?!\ell_1; \mathbf{p}?!\ell \oplus \mathbf{r}?!\ell_2; \mathbf{p}?!\ell)$ has the required shape. Applying Rule [ICOMM-OUT] we get $G \parallel \langle \mathbf{p}, \ell, \mathbf{q} \rangle \xrightarrow{\mathbf{pq}?!\ell} \mathbf{pq}?!\ell; G' \parallel \emptyset$. The projection $(\mathbf{pq}?!\ell; G') \vdash \mathbf{q}$ would not be defined since $G' \vdash \mathbf{q} = \mathbf{r}?!\ell_1; \mathbf{p}?!\ell \oplus \mathbf{r}?!\ell_2; \mathbf{p}?!\ell$ does not have the required shape.

**Lemma 3.13.** Let $G \parallel \mathcal{M}$ be well formed.

1. If $G \parallel \mathcal{M} \xrightarrow{\mathbf{pq}?!\ell} G' \parallel \mathcal{M}'$, then $\mathcal{M}' \equiv \mathcal{M} \cdot \langle \mathbf{p}, \ell, \mathbf{q} \rangle$ and $G \vdash \mathbf{p} = \bigoplus_{i \in I} \mathbf{q}! \ell_i; P_i$ and $\ell = \ell_k$ and $G' \vdash \mathbf{p} = P_k$ for some $k \in I$ and $G \vdash \mathbf{r} \le G' \vdash \mathbf{r}$ for all $r \neq \mathbf{p}$.

2. If $G \parallel \mathcal{M} \xrightarrow{\mathbf{pq}?!\ell} G' \parallel \mathcal{M}'$, then $\mathcal{M} \equiv \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M}'$ and $G \vdash \mathbf{q} = \mathbf{pq}?!\ell; G' \vdash \mathbf{q}$ and $G \vdash \mathbf{r} \le G' \vdash \mathbf{r}$ for all $r \neq \mathbf{q}$.
The LTS also preserves balancing of asynchronous types.

**Lemma 3.14.** If $\vdash^b G \parallel \mathcal{M}$ and $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$, then $\vdash^b G' \parallel \mathcal{M}'$.

We are now able to show that transitions preserve well-formedness of asynchronous types.

**Lemma 3.15.** If $G \parallel \mathcal{M}$ is a well formed asynchronous type and $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$, then $G' \parallel \mathcal{M}'$ is a well formed asynchronous type too.

**Proof:** Let $\beta = \text{pq}\!\ell$. By Lemma 3.13(1) we have that $G' \upharpoonright r$ is defined for all $r \in \text{play}(G)$. Similarly for $\beta = \text{pq}\?\ell$, using Lemma 3.13(2). The proof that $\text{depth}(G'', r)$ is finite for all $r$ and $G''$ subtree of $G'$ is easy by induction on the transition rules of Figure 5. Finally, from Lemma 3.14 we have that $G' \parallel \mathcal{M}'$ is balanced.

By virtue of this lemma, we will henceforth only consider well-formed asynchronous types.

We end this section with the expected results of Subject Reduction, Session Fidelity [3, 4] and Progress [28, 29], which rely as usual on Inversion and Canonical Form lemmas.

**Lemma 3.16. (Inversion)**

If $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$, then $P \leq G \upharpoonright p$ for all $p\llbracket P \rrbracket \in \mathbb{N}$.

**Lemma 3.17. (Canonical Form)**

If $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$ and $p \in \text{play}(G)$, then $p\llbracket P \rrbracket \in \mathbb{N}$ and $P \leq G \upharpoonright p$.

**Theorem 3.18. (Subject Reduction)**

If $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$ and $N \parallel \mathcal{M} \xrightarrow{\beta} N' \parallel \mathcal{M}'$, then $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$ and $\vdash N' \parallel \mathcal{M}' : G' \parallel \mathcal{M}'$.

**Proof:** Let $\beta = \text{pq}\!\ell$. By Rule [SEND] of Figure 1, $p\llbracket \bigoplus_{i \in I} q!\ell_i; P_i \rrbracket \in \mathbb{N}$ and $p\llbracket P_k \rrbracket \in \mathbb{N}'$ and $\mathcal{M}' = \mathcal{M} \cdot \langle p, \ell_k, q \rangle$ and $\ell = \ell_k$ for some $k \in I$. Moreover $r\llbracket R \rrbracket \in \mathbb{N}$ iff $r\llbracket R \rrbracket \in \mathbb{N}'$ for all $r \neq p$. From Lemma 3.16 we get

1. $\bigoplus_{i \in I} q!\ell_i; P_i \leq G \upharpoonright p$, which implies $G \upharpoonright p = \bigoplus_{i \in I} q!\ell_i; P'_i$ with $P_i \leq P'_i$ for all $i \in I$ from Rule $[\leq \text{-OUT}]$ of Figure 4, and

2. $R \leq G \upharpoonright r$ for all $r \neq p$ such that $r\llbracket R \rrbracket \in \mathbb{N}$.

By Lemma 3.11(1) $G \parallel \mathcal{M} \xrightarrow{\text{pq}\ell_k} G_k \parallel \mathcal{M} \cdot \langle p, \ell_k, q \rangle$ and $G_k \upharpoonright p = P'_k$, which implies $P_k \leq G_k \upharpoonright p$. By Lemma 3.13(1) $G \upharpoonright r \leq G_k \upharpoonright r$ for all $r \neq p$. By transitivity of $\leq$ we have $R \leq G_k \upharpoonright r$ for all $r \neq p$. We can then choose $G' = G_k$.

Let $\beta = \text{pq}\?\ell$. By Rule [RCV] of Figure 1, $q\llbracket \sum_{j \in J} p?\ell_j; Q_j \rrbracket \in \mathbb{N}$ and $q\llbracket Q_k \rrbracket \in \mathbb{N}'$ and $\mathcal{M} = \langle p, \ell_k, q \rangle \cdot \mathcal{M}'$ and $\ell = \ell_k$ for some $k \in J$. Moreover $r\llbracket R \rrbracket \in \mathbb{N}$ iff $r\llbracket R \rrbracket \in \mathbb{N}'$ for all $r \neq q$. From Lemma 3.16 we get

1. $\sum_{j \in J} p?\ell_j; Q_j \leq G \upharpoonright q$, which implies $G \upharpoonright q = \sum_{j \in I} p?\ell_j; Q'_j$ with $I \subseteq J$ and $Q_i \leq Q'_i$ for all $i \in I$ from Rule $[\leq \text{-IN}]$ of Figure 4, and
2. $R \le G \upharpoonright r$ for all $r \neq q$ such that $r[[R]] \in N$.

By Lemma 3.11(2), since $\mathcal{M} = \langle p, \ell_k, q \rangle \cdot \mathcal{M}',$ we get $G \parallel \mathcal{M} \xrightarrow{pq?\ell_k} G_k \parallel \mathcal{M}'$ and $I = \{k\}$ and $G_k \upharpoonright q = Q'_k$, which implies $Q_k \le G_k \upharpoonright p$. By Lemma 3.13(2) $G \upharpoonright r \le G_k \upharpoonright r$ for all $r \neq q$. By transitivity of $\le$ we have $R \le G_k \upharpoonright r$ for all $r \neq q$. We can then choose $G' = G_k$.

**Theorem 3.19. (Session Fidelity)**

If $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$ and $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$, then

$$N \parallel \mathcal{M} \xrightarrow{\beta} N' \parallel \mathcal{M}' \text{ and } \vdash N' \parallel \mathcal{M}' : G' \parallel \mathcal{M}'$$

**Proof:** Let $\beta = pq!\ell$. By Lemma 3.13(1) $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, \ell, q \rangle$, $G \upharpoonright p = \bigoplus_{i \in I} p!\ell_i; P_i$, $\ell = \ell_k$, $G' \upharpoonright p = P_k$ for some $k \in I$ and $G \upharpoonright r \le G' \upharpoonright r$ for all $r \ne p$. From Lemma 3.17 we get $N \equiv p[[P]] \parallel N''$ and

1. $P = \bigoplus_{i \in I} q!\ell_i; P'_i$ with $P'_i \le P_i$ for all $i \in I$, from Rule $[\le \text{-OUT}]$ of Figure 4, and

2. $R \le G \upharpoonright r$ for all $r[[R]] \in N''$.

We can then choose $N' = p[[P'_k]] \parallel N''$.

Let $\beta = pq?\ell$. By Lemma 3.13(2) $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}',$ $G \upharpoonright q = p?\ell; P$, $G' \upharpoonright q = P$ and $G \upharpoonright r \le G' \upharpoonright r$ for all $r \ne q$. From Lemma 3.17 we get $N \equiv q[[Q]] \parallel N''$ and

1. $Q = p?\ell; P' + Q'$ with $P' \le P$, from Rule $[\le \text{-IN}]$ of Figure 4, and

2. $R \le G \upharpoonright r$ for all $r[[R]] \in N''$.

We can then choose $N' = q[[P']]] \parallel N''$.

We are now able to prove that in a typable network, every participant whose process is not terminated may eventually perform an action, and every message that is stored in the queue is eventually read. This property is generally referred to as progress [34].

**Theorem 3.20. (Progress)**

A typable network $N \parallel \mathcal{M}$ satisfies progress, namely:

1. $p[[P]] \in N$ implies $N \parallel \mathcal{M} \xrightarrow{\tau \cdot \beta} N' \parallel \mathcal{M}'$ with $\text{play}(\beta) = \{p\}$;

2. $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}_1$ implies $N \parallel \mathcal{M} \xrightarrow{\tau \cdot pq?\ell} N' \parallel \mathcal{M}'$.

**Proof:** By hypothesis $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$ for some $G$.

(1) If $P$ is an output process, then it can immediately move. Let then $P$ be an input process. From $p[[P]] \in N$ we get $p \in \text{play}(G)$ and therefore $\text{depth}(G, p) > 0$. Moreover, since $G$ is bounded, it must be $\text{depth}(G, p) < \infty$. We prove by induction on $\text{depth}(G, p)$ that $0 < \text{depth}(G, p) < \infty$ implies $G \parallel \mathcal{M} \xrightarrow{\tau \cdot \beta} G' \parallel \mathcal{M}'$ with $\text{play}(\beta) = \{p\}$. By Session Fidelity (Theorem 3.19) it will follow that $N \parallel \mathcal{M} \xrightarrow{\tau \cdot \beta} N' \parallel \mathcal{M}'$. Let $d = \text{depth}(G, p)$.
Case $d=1$. Here $G = pq^?\ell; G'$. Since $G \parallel \mathcal{M}$ is balanced, $\mathcal{M} \equiv \langle p, \ell, p \rangle \cdot \mathcal{M}'$ by Rule [IN] of Figure 3. Then $G \parallel \mathcal{M} \xrightarrow{pq^?\ell} G' \parallel \mathcal{M}'$ by Rule [EXT-IN] of Figure 5.

Case $d > 1$. Here we have either $G = \boxplus_{i \in I} \mathrm{rs!}\ell_i; G_i$ with $r \neq p$ or $G = \mathrm{rs?}\ell; G'''$ with $s \neq p$. By Lemma 3.5 this implies $\mathrm{depth}(G_i, p) < d$ for all $i \in I$ in the first case, and $\mathrm{depth}(G''', p) < d$ in the second case. Hence in both cases, by applying Rule [EXT-OUT] or Rule [EXT-IN] of Figure 5, we get $G \parallel \mathcal{M} \xrightarrow{\beta'} G'' \parallel \mathcal{M}'$. Since either $G'' = G_k$ for some $k \in I$ or $G'' = G'''$ we get $\mathrm{play}(\beta') \neq \{p\}$ and $\mathrm{depth}(G'', p) < d$. In case $G$ is a choice of outputs we get $p \in \mathrm{play}(G'')$ by projectability of $G$ if $p \neq s$ and by balancing of $G \parallel \mathcal{M}$ if $p = s$. Thus $0 < \mathrm{depth}(G'', p) < d < \infty$. We may then apply induction to get $G'' \parallel \mathcal{M}'' \xrightarrow{\tau \cdot \beta} G' \parallel \mathcal{M}'$ with $\mathrm{play}(\beta) = \{p\}$. Therefore $G \parallel \mathcal{M} \xrightarrow{\beta' \cdot \tau \cdot \beta} G' \parallel \mathcal{M}'$ is the required transition sequence.

(2) Let the *input depth* of the input $pq^?\ell$ in $G$, notation $\mathrm{idepth}(G, pq^?\ell)$, be inductively defined by:

$$
\begin{align*}
\mathrm{idepth}(\boxplus_{i \in I} \mathrm{rs!}\ell_i; G_i, pq?\ell) &= 1 + \max_{i \in I} \{\mathrm{idepth}(G_i, pq?\ell)\} \\
\mathrm{idepth}(\mathrm{rs?}\ell'; G', pq?\ell) &= \begin{cases} 1 & \text{if } pq?\ell = \mathrm{rs?}\ell' \\ \infty & \text{if } p = r \text{ and } q = s \text{ and } \ell \neq \ell' \\ 1 + \mathrm{idepth}(G', pq?\ell) & \text{otherwise} \end{cases} \\
\mathrm{idepth}(\mathrm{End}, pq?\ell) &= \infty
\end{align*}
$$

By hypothesis $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}_1$.

We show that, for all $\mathcal{M}$ and $G$, $\vdash^b G \parallel \langle p, \ell, q \rangle \cdot \mathcal{M}$ implies that $\mathrm{idepth}(G, pq^?\ell)$ is finite. The proof is by induction on $\maxPath(G)$ defined as the maximum length of a path from the root of $G$ to either a leaf (if the path is finite) or the first cyclic global type encountered (if the path is infinite). Since $G$ is regular every infinite path starting from its root must contain a cyclic global type, so $\maxPath(G) = n$ for some $n$.

If $n = 0$ either $G = \mathrm{End}$ or $G$ is cyclic. Therefore $\vdash^b G \parallel \langle p, \ell, q \rangle \cdot \mathcal{M}$ cannot hold and the statement is true (Rules [End] and [OUT] of Figure 3 require an empty queue).

If $n > 0$, we consider the two possible shapes of $G$.

Let $G = \mathrm{rs?}\ell'; G'$. If $r = p, s = q$ and $\ell' \neq \ell$, then $\vdash^b G \parallel \langle p, \ell, q \rangle \cdot \mathcal{M}$ cannot hold and the statement is true (Rule [IN] requires a queue starting with $\langle p, \ell', q \rangle$). If $r = p, s = q$ and $\ell' = \ell$, then $\mathrm{idepth}(G, pq?\ell) = 1$. Otherwise $\maxPath(G') = n-1$ and, since $\vdash^b G \parallel \langle p, \ell, q \rangle \cdot \mathcal{M}$, $\langle p, \ell, q \rangle \cdot \mathcal{M} \equiv \langle r, \ell', s \rangle \cdot \langle p, \ell, q \rangle \cdot \mathcal{M}'$ for some $\mathcal{M}'$ (Rule [IN]). Moreover, $\vdash^b G' \parallel \langle p, \ell, q \rangle \cdot \mathcal{M}'$. By induction hypotheses we get that $\mathrm{idepth}(G', pq?\ell)$ is finite. Therefore $\mathrm{idepth}(G, pq?\ell)$ is finite.

If $G = \boxplus_{i \in I} \mathrm{rs!}\ell_i; G_i$, then for all $i \in I$, $\maxPath(G_i) < n$ and $\vdash^b G_i \parallel \langle p, \ell, q \rangle \cdot \mathcal{M} \cdot \langle r, \ell_i, s \rangle$ (Rule [OUT]). By induction hypotheses we get that $\mathrm{idepth}(G_i, pq?\ell)$ is finite for all $i \in I$. Therefore $\mathrm{idepth}(G, pq?\ell)$ is finite.

More precisely $\mathrm{idepth}(G, pq?\ell)$ is the number of rule applications between the rule which introduces $\langle p, \ell, q \rangle$ and the conclusion in the derivation of $\vdash^b G \parallel \langle p, \ell, q \rangle \cdot \mathcal{M}_1$.

We prove by induction on $\mathrm{idepth}(G, p)$ that $G \parallel \mathcal{M} \xrightarrow{\tau \cdot pq?\ell} G' \parallel \mathcal{M}'$. By Session Fidelity (Theorem 3.19) it will follow that $N \parallel \mathcal{M} \xrightarrow{\tau \cdot pq?\ell} N' \parallel \mathcal{M}'$. Let $id = \mathrm{idepth}(G, p)$.

Case $id = 1$. Here $G = pq?\ell; G'$, which implies $G \parallel \mathcal{M} \xrightarrow{pq?\ell} G' \parallel \mathcal{M}_1$ by Rule [EXT-IN] of Figure 5.

Case $id > 1$. As in the proof of Statement (1), by applying Rule [EXT-OUT] or Rule [EXT-IN] of Figure 5 we get
$$G \parallel \mathcal{M} \xrightarrow{\beta} G'' \parallel \mathcal{M}''$$

where $\beta \neq pq?\ell$ and thus $idepth(G'', pq?\ell) < id$. By induction $G'' \parallel \mathcal{M}'' \xrightarrow{\tau \cdot pq?\ell} G' \parallel \mathcal{M}'$. We conclude that $G \parallel \mathcal{M} \xrightarrow{\beta \cdot \tau \cdot pq?\ell} G' \parallel \mathcal{M}'$ is the required transition sequence.

The proof of Theorem 3.20 shows that the desired transition sequences use only Rules [EXT-OUT] and [EXT-IN] and the output choice is arbitrary. Moreover the lengths of these transition sequences are bounded by depth(G, p) and idepth(G, pq?\ell), respectively.

# 4. Event Structures

We recall the definitions of *Prime Event Structure* (PES) from [20] and *Flow Event Structure* (FES) from [17]. The class of FESs is more general than that of PESs, in that it allows for disjunctive causality and does not require causality to be a transitive relation. As we shall see in Sections 5 and 6, PESs are sufficient to interpret processes, while we need FESs to interpret networks. The reader is referred to [35] for a comparison of the various classes of event structures.

This section is borrowed from [36] and therefore it is also shared with its extended version [14].

## Definition 4.1. (Prime Event Structure)

A *prime event structure* (PES) is a tuple $S = (E, \leq, \#)$ where:

1. $E$ is a denumerable set of events;

2. $\leq \subseteq (E \times E)$ is a partial order relation, called the *causality relation*;

3. $\# \subseteq (E \times E)$ is an irreflexive symmetric relation, called the *conflict relation*, satisfying the property: $\forall e, e', e'' \in E : e \# e' \leq e'' \Rightarrow e \# e''$ (*conflict hereditariness*).

## Definition 4.2. (Flow Event Structure)

A *flow event structure* (FES) is a tuple $S = (E, <, \#)$ where:

1. $E$ is a denumerable set of events;

2. $< \subseteq (E \times E)$ is an irreflexive relation, called the *flow relation*;

3. $\# \subseteq (E \times E)$ is a symmetric relation, called the *conflict relation*.

Note that the flow relation is not required to be transitive, nor acyclic (its reflexive and transitive closure is just a preorder, not necessarily a partial order). Intuitively, the flow relation represents a possible *direct causality* between two events. Observe also that in a FES the conflict relation is not required to be irreflexive nor hereditary; indeed, FESs may exhibit self-conflicting events, as well as disjunctive causality (an event may have conflicting causes).

Any PES $S = (E, \leq, \#)$ may be regarded as a FES, with $<^-$ given by $<^-$ (the strict ordering) or by the covering relation of $\leq$.

We now recall the definition of *configuration* for event structures. Intuitively, a configuration is a set of events having occurred at some stage of the computation. Thus, the semantics of an event structure $S$ is given by its poset of configurations ordered by set inclusion, where $\mathcal{X}_1 \subset \mathcal{X}_2$ means that $S$ may evolve from $\mathcal{X}_1$ to $\mathcal{X}_2$.
**Definition 4.3. (PES configuration)**

Let $S = (E, \leq, \#)$ be a prime event structure. A configuration of $S$ is a finite subset $\mathcal{X}$ of $E$ such that:

1. $\mathcal{X}$ is downward-closed: $e' \leq e \in \mathcal{X} \Rightarrow e' \in \mathcal{X}$;

2. $\mathcal{X}$ is conflict-free: $\forall e, e' \in \mathcal{X}, \neg(e \# e')$.

The definition of configuration for FESs is slightly more elaborated. For a subset $\mathcal{X}$ of $E$, let $\prec_{\mathcal{X}}$ be the restriction of the flow relation to $\mathcal{X}$ and $\prec_{\mathcal{X}}^*$ be its transitive and reflexive closure.

**Definition 4.4. (FES configuration)**

Let $S = (E, \prec, \#)$ be a flow event structure. A configuration of $S$ is a finite subset $\mathcal{X}$ of $E$ such that:

1. $\mathcal{X}$ is downward-closed up to conflicts: $e' \prec e \in \mathcal{X}, e' \notin \mathcal{X} \Rightarrow \exists e'' \in \mathcal{X}. e' \# e'' \prec e$;

2. $\mathcal{X}$ is conflict-free: $\forall e, e' \in \mathcal{X}, \neg(e \# e')$;

3. $\mathcal{X}$ has no causality cycles: the relation $\prec_{\mathcal{X}}^*$ is a partial order.

Condition (2) is the same as for prime event structures. Condition (1) is adapted to account for the more general – non-hereditary – conflict relation. It states that any event appears in a configuration with a “complete set of causes”. Condition (3) ensures that any event in a configuration is actually reachable at some stage of the computation.

If $S$ is a prime or flow event structure, we denote by $C(S)$ its set of configurations. Then, the domain of configurations of $S$ is defined as follows:

**Definition 4.5. (ES configuration domain)**

Let $S$ be a prime or flow event structure with set of configurations $C(S)$. The domain of configurations of $S$ is the partially ordered set $D(S)=_{\text{def}}(C(S), \subseteq)$.

We recall from [35] a useful characterisation for configurations of FESs, which is based on the notion of proving sequence, defined as follows:

**Definition 4.6. (Proving sequence)**

Given a flow event structure $S = (E, \prec, \#)$, a proving sequence in $S$ is a sequence $e_1; \cdots; e_n$ of distinct non-conflicting events (i.e. $i \neq j \Rightarrow e_i \neq e_j$ and $\neg(e_i \# e_j)$ for all $i, j$) satisfying:

$$ \forall i \leq n \forall e \in E : \ e \prec e_i \Rightarrow \exists k < i. \ \text{either } e = e_k \text{ or } e \# e_k \prec e_i $$

Note that any prefix of a proving sequence is itself a proving sequence.

We have the following characterisation of configurations of FESs in terms of proving sequences.

**Proposition 4.7. (Representation of configurations as proving sequences [35])**

Given a flow event structure $S = (E, \prec, \#)$, a subset $\mathcal{X}$ of $E$ is a configuration of $S$ if and only if it can be enumerated as a proving sequence $e_1; \cdots; e_n$.

Since PESs may be viewed as particular FESs, we may use Definition 4.6 and Proposition 4.7 both for the FESs associated with networks (see Section 6) and for the PESs associated with asynchronous global types (see Section 7). Note that for a PES the condition of Definition 4.6 simplifies to

$$ \forall i \leq n \forall e \in E : \ e < e_i \Rightarrow \exists k < i. \ e = e_k $$
# 5. Event Structure Semantics of Processes

In this section, we present our ES semantics for processes and show that the obtained ESs are PESs. This semantics coincides with the one given for processes of synchronous networks in our previous work [36]. Indeed, a design choice of our ES semantics is to implement asynchrony at the level of networks, and not at the level of processes. Thus, processes are agnostic with respect to the communication mode of the network, and sequentiality between their actions is always interpreted as causality.

A *process event*, namely an event in the ES of a process, is an occurrence of a send or receive action preceded by its *causal history*, i.e., by the sequence of actions that caused that occurrence in the process. Therefore, different occurrences of the same send or receive action in the process give rise to different process events in the associated ES. Indeed, process events correspond to *paths* in the syntactic tree of a process.

Our ES semantics for processes will be the basis for defining the ES semantics for networks in Section 6, which will reflect, as expected, the asynchronous nature of communication.

We start by introducing process events, which are non-empty sequences of atomic actions $\pi$ as defined at the beginning of Section 2.

## Definition 5.1. (Process event)

*Process events* (p-events for short) $\eta, \eta'$ are defined by:

$$ \eta ::= \pi \mid \pi \cdot \eta $$

We denote by $\mathcal{PE}$ the set of p-events.

Note the difference with the sequences $\vec{\pi}$ used in Figure 2, where actions are separated by “;”.

Let $\zeta$ denote a (possibly empty) sequence of actions, and $\sqsubseteq$ denote the prefix ordering on such sequences. Each p-event $\eta$ may be written either in the form $\eta = \pi \cdot \zeta$ or in the form $\eta = \zeta \cdot \pi$. We shall feel free to use any of these forms. When a p-event is written as $\eta = \zeta \cdot \pi$, then $\zeta$ may be viewed as the *causal history* of $\eta$, namely the sequence of actions that must have been executed by the process for $\eta$ to be able to happen.

We define the *action* of a p-event to be its last atomic action:

$$ \mathrm{act}(\zeta \cdot \pi) = \pi $$

A p-event $\eta$ is an *output p-event* if $\mathrm{act}(\eta)$ is an output and an *input p-event* if $\mathrm{act}(\eta)$ is an input.

## Definition 5.2. (Causality and conflict relations on p-events)

The *causality relation* $\leq$ and the *conflict relation* $\#^*$ on the set of p-events $\mathcal{PE}$ are defined by:

1. $\eta \sqsubseteq \eta' \Rightarrow \eta \leq \eta'$;

2. $\pi \neq \pi' \Rightarrow \zeta \cdot \pi \cdot \zeta' \#^* \zeta \cdot \pi' \cdot \zeta''$.

## Definition 5.3. (Event structure of a process)

The *event structure of process* $P$ is the triple

$$ S^P(P) = (\mathcal{PE}(P), \leq_P, \#_P) $$

where:

1. $\mathcal{PE}(P) \subseteq \mathcal{PE}$ is the set of sequences of decorations along the nodes and edges of a path from the root to an edge in the tree of $P$;
2. $\le_P$ is the restriction of $\le$ to the set $\mathcal{PE}(P)$;

3. $\#P$ is the restriction of $\#$ to the set $\mathcal{PE}(P)$.

In the following we shall feel free to drop the subscript in $\le_P$ and $\#P$.

Note that the set $\mathcal{PE}(P)$ may be denumerable, as shown by the following example.

**Example 5.4.** If $P = q!l; P \oplus q!l'$, then

$$ \mathcal{PE}(P) = \underbrace{\{q!l \dots q!l \mid n \ge 1\}}_{n} \cup \underbrace{\{q!l \dots q!l \cdot q!l' \mid n \ge 0\}}_{n} $$

We conclude this section by stating that the ESs of processes are PESs. The proof is easy and may be found in [14].

**Proposition 5.5.** Let $P$ be a process. Then $S^P(P)$ is a prime event structure with an empty concurrency relation.

# 6. Event Structure Semantics of Networks

We present now the ES semantics of networks, which is grounded on that of processes.

Network events are simply process events located at some participant of the network. As we are considering asynchronous communication, matching output and input events are not paired together to yield a single network event, but instead they are kept separate, with the first representing the enqueuing of a message in the queue, and the second the de queuing of a message from the queue. The event structure of a network has to take into account the fact that the queue may already contain some messages. In an asynchronous setting, output events can always happen, provided that all events that causally precede them have already been executed. Input events, on the other side, must wait for the expected message to have been enqueued by the sender.

This asymmetry is reflected in the definition of the *narrowing function* (Definition 6.8), which we use - as in our companion paper [14] dealing with synchronous communication - to restrict the set of potential network events by discarding those that are not causally well-founded. In the present case, narrowing will keep all output events (whose predecessors have not been discarded), while it will keep only those input events that are “justified” by an output event (Definition 6.7), or whose expected message in already on the queue. To check that an output event (send of participant p towards q) justifies an input event (receive of participant q from p), since messages sent by p must be read by q in the order they were sent, we look at the histories of the two events to check their “duality” (Clause (1b) Definition 6.6). As discussed before Definition 6.5, this notion of duality is more flexible than the standard one (which matches a send in one participant with a receive in the other), due to the use of a preorder that extends the standard duality check by allowing output actions to be anticipated over input actions as in [21].

We start by defining the *o-trace of a queue* $\mathcal{M}$, notation otr($\mathcal{M}$), which is the sequence of output communications corresponding to the messages in the queue. We use $\omega$ to range over o-traces.

**Definition 6.1. (o-trace)**

The *o-trace corresponding to a queue* is defined by

$$ \mathrm{otr}(\emptyset) = \epsilon \quad \mathrm{otr}(\langle p, l, q \rangle \cdot \mathcal{M}) = pq!l \cdot \mathrm{otr}(\mathcal{M}) $$
O-traces are considered modulo the following equivalence $\cong$, which mimics the structural equivalence on queues.

**Definition 6.2. (o-trace equivalence $\cong$)**

The equivalence $\cong$ on o-traces is the least equivalence such that

$$ \omega \cdot pq!\ell \cdot rs!\ell' \cdot \omega' \cong \omega \cdot rs!\ell' \cdot pq!\ell \cdot \omega' \quad \text{if } p \neq r \text{ or } q \neq s $$

Network events are p-events associated with a participant.

**Definition 6.3. (Network event)**

1. Network events $\rho, \rho'$, also called *n-events*, are p-events located at some participant p, written $p ::= \eta$.

2. We define $i/o(\rho) = \begin{cases} pq!\ell & \text{if } \rho = p ::= \zeta \cdot q!\ell \\ pq?\ell & \text{if } \rho = q ::= \zeta \cdot p?\ell \end{cases}$

and we say that $\rho$ is an *output n-event* representing the communication $pq!\ell$ or an *input n-event* representing the communication $pq?\ell$, respectively.

3. We denote by $\mathcal{NE}$ the set of n-events.

In order to define the flow relation between an output n-event $p ::= \zeta \cdot q!\ell$ and the matching input n-event $q ::= \zeta \cdot p?\ell$, we introduce a duality relation on projections of action sequences, see Definition 6.5. We first define the projection of traces on participants, producing action sequences (Definition 6.4(1)), and then the projection of action sequences on participants, producing sequences of *undirected actions* of the form $!\ell$ and $?\ell$ (Definition 6.4(2)).

In the sequel, we will use the symbol $\dagger$ to stand for either $!$ or $?$. Then $p\dagger\ell$ will stand for either $p!\ell$ or $p?\ell$. Similarly, $\dagger\ell$ will stand for either $!\ell$ or $?\ell$.

**Definition 6.4. (Projections)**

1. The projection of a trace on a participant is defined by:

$$ \epsilon @ r = \epsilon \qquad (\beta \cdot \tau) @ r = \begin{cases} q!\ell \cdot \tau @ r & \text{if } \beta = rq!\ell \\ p?\ell \cdot \tau @ r & \text{if } \beta = pr?\ell \\ \tau @ r & \text{otherwise} \end{cases} $$

2. The projection of an action sequence on a participant is defined by:

$$ \epsilon \vec{r} = \epsilon \qquad (\pi \cdot \zeta) \vec{r} = \begin{cases} \dagger\ell \cdot \zeta \vec{r} & \text{if } \pi = r \dagger \ell \\ \zeta \vec{r} & \text{otherwise} \end{cases} $$

We use $\chi$ to range over sequences of output actions and $\vartheta$ to range over sequences of undirected actions.

We now introduce a variant of the standard duality relation on sequences of undirected actions. This relation is meant to compare the sequences of actions of two participants communicating with each other, in order to check that they match with each other. In a synchronous setting, these sequences would be required to be in the standard symmetric duality relation $\bowtie$, as defined in Clause (1) of Definition 6.5, with an input of a label matching an output of the same label and viceversa. In our asynchronous setting, the duality relation needs to reflect the fact, first observed in [21], that it is “better” to anticipate outputs. To this end, in Clause (2) of Definition 6.5 we define a partial order on sequences of actions whereby a sequence is better than (i.e., less than
or equal to) another one if it anticipates outputs over inputs. Finally, to compare the sequences of actions of two participants communicating with each other, in Clause (3) of Definition 6.5 we define our weak duality relation $\preceq \bowtie \simeq$, a symmetric relation that relates two sequences which are both less than or equal to two sequences related by $\bowtie$. In this way, we allow outputs to be anticipated in both sequences.

**Definition 6.5. (Partial order and duality relations on undirected action sequences)**

The three relations $\bowtie$, $\preceq$ and $\simeq \bowtie \simeq$ on undirected action sequences are defined as follows:

1. The duality relation $\bowtie$ on undirected action sequences is defined by:

$$ \epsilon \bowtie \epsilon \qquad \vartheta \bowtie \vartheta' \Rightarrow !\ell.\vartheta \bowtie ?\ell.\vartheta' \text{ and } ?\ell.\vartheta \bowtie !\ell.\vartheta' $$

2. The partial order relation $\preceq$ on undirected action sequences is defined as the smallest partial order such that:

$$ \vartheta \cdot !\ell \cdot ?\ell' \cdot \vartheta' \preceq \vartheta \cdot ?\ell' \cdot !\ell \cdot \vartheta' $$

3. The weak duality relation $\preceq \bowtie \simeq$ on undirected action sequences is defined by:

$$ \vartheta_1 \preceq \bowtie \simeq \vartheta_2 \quad \text{if} \quad \vartheta'_1 \bowtie \vartheta'_2 \text{ for some } \vartheta'_1, \vartheta'_2 \text{ such that } \vartheta_1 \preceq \vartheta'_1 \text{ and } \vartheta_2 \preceq \vartheta'_2 $$

For example !$\ell_1 \cdot !\ell_3 \cdot ?\ell_2 \cdot ?\ell_4 \preceq !\ell_1 \cdot ?\ell_2 \cdot !\ell_3 \cdot ?\ell_4$ and !$\ell_2 \cdot !\ell_4 \cdot ?\ell_1 \cdot ?\ell_3 \preceq ?\ell_1 \cdot !\ell_2 \cdot ?\ell_3 \cdot !\ell_4$ and !$\ell_1 \cdot ?\ell_2 \cdot !\ell_3 \cdot ?\ell_4 \bowtie ?\ell_1 \cdot !\ell_2 \cdot ?\ell_3 \cdot !\ell_4$ imply !$\ell_1 \cdot !\ell_3 \cdot ?\ell_2 \cdot ?\ell_4 \preceq \bowtie \simeq !\ell_2 \cdot !\ell_4 \cdot ?\ell_1 \cdot ?\ell_3$.

We may now define the flow and conflict relations on n-events. Notably the flow relation is parametrised on an o-trace representing the queue.

**Definition 6.6. ($\omega$-flow and conflict relations on n-events)**

The $\omega$-flow relation $\prec^\omega$ and the conflict relation $\#^\omega$ on the set of n-events $\mathcal{N}\mathcal{E}$ are defined by:

1. (a) $\eta < \eta' \Rightarrow \mathbf{p} :: \eta <^\omega \mathbf{p} :: \eta'$;

(b) $(\omega \@ \mathbf{p} \cdot \zeta) \upharpoonright \mathbf{q} \preceq \bowtie \simeq (\omega \@ \mathbf{q} \cdot \zeta'') \upharpoonright \mathbf{p}$ and $(\zeta' \cdot \mathbf{p} ? \ell) \upharpoonright \mathbf{p} \preceq (\zeta'' \cdot \mathbf{p} ? \ell \cdot \chi) \upharpoonright \mathbf{p}$ for some $\zeta''$ and $\chi \Rightarrow \mathbf{p} :: \zeta \cdot \mathbf{q} ! \ell <^\omega \mathbf{q} :: \zeta' \cdot \mathbf{p} ? \ell$;

2. $\eta \# \eta' \Rightarrow \mathbf{p} :: \eta \# \mathbf{p} :: \eta'$.

Clause (1a) defines flows within the same “locality” $\mathbf{p}$, which we call *local flows*, while Clause (1b) defines flows between different localities, which we call *cross-flows*: these are flows between an output of $\mathbf{p}$ towards $\mathbf{q}$ and the corresponding input of $\mathbf{q}$ from $\mathbf{p}$. The condition in Clause (1b) expresses a sort of relaxed duality between the history of the output and the history of the input: the intuition is that if $\mathbf{q}$ has some outputs towards $\mathbf{p}$ occurring in $\zeta'$, namely before its input $\mathbf{p} ? \ell$, then when checking for duality these outputs can be moved after $\mathbf{p} ? \ell$, namely in $\chi$, because $\mathbf{q}$ does not need to wait until $\mathbf{p}$ has consumed these outputs to perform its input $\mathbf{p} ? \ell$. This condition can be seen at work in Examples 6.12 and 6.13.

The reason for parametrising the flow relation with an o-trace $\omega$ is that the cross-flow relation depends on $\omega$, which in the FES of a network $N \parallel \mathcal{M}$ will be the image through the mapping otr (see Definition 6.1) of the queue $\mathcal{M}$.

For example, we have a cross-flow $\rho <^\omega \rho'$ between the following n-events

$$ \rho = \mathbf{p} :: r ? \ell_4 \cdot \mathbf{q} ? \ell_3 \cdot \mathbf{q} ! \ell <^\omega \mathbf{q} :: \mathbf{p} ! \ell' \cdot \mathbf{p} ? \ell_1 \cdot \mathbf{p} ? \ell_2 \cdot \mathbf{p} ? \ell = \rho' $$

where

$$ \omega = \mathbf{p} \mathbf{q} ! \ell_1 \cdot \mathbf{p} \mathbf{q} ! \ell_2 \cdot \mathbf{q} \mathbf{s} ! \ell_5 \cdot \mathbf{q} \mathbf{p} ! \ell_3 $$
since in this case $\zeta = r?\ell_4 \cdot q?\ell_3$ and $\zeta' = p!\ell' \cdot p?\ell_1 \cdot p?\ell_2$, and thus, taking $\zeta'' = p?\ell_1 \cdot p?\ell_2$ and $\chi = p!\ell'$, we obtain

$$ (\omega \@ p \cdot \zeta)^{\vec{\Gamma}} q = !\ell_1 \cdot !\ell_2 \cdot ?\ell_3 \stackrel{\sim}{\le} ?\ell_3 \cdot !\ell_1 \cdot !\ell_2 \bowtie !\ell_3 \cdot ?\ell_1 \cdot ?\ell_2 = (\omega \@ q \cdot \zeta'')^{\vec{\Gamma}} p $$

and

$$ (\zeta' \cdot p?\ell)^{\vec{\Gamma}} p = !\ell' \cdot ?\ell_1 \cdot ?\ell_2 \cdot ?\ell \stackrel{\sim}{\le} ?\ell_1 \cdot ?\ell_2 \cdot ?\ell \cdot !\ell' = (\zeta'' \cdot p?\ell \cdot \chi)^{\vec{\Gamma}} p $$

When $\rho = p :: \eta \prec^\omega q :: \eta' = \rho'$ and $p \neq q$, then by definition $\rho$ is an output and $\rho'$ is an input. In this case we say that the output $\rho$ $\omega$-justifies the input $\rho'$, or symmetrically that the input $\rho'$ is $\omega$-justified by the output $\rho$. An input n-event may also be justified by a message in the queue. Both justifications are formalised by the following definition.

**Definition 6.7. (Justifications of n-events)**

1. The input n-event $\rho$ is $\omega$-justified by the output n-event $\rho'$ if $\rho' \prec^\omega \rho$ and they are located at different participants.

2. The input n-event $\rho = q :: \zeta \cdot p?\ell$ is $\omega$-queue-justified if there exists $\omega'$ such that $\omega' \cdot pq!\ell$ is a prefix of $\omega$ (modulo $\cong$) and $p :: (\omega' \@ p) \cdot q!\ell \prec^\epsilon \rho$.

The condition $p :: (\omega' \@ p) \cdot q!\ell \prec^\epsilon \rho$ ensures that the inputs from $p$ in $\zeta$ will consume exactly the messages from $p$ to $q$ in the queue $\omega'$. For example, if $\omega = pq!\ell \cdot pq!\ell$, then both $q :: p!\ell' \cdot p?\ell$ and $q :: p!\ell' \cdot p?\ell \cdot p?\ell$ are $\omega$-queue-justified. On the other hand, if $\omega = pq!\ell$, then $q :: p!\ell' \cdot p?\ell$ is $\omega$-queue-justified, but $q :: p!\ell' \cdot p?\ell \cdot p?\ell$ is not $\omega$-queue-justified.

To define the set of n-events associated with a network, we filter the set of all its potential n-events by keeping only

* those n-events whose constituent p-events have all their predecessors appearing in some other n-event of the network and

* those input n-events that are either queue-justified or justified by output n-events of the network.

**Definition 6.8. (Narrowing)**

Given a set $E$ of n-events and an o-trace $\omega$, we define the narrowing of $E$ with respect to $\omega$ (notation $\mathrm{nr}(E, \omega)$) as the greatest fixpoint of the function $f_{E,\omega}$ on sets of n-events defined by:

$$ f_{E,\omega}(X) = \{ \rho \in E \mid \begin{array}{l} \rho = p :: \eta \cdot \pi \Rightarrow p :: \eta \in X \text{ and} \\ (\rho \text{ is an input n-event} \Rightarrow \rho \text{ is either } \omega\text{-queue-justified} \\ \phantom{(\rho \text{ is an input n-event} \Rightarrow \rho \text{ is either }} \text{or } \omega\text{-justified by some } \rho' \in X) \end{array} \} $$

Thus, $\mathrm{nr}(E, \omega)$ is the greatest set $X \subseteq E$ such that $X = f_{E,\omega}(X)$.

Note that we could not have taken $\mathrm{nr}(E, \omega)$ to be the least fixpoint of $f_{E,\omega}$ rather than its greatest fixpoint. Indeed, the least fixpoint of $f_{E,\omega}$ would be the empty set.

It is easy to verify that the n-events which are discarded by the narrowing while their local predecessors are not discarded must be input events. More precisely:

**Fact 6.9.** If $\rho \in E$ and $\rho \notin \mathrm{nr}(E, \omega)$ and either $\rho = p :: \pi$ or $\rho = p :: \eta \cdot \pi$ with $p :: \eta \in \mathrm{nr}(E, \omega)$, then $\rho$ is an input event.

We have now enough machinery to define the ES of networks.
**Definition 6.10. (Event structure of a network)**

The event structure of the network $N \parallel \mathcal{M}$ is the triple:

$$S^{\mathcal{N}}(N \parallel \mathcal{M}) = (\mathcal{N}\mathcal{E}(N \parallel \mathcal{M}), \prec_{N\parallel\mathcal{M}}^{\omega}, \#_{N\parallel\mathcal{M}})$$

where $\omega = \text{otr}(\mathcal{M})$ and

1. $\mathcal{N}\mathcal{E}(N \parallel \mathcal{M}) = \text{nr}(\mathcal{D}\mathcal{E}(N), \omega)$, where $\mathcal{D}\mathcal{E}(N) = \{p :: \eta \mid \eta \in \mathcal{P}\mathcal{E}(P) \text{ with } p[\llap{P}] \in N\}$;

2. $\prec_{N\parallel\mathcal{M}}^{\omega}$ is the restriction of $\prec^{\omega}$ to the set $\mathcal{N}\mathcal{E}(N \parallel \mathcal{M})$;

3. $\#_{N\parallel\mathcal{M}}$ is the restriction of $\#^\omega$ to the set $\mathcal{N}\mathcal{E}(N \parallel \mathcal{M})$.

The following example shows how the operation of narrowing prunes the set of potential n-events of a network ES. It also illustrates the interplay between the two conditions in the definition of narrowing.

**Example 6.11.** Consider the network $N \parallel \emptyset$, where $N = p[\llap{q?\ell}; r!\ell'] \parallel r[\llap{p?\ell'}]$. The set of potential n-events of $S^{\mathcal{N}}(N \parallel \emptyset)$ is $\{p :: q?\ell, p :: q?\ell; r!\ell', r :: p?\ell'\}$. The n-event $p :: q?\ell$ is cancelled, since it is neither $\emptyset$-queue-justified nor $\emptyset$-justified by another n-event of the ES. Then $p :: q?\ell; r!\ell'$ is cancelled since it lacks its predecessor $p :: q?\ell$. Lastly $r :: p?\ell'$ is cancelled, since it is neither $\emptyset$-queue-justified nor $\emptyset$-justified by another n-event of the ES. Notice that $p :: q?\ell; r!\ell'$ would have $\emptyset$-justified $r :: p?\ell'$, if it had not been cancelled. We conclude that $\mathcal{N}\mathcal{E}(N \parallel \emptyset) = \emptyset$.

The following two examples illustrate the definitions given in this section.

**Example 6.12.** Consider the ES associated with the network $N \parallel \emptyset$, with

$$N = p[\llap{q?\ell}; q?\ell'; q!\ell; q?\ell'] \parallel q[\llap{p?\ell'}; p?\ell; p!\ell'; p?\ell]$$

The n-events of $S^{\mathcal{N}}(N \parallel \emptyset)$ are:

$$\begin{align*}
\rho_1 &= p :: q!\ell & \rho'_1 &= q :: p!\ell' \\
\rho_2 &= p :: q!\ell \cdot q?\ell' & \rho'_2 &= q :: p!\ell' \cdot p?\ell' \\
\rho_3 &= p :: q!\ell \cdot q?\ell' \cdot q!\ell & \rho'_3 &= q :: p!\ell' \cdot p?\ell' \cdot p!\ell' \\
\rho_4 &= p :: q!\ell \cdot q?\ell' \cdot q!\ell \cdot q?\ell' & \rho'_4 &= q :: p!\ell' \cdot p?\ell' \cdot p!\ell' \cdot p?\ell'
\end{align*}$$

The $\epsilon$-flow relation is given by the cross-flows $\rho_1 \prec^\epsilon \rho'_2$, $\rho_3 \prec^\epsilon \rho'_4$, $\rho'_1 \prec^\epsilon \rho_2$, $\rho'_3 \prec^\epsilon \rho_4$, as well as by the local flows $\rho_i \prec^\epsilon \rho_j$ and $\rho'_i \prec^\epsilon \rho'_j$ for all $i, j$ such that $i \in \{1, 2, 3\}$, $j \in \{2, 3, 4\}$ and $i < j$. The conflict relation is empty.

The configurations of $S^{\mathcal{N}}(N \parallel \emptyset)$ are:

$$\begin{align*}
\{\rho_1\} & \{\rho'_1\} & \{\rho_1, \rho'_1\} & \{\rho_1, \rho'_1, \rho_2\} & \{\rho_1, \rho'_1, \rho'_2\} & \{\rho_1, \rho'_1, \rho_2, \rho'_2\} \\
\{\rho_1, \rho'_1, \rho_2, \rho_3\} & \{\rho_1, \rho'_1, \rho'_2, \rho'_3\} & \{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho_3\} & \{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho'_3\} & \{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho'_3\} \\
\{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho_3, \rho'_3\} & \{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho_3, \rho'_3, \rho_4\} \\
\{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho_3, \rho'_3, \rho'_4\} & \{\rho_1, \rho'_1, \rho_2, \rho'_2, \rho_3, \rho'_3, \rho_4, \rho'_4\}
\end{align*}$$

The network $N \parallel \emptyset$ can evolve in two steps to the network:

$$N' \parallel \mathcal{M}' = p[\llap{q?\ell'}; q!\ell; q?\ell'] \parallel q[\llap{p?\ell'}; p!\ell'; p?\ell] \parallel \langle p, \ell, q \rangle \cdot \langle q, \ell', p \rangle$$

The n-events of $S^{\mathcal{N}}(N' \parallel \mathcal{M}')$ are:

$$\begin{align*}
\rho_5 &= p :: q?\ell' & \rho'_5 &= q :: p?\ell' \\
\rho_6 &= p :: q?\ell' \cdot q!\ell & \rho'_6 &= q :: p?\ell' \cdot p!\ell' \\
\rho_7 &= p :: q?\ell' \cdot q!\ell \cdot q?\ell' & \rho'_7 &= q :: p?\ell' \cdot p!\ell' \cdot p?\ell'
\end{align*}$$
Let $\omega = \text{pq!}\ell \cdot \text{qp!}\ell'$. The $\omega$-flow relation is given by the cross-flows $\rho_6 \prec^\omega \rho'_7$, $\rho'_6 \prec^\omega \rho_7$, and by the local flows $\rho_i \prec^\omega \rho_j$ and $\rho'_i \prec^\omega \rho'_j$ for all $i, j$ such that $i \in \{5, 6\}, j \in \{6, 7\}$ and $i < j$. The input n-events $\rho_5$ and $\rho'_5$, which are the only ones without causes, are $\omega$-queue-justified. The conflict relation is empty.

The network $N' \parallel \mathcal{M}'$ can evolve in five steps to the network:

$$N'' \parallel \mathcal{M}'' = q[[p?\ell]] \parallel \langle p, \ell, q \rangle$$

The only n-event of $S^N(N'' \parallel \mathcal{M}'')$ is $q :: p?\ell$.

**Example 6.13.** Let $N = p[[q!\ell_1; r!\ell \oplus q!\ell_2; r!\ell]] \parallel q[[p?\ell_1 + p?\ell_2]] \parallel r[[p?\ell]]$. The n-events of $S^N(N \parallel \emptyset)$ are:

$$\begin{align*}
\rho_1 &= p :: q!\ell_1 & \rho'_1 &= q :: p?\ell_1 \\
\rho_2 &= p :: q!\ell_2 & \rho'_2 &= q :: p?\ell_2 \\
\rho_3 &= p :: q!\ell_1 \cdot r!\ell & \rho''_1 &= r :: p?\ell_1 \\
\rho_4 &= p :: q!\ell_2 \cdot r!\ell & &
\end{align*}$$

The $\epsilon$-flow relation is given by the local flows $\rho_1 \prec^\epsilon \rho_3$, $\rho_2 \prec^\epsilon \rho_4$, and by the cross-flows $\rho_1 \prec^\epsilon \rho'_1$, $\rho_2 \prec^\epsilon \rho'_2$, $\rho_3 \prec^\epsilon \rho''_1$, $\rho_4 \prec^\epsilon \rho''_2$. The conflict relation is given by $\rho_1 \# \rho_2$, $\rho_1 \# \rho_4$, $\rho_2 \# \rho_3$, $\rho_3 \# \rho_4$ and $\rho'_1 \# \rho'_2$. Notice that $\rho_3$ and $\rho_4$ are conflicting causes of $\rho''_1$. Figure 6(a) in Section 8 illustrates this event structure. The configurations are

$$\begin{align*}
\{\rho_1\} & \quad \{\rho_1, \rho_3\} & \quad \{\rho_1, \rho'_1\} & \quad \{\rho_1, \rho_3, \rho'_1\} & \quad \{\rho_1, \rho_3, \rho''_1\} & \quad \{\rho_1, \rho_3, \rho'_1, \rho''_1\} \\
\{\rho_2\} & \quad \{\rho_2, \rho_4\} & \quad \{\rho_2, \rho'_2\} & \quad \{\rho_2, \rho_4, \rho'_2\} & \quad \{\rho_2, \rho_4, \rho''_1\} & \quad \{\rho_2, \rho_4, \rho'_2, \rho''_1\}
\end{align*}$$

The network $N \parallel \mathcal{M}$ can evolve in one step to the network:

$$N' \parallel \mathcal{M}' = p[[r!\ell]] \parallel q[[p?\ell_1 + p?\ell_2]] \parallel r[[p?\ell]] \parallel \langle p, \ell_1, q \rangle$$

The n-events of $S^N(N' \parallel \mathcal{M}')$ are $\rho_5 = p :: r!\ell$, $\rho'_3 = q :: p?\ell_1$ and $\rho''_2 = r :: p?\ell$. Let $\omega = \text{pq!}\ell_1$. The $\omega$-flow relation is given by the cross-flow $\rho_5 \prec^\omega \rho''_2$. Notice that the input n-event $\rho'_3$ is $\omega$-queue-justified, and that there is no n-event corresponding to the branch $p?\ell_2$ of $q$, since such an n-event would not be $\omega$-queue-justified. Hence the conflict relation is empty. The configurations are

$$\{\rho_5\} \quad \{\rho'_3\} \quad \{\rho_5, \rho'_3\} \quad \{\rho_5, \rho''_2\} \quad \{\rho_5, \rho'_3, \rho''_2\}$$

It is easy to show that the ESs of networks are FESs.

**Proposition 6.14.** Let $N \parallel \mathcal{M}$ be a network. Then $S^N(N \parallel \mathcal{M})$ is a flow event structure.

**Proof:** Let $\omega = \text{otr}(\mathcal{M})$. The relation $\prec^\omega$ is irreflexive since:

1. $\eta < \eta'$ implies $p :: \eta \neq p :: \eta'$;

2. $p \neq q$ implies $p :: \zeta \cdot q!\ell \neq q :: \zeta' \cdot p?\ell$.

Symmetry of the conflict relation between n-events follows from the corresponding property of conflict between p-events.

In the remainder of this section we show that projections of n-event configurations give p-event configurations. We start by formalising the projection function of n-events to p-events and showing that it is downward surjective.
**Definition 6.15. (Projection of n-events to p-events)**

The projection function $proj_p(\cdot)$ is defined by:

$$ proj_p(\rho) = \begin{cases} \eta & \text{if } \rho = p :: \eta \\ \text{undefined} & \text{otherwise} \end{cases} $$

The projection function $proj_p(\cdot)$ is extended to sets of n-events in the obvious way:

$$ proj_p(X) = \{\eta \mid \exists \rho \in X . \text{proj}_p(\rho) = \eta\} $$

**Proposition 6.16. (Downward surjectivity of projection)**

Let

$$ p[\llbracket P \rrbracket] \in \mathcal{N} \text{ and } S^{\mathcal{N}}(\mathcal{N} \parallel \mathcal{M}) = (\mathcal{NE}(\mathcal{N} \parallel \mathcal{M}), <^{\omega}, \#) \text{ and } S^{\mathcal{P}}(P) = (\mathcal{PE}(P), \le_P, \#_P) $$

Then the partial function $proj_p: \mathcal{NE}(\mathcal{N} \parallel \mathcal{M}) \to \mathcal{PE}(P)$ is downward surjective.

**Proof:** Follows immediately from the fact that $\mathcal{NE}(\mathcal{N} \parallel \mathcal{M})$ is the narrowing of a set of n-events $p :: \eta$ with $\omega = \text{otr}(\mathcal{M})$ and $p[\llbracket P \rrbracket] \in \mathcal{N}$ and $\eta \in \mathcal{PE}(P)$.

The operation of narrowing on network events makes sure that each configuration of the ES of a network projects down to configurations of the ESs of the component processes.

**Proposition 6.17. (Projection preserves configurations)**

Let $p[\llbracket P \rrbracket] \in \mathcal{N}$. If $\mathcal{X} \in C(S^{\mathcal{N}}(\mathcal{N} \parallel \mathcal{M}))$, then $proj_p(\mathcal{X}) \in C(S^{\mathcal{P}}(P))$.

**Proof:** Let $\mathcal{X} \in C(S^{\mathcal{N}}(\mathcal{N} \parallel \mathcal{M}))$ and $\mathcal{Y} = proj_p(\mathcal{X})$. We want to show that $\mathcal{Y} \in C(S^{\mathcal{P}}(P))$, namely that $\mathcal{Y}$ satisfies Conditions (1) and (2) of Definition 4.3.

(1) **Downward-closure.** Let $\eta \in \mathcal{Y}$. Since $\mathcal{Y} = proj_p(\mathcal{X})$, there exists $\rho \in \mathcal{X}$ such that $\rho = p :: \eta$. Suppose $\eta' < \eta$. From Proposition 6.16 there exists $\rho' \in \mathcal{NE}(\mathcal{N} \parallel \mathcal{M})$ such that $\rho' = p :: \eta'$. Let $\omega = \text{otr}(\mathcal{M})$. By Definition 6.6(1a) we have then $\rho' <^{\omega} \rho$. Since $\mathcal{X}$ is left-closed up to conflicts, we know that either $\rho' \in \mathcal{X}$ or there exists $\rho'' \in \mathcal{X}$ such that $\rho'' \# \rho'$ and $\rho'' < \rho$. We examine the two cases in turn:

* $\rho' \in \mathcal{X}$. Then, since $\eta' = proj_p(\rho')$, we have $\eta' \in proj_p(\mathcal{X}) = \mathcal{Y}$ and we are done.

* $\exists \rho'' \in \mathcal{X}. \rho'' \# \rho' \text{ and } \rho'' < \rho$. From $\rho'' \# \rho'$ we get $\rho'' = p :: \eta'' \text{ and } \eta'' \# \eta'$. This implies $\eta'' \# \eta$. By Definition 6.6(2) this implies $\rho \# \rho'$, contradicting the hypothesis that $\mathcal{X}$ is conflict-free. So this case is impossible.

(2) **Conflict-freeness.** Ad absurdum, suppose there exist $\eta, \eta' \in \mathcal{Y}$ such that $\eta \# \eta'$. Then, since $\mathcal{Y} = proj_p(\mathcal{X})$, there must exist $\rho, \rho' \in \mathcal{X}$ such that $\rho = p :: \eta$ and $\rho' = p :: \eta'$. By Definition 6.6(2) this implies $\rho \# \rho'$, contradicting the hypothesis that $\mathcal{X}$ is conflict-free.

Notice that there are configurations of $C(S^{\mathcal{P}}(P))$ which cannot be obtained by projecting configurations of $C(S^{\mathcal{N}}(\mathcal{N} \parallel \mathcal{M}))$ in spite of the condition $p[\llbracket P \rrbracket] \in \mathcal{N}$. A simple example is $p[\llbracket q?\ell \rrbracket] \parallel \emptyset$.
# 7. Event Structure Semantics of Asynchronous Types

We define now the ES semantics of asynchronous types, which is based on particular traces. In the ES of an asynchronous type, as in the ES of a network, an event represents a particular occurrence of an input or output communication, preceded by its causal history. However, while in the ES of a network an event is a located process event, and the causal history of an input or output action is its *local history* within the participant where it is located, in the ES of an asynchronous type the causal history of a communication is its *global history*, which may include communications from other participants. Recall that an asynchronous type is a global type coupled with a queue. Then, the global history of a communication is obtained by taking the trace labelling the path that leads to that communication in the tree of the global type, and removing from it all the communications that do not cause the last one. A trace of this kind, with the property that all its communications cause a subsequent communication in the trace, will be called *pointed*. Moreover, since a communication may have concurrent causes, whose order in the computation is irrelevant, such pointed traces will be considered up to permutation of concurrent communications. So far, the treatment is very similar to the one proposed for the synchronous case in [14]. However, asynchrony introduces additional subtleties in the definition of causality and concurrency among communications. Indeed, two communications will be causally related not only when they have the same player, but also when one of them is an output pq?ℓ and the other is the matching input pq?ℓ (Definition 7.1). Moreover, this matching relation is affected by the presence of the queue (since an input can match either a message in the queue or an output in its trace within the global type), so it has to be computed relatively to a prefixing output trace that represents the queue. This gives rise to a notion of well-formedness for traces (Definition 7.2) that reflects the balancing condition for asynchronous types. Similarly, the concurrency relation between adjacent communications (Definition 7.3) and the resulting permutation equivalence (Definition 7.5), as well as the notion of pointedness (Definition 7.7), will have to be defined relatively to a prefixing output trace.

To sum up, the events in the ES of an asynchronous type will be pairs made of an output trace representing the queue of the type (taken up to an equivalence that reflects the structural congruence on queues, see Definition 6.2), and of a trace (taken up to permutation equivalence, see Definition 7.5) that is pointed with respect to the queue output trace (Definition 7.13) and which is obtained from a trace of the global type by removing only the communications that are not causes of the last one (Definition 7.17).

Although the events of an asynchronous type ES have a more complex and indirect definition than the events of a network ES, they have two important benefits with respect to the latter:

* the relations of causality and conflict are very simple to define on them (Definition 7.16);

* they do not raise well-foundedness issues, since they are extracted from paths in the tree of the global type by removing only the unnecessary communications (Definition 7.17).

For traces $\tau$, as given in Definition 2.3, we use the following notational conventions:

* We denote by $\tau[i]$ the $i$-th element of $\tau$, $i > 0$.

* If $i \le j$, we define $\tau[i \dots j] = \tau[i] \cdots \tau[j]$ to be the subtrace of $\tau$ consisting of the $(j-i+1)$ elements starting from the $i$-th one and ending with the $j$-th one. If $i > j$, we define $\tau[i \dots j]$ to be the empty trace $\epsilon$.

If not otherwise stated we assume that $\tau$ has $n$ elements, so $\tau = \tau[1 \dots n]$.
In the traces appearing in events, we want to require that every input matches a corresponding output. This is checked using the *multiplicity of pq† in τ*, defined by induction as follows:

$$m(pq\dagger, \epsilon) = 0 \qquad m(pq\dagger, \beta \cdot \tau) = \begin{cases} m(pq\dagger, \tau) + 1 & \text{if } \beta = pq\dagger\ell \\ m(pq\dagger, \tau) & \text{otherwise} \end{cases}$$

where $\dagger \in \{!, ?\}$ (as in Definition 6.4).

An input of $q$ from $p$ matches a preceding output from $p$ to $q$ in a trace if it has the same label $\ell$ and the number of inputs from $p$ to $q$ in the subtrace before the given input is equal to the number of outputs from $p$ to $q$ in the subtrace before the given output. This is formalised using the above multiplicity notion and the positions of communications in traces.

**Definition 7.1. (Matching)**

The input $\tau[j] = pq?\ell$ matches the output $\tau[i] = pq!\ell$ in $\tau$, dubbed $i \propto \tau j$, if $i < j$ and $m(pq!, \tau[1 \dots i - 1]) = m(pq?, \tau[1 \dots j - 1])$.

For example, if $\tau = pq!\ell; pq!\ell; pq!\ell; pq?\ell; pq?\ell$, then $1 \propto \tau 4$ and $2 \propto \tau 5$, while no input matches the output at position 3, denoted by $\neg(3 \propto \tau 4)$ and $\neg(3 \propto \tau 5)$. Similarly, if $\tau = pq!\ell; pq!\ell'; pq?\ell'; pq?\ell'$, then $2 \propto \tau 4$, while no output is matched by the input at position 3.

As mentioned earlier, o-traces will be used to represent queues and general traces are paths in global type trees. We want to define an equivalence relation on general traces, which allows us to exchange the order of adjacent communications when this order is not essential. This is the case if the communications have different players and in addition they are not matching according to Definition 7.1. However, the matching relation must also take into account the fact that some outputs are already on the queue. So we will consider well-formedness with respect to a prefixing o-trace. We proceed as follows:

* we start with well-formed traces (Definition 7.2);

* we define the swapping relation $\triangleright_{\omega}$ which allows two communications to be interchanged in a trace $\tau$, when these communications are independent in the trace $\omega \cdot \tau$ (Definition 7.3);

* then we show that $\triangleright_{\omega}$ preserves $\omega$-well-formedness (Lemma 7.4);

* finally we define the equivalence $\approx_{\omega}$ on $\omega$-well-formed traces (Definition 7.5).

In a well-formed trace each input must have a corresponding output. A matching input/output pair corresponds to a communication in the standard global types of [4]. So, if we find an input at some position in a trace, the corresponding output must already occur at some earlier position in the trace. We also introduce a notion of well-formedness with respect to a prefixing trace, where the prefix represents communications that have already occurred.

**Definition 7.2. (Well-formedness)**

1. A trace $\tau$ is *well formed* if every input matches an output in $\tau$.

2. A trace $\tau$ is $\tau'$-well formed if $\tau' \cdot \tau$ is well formed.

As an example, the trace $\tau = pq!\ell \cdot pq!\ell' \cdot pq?\ell'$ is not well formed since the input $pq?\ell'$ in the third position does not match the output $pq!\ell'$ in the second position, i.e., $\neg(2 \propto \tau 3)$. On the other hand, $\tau$ is $pq!\ell'$-well formed, since $pq!\ell' \cdot \tau$ is well formed given that the input $pq?\ell'$ in the fourth position matches the output $pq!\ell'$ in the first position, i.e., $1 \propto pq!\ell' \cdot \tau 4$.
Notice that any o-trace is well formed and any well-formed trace of length 1 must be an output. A well-formed trace of length 2 can consist of either two outputs or an output followed by the matching input. Note also that, if in Definition 7.2(2) the trace $\tau'$ is an o-trace, then it may be viewed as representing a queue, and therefore in this case the matching between an input in $\tau$ and an output in $\tau'$ is akin to the balancing condition of Rule [IN] in Figure 3 for asynchronous types.

**Definition 7.3. (Swapping)**

Let $\tau$ be $\omega$-well formed. We say that $\tau \omega$-swaps to $\tau'$, notation $\tau \triangleright_{\omega} \tau'$, if

$$ \tau = \tau[1 \dots i-1] \cdot \beta \cdot \beta' \cdot \tau'' \quad \tau' = \tau[1 \dots i-1] \cdot \beta' \cdot \beta \cdot \tau'' \quad \text{and} \\ \text{play}(\beta) \cap \text{play}(\beta') = \emptyset \quad \text{and} \quad \neg(i + |\omega| \propto \omega \cdot \tau' i + 1 + |\omega|) $$

For instance, if $\omega = \text{pq!l}$ and $\tau = \text{pq!l} \cdot \text{pq?l}$, then $\tau \omega$-swaps to $\tau' = \text{pq?l} \cdot \text{pq!l}$ because the input in $\tau$ matches the output in $\omega$ and therefore it is independent from the output in $\tau$.

**Lemma 7.4.** If $\tau$ is $\omega$-well formed and $\tau \triangleright_{\omega} \tau'$, then $\tau'$ is $\omega$-well formed too.

**Proof:** Let $\tau = \tau[1 \dots i-1] \cdot \beta \cdot \beta' \cdot \tau_1$ and $\tau' = \tau[1 \dots i-1] \cdot \beta' \cdot \beta \cdot \tau_1$. We want to prove that $\omega \cdot \tau'$ is well formed. To this end, we will show that if $\beta$ or $\beta'$ is an input, then it matches an output that occurs in the prefix $(\omega \cdot \tau)[1 \dots i-1 + |\omega|]$ of $\omega \cdot \tau'$. Note that it must be $\beta \neq \beta'$, since by hypothesis $\text{play}(\beta) \cap \text{play}(\beta') = \emptyset$.

Suppose $\beta'$ is an input. Since $\tau$ is $\omega$-well formed, $\beta'$ matches an output in $(\omega \cdot \tau)[1 \dots i-1+|\omega|] \cdot \beta$. This output cannot be $\beta$, since by hypothesis $\neg(i + |\omega| \propto \omega \cdot \tau' i + 1 + |\omega|)$. Hence $\beta'$ matches an output which occurs in the prefix $(\omega \cdot \tau)[1 \dots i-1 + |\omega|]$ of $\omega \cdot \tau'$.

Suppose now $\beta = \text{pq?l}$ and $\text{m}(\text{pq?}, (\omega \cdot \tau)[1 \dots i-1 + |\omega|]) = m$. Since $\tau$ is $\omega$-well formed, $\beta$ matches an output $(\omega \cdot \tau)[j] = \text{pq!l}$ in the prefix $(\omega \cdot \tau)[1 \dots i-1 + |\omega|]$ of $\omega \cdot \tau$. Then $1 \le j < i + |\omega|$ and $\text{m}(\text{pq!}, (\omega \cdot \tau)[1 \dots j-1 + |\omega|]) = m$. Since $\beta \neq \beta'$, we get also $\text{m}(\text{pq?}, (\omega \cdot \tau')[1 \dots i + |\omega|]) = m$. Then $\beta$ matches $(\omega \cdot \tau)[j]$ also in $\omega \cdot \tau'$.

From the previous lemma and the observation that, if $\tau$ is $\omega$-well formed and $\tau'$ is obtained by swapping the $i$-th and $(i+1)$-th element of $\tau$, then $\text{play}(\tau'[i]) \cap \text{play}(\tau'[i+1]) = \emptyset$ and $\neg(i + |\omega| \propto \omega \cdot \tau' i + 1 + |\omega|)$, we deduce that the swapping relation is symmetric. This allows us to define $\approx_{\omega}$ as the equivalence relation induced by the swapping relation.

**Definition 7.5. (Equivalence $\approx_{\omega}$ on $\omega$-well-formed traces)**

The equivalence $\approx_{\omega}$ on $\omega$-well-formed traces is the reflexive and transitive closure of $\triangleright_{\omega}$.

Observe that for o-traces all the equivalences $\approx_{\omega}$ collapse to $\approx_{\epsilon}$ and $\approx_{\epsilon} \subset \cong$, where $\cong$ is the o-trace equivalence given in Definition 6.2. Indeed, it should be clear that $\approx_{\epsilon} \subset \cong$. To show $\approx_{\epsilon} \neq \cong$, consider $\omega = \text{pq!l} \cdot \text{pr!l}'$ and $\omega' = \text{pr!l}' \cdot \text{pq!l}$. Then $\omega \cong \omega'$ but $\omega \not\cong_{\epsilon} \omega'$. This agrees with the fact that o-traces represent messages in queues, while general traces represent future communication actions.

Another constraint that we want to impose on traces in order to build events is that each communication must be a cause of at least one of those that follow it. This happens when:

* either the two communications have the same player, in which case we say that the first communication is required in the trace (Definition 7.6);
* or the first communication is an output and the second is the matching input.

We call pointedness the property of a trace in which each communication, except the last one, satisfies one of the two conditions above. Like well-formedness, also pointedness is parameterised on traces. We first define required communications.

**Definition 7.6. (Required communication)**

We say that $\tau[i]$ is required in $\tau$, notation $\text{req}(i, \tau)$, if $\text{play}(\tau[i]) \subseteq \text{play}(\tau[(i+1) \dots n])$, where $n = |\tau|$.

Note that by definition the last element $\tau[n]$ is not required in $\tau$.

**Definition 7.7. (Pointedness)**

The trace $\tau$ is $\tau'$-pointed if $\tau$ is $\tau'$-well formed and for all $i$, $1 \le i < n$, one of the following holds:

1. either $\text{req}(i, \tau)$

2. or $i + |\tau'| \propto \tau' \cdot \tau j + |\tau'|$ for some $j > i$.

Observe that the two conditions of the above definition are reminiscent of the two kinds of causal-
ity - local flow and cross-flow - discussed for network events in Section 6 (Definition 6.6). Indeed,
Condition (1) holds if $\tau[i]$ is a local cause of some $\tau[j]$, $j > i$, while Condition (2) holds if $\tau[i]$ is
a cross-cause of some $\tau[j]$, $j > i$.

Note also that the conditions of Definition 7.7 must be satisfied only by every $\tau[i]$ with $i < n$, thus they hold vacuously for any single communication and for the empty trace. This does not imply that a single-communication trace $\tau$ is $\tau'$-pointed for any $\tau'$, since to this end $\tau$ also needs to be $\tau'$-well formed. For instance, the trace $\text{qp}?\ell$ is not $\epsilon$-well formed nor $\text{pq}?\ell$-well formed (beware not to confuse $\text{qp}?\ell$ with $\text{pq}?\ell$). If $\tau = \tau_1 \cdot \beta \cdot \beta'$ is $\tau'$-pointed, then either $\text{play}(\beta) = \text{play}(\beta')$ or $\beta'$ matches $\beta$ in $\tau' \cdot \tau$, i.e., $|\tau_1| + 1 + |\tau'| \propto \tau' \cdot |\tau_1| + 2 + |\tau'|$. Also, if a trace $\tau$ is $\tau'$-pointed for some $\tau'$, we know that each communication in $\tau$ must be executed before the last one. Indeed, the reader familiar with ESs will have noticed that pointed traces are very similar in spirit to ES prime configurations.

**Example 7.8.** Let $\omega = \text{pq}?\ell \cdot \text{rq}?\ell$ and $\tau = \text{pq}?\ell \cdot \text{pq}?\ell \cdot \text{rq}?\ell$. The trace $\tau$ is not $\omega$-pointed, since the output $\text{pq}?\ell$ in $\tau$ is not matched by any input in $\omega \cdot \tau$ (the input $\text{pq}?\ell$ in $\tau$ matches the output $\text{pq}?\ell$ in $\omega$) and it is not required in $\tau$ because its player $p$ is neither the player of $\text{pq}?\ell$ nor the player of $\text{rq}?\ell$. So the condition of Definition 7.7 is not satisfied for the output $\text{pq}?\ell$ in $\tau$. Instead the trace $\tau' = \text{pq}?\ell \cdot \text{rq}?\ell$ is $\omega$-pointed, as well as the trace $\tau'' = \text{rq}?\ell \cdot \text{pq}?\ell$.

Pointedness is preserved by suffixing.

**Lemma 7.9.** If $\tau$ is $\tau'$-pointed and $\tau = \tau_1 \cdot \tau_2$, then $\tau_2$ is $\tau' \cdot \tau_1$-pointed.

**Proof:** Immediate, since $(\tau' \cdot \tau_1) \cdot \tau_2 = \tau' \cdot (\tau_1 \cdot \tau_2)$ and $\tau_2$ is a suffix of $\tau$ and therefore its elements are a subset of those of $\tau$.
Note on the other hand that if $\tau$ is $\tau'$-pointed and $\tau' = \tau'_1 \cdot \tau'_2$, then it is not true that $\tau'_2 \cdot \tau$ is $\tau'_1$-pointed, because in this case the set of elements of $\tau'_2 \cdot \tau$ is a superset of that of $\tau$. For instance, if $\tau'_1 = \epsilon$, $\tau'_2 = pq!\ell$ and $\tau = rs!\ell' \cdot rs?\ell'$, then $\tau'_2 \cdot \tau$ is not $\tau'_1$-pointed.

A useful property of $\omega$-pointedness is that it is preserved by the equivalence $\approx_\omega$, which does not change the rightmost communication in $\omega$-pointed traces. We use last($\tau$) to denote the last communication of $\tau$.

**Lemma 7.10.** Let $\tau$ be $\omega$-pointed and $\tau \approx_\omega \tau'$. Then $\tau'$ is $\omega$-pointed and last($\tau'$) = last($\tau$).

**Proof:** Let $\tau \approx_\omega \tau'$. By Definition 7.5 $\tau'$ is obtained from $\tau$ by $m$ swaps of adjacent communications. The proof is by induction on the number $m$ of swaps.

*Case $m = 0$. The result is obvious.*

*Case $m > 0$. In this case there is $\tau_1$ obtained from $\tau$ by $m-1$ swaps of adjacent communications and there are $\beta, \beta', \tau_2$ such that*

$$ \tau_1 = \tau_1[1 \dots i-1] \cdot \beta \cdot \beta' \cdot \tau_2 \approx_\omega \tau_1[1 \dots i-1] \cdot \beta' \cdot \beta \cdot \tau_2 = \tau' \\ \text{and } \mathrm{play}(\beta) \cap \mathrm{play}(\beta') = \emptyset \text{ and } \neg(i + |\omega| \propto \omega \cdot \tau_1 i + 1 + |\omega|) $$

By induction hypothesis $\tau_1$ is $\omega$-pointed and last($\tau_1$) = last($\tau$).

To show that $\tau'$ is $\omega$-pointed, observe that $\mathrm{play}(\beta) \cap \mathrm{play}(\beta') = \emptyset$ implies:

$$ \mathrm{play}(\beta) \subseteq \mathrm{play}(\beta') \cup \mathrm{play}(\tau_2) \Leftrightarrow \mathrm{play}(\beta) \subseteq \mathrm{play}(\tau_2) $$

$$ \mathrm{play}(\beta') \subseteq \mathrm{play}(\tau_2) \Leftrightarrow \mathrm{play}(\beta') \subseteq \mathrm{play}(\beta) \cup \mathrm{play}(\tau_2) $$

From this we deduce $\mathrm{req}(i, \tau_1) \iff \mathrm{req}(i, \tau')$ and $\mathrm{req}(i+1, \tau_1) \iff \mathrm{req}(i+1, \tau')$, so if both $\tau_1[i]$ and $\tau_1[i+1]$ are required in $\tau_1$ we are done.

Otherwise, suppose that $i+|\omega| \propto \omega \cdot \tau_1 j + |\omega|$ where either $\mathrm{req}(j, \tau_1)$ or $j = n$. If $\mathrm{req}(j, \tau_1)$ then also $\mathrm{req}(j, \tau')$, as we just saw. Now, $j$ cannot be $i+1$ since by hypothesis $\neg(i+|\omega| \propto \omega \cdot \tau_1 i + 1 + |\omega|)$. This implies $i+1+|\omega| \propto \omega \cdot \tau' j + |\omega|$. Similarly we can show that $i+1+|\omega| \propto \omega \cdot \tau_1 j + |\omega|$ implies $i+|\omega| \propto \omega \cdot \tau' j + |\omega|$. Therefore $\tau'$ is $\omega$-pointed.

To show that last($\tau$) = last($\tau'$), assume ad absurdum that $\tau_2 = \epsilon$. Then $\tau_1[1 \dots i-1] \cdot \beta \cdot \beta'$ is $\omega$-pointed and thus, as observed after Definition 7.7, we have either $\mathrm{play}(\beta) \cap \mathrm{play}(\beta') \neq \emptyset$ or $i+|\omega| \propto \omega \cdot \tau_1 i + 1 + |\omega|$. In both cases $\beta$ and $\beta'$ cannot be swapped. So it must be $\tau_2 \neq \epsilon$.

We now relate asynchronous types with pairs of o-traces and traces.

**Lemma 7.11.** If $\vdash^b G \parallel M$ and $\omega = \mathrm{otr}(M)$ and $\tau \in \mathrm{Tr}^+(G)$, then $\tau$ is $\omega$-well formed.

**Proof:** We prove by induction on $\tau$ that $\vdash^b G \parallel M$ implies that $\omega \cdot \tau$ is well formed.

*Case $\tau = \beta$. If $\beta$ is an output the result is obvious. If $\beta = pq?\ell$, by Rule [IN] of Figure 3, we get $M \equiv (\langle p, \ell, q \rangle) \cdot M'$. Therefore $\omega = pq!\ell \cdot \omega'$ and $\omega \cdot \beta$ is well formed.*

*Case $\tau = \beta \cdot \tau'$ with $\tau' \in \mathrm{Tr}^+(G')$. If $\beta = pq!\ell$, then $G = \underset{i \in I}{\boxplus} pq!\ell_i; G_i$ and $\ell = \ell_k$ and $G' = G_k$ for some $k \in I$. From $\vdash^b G \parallel M$ and Rule [OUT] of Figure 3, we get $\vdash^b G' \parallel M \cdot (\langle p, \ell, q \rangle)$. By induction hypothesis on $\tau'$, the trace $\mathrm{otr}(M \cdot (\langle p, \ell, q \rangle)) \cdot \tau'$ is well formed. So since $\mathrm{otr}(M \cdot (\langle p, \ell, q \rangle)) = \omega \cdot pq!\ell$ we get that $\omega \cdot \tau$ is well formed.*
If $\beta = \text{pq?}\ell$, then $G = \text{pq?}\ell; G'$. From $\vdash^b G \parallel \mathcal{M}$ and Rule [IN] of Figure 3, we get $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}'$ and $\vdash^b G' \parallel \mathcal{M}'$. Let $\omega' = \text{otr}(\mathcal{M}')$. Then $\omega \cong \text{pq?}\ell \cdot \omega'$. By induction hypothesis on $\tau'$ the trace $\omega' \cdot \tau'$ is well formed. We want now to show that also the trace $\tau'' = \omega \cdot \tau = \text{pq?}\ell \cdot \omega' \cdot \text{pq?}\ell \cdot \tau'$ is well formed, namely that in $\tau''$ every input matches an output. Note that the first input in $\tau''$ is $\tau''[[\omega| + 1]] = \text{pq?}\ell$. This input matches the output $\tau''[1] = \text{pq?}\ell$. For inputs $\tau''[i]$ with $i > |\omega| + 1$, we know that $\tau''[i] = (\omega' \cdot \tau')[i - 2]$, where $(\omega' \cdot \tau')[i - 2]$ matches some output $(\omega' \cdot \tau')[j]$ in $\omega' \cdot \tau'$. Then $\tau''[i]$ matches $\tau''[j + 1]$ if $j \le |\omega'|$ and $\tau''[j + 2]$ otherwise. This proves that $\omega \cdot \tau$ is well formed.

We have now enough machinery to define events of asynchronous types, which are equivalence classes of pairs whose first elements are o-traces $\omega$ (representing queues) and whose second elements are traces $\tau$ (representing paths in the global type components of the asynchronous types). The traces $\omega$ and $\tau$ are considered respectively modulo $\cong$ and modulo $\approx_{\omega}$. The trace $\tau$ is $\omega$-well formed, reflecting the balancing of asynchronous types. The communication represented by an event is the last communication of $\tau$.

**Definition 7.12. (Type event)**

1. The equivalence $\sim$ on pairs $(\omega, \tau)$, where $\tau \neq \epsilon$ is $\omega$-pointed, is the least equivalence such that

$$ (\omega, \tau) \sim (\omega', \tau') \text{ if } \omega \cong \omega' \text{ and } \tau \approx_{\omega} \tau' $$

2. A type event (t-event) $\delta = [\omega, \tau]_{\sim}$ is the equivalence class of the pair $(\omega, \tau)$. The communication of $\delta$, notation $i/o(\delta)$, is defined to be last($\tau$).

3. We denote by $\mathcal{TE}$ the set of t-events.

Notice that the function $i/o$ can be applied both to an n-event (Definition 6.3(2)) and to a t-event (Definition 7.12(2)). In all cases the result is a communication.

Given an o-trace $\omega$ and an arbitrary trace $\tau$, we want to build a t-event $[\omega, \tau']_{\sim}$ (Definition 7.14). To this aim we scan $\tau$ from right to left and remove all and only the communications $\tau[i]$ which make $\tau$ violate the $\omega$-pointedness property.

**Definition 7.13. (Trace filtering)**

The filtering of $\tau \cdot \tau'$ by $\omega$ with cursor at $\tau$, denoted by $\tau \lceil_{\omega} \tau'$, is defined by induction on $\tau$ as follows:

$$ \epsilon \lceil_{\omega} \tau' = \tau' \qquad (\tau'' \cdot \beta) \lceil_{\omega} \tau' = \begin{cases} \tau'' \lceil_{\omega} (\beta \cdot \tau') & \text{if } \beta \cdot \tau' \text{ is } (\omega \cdot \tau'')\text{-pointed} \\ \tau'' \lceil_{\omega} \tau' & \text{otherwise} \end{cases} $$

For example $\text{pq?}\ell \cdot \text{pq?}\ell \lceil_{\text{pq?}\ell} \epsilon = \text{pq?}\ell \lceil_{\text{pq?}\ell} \epsilon = \epsilon \lceil_{\text{pq?}\ell} \text{pq?}\ell = \text{pq?}\ell$. The resulting trace can also be empty, in case the last communication is an input and $\tau \cdot \tau'$ is not $\omega$-well formed. For instance, $\text{pq?}\ell \lceil_{\text{pq?}\ell} \epsilon = \epsilon \lceil_{\text{pq?}\ell} \epsilon = \epsilon$ because $\text{pq?}\ell$ is not $\text{pq?}\ell$-well formed. It is easy to verify that $\tau \lceil_{\omega} \tau'$ is a subtrace of $\tau \cdot \tau'$, and that if $\tau$ is $\omega$-pointed, then $\tau \lceil_{\omega} \epsilon = \tau$.

**Definition 7.14. (t-event of a pair)**

Let $\tau \neq \epsilon$ be $\omega$-well formed. The t-event generated by $\omega$ and $\tau$, notation $\text{ev}(\omega, \tau)$, is defined to be $\text{ev}(\omega, \tau) = [\omega, \tau \lceil_{\omega} \epsilon]_{\sim}$.
Hence the trace of the event $ev(\omega, \tau)$ is the filtering of $\tau$ by $\omega$ with cursor at the end of $\tau$. This definition is sound since $\omega \cong \omega'$ implies $\tau \frown_{\omega} \tau' = \tau \frown_{\omega'} \tau'$. Moreover the communication of $ev(\omega, \tau)$ is the last communication of $\tau$.

**Lemma 7.15.** If $ev(\omega, \tau)$ is defined, then $\tau \frown_{\omega} \epsilon \neq \epsilon$ and $i/o(ev(\omega, \tau)) = last(\tau \frown_{\omega} \epsilon) = last(\tau)$.

**Proof:** Let $\tau \neq \epsilon$ be $\omega$-well formed and $\tau = \tau' \cdot \beta$. Then $\beta$ is $(\omega \cdot \tau')$-well formed by Definition 7.2. This implies that $\beta$ is $(\omega \cdot \tau')$-pointed by Definition 7.7, and thus $\tau \frown_{\omega} \epsilon = (\tau' \cdot \beta) \frown_{\omega} \epsilon = \tau' \frown_{\omega} \beta$. This gives $i/o(ev(\omega, \tau)) = last(\tau \frown_{\omega} \epsilon) = last(\tau)$.

Since the o-traces in the t-events of an asynchronous type correspond to the queue, we define the causality and conflict relations only between t-events with the same o-traces. Causality is then simply prefixing of traces modulo $\approx_{\omega}$, while conflict is induced by the conflict relation on the p-events obtained by projecting the traces on participants (Definition 6.4(1)).

**Definition 7.16. (Causality and conflict relations on t-events)**

The causality relation $\leq$ and the conflict relation $\#$ on the set of t-events $\mathcal{T}\mathcal{E}$ are defined by:

1. $[\omega, \tau] \sim \leq [\omega, \tau'] \sim$ if $\tau' \approx_{\omega} \tau \cdot \tau_1$ for some $\tau_1$;

2. $[\omega, \tau] \sim \# [\omega, \tau'] \sim$ if $\tau \@ p \# \tau' \@ p$ for some p.

Concerning Clause (1), note that the relation $\leq$ is able to express cross-causality as well as local causality, thanks to the hypothesis of $\omega$-well formedness of $\tau$ in any t-event $[\omega, \tau]$. Indeed, this hypothesis implies that, whenever $\tau$ ends by an input pq?l, then the matched output pq!l must appear either in $\omega$, in which case the output has already occurred, or at some position i in $\tau$. In the latter case, the t-event $ev(\omega, \tau[1...i])$, which represents the output pq!l, is such that $ev(\omega, \tau[1...i]) \leq [\omega, \tau]$.

As regards Clause (2), note that if $\tau \approx_{\omega} \tau'$, then $\tau \@ p = \tau' \@ p$ for all p, because $\approx_{\omega}$ does not swap communications with the same player. Hence, conflict is well defined, since it does not depend on the trace chosen in the equivalence class. The condition $\tau \@ p \# \tau' \@ p$ states that participant p does the same actions in both traces up to some point, after which it performs two different actions in $\tau$ and $\tau'$.

We get the events of an asynchronous type $G \parallel \mathcal{M}$ by applying the function ev to the pairs made of the o-trace representing the queue $\mathcal{M}$ and a trace in the tree of G. Lemma 7.11 and Definition 7.14 ensure that ev is defined. We then build the ES associated with an asynchronous type $G \parallel \mathcal{M}$ as follows.

**Definition 7.17. (Event structure of an asynchronous type)**

The event structure of the asynchronous type $G \parallel \mathcal{M}$ is the triple

$$S^T(G \parallel \mathcal{M}) = (\mathcal{T}\mathcal{E}(G \parallel \mathcal{M}), \leq_{G\parallel\mathcal{M}}, \#_{G\parallel\mathcal{M}})$$

where:

1. $\mathcal{T}\mathcal{E}(G \parallel \mathcal{M}) = \{ev(\omega, \tau) \mid \omega = otr(\mathcal{M}) \& \tau \in \text{Tr}^+(G)\}$;

2. $\leq_{G\parallel\mathcal{M}}$ is the restriction of $\leq$ to the set $\mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$;

3. $\#_{G\parallel\mathcal{M}}$ is the restriction of $\#$ to the set $\mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$.
**Example 7.18.** The network of Example 6.13 can be typed by the asynchronous type G $|| \emptyset$ with G = pq!l₁; pq?l₁; pr!l; pr?l ⊕ pq!l₂; pq?l₂; pr!l; pr?l. The t-events of $S^T(G || \emptyset)$ are:

$$ \delta_1 = [\epsilon, pq!l_1]_{\sim} $$

$$ \delta'_1 = [\epsilon, pq!l_1 \cdot pq?l_1]_{\sim} $$

$$ \delta_2 = [\epsilon, pq!l_2]_{\sim} $$

$$ \delta'_2 = [\epsilon, pq!l_2 \cdot pq?l_2]_{\sim} $$

$$ \delta_3 = [\epsilon, pq!l_1 \cdot pr!l]_{\sim} $$

$$ \delta''_1 = [\epsilon, pq!l_1 \cdot pr!l \cdot pr?l]_{\sim} $$

$$ \delta_4 = [\epsilon, pq!l_2 \cdot pr!l]_{\sim} $$

$$ \delta''_2 = [\epsilon, pq!l_2 \cdot pr!l \cdot pr?l]_{\sim} $$

The causality relation is given by $\delta_1 \le \delta_3$, $\delta_1 \le \delta'_1$, $\delta_2 \le \delta_4$, $\delta_2 \le \delta'_2$, $\delta_3 \le \delta''_1$, $\delta_4 \le \delta''_2$, $\delta_1 \le \delta''_2$, $\delta_2 \le \delta''_2$. The conflict relation is given by $\delta_1 \# \delta_2$ and all the conflicts inherited from it. Figure 6(b) in Section 8 illustrates this event structure.

The following example shows that, due to the fact that global types are not able to represent concurrency explicitly, two forking traces in the tree representation of G do not necessarily give rise to two conflicting events in $S^T(G || M)$.

**Example 7.19.** Let G = pq!l; (rs!l₁; pq?l; rs?l₁ ⊕ rs!l₂; pq?l; rs?l₂). Then $S^T(G || \emptyset)$ contains the t-event $[\epsilon, pq!l \cdot pq?l]_{\sim}$ generated by the two forking traces in Tr⁺(G):

$$ pq!l \cdot rs!l_1 \cdot pq?l $$

$$ pq!l \cdot rs!l_2 \cdot pq?l $$

Note on the other hand that if we replace r by q in G, namely if we consider the global type G' = pq!l; (qs!l₁; pq?l; qs?l₁ ⊕ qs!l₂; pq?l; qs?l₂), then $S^T(G' || \emptyset)$ contains $\delta = [\epsilon, pq!l \cdot qs!l_1 \cdot pq?l]_{\sim}$ and $\delta' = [\epsilon, pq!l \cdot qs!l_2 \cdot pq?l]_{\sim}$. Here $\delta \# \delta'$ because

$$ (pq!l \cdot qs!l_1 \cdot pq?l) \text{ @ q} = s!l_1 \cdot p?l \# s!l_2 \cdot p?l = (pq!l \cdot qs!l_2 \cdot pq?l) \text{ @ q} $$

So, here the two occurrences of pq?l in the type are represented by two distinct events that are in conflict.

We end this section by showing that the obtained ES is a PES.

**Proposition 7.20.** Let G $|| M$ be an asynchronous type. Then $S^T(G || M)$ is a prime event structure.

**Proof:** We show that $\le$ and $\#$ satisfy Properties (2) and (3) of Definition 4.1. Reflexivity and transitivity of $\le$ follow easily from the properties of concatenation and the properties of the two equivalences in Definitions 6.2 and 7.5. As for antisymmetry note that, by Clause (1) of Definition 7.16, if $[\omega, \tau]_{\sim} \le [\omega, \tau']_{\sim}$ and $[\omega, \tau']_{\sim} \le [\omega, \tau]_{\sim}$, then $\tau \cdot \tau_1 \approx_{\omega} \tau'$ and $\tau' \cdot \tau_2 \approx_{\omega} \tau$ for some $\tau_1$ and $\tau_2$. Hence $\tau \cdot \tau_1 \cdot \tau_2 \approx_{\omega} \tau$, which implies $\tau_1 = \tau_2 = \epsilon$, i.e. $\tau \approx_{\omega} \tau'$.

The conflict between t-events inherits irreflexivity, symmetry and hereditariness from the conflict between p-events. In particular, for hereditariness, suppose that $[\omega, \tau]_{\sim} \# [\omega, \tau']_{\sim} \le [\omega, \tau'']_{\sim}$. Then $\tau'' \approx_{\omega} \tau' \cdot \tau_1$ for some $\tau_1$ and $\tau'' @ p = (\tau' \cdot \tau_1) @ p = (\tau' @ p) \cdot (\tau_1 @ p) \# \tau @ p$ since $\tau' @ p \# \tau @ p$.

# 8. Equivalence of the two Event Structure Semantics

In the previous two sections, we defined the ES semantics of networks and types, respectively. As expected, the FES of a network is not isomorphic to the PES of its type, unless the former is
$$N = p[[q!l_1; r!l \oplus q!l_2; r!l]] \parallel q[[p?l_1 + p?l_2]] \parallel r[[p?l]]$$

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

$$G = pq!l_1; pq?l_1; pr!l; pr?l \boxplus pq!l_2; pq?l_2; pr!l; pr?l$$

<figure><img src="image_4.png" /><figcaption>Figure 6. (a) FES of N $||$ ∅ in Example 6.13.</figcaption></figure>

<caption>(b) PES of G $||$ ∅ in Example 7.18.</caption>
itself a PES. As an example, consider the network FES pictured in Figure 6(a) (where the arrows represent the flow relation) and its type PES pictured in Figure 6(b) (where the arrows represent the covering relation of causality and inherited conflicts are not shown). The rationale is that events in the network FES record the *local history* of a communication, while events in the type FES record its *global causal history*, which contains more information. Indeed, while the network FES may be obtained from the type PES simply by projecting each t-event on the player of its last communication, the inverse construction is not as direct: essentially, one needs to construct the configuration domain of the network FES, and from this, by selecting the complete prime configurations according to the classic construction of [20], retrieve the type PES. To show that this is indeed the type PES, however, we would need to rely on well-formedness properties of the network FES, namely on semantic counterparts of the well-formedness properties of types. We will not follow this approach here. Instead, we will compare the FESs of networks and the PESs of their types at a more operational level, by looking at the configuration domains they generate.

In the rest of this section we establish our main theorem for typed networks, namely the isomorphism between the configuration domain of the FES of the network and the configuration domain of the PES of its asynchronous type. To prove the various results leading to this theorem, we will largely use the characterisation of configurations as proving sequences, given in Proposition 4.7. Let us briefly sketch how these results are articulated.

The proof of the isomorphism is grounded on the Subject Reduction Theorem (Theorem 3.18) and the Session Fidelity Theorem (Theorem 3.19). These theorems state that if $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$, then $N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}'$ if and only if $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$, and in both directions $\vdash N' \parallel \mathcal{M}' : G' \parallel \mathcal{M}'$. We can then relate the ESs of networks and asynchronous types by connecting them through the traces of their transition sequences, and by taking into account the queues by means of the mapping otr given by Definition 6.1. This is achieved as follows.

If $N \parallel \mathcal{M} \xrightarrow{\tau} \text{otr}(\mathcal{M}) = \omega$, then the function nec (Definition 8.6) applied to $\omega$ and $\tau$ gives a proving sequence in $S^N(N \parallel \mathcal{M})$ (Theorem 8.10). Vice versa, if $\rho_1; \dots; \rho_n$ is a proving sequence in $S^N(N \parallel \mathcal{M})$, then $N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}'$, where $\tau = i/o(\rho_1) \cdots i/o(\rho_n)$ and $i/o$ is the mapping given in Definition 6.3(2) (Theorem 8.11).

Similarly, if $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$ and $\text{otr}(\mathcal{M}) = \omega$, then the function tec (Definition 8.19) applied to $\omega$ and $\tau$ gives a proving sequence in $S^T(G \parallel \mathcal{M})$ (Theorem 8.24). Lastly, if $\delta_1; \dots; \delta_n$ is a proving sequence in $S^T(G \parallel \mathcal{M})$, then $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$, where $\tau = i/o(\delta_1) \cdots i/o(\delta_n)$ and $i/o$ is the mapping given in Definition 7.12(2) (Theorem 8.25).

It is then natural to split this section in three subsections: the first establishing the relationship between network transition sequences and proving sequences of their event structure, the second doing the same for asynchronous types and finally a third subsection in which the isomorphism between the two configuration domains is proved relying on these relationships.

## 8.1. Transition Sequences of Networks and Proving Sequences of their ESs

We start by showing how network communications affect n-events in the associated ES. To this aim we define two partial operators ♦ and ◇, which applied to a communication $\beta$ and an n-event $\rho$ yield another n-event $\rho'$ (when defined). The intuition is that $\rho'$ represents the event $\rho$ as it will be after the communication $\beta$, or as it was before the communication $\beta$, respectively. So, in particular, if $\{p\} = \text{play}(\beta)$ and $\rho$ is not located at $p$, it will remain unchanged under both mappings ♦ and ◇. We shall now explain in more detail how these operators work.
The operator ♦, when applied to $\beta$ and $\rho$, yields the n-event $\rho'$ obtained from $\rho$ after executing the communication $\beta$, if this event exists. We call $\beta♦\rho$ the residual of $\rho$ after $\beta$. So, if $\beta = pq!l$ and $\rho$ is located at p and its p-event starts with the action $q!l$, then the p-event of $\rho'$ is obtained by removing this action, provided the result is still a p-event (this will not be the case if the p-event of $\rho$ is a simple action); otherwise, the operation is not defined. If $\beta = pq?l$ and $\rho$ is located at q and its p-event starts with the action $p?l$, the p-event of $\rho'$ is obtained by removing $p?l$, if possible; otherwise, the operation is not defined.

The operator ◊, when applied to $\beta$ and $\rho$, yields the n-event $\rho'$ obtained from $\rho$ before executing the communication $\beta$. We call $\beta◊\rho$ the retrieval of $\rho$ before $\beta$. So, if $\beta = pq!l$ and $\rho$ is located at p, the p-event of $\rho'$ is obtained by adding $q!l$ in front of the p-event of $\rho$. If $\beta = pq?l$ and $\rho$ is located at q, the p-event of $\rho'$ is obtained by adding $p?l$ in front of the p-event of $\rho$. We use the projection $\tau @ r$ of a trace on a participant given in Definition 6.4(1).

**Definition 8.1. (Residual and retrieval of an n-event with respect to a communication)**

1. The residual of an n-event $r :: \eta$ after a communication $\beta$ is defined by

$$ \beta \diamond (r :: \eta) = r :: \eta' \quad \text{if } \eta = (\beta @ r) \cdot \eta' $$

2. The retrieval of an n-event $r :: \eta$ before a communication $\beta$ is defined by

$$ \beta \diamond (r :: \eta) = r :: (\beta @ r) \cdot \eta $$

Notice that in Clause (1) of the above definition $\eta' \neq \epsilon$, see Definition 5.1. So $\beta♦(r :: \eta)$ is not defined if $\{r\} = \text{play}(\beta)$ and either $\eta$ is just an atomic action or $\beta @ r$ is not the first action of $\eta$.

Observe also that the operators ♦ and ◊ preserve the communication of n-events, namely

$$ i/o(\beta \diamond \rho) = i/o(\beta \diamond \rho) = i/o(\rho) $$

Residual and retrieval are inverse of each other.

**Lemma 8.2.** 1. If $\beta♦\rho$ is defined, then $\beta◊(\beta♦\rho) = \rho$.

$$ 2. \beta \diamond (\beta \diamond \rho) = \rho. $$

The residual and retrieval operators on n-events are mirrored by (partial) mappings on o-traces, which it is handy to define explicitly.

**Definition 8.3.** The partial mappings $\beta \triangleright \omega$ and $\beta \triangleright \omega$ are defined by:

1. $pq!l \triangleright \omega = \omega \cdot pq!l$ and $pq?l \triangleright \omega = \omega'$ if $\omega \cong pq!l \cdot \omega'$;

2. $pq!l \triangleright \omega = \omega'$ if $\omega \cong \omega' \cdot pq!l$ and $pq?l \triangleright \omega = pq!l \cdot \omega$.

It is easy to verify that if $\beta \triangleright \omega$ is defined, then $\beta \triangleright \beta \triangleright \omega \cong \omega$, and if $\beta \triangleright \omega$ is defined, then $\beta \triangleright \beta \triangleright \omega \cong \omega$.

We can show that the operators $\triangleright$ and $\triangleright$ applied to a communication $\beta$ modify the queues in the same way as the (forward or backward) execution of $\beta$ would do in the underlying network.

**Lemma 8.4.** If $N \parallel \mathcal{M} \xrightarrow{\beta} N' \parallel \mathcal{M}'$, then $\beta \triangleright \text{otr}(\mathcal{M}) \cong \text{otr}(\mathcal{M}')$ and $\beta \triangleright \text{otr}(\mathcal{M}') \cong \text{otr}(\mathcal{M})$.

**Proof:** From $N \parallel \mathcal{M} \xrightarrow{\beta} N' \parallel \mathcal{M}'$ we get $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, l, q \rangle$ if $\beta = pq!l$ and $\mathcal{M} \equiv \langle p, l, q \rangle \cdot \mathcal{M}'$ if $\beta = pq?l$. In the first case, we have $\text{otr}(\mathcal{M}') \cong \text{otr}(\mathcal{M}) \cdot pq!l \cong \beta \triangleright \text{otr}(\mathcal{M})$, whence
also $\beta \triangleright \text{otr}(M') \cong \beta \triangleright \beta \triangleright \text{otr}(M) \cong \text{otr}(M)$. In the second case, we have $\text{otr}(M) \cong \text{pq!l} \cdot \text{otr}(M') \cong \beta \triangleright \text{otr}(M')$, whence also $\beta \triangleright \text{otr}(M) \cong \beta \triangleright \beta \triangleright \text{otr}(M') \cong \text{otr}(M')$.

The residual and retrieval operators preserve the $\omega$-flow and conflict relations. For the flow relation the parametrising o-traces are obtained by the previously defined mappings.

**Lemma 8.5.** 1. If $\rho \prec \omega \rho'$ and $\beta \diamond \rho$ and $\beta \diamond \rho'$ and $\beta \triangleright \omega$ are defined, then $\beta \diamond \rho \prec \beta \triangleright \omega \beta \diamond \rho'$.

2. If $\rho \prec \omega \rho'$ and $\beta \triangleright \omega$ is defined, then $\beta \diamond \rho \prec \beta \triangleright \omega \beta \diamond \rho'$.

3. If $\rho \# \rho'$ and both $\beta \diamond \rho$ and $\beta \diamond \rho'$ are defined, then $\beta \diamond \rho \# \beta \diamond \rho'$.

4. If $\rho \# \rho'$, then $\beta \diamond \rho \# \beta \diamond \rho'$.

We now define the total function nec, which yields sequences of n-events starting from a trace. The definition makes use of the projection given in Definition 6.4(1).

**Definition 8.6. (n-events from traces)**

We define the sequence of n-events corresponding to the trace $\tau$ by

$$ \text{nec}(\tau) = \rho_1; \dots; \rho_n $$

where

$$ \rho_i = p_i :: \eta_i \quad \text{if} \quad \{p_i\} = \text{play}(\tau[i]) \text{ and } \eta_i = \tau[1 \dots i] @ p_i $$

It is immediate to see that, if $\tau = \text{pq!l}$ or $\tau = \text{pq?l}$, then nec($\tau$) consists only of the n-event $p :: q!l$ or of the n-event $q :: p?l$, respectively, because $\tau[1 \dots 1] = \tau[1]$.

We show now that two n-events appearing in the sequence generated from a given trace $\tau$ cannot be in conflict. Moreover, from nec($\tau$) we can recover $\tau$ by means of the function i/o of Definition 6.3(2).

**Lemma 8.7.** Let nec($\tau$) = $\rho_1; \dots; \rho_n$.

1. If $1 \le k, l \le n$, then $\neg(\rho_k \# \rho_l)$;

2. $\tau[i] = i/o(\rho_i)$ for all $i, 1 \le i \le n$.

**Proof:** (1) Let $\rho_i = p_i :: \eta_i$ for all $i, 1 \le i \le n$. If $p_k \ne p_l$, then $\rho_k$ and $\rho_l$ cannot be in conflict. If $p_k = p_l$, then by Definition 8.6 either $\eta_k < \eta_l$ or $\eta_k < \eta_l$. So in all cases we have $\neg(\rho_k \# \rho_l)$.

(2) Immediate from Definition 8.6.

The following lemma relates the operators $\diamond$ and $\diamondsuit$ with the mapping nec. This will be handy for the proof of Theorem 8.10.

**Lemma 8.8.** 1. Let $\tau = \beta \cdot \tau'$. If nec($\tau$) = $\rho_1; \dots; \rho_n$ and nec($\tau'$) = $\rho'_2; \dots; \rho'_n$, then $\beta \diamond \rho_i = \rho'_i$ for all $i, 2 \le i \le n$.

2. Let $\tau = \beta \cdot \tau'$. If nec($\tau$) = $\rho_1; \dots; \rho_n$ and nec($\tau'$) = $\rho'_2; \dots; \rho'_n$, then $\beta \diamond \rho'_i = \rho_i$ for all $i, 2 \le i \le n$.
**Proof:** (1) Note that $\tau[i] = \tau'[i-1]$ for all $i, 2 \le i \le n$. Then we can assume $\rho_i = p_i :: \eta_i$ for all $i, 1 \le i \le n$ and $\rho'_i = p_i :: \eta'_i$ for all $i, 2 \le i \le n$. By Definition 8.6 $\eta_i = \tau[1...i]@p_i = (\beta \cdot \tau'[1...i-1])@p_i$ for all $i, 1 \le i \le n$ and $\eta'_i = \tau'[1...i-1]@p_i$ for all $i, 2 \le i \le n$. Then we get $\beta \blacklozenge \rho_i = \beta \blacklozenge (p_i :: \beta @p_i \cdot \eta'_i) = p_i :: \eta'_i = \rho'_i$ for all $i, 2 \le i \le n$.

(2) From Point (1) and Lemma 8.2(1).

We end this subsection with the two theorems for networks discussed at the beginning of the whole section. We first show that two n-events which $\omega$-justify the same n-event of the same network must be in conflict.

**Lemma 8.9.** Let $\rho, \rho_1, \rho_2 \in \mathcal{NE}(N \parallel M), \omega = \text{otr}(M)$ and $\rho_i \prec^\omega \rho$ for $i \in \{1, 2\}$, where each $\rho_i \prec^\omega \rho$ is derived by Clause (1b) of Definition 6.6. Then $\rho_1 \# \rho_2$.

**Proof:** Clause (1b) of Definition 6.6 prescribes $\rho = q :: \zeta \cdot p?\ell, \rho_i = p :: \zeta_i \cdot q!\ell$ and
$$ (*) (\omega @ p \cdot \zeta_i) \upharpoonright q \stackrel{\sim}{\rightleftharpoons} (\omega @ q \cdot \zeta'_i) \upharpoonright p $$
$$ (**) (\zeta \cdot p?\ell) \upharpoonright p \stackrel{\sim}{\rightleftharpoons} (\zeta'_i \cdot p?\ell \cdot \chi_i) \upharpoonright p $$

for some $\zeta'_i$ and $\chi_i$, where $i \in \{1, 2\}$. Let $n$ be the number of occurrences of $p?\ell$ in $\zeta, n_i$ be the number of occurrences of $q!\ell$ in $\zeta_i$ and $n'_i$ be the number of occurrences of $p?\ell$ in $\zeta'_i$. From (*) we get $n_i = n'_i$ and from (**) we get $n = n'_i$ for $i \in \{1, 2\}$. Then $n_i = n_j$ for $\{i, j\} = \{1, 2\}$. Assume ad absurdum $\rho_i \prec^\omega \rho_j$ for some $i, j \in \{1, 2\}, i \neq j$. Then $\rho_i \prec^\omega \rho_j$ is derived by Clause (1a) of Definition 6.6, thus $\zeta_i \cdot q!\ell \sqsubseteq \zeta_j \cdot q!\ell$, that is $\zeta_i \cdot q!\ell \sqsubseteq \zeta_j$. This means that $\zeta_j$ contains at least one more occurrence of $q!\ell$ than $\zeta_i$, namely $n_i < n_j$, which is a contradiction.

**Theorem 8.10.** If $N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}'$, then nec(otr($\mathcal{M}$), $\tau$) is a proving sequence in the event structure $S^N(N \parallel \mathcal{M})$.

**Proof:** The proof is by induction on $\tau$. Let $\omega = \text{otr}(\mathcal{M})$.

Case $\tau = \beta$. Assume first that $\beta = pq!\ell$. From $N \parallel \mathcal{M} \xrightarrow{\beta} N' \parallel \mathcal{M}'$ we get $p\llbracket \bigoplus_{i \in I} q!\ell_i; P_i \rrbracket \in N$ with $\ell = \ell_k$ for some $k \in I$. Thus $p\llbracket P_k \rrbracket \in N'$ and $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, \ell, q \rangle$. By Definition 5.3(1) $q!\ell \in \mathcal{PE}(\bigoplus_{i \in I} q!\ell_i; P_i)$. By Definition 6.10(1) $p :: q!\ell \in \mathcal{NE}(N \parallel \mathcal{M})$. By Definition 8.6 nec($\beta$) = $\rho_1 = p :: q!\ell$. Clearly, $\rho_1$ is a proving sequence in $S^N(N \parallel \mathcal{M})$, since $\rho \prec^\omega \rho_1$ would imply $\rho = p :: \eta$ for some $\eta$ such that $\eta < q!\ell$, which is not possible.

Assume now that $\beta = pq?\ell$. In this case we get $q\llbracket \bigcup_{i \in I} p?\ell_i; Q_i \rrbracket \in N$ with $\ell = \ell_k$ for some $k \in I$. Thus $q\llbracket Q_k \rrbracket \in N'$ and $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}'$. With a similar reasoning as in the previous case, we obtain nec($\beta$) = $\rho_1 = q :: p?\ell$. Since $\omega \cong pq!\ell \cdot \omega'$, where $\omega' = \text{otr}(\mathcal{M}')$, it is immediate to see that $\rho_1$ is $\omega$-queue-justified. As in the previous case, there is no event $\rho$ in $\mathcal{NE}(N \parallel \mathcal{M})$ such that $\rho \prec^\omega \rho_1$, and thus $\rho_1$ is a proving sequence in $S^N(N \parallel \mathcal{M})$.

Case $\tau = \beta \cdot \tau'$ with $\tau' \neq \epsilon$. In this case, from $N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}'$ we get
$$ N \parallel \mathcal{M} \xrightarrow{\beta} N'' \parallel \mathcal{M}'' \xrightarrow{\tau'} N' \parallel \mathcal{M}' $$

for some $N''$, $\mathcal{M}''$. Let $\omega' = \text{otr}(\mathcal{M}'')$. By Lemma 8.4 $\omega = \beta \triangleright \omega'$. Let nec($\tau$) = $\rho_1; \dots; \rho_n$ and nec($\tau'$) = $\rho_2'; \dots; \rho'_n$. By induction nec($\tau'$) is a proving sequence in $S^N(N'' \parallel \mathcal{M}'')$. By Lemma 8.8(2) $\beta \diamond \rho'_j = \rho_j$ for all $j, 2 \le j \le n$. We show that $\rho_j \in \mathcal{NE}(N \parallel \mathcal{M})$ for all $j,$
2 ≤ j ≤ n. Let ad absurdum *k* (2 ≤ k ≤ n) be the minimum index such that ρ_k ∉ N>E(N || M).
By Fact 6.9, ρ_k should be an input which is not ω-queue justified and β ♦ ρ' should be undefined
for all ρ' ω'-justifying ρ'_k. Since ρ'_k ∈ N>E(N'' || M''), either ρ'_k is ω'-queue-justified or ρ'_k is
ω'-justified by some output, which must be an event ρ'_l for some l < k, 2 ≤ l ≤ n given that
ρ'_2; · · · ; ρ'_n is a proving sequence. In the first case ρ_k is ω-queue-justified. In the second case, we
get β ♦ ρ'_l ∈ N>E(N || M) since l < k. So, in both cases we reach a contradiction. Finally, from
the proof of the base case we know that ρ_1 = p :: β @ p ∈ N>E(N || M) where {p} = play(β).
What is left to show is that ρ_1; · · · ; ρ_n is a proving sequence in S>N>(N || M). By Lemma 8.7(1)
no two events in this sequence can be in conflict. Let ρ ∈ N>E(N || M) and ρ ≺^ω ρ_h for some h,
1 ≤ h ≤ n. As argued in the base case, this implies h > 1. We distinguish two cases, depending
on whether β ♦ ρ is defined or not.

If $\beta \diamond \rho$ is defined, let $\rho' = \beta \diamond \rho$.

If $\rho' \in \mathcal{N}\mathcal{E}(N'' \parallel M'')$, then by Lemma 8.5(1) we have $\rho' \prec^{\omega'} \beta \diamond \rho_h$. By Lemma 8.8(1) $\beta \diamond \rho_j = \rho'_j$ for all $j, 2 \le j \le n$. Thus we have $\rho' \prec^{\omega'} \rho'_h$. Since nec($\tau'$) is a proving sequence in $S^N(N'' \parallel M'')$, by Definition 4.6 there is $l < h$ such that either $\rho' = \rho'_l$ or $\rho' \# \rho'_l \prec \rho'_h$. In the first case we have $\rho = \beta \diamond \rho' = \beta \diamond \rho'_l = \rho_l$. In the second case, from $\rho' \# \rho'_l$ we deduce $\rho \# \rho_l$ by Lemma 8.5(4), and from $\rho'_l \prec^{\omega'} \rho'_h$ we deduce $\rho_l \prec^{\omega} \rho_h$ by Lemma 8.5(2).

If instead $\rho' \notin \mathcal{N}\mathcal{E}(N'' \parallel M'')$, we distinguish two cases according to whether $\rho \prec^\omega \rho_h$ is deduced by Clause (1a) or by Clause (1b) of Definition 6.6. If $\rho \prec^\omega \rho_h$ by Clause (1a) of Definition 6.6, then $\rho' \prec^{\omega'} \rho'_h$ again by Clause (1a) of Definition 6.6 as proved in Lemma 8.5(1). Then $\rho' \notin \mathcal{N}\mathcal{E}(N'' \parallel M'')$ implies $\rho'_h \notin \mathcal{N}\mathcal{E}(N'' \parallel M'')$ by narrowing, so this case is impossible. If $\rho \prec^\omega \rho_h$ by Clause (1b) of Definition 6.6, then $\rho_h$ is an input and $\rho$ $\omega$-justifies $\rho_h$. Then also $\rho'_h$ is an input and by definition of proving sequence there is $\rho'_k$ for some $k, 2 \le k \le n$ which $\omega$-justifies $\rho'_h$. Then $\rho_k$ $\omega$-justifies $\rho_h$ by Lemma 8.5(2). Since $\rho$ and $\rho_k$ both $\omega$-justify $\rho_h$ we get $\rho \# \rho_k$ by Lemma 8.9.

If $\beta \diamond \rho$ is undefined, then by Definition 8.1(1) either $\rho = \rho_1$ or $\rho = p :: \pi \cdot \zeta$ with $\pi \neq \beta @ p$, which implies $\rho \# \rho_1$. In the first case we are done. So, suppose $\rho \# \rho_1$. Let $\pi' = \beta @ p$. Since $\rho$ and $\rho_1$ are n-events in $\mathcal{N}\mathcal{E}(N \parallel M)$, we may assume $\pi = q!\ell$ and $\pi' = q!\ell'$ and therefore $\beta = pq!\ell'$. Indeed, we know that $\text{play}(\beta) = \{p\}$, and $\beta$ cannot be an input $qp?\ell'$ since in this case there should be $\rho_0 = p :: q?\ell \in \mathcal{N}\mathcal{E}(N \parallel M)$ by narrowing, and the two input n-events $\rho_0$ and $\rho_1 = p :: q?\ell'$ could not be both $\omega$-queue-justified. Note that $\rho$ cannot be a local cause of $\rho_h$, i.e $\rho \prec^\omega \rho_h$ cannot hold by Clause (1a) of Definition 6.6, because $\rho_h = p :: \pi \cdot \zeta \cdot \eta$ would imply $\rho_h \# \rho_1$, contradicting what said above. Therefore $\rho$ is a cross-cause of $\rho_h$, i.e $\rho \prec^\omega \rho_h$ holds by Clause (1b) of Definition 6.6, so $\rho = p :: \pi \cdot \zeta' \cdot r!\ell''$ and $\rho_h = r :: \zeta'' \cdot p?\ell'$. We know that $\rho_h = \beta \diamond \rho'_h$. By Definition 8.1(2) we have $\rho'_h = r :: \zeta'' \cdot p?\ell''$, because $r$ is the receiver of a message sent by $p$ and thus by construction $r \neq p$. Since $\rho'_h$ is an input n-event in $\mathcal{N}\mathcal{E}(N'' \parallel M'')$, it must either be justified by the queue $\omega \cdot \beta$ or have a cross-cause in $\mathcal{N}\mathcal{E}(N'' \parallel M'')$. Since $\rho_h$ is not $\omega$-queue-justified (because $\rho \prec^\omega \rho_h$), the only way for $\rho'_h$ to be $\omega \cdot \beta$-queue-justified would be that $\text{pr!}\ell'' = \beta$, that is $r = q$ and $\ell'' = \ell'$, and that $(*)$ $(\omega @ p) \vdash q \cong \cong \cong \zeta_0 \vdash p$ and $(\zeta'' \cdot p?\ell') \vdash p \cong (\zeta_0 \cdot p?\ell' \cdot \chi) \vdash p$ for some $\zeta_0$ and $\chi$, see Definition 6.7. This means that $\zeta_0 \vdash p$ is the subsequence of $\zeta'' \vdash p$ obtained by keeping all and only its inputs. Now, if $\rho'_h = q :: \zeta'' \cdot p?\ell'$, then $\rho_h = q :: \zeta'' \cdot p?\ell'$. Since $\rho = p :: q!\ell \cdot \zeta' \cdot q!\ell'$ is a cross-cause of $\rho_h$, we have $(**)$ $(\omega @ p \cdot q!\ell \cdot \zeta') \vdash q \cong \cong \cong (\omega @ q \cdot \zeta_1 \cdot \chi') \vdash p$ and $(\zeta'' \cdot p?\ell') \vdash p \cong (\zeta_1 \cdot p?\ell' \cdot \chi') \vdash p$ for some $\zeta_1$ and $\chi'$, see Clause (1b) of Definition 6.6. It follows that the inputs in $\zeta_1 \vdash p$ coincide with the inputs in $\zeta'' \vdash p$ and thus with those in $\zeta_0 \vdash p$. From $(*)$ we know that all inputs in $\zeta_0 \vdash p$ match some output in $(\omega @ p) \vdash q$. Therefore no input in $(\omega @ q \cdot \zeta_1 \cdot \chi') \vdash p$ can match the output $q!\ell$ in $(\omega @ p \cdot q!\ell \cdot \zeta') \vdash q$, contradicting $(***)$. Hence $\rho'_h$ must have a cross-cause in
$\mathcal{N}\mathcal{E}(\mathbb{N}'' \parallel \mathcal{M}'')$. Let $\rho'$ be such a cross-cause. Then $\rho' = \mathbf{p} :: \zeta_2 \cdot \mathbf{r}!\ell''$ for some $\zeta_2$. Since nec($\tau'$) is a proving sequence in $\mathcal{S}^N(\mathbb{N}'' \parallel \mathcal{M}'')$, by Definition 4.6 there is $l < h$ such that either $\rho' = \rho'_l$ or $\rho' \# \rho'_l < \rho'_h$. In the first case $\beta \diamond \rho' = \beta \diamond \rho'_l = \rho_l < \rho_h$, and $(\beta \diamond \rho') \# \rho$ because $\beta \diamond \rho' = \mathbf{p} :: \pi' \cdot \zeta_2 \cdot \mathbf{r}!\ell''$. In the second case, let $\rho'_l = \mathbf{p} :: \eta$ for some $\eta$. From $\rho' \# \rho'_l < \rho'_h$ we derive $\beta \diamond \rho' \# \beta \diamond \rho'_l < \beta \diamond \rho'_h$ by Lemma 8.5(4) and (2). This implies $\rho_l = \beta \diamond \rho'_l = \mathbf{p} :: \pi' \cdot \eta$. Hence $\rho \# \rho_l < \rho_h$.

**Theorem 8.11.** If $\rho_1; \cdots; \rho_n$ is a proving sequence in $\mathcal{S}^N(\mathbb{N} \parallel \mathcal{M})$, then $\mathbf{N} \parallel \mathcal{M} \xrightarrow{\tau} \mathbf{N}' \parallel \mathcal{M}'$ where $\tau = i/o(\rho_1) \cdots i/o(\rho_n)$.

**Proof:** The proof is by induction on the length $n$ of the proving sequence. Let $\omega = \mathrm{otr}(\mathcal{M})$.

Case $n = 1$. Let $i/o(\rho_1) = \beta$ where $\beta = \mathbf{pq}?!\ell$. The proof for $\beta = \mathbf{pq}?!\ell$ is similar and simpler. By Definition 6.10(1) $\rho_1 = \mathbf{q} :: \zeta \cdot \mathbf{p}?!\ell$. Note that it must be $\zeta = \epsilon$, since otherwise we would have $\mathbf{q} :: \zeta \in \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$ by narrowing, where $\mathbf{q} :: \zeta <^\omega \rho_1$ by Definition 6.6(1)(a), contradicting the hypothesis that $\rho_1$ is minimal. Moreover, $\rho_1$ cannot be $\omega$-justified by an output n-event $\rho \in \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$, because this would imply $\rho <^\omega \rho_1$, contradicting again the minimality of $\rho_1$. Hence, by Definition 6.10(1) $\rho_1 = \mathbf{q} :: \mathbf{p}?!\ell$ must be $\omega$-queue-justified, which means that $\omega \cong \mathbf{pq}?!\ell \cdot \omega'$. Thus $\mathcal{M} \equiv \langle \mathbf{p}, \ell, \mathbf{q} \rangle \cdot \mathcal{M}'$, where $\mathrm{otr}(\mathcal{M}') = \omega'$. By Definition 5.3(1) and Definition 6.10(1) we have $\mathbf{N} \equiv \mathbf{q}[[\sum_{i \in I} \mathbf{p}?!\ell_i; Q_i]] \parallel \mathbb{N}_0$ where $\ell_k = \ell$ for some $k \in I$. We may then conclude that $\mathbf{N} \parallel \mathcal{M} \xrightarrow{\beta} \mathbf{q}[[Q_k]] \parallel \mathbb{N}_0 \parallel \mathcal{M}' = \mathbf{N}' \parallel \mathcal{M}'$.

Case $n > 1$. Let $i/o(\rho_1) = \beta$ and $\mathbf{N} \parallel \mathcal{M} \xrightarrow{\beta} \mathbb{N}'' \parallel \mathcal{M}''$ be the corresponding transition as obtained from the base case. Let $\omega' = \mathrm{otr}(\mathcal{M}'')$. By Lemma 8.4 $\omega' = \beta \triangleright \omega$. We show that $\beta \diamond \rho_j$ is defined for all $j, 2 \le j \le n$. If $\beta \diamond \rho_k$ were undefined for some $k, 2 \le k \le n$, then by Definition 8.1(1) either $\rho_k = \rho_1$ or $\rho_k = \mathbf{p} :: \pi \cdot \zeta$ where $\{\mathbf{p}\} = \mathrm{play}(\beta)$ and $\pi \neq \beta @ \mathbf{p}$, which implies $\rho_k \# \rho_1$. So both cases are impossible. Thus we may define $\rho'_j = \beta \diamond \rho_j$ for all $j, 2 \le j \le n$. We show that $\rho'_j \in \mathcal{N}\mathcal{E}(\mathbb{N}'' \parallel \mathcal{M}'')$ for all $j, 2 \le j \le n$. Let ad absurdum $k$ ($2 \le k \le n$) be the minimum index such that $\rho'_k \notin \mathcal{N}\mathcal{E}(\mathbb{N}'' \parallel \mathcal{M}'')$. By Fact 6.9, $\rho'_k$ should be an input which is not $\omega'$-queue justified and $\beta \diamond \rho'$ should be undefined for all $\rho' \omega$-justifying $\rho'_k$. Since $\rho_k \in \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$, either $\rho_k$ is $\omega$-queue justified or $\rho_k$ is $\omega$-justified by some output, which must be an event $\rho_l$ for some $l < k, 2 \le l \le n$ given that $\rho_1, \dots, \rho_n$ is a proving sequence. In the first case $\rho'_k$ is $\omega'$-queue justified. In the second case we get $\beta \diamond \rho_l \in \mathcal{N}\mathcal{E}(\mathbb{N}'' \parallel \mathcal{M}'')$ since $l < k$. So in both cases we reach a contradiction.

We show that $\rho'_2; \cdots; \rho'_n$ is a proving sequence in $\mathcal{S}^N(\mathbb{N}'' \parallel \mathcal{M}'')$. By Lemma 8.2(1) $\rho_j = \beta \diamond \rho'_j$ for all $j, 2 \le j \le n$. Then by Lemma 8.5(4) no two n-events in the sequence $\rho'_2; \cdots; \rho'_n$ can be in conflict.

Let $\rho \in \mathcal{N}\mathcal{E}(\mathbb{N}'' \parallel \mathcal{M}'')$ and $\rho <^{\omega'} \rho'_h$ for some $h, 2 \le h \le n$. Let $\rho' = \beta \diamond \rho$. By Lemma 8.5(2) $\beta \diamond \rho <^{\omega} \beta \diamond \rho'_h = \rho_h$. Therefore $\rho' <^{\omega} \rho_h$. If $\rho' \in \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$, since $\rho_1; \cdots; \rho_n$ is a proving sequence in $\mathcal{S}^N(\mathbb{N} \parallel \mathcal{M})$, by Definition 4.6 there is $l < h$ such that either $\rho' = \rho_l$ or $\rho' \# \rho_l < \rho_h$. In the first case, by Lemma 8.2(2) we get $\rho = \beta \diamond \rho' = \beta \diamond \rho_l = \rho'_l$. In the second case, by Lemma 8.5(1) and (3) we get $\rho \# \rho'_l <^{\omega} \rho'_h$. If $\rho' \notin \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$ we distinguish two cases according to whether $\rho <^{\omega'} \rho'_h$ is deduced by Clause (1a) or Clause (1b) of Definition 6.6. If $\rho <^{\omega'} \rho'_h$ by Clause (1a) of Definition 6.6, then $\rho' <^{\omega} \rho_h$ again by Clause (1a) of Definition 6.6 as proved in Lemma 8.5(1). Then $\rho \notin \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$ implies $\rho_h \notin \mathcal{N}\mathcal{E}(\mathbb{N} \parallel \mathcal{M})$ by narrowing, so this case is impossible. If $\rho <^{\omega'} \rho'_h$ by Clause (1b) of Definition 6.6, then $\rho'_h$ is an input and $\rho^{\omega'}$-justifies $\rho'_h$. Then also $\rho_h$ is an input and by definition of proving sequence there is $\rho_k$ for
some $k < h, 2 \le k \le n$ which $\omega$-justifies $\rho_h$. Then $\rho'_k \omega'$-justifies $\rho'_h$ by Lemma 8.5(2). Since $\rho$ and $\rho'_k$ both $\omega'$-justify $\rho'_h$ we get $\rho \# \rho'_k$ by Lemma 8.9.

We have shown that $\rho'_2; \dots; \rho'_n$ is a proving sequence in the event structure $S^N(N'' \parallel M'')$. By induction $N'' \parallel M'' \xrightarrow{\tau'} N' \parallel M'$ where $\tau' = i/o(\rho'_2) \dots i/o(\rho'_n)$. Since $i/o(\rho'_j) = i/o(\rho_j)$ for all $j, 2 \le j \le n$, we have $\tau = \beta \cdot \tau'$. Hence $N \parallel M \xrightarrow{\beta} N'' \parallel M'' \xrightarrow{\tau'} N' \parallel M'$ is the required transition sequence.

**Remark 8.12.** We can show that if $N \parallel M \xrightarrow{\beta} N'$ $\parallel M'$ and $\rho \in \mathcal{N}\mathcal{E}(N' \parallel M')$, then we get $\beta \diamond \rho \in \mathcal{N}\mathcal{E}(N \parallel M)$. The use of this property would simplify the proof of Theorem 8.11, since we would avoid to consider the case $\beta \diamond \rho \notin \mathcal{N}\mathcal{E}(N \parallel M)$. Instead, the fact that $N \parallel M \xrightarrow{\beta} N'$ $\parallel M'$ and $\rho \in \mathcal{N}\mathcal{E}(N \parallel M)$ and $\beta \diamond \rho$ is defined does not imply $\beta \diamond \rho \in \mathcal{N}\mathcal{E}(N' \parallel M')$. An example is

$$ \begin{align*} \rho[\mathbf{q}?\ell] &\parallel \rho[\mathbf{r}?\ell_1; \mathbf{p}?\ell \oplus \mathbf{r}?\ell_2] \parallel \rho[\mathbf{q}?\ell_1 + \mathbf{q}?\ell_2] \parallel \emptyset \xrightarrow{qr?\ell_2} \\ \rho[\mathbf{q}?\ell] &\parallel \rho[\mathbf{0}] \parallel \rho[\mathbf{q}?\ell_1 + \mathbf{q}?\ell_2] \parallel \langle \mathbf{q}, \ell_2, \mathbf{r} \rangle \end{align*} $$

with $\beta = qr?\ell_2$ and $\rho = p :: q?\ell$. Our choice is justified both by the shortening of the whole proofs and by the uniformity between the proofs of Theorems 8.10 and 8.11.

## 8.2. Transition Sequences of Asynchronous Types and Proving Sequences of their ESs

We introduce two operators $\bullet$ and $\circ$ for t-events, which play the same role as the operators $\diamond$ and $\diamondsuit$ for n-events. In defining these operators we must make sure that, in the resulting t-event $[\omega', \tau']_{\sim}$, the trace $\tau'$ is $\omega'$-pointed, see Definition 7.12(1) and (2).

Let us start with the formal definition, and then we shall explain it in detail.

**Definition 8.13. (Residual and retrieval of a t-event with respect to a communication)**

1. The residual of a t-event $[\omega, \tau]_{\sim}$ after a communication $\beta$ is defined by:

$$ \beta \bullet [\omega, \tau]_{\sim} = \begin{cases} [\beta \triangleright \omega, \tau']_{\sim} & \text{if } \tau \approx_{\omega} \beta \cdot \tau' \text{ with } \tau' \neq \epsilon \\ [\beta \triangleright \omega, \tau]_{\sim} & \text{if } \text{play}(\beta) \not\subseteq \text{play}(\tau) \end{cases} $$

2. The retrieval of a t-event $[\omega, \tau]_{\sim}$ before a communication $\beta$ is defined by:

$$ \beta \circ [\omega, \tau]_{\sim} = \begin{cases} [\beta \triangleright \omega, \beta \cdot \tau]_{\sim} & \text{if } \beta \cdot \tau \text{ is } \beta \triangleright \omega\text{-pointed} \\ [\beta \triangleright \omega, \tau]_{\sim} & \text{if } \text{play}(\beta) \not\subseteq \text{play}(\tau) \end{cases} $$

Note that the operators $\bullet$ and $\circ$ preserve the communication of t-events, namely $i/o(\beta \bullet \delta) = i/o(\beta \circ \delta) = i/o(\delta)$, and transform the o-trace using the operators $\triangleright$ and $\triangleright$, see Definition 8.3. We now explain the transformation of the trace $\tau$.

Consider first the case of $\beta \bullet [\omega, \tau]_{\sim}$. If the communication $\beta$ can be brought to the head of the trace $\tau$ using the equivalence $\approx_{\omega}$, we obtain the residual of $[\omega, \tau]_{\sim}$ after $\beta$ by removing the message $\beta$ from the head of the trace, provided this does not result in the empty trace (otherwise, the residual is undefined). Then, letting $\omega' = \beta \triangleright \omega$, it is easy to see that the trace $\tau'$ is $\omega'$-pointed, since it is a suffix of $\tau = \beta \cdot \tau'$ which is $\omega$-pointed (see Lemma 7.9). On the other hand, if $\text{play}(\beta) \not\subseteq \text{play}(\tau)$, then the residual of $[\omega, \tau]_{\sim}$ after $\beta$ is simply obtained by
leaving the trace unchanged. In this case, letting again $\omega' = \beta \triangleright \omega$, the $\omega'$-pointedness of $\tau$ follows immediately from its $\omega$-pointedness. For instance, consider the t-event $[\text{pr}\!\ell', \text{pr}\?\ell']_{\sim}$ where $\omega = \text{pr}\!\ell'$ and $\tau = \text{pr}\?\ell'$. Observe that $p$ occurs in $\tau$, but $p \notin \text{play}(\tau)$. Then we have $\text{pq}\!\ell \bullet [\text{pr}\!\ell', \text{pr}\?\ell']_{\sim} = [\text{pr}\!\ell' \cdot \text{pq}\!\ell, \text{pr}\?\ell']_{\sim}$.

Next, consider the definition of $\beta \circ [\omega, \tau]_{\sim}$. The resulting trace will be the prefixing of $\tau$ by $\beta$ if it is $\beta \triangleright \omega$-pointed. Otherwise the resulting trace is $\tau$ if $\text{play}(\beta)$ is not a player of $\tau$. For instance, for the t-event $[\text{pq}\!\ell, \text{pq}\?\ell]_{\sim}$, where $\omega = \text{pq}\!\ell$ and $\tau = \text{pq}\?\ell$, we have $p \notin \text{play}(\tau)$, but $1 \asymp \text{pq}\!\ell \cdot \text{pq}\?\ell$ 2, thus $\text{pq}\!\ell \circ [\text{pq}\!\ell, \text{pq}\?\ell]_{\sim} = [\epsilon, \text{pq}\!\ell \cdot \text{pq}\?\ell]_{\sim}$. On the other hand, for the t-event $[\text{pq}\!\ell, \text{rs}\!\ell' \cdot \text{rs}\?\ell']_{\sim}$, where $\omega = \text{pq}\!\ell$ and $\tau = \text{rs}\!\ell' \cdot \text{rs}\?\ell'$, we have $p \notin \text{play}(\tau)$ and $\neg(1 \asymp \text{pq}\!\ell \cdot \text{rs}\!\ell' \cdot \text{rs}\?\ell' 2)$ and $\neg(1 \asymp \text{pq}\!\ell \cdot \text{rs}\!\ell' \cdot \text{rs}\?\ell' 3)$, so $\text{pq}\!\ell \circ [\text{pq}\!\ell, \text{rs}\!\ell' \cdot \text{rs}\?\ell']_{\sim} = [\epsilon, \text{rs}\!\ell' \cdot \text{rs}\?\ell']_{\sim}$.

Lemma 8.15 is the analogous of Lemma 8.2 as regards the first two statements. The remaining two statements establish some commutativity properties of the mappings $\bullet$ and $\circ$ when applied to two communications with different players. These properties rely on the corresponding commutativity properties for the mappings $\triangleright$ and $\triangleright$ on o-traces, given in Lemma 8.14. Note that these properties are needed for $\bullet$ and $\circ$ whereas they were not needed for $\diamond$ and $\Diamond$, because the Rules [ICOMM-OUT] and [ICOMM-IN] of Figure 5 allow transitions to occur inside asynchronous types, whereas the LTS for networks only allows transitions for top-level communications. In fact Statements (3) and (4) of Lemma 8.15 are used in the proof of Lemma 8.18.

**Lemma 8.14.** Let $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$.

1. If both $\beta_2 \triangleright \omega$ and $\beta_2 \triangleright (\beta_1 \triangleright \omega)$ are defined, then $\beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega)$.

2. If both $\beta_1 \triangleright \omega$ and $\beta_2 \triangleright \omega$ are defined, then $\beta_1 \triangleright (\beta_2 \triangleright \omega)$ is defined and $\beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega)$.

**Lemma 8.15.** 1. If $\beta \bullet \delta$ is defined, then $\beta \circ (\beta \bullet \delta) = \delta$.

2. If $\beta \circ \delta$ is defined, then $\beta \circ (\beta \circ \delta) = \delta$.

3. If both $\beta_2 \bullet \delta$, $\beta_2 \circ (\beta_1 \circ \delta)$ are defined, and $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$, then $\beta_1 \circ (\beta_2 \circ \delta) = \beta_2 \circ (\beta_1 \circ \delta)$.

4. If both $\beta_1 \circ \delta$, $\beta_2 \circ \delta$ are defined, and $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$, then $\beta_1 \circ (\beta_2 \circ \delta)$ is defined and $\beta_1 \circ (\beta_2 \circ \delta) = \beta_2 \circ (\beta_1 \circ \delta)$.

The next lemma shows that the residual and retrieval operators on t-events preserve causality and that the retrieval operator preserves conflict. It is the analogous of Lemma 8.5, but without the statement corresponding to Lemma 8.5(3), which is true but not required for later results. The difference is due to the fact that ESs of networks are FESs, while those of asynchronous types are PESs. This appears clearly when looking at the proof of Theorem 8.11 which uses Lemma 8.5(3), while that of Theorem 8.25 does not need the corresponding property.

**Lemma 8.16.** 1. If $\delta_1 < \delta_2$ and both $\beta \bullet \delta_1, \beta \circ \delta_2$ are defined, then $\beta \circ \delta_1 < \beta \bullet \delta_2$.

2. If $\delta_1 < \delta_2$ and $\beta \circ \delta_1$ is defined, then $\beta \circ \delta_1 < \beta \circ \delta_2$.

3. If $\delta_1 \# \delta_2$ and both $\beta \circ \delta_1, \beta \circ \delta_2$ are defined, then $\beta \circ \delta_1 \# \beta \circ \delta_2$.

We show now that the operator $\bullet$ starting from t-events of $G \parallel \mathcal{M}$ builds t-events of asynchronous types whose global types are subtypes of $G$ composed in parallel with the queues given by the balancing of Figure 3. Symmetrically, $\circ$ builds t-events of an asynchronous type $G \parallel \mathcal{M}$ from
t-events of the immediate subtypes of G composed in parallel with the queues given by the balancing of Figure 3.

**Lemma 8.17.** 1. If $\delta \in \mathcal{TE}(\coprod_{i \in I} pq!l_i; G_i \parallel \mathcal{M})$ and $pq!l_k \bullet \delta$ is defined, then $pq!l_k \bullet \delta \in \mathcal{TE}(G_k \parallel \mathcal{M} \cdot (p, l_k, q))$ where $k \in I$.

2. If $\delta \in \mathcal{TE}(pq?l; G \parallel (p, l, q) \cdot \mathcal{M})$ and $pq?l \bullet \delta$ is defined, then $pq?l \bullet \delta \in \mathcal{TE}(G \parallel \mathcal{M})$.

3. If $\delta \in \mathcal{TE}(G \parallel \mathcal{M} \cdot (p, l, q))$, then $pq!l \circ \delta \in \mathcal{TE}(\coprod_{i \in I} pq!l_i; G_i \parallel \mathcal{M})$ where $l = l_k$ and $G = G_k$ for some $k \in I$.

4. If $\delta \in \mathcal{TE}(G \parallel \mathcal{M})$, then $pq?l \circ \delta \in \mathcal{TE}(pq?l; G \parallel (p, l, q) \cdot \mathcal{M})$.

The operators $\bullet$ and $\circ$ modify t-events in the same way as the transitions in the LTS would do. This is formalised and proved in the following lemma. Notice that $\diamond$ enjoys this property, while $\diamond$ does not, see Remark 8.12.

**Lemma 8.18.** Let $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$. Then otr($\mathcal{M}$) $\cong$ $\beta \triangleright$ otr($\mathcal{M}'$) and

1. if $\delta \in \mathcal{TE}(G \parallel \mathcal{M})$ and $\beta \bullet \delta$ is defined, then $\beta \bullet \delta \in \mathcal{TE}(G' \parallel \mathcal{M}')$;

2. if $\delta \in \mathcal{TE}(G' \parallel \mathcal{M}')$, then $\beta \circ \delta \in \mathcal{TE}(G \parallel \mathcal{M})$.

The function tec, which builds a sequence of t-events corresponding to a pair $(\omega, \tau)$, is simply defined applying the function ev to $\omega$ and to the prefixes of $\tau$.

**Definition 8.19.** (t-events from pairs of o-traces and traces)

Let $\tau \neq \epsilon$ be $\omega$-well formed. We define the sequence of global events corresponding to $\omega$ and $\tau$ by

$$ \mathrm{tec}(\omega, \tau) = \delta_1; \dots; \delta_n $$

where $\delta_i = \mathrm{ev}(\omega, \tau[1 \dots i])$ for all $i, 1 \le i \le n$.

The following lemma establishes the soundness of the above definition.

**Lemma 8.20.** If $\tau \neq \epsilon$ is $\omega$-well formed, then:

1. $\tau[1 \dots i]$ is $\omega$-well formed for all $i, 1 \le i \le n$;

2. $\mathrm{ev}(\omega, \tau[1 \dots i])$ is defined and $i/o(\mathrm{ev}(\omega, \tau[1 \dots i])) = \tau[i]$ for all $i, 1 \le i \le n$.

**Proof:** The proof of (1) is immediate since by Definitions 7.1 and 7.2 every prefix of an $\omega$-well formed trace is $\omega$-well formed. Fact (2) follows from Fact (1), Definition 7.14 and Lemma 7.15.

As for the function nec (Lemma 8.7), the t-events in a sequence generated by the function tec are not in conflict, and we can retrieve $\tau$ from $\mathrm{tec}(\omega, \tau)$ by using the function i/o given in Definition 7.12(2).

**Lemma 8.21.** Let $\tau \neq \epsilon$ be $\omega$-well formed and $\mathrm{tec}(\omega, \tau) = \delta_1; \dots; \delta_n$.

1. If $1 \le k, l \le n$, then $\neg(\delta_k \# \delta_l)$;
2. $\tau[i] = i/o(\delta_i)$ for all $i$, $1 \le i \le n$.

The following lemma, together with Lemma 8.20, ensures that $\mathrm{tec}(\omega, \tau)$ is defined when $\omega = \mathrm{otr}(\mathcal{M})$ and $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$.

**Lemma 8.22.** If $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$ and $\omega = \mathrm{otr}(\mathcal{M})$, then $\tau$ is $\omega$-well formed.

The following lemma mirrors Lemma 8.8.

**Lemma 8.23.** 1. Let $\tau = \beta \cdot \tau'$ and $\omega' = \beta \triangleright \omega$. If $\mathrm{tec}(\omega, \tau) = \delta_1; \dots; \delta_n$ and $\mathrm{tec}(\omega', \tau') = \delta'_2; \dots; \delta'_n$, then $\beta \bullet \delta_i = \delta'_i$ for all $i, 2 \le i \le n$.

2. Let $\tau = \beta \cdot \tau'$ and $\omega = \beta \triangleright \omega'$. If $\mathrm{tec}(\omega, \tau) = \delta_1; \dots; \delta_n$ and $\mathrm{tec}(\omega', \tau') = \delta'_2; \dots; \delta'_n$, then $\beta \circ \delta'_i = \delta_i$ for all $i, 2 \le i \le n$.

We end this subsection with the two theorems for asynchronous types discussed at the beginning of the whole section, which relate the transition sequences of an asynchronous type with the proving sequences of the associated PES.

**Theorem 8.24.** If $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$, then $\mathrm{tec}(\mathrm{otr}(\mathcal{M}), \tau)$ is a proving sequence in the event structure $S^T(G \parallel \mathcal{M})$.

**Proof:** Let $\omega = \mathrm{otr}(\mathcal{M})$. By Lemma 8.22 $\tau$ is $\omega$-well formed. Then by Lemma 8.20 $\mathrm{tec}(\omega, \tau)$ is defined and by Definition 8.19 $\mathrm{tec}(\omega, \tau) = \delta_1; \dots; \delta_n$, where $\delta_i = \mathrm{ev}(\omega, \tau[1 \dots i])$ for all $i, 1 \le i \le n$. We proceed by induction on $\tau$.

*Case* $\tau = \beta$. In this case, $\mathrm{tec}(\omega, \beta) = \delta_1 = \mathrm{ev}(\omega, \beta)$. By Definition 7.14 we have $\mathrm{ev}(\omega, \beta) = [\omega, \beta \upharpoonright \omega \epsilon]$. By Definition 7.13 $[\omega, \beta \upharpoonright \omega \epsilon] = [\omega, \beta]$, since $\beta$ is $\omega$-well formed.

We use now a further induction on the inference of the transition $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$, see Figure 5.

*Base Subcases.* The rule applied is [EXT-OUT] or [EXT-IN]. Therefore $\beta \in \mathrm{Tr}^+(G)$. By Definition 7.17(1) this implies $\mathrm{ev}(\omega, \beta) \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$.

*Inductive Subcases.* If the last applied Rule is [ICOMM-OUT], then $G = \coprod_{i \in I} \mathrm{pq!l}_i; G_i$ and $G' = \coprod_{i \in I} \mathrm{pq!l}_i; G'_i$ and $G_i \parallel \mathcal{M} \cdot \langle \mathrm{p}, \ell_i, \mathrm{q} \rangle \xrightarrow{\beta} G'_i \parallel \mathcal{M}' \cdot \langle \mathrm{p}, \ell_i, \mathrm{q} \rangle$ for all $i \in I$ and $\mathrm{p} \notin \mathrm{play}(\beta)$. We have $\mathrm{otr}(\mathcal{M} \cdot \langle \mathrm{p}, \ell_i, \mathrm{q} \rangle) = \omega \cdot \mathrm{pq!l}_i$. By induction we get $\mathrm{tec}(\omega \cdot \mathrm{pq!l}_i, \beta) = \delta'_i = [\omega \cdot \mathrm{pq!l}_i, \beta] \in \mathcal{T}\mathcal{E}(G_i \parallel \mathcal{M} \cdot \langle \mathrm{p}, \ell_i, \mathrm{q} \rangle)$. By Lemma 8.17(3) $\mathrm{pq!l}_i \circ \delta'_i \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$. Now, from $\mathrm{p} \notin \mathrm{play}(\beta)$ it follows that $\mathrm{pq!l}_i$ is not a local cause of $\beta$, namely $\neg(\mathrm{req}(1, \mathrm{pq!l}_i \cdot \beta))$. From Lemma 8.22 $\beta$ is $\omega$-well-formed. So, if $\beta$ is an input, its matched output must be in $\omega$. Hence $\mathrm{pq!l}_i$ is not a cross-cause of $\beta$, namely $\neg(1 + |\omega| \propto \omega \cdot \mathrm{pq!l}_i \cdot \beta 2 + |\omega|)$. Therefore $\mathrm{pq!l}_i \cdot \beta$ is not $\omega$-pointed. By Definition 8.13(2) we get $\mathrm{pq!l}_i \circ \delta'_i = [\omega, \beta] \sim = \delta_1$. We conclude again that $\delta_1 \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$ and clearly $\delta_1$ is a proving sequence in $S^T(G \parallel \mathcal{M})$ since $\beta$ has no proper prefix.

If the last applied Rule is [ICOMM-IN] the proof is similar.

*Case* $\tau = \beta \cdot \tau'$ with $\tau' \neq \epsilon$. From $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$ we get $G \parallel \mathcal{M} \xrightarrow{\beta} G'' \parallel \mathcal{M}'' \xrightarrow{\tau'} G' \parallel \mathcal{M}'$ for some $G''$, $\mathcal{M}'$. Let $\omega' = \mathrm{otr}(\mathcal{M}'')$. By Lemma 8.22 $\tau'$ is $\omega'$-well formed. Thus $\mathrm{tec}(\omega', \tau')$ is defined by Lemma 8.20. Let $\mathrm{tec}(\omega', \tau') = \delta'_2; \dots; \delta'_n$. By induction $\mathrm{tec}(\omega', \tau')$ is
a proving sequence in $S^T(G'' \parallel M'')$. By Lemma 8.23(2) $\delta_j = \beta \circ \delta'_j$ for all $j, 2 \le j \le n$. By Lemma 8.18(2) this implies $\delta_j \in \mathcal{TE}(G \parallel M)$ for all $j, 2 \le j \le n$. From the proof of the base case we know that $\delta_1 = [\omega, \beta] \sim \in \mathcal{TE}(G \parallel M)$. What is left to show is that tec($\omega, \tau$) is a proving sequence in $S^T(G \parallel M)$. By Lemma 8.21(1) no two events in this sequence can be in conflict. Let $\delta \in \mathcal{TE}(G \parallel M)$ and $\delta < \delta_k$ for some $k, 1 \le k \le n$. Note that this implies $j > 1$. If $\beta \circ \delta$ is undefined, then by Definition 8.13(1) either $\delta = \delta_1$ or $\delta = [\omega, \tau] \sim$ with $\tau \not\approx_{\omega} \beta \cdot \tau'$ and $\text{play}(\beta) \subseteq \text{play}(\tau)$. In the first case we are done. In the second case $\tau \text{ @ play}(\beta) \# \beta \text{ @ play}(\beta)$, which implies $\delta_1 \# \delta$. Since $\delta < \delta_k$ and conflict is hereditary, it follows that $\delta_1 \# \delta_k$, which contradicts what said above. Hence this second case is not possible. If $\beta \circ \delta$ is defined, by Lemma 8.18(1) $\beta \circ \delta \in \mathcal{TE}(G'' \parallel M'')$ and by Lemma 8.16(1) $\beta \circ \delta < \beta \circ \delta_k$. Let $\delta' = \beta \circ \delta$. By Lemma 8.23(1) $\beta \circ \delta_j = \delta'_j$ for all $j, 2 \le j \le n$. Thus we have $\delta' < \delta'_k$. Since tec($\omega', \tau'$) is a proving sequence in $S^T(G'' \parallel M'')$, by Definition 4.6 there is $h < k$ such that $\delta' = \delta'_h$. By Lemma 8.15(1) we derive $\delta = \beta \circ \delta' = \beta \circ \delta'_h = \delta_h$.

**Theorem 8.25.** If $\delta_1; \dots; \delta_n$ is a proving sequence in $S^T(G \parallel M)$, then $G \parallel M \xrightarrow{\tau} G' \parallel M'$ where $\tau = i/o(\delta_1) \cdots i/o(\delta_n)$.

**Proof:** The proof is by induction on the length $n$ of the proving sequence. Let $\omega = \text{otr}(M)$.

*Case n = 1.* Let $i/o(\delta_1) = \beta$. Since $\delta_1$ is the first event of a proving sequence, it can have no causes, so it must be $\delta_1 = [\omega, \beta] \sim$. We show this case by induction on $d = \text{depth}(G, \text{play}(\beta))$.

*Subcase d = 1.* If $\beta = \text{pq!l}$ we have $G = \coprod_{i \in I} \text{pq!l}_i; G_i$ with $l_k = l$ for some $k \in I$. We deduce $G \parallel M \xrightarrow{\beta} G_k \parallel M \cdot (\langle p, l, q \rangle)$ by applying Rule [EXT-OUT]. If $\beta = \text{pq?l}$ we have $G = \text{pq?l}; G'$. Since $G \parallel M$ is well formed, by Rule [IN] of Figure 3 we get $M \equiv (\langle p, l, q \rangle) \cdot M'$. We deduce $G \parallel M \xrightarrow{\beta} G' \parallel M'$ by applying Rule [EXT-IN].

*Subcase d > 1.* We are in one of the two situations:

1. $G = \coprod_{i \in I} \text{rs!l}_i; G_i$ with $r \notin \text{play}(\beta)$;

2. $G = \text{rs?l'}; G''$ with $s \notin \text{play}(\beta)$.

In situation (1), $r \notin \text{play}(\beta)$ implies that $\text{rs!l}_i \bullet \delta_1$ is defined for all $i \in I$ by Definition 8.13(1). By Lemma 8.17(1) $\text{rs!l}_i \bullet \delta_1 \in \mathcal{TE}(G_i \parallel M \cdot (\langle p, l_i, q \rangle))$ for all $i \in I$. Lemma 3.5(1) implies $\text{depth}(G, \text{play}(\beta)) > \text{depth}(G_i, \text{play}(\beta))$ for all $i \in I$. By induction hypothesis we have $G_i \parallel M \cdot (\langle p, l_i, q \rangle) \xrightarrow{\beta} G'_i \parallel M' \cdot (\langle p, l_i, q \rangle)$ for all $i \in I$. Then we may apply Rule [ICOMM-OUT] to deduce

$$ \coprod_{i \in I} \text{rs!l}_i; G_i \parallel M \xrightarrow{\beta} \coprod_{i \in I} \text{rs!l}_i; G'_i \parallel M' $$

In situation (2), since $G \parallel M$ is well formed we get $M \equiv (\langle r, l', s \rangle) \cdot M''$ by Rule [IN] of Figure 3. Hence $\omega \cong \text{rs!l}' \cdot \omega'$. This and $s \notin \text{play}(\beta)$ imply that $\text{rs?l}' \bullet \delta_1$ is defined by Definition 8.13(1). By Lemma 8.17(2) $\text{rs?l}' \bullet \delta_1 \in \mathcal{TE}(G'' \parallel M'')$. Lemma 3.5(2) gives $\text{depth}(G, \text{play}(\beta)) > \text{depth}(G'', \text{play}(\beta))$. By induction hypothesis $G'' \parallel M'' \xrightarrow{\beta} G''' \parallel M'''$. Then we may apply Rule [ICOMM-IN] to deduce

$$ \text{rs?l'}; G'' \parallel (\langle r, l', s \rangle) \cdot M'' \xrightarrow{\beta} \text{rs?l'}; G''' \parallel (\langle r, l', s \rangle) \cdot M''' $$

*Case n > 1.* Let $i/o(\delta_1) = \beta$, and $G \parallel M \xrightarrow{\beta} G'' \parallel M''$ be the corresponding transition as obtained from the base case. We show that $\beta \circ \delta_j$ is defined for all $j, 2 \le j \le n$. If $\beta \circ \delta_k$ were
undefined for some $k$, $2 \le k \le n$, then by Definition 8.13(1) either $\delta_k = \delta_1$ or $\delta_k = [\omega, \tau]_{\sim}$ with $\tau \not\approx_{\omega} \beta \cdot \tau'$ and $\text{play}(\beta) \subseteq \text{play}(\tau)$. In the second case $\beta @ \text{play}(\beta) \# \tau @ \text{play}(\beta)$, which implies $\delta_k \# \delta_1$. So both cases are impossible. If $\beta \bullet \delta_j$ is defined, by Lemma 8.18(1) we may define $\delta'_j = \beta \bullet \delta_j \in \mathcal{T}\mathcal{E}(G'' \parallel \mathcal{M}'')$ for all $j, 2 \le j \le n$. We show that $\delta'_2; \dots; \delta'_n$ is a proving sequence in $\mathcal{S}^T(G'' \parallel \mathcal{M}'')$. By Lemma 8.15(1) $\delta_j = \beta \circ \delta'_j$ for all $j, 2 \le j \le n$. Then by Lemma 8.16(3) no two events in this sequence can be in conflict.

Let $\delta \in \mathcal{T}\mathcal{E}(G'' \parallel \mathcal{M}'')$ and $\delta < \delta'_h$ for some $h, 2 \le h \le n$. By Lemma 8.18(2) $\beta \circ \delta$ and $\beta \circ \delta'_h$ belong to $\mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$. By Lemma 8.16(2) $\beta \circ \delta < \beta \circ \delta'_h$. By Lemma 8.15(1) $\beta \circ \delta'_h = \delta_h$. Let $\delta' = \beta \circ \delta$. Then $\delta' < \delta_h$ implies, by Definition 4.6 and the fact that $\mathcal{S}^T(G \parallel \mathcal{M})$ is a PES, that there is $l < h$ such that $\delta' = \delta_l$. By Lemma 8.15(2) we get $\delta = \beta \bullet \delta' = \beta \bullet \delta_l = \delta'_l$.

We have shown that $\delta'_2; \dots; \delta'_n$ is a proving sequence in $\mathcal{S}^T(G'' \parallel \mathcal{M}'')$. By induction we get $G'' \parallel \mathcal{M}'' \xrightarrow{\tau'} G' \parallel \mathcal{M}'$ where $\tau' = i/o(\delta'_2) \cdots i/o(\delta'_n)$. Let $\tau = i/o(\delta_1) \cdots i/o(\delta_n)$. Since $i/o(\delta'_j) = i/o(\delta_j)$ for all $j, 2 \le j \le n$, we have $\tau = \beta \cdot \tau'$. Therefore $G \parallel \mathcal{M} \xrightarrow{\beta} G'' \parallel \mathcal{M}'' \xrightarrow{\tau'} G' \parallel \mathcal{M}'$ is the required transition sequence.

## 8.3. Isomorphism

We are finally able to show that the ES interpretation of a network is equivalent, when the session is typable, to the ES interpretation of its asynchronous type.

To prove our main theorem, we will also use the following separation result from [35] (Lemma 2.8 p. 12). Recall from Section 4 that $\mathcal{C}(S)$ denotes the set of configurations of $S$.

**Lemma 8.26. (Separation [35])**

Let $S = (E, <, \#)$ be a flow event structure and $\mathcal{X}, \mathcal{X}' \in \mathcal{C}(S)$ be such that $\mathcal{X} \subset \mathcal{X}'$. Then there exist $e \in \mathcal{X}' \setminus \mathcal{X}$ such that $\mathcal{X} \cup \{e\} \in \mathcal{C}(S)$.

We may now establish the isomorphism between the domain of configurations of the FES of a typable network and the domain of configurations of the PES of its asynchronous type. In the proof of this result, we will use the characterisation of configurations as proving sequences, given in Proposition 4.7. We will also take the freedom of writing $\rho_1; \cdots; \rho_n \in \mathcal{C}(\mathcal{S}^N(N \parallel \mathcal{M}))$ to mean that $\rho_1; \cdots; \rho_n$ is a proving sequence such that $\{\rho_1, \dots, \rho_n\} \in \mathcal{C}(\mathcal{S}^N(N \parallel \mathcal{M}))$, and similarly for $\delta_1; \cdots; \delta_n \in \mathcal{C}(\mathcal{S}^T(G \parallel \mathcal{M}))$.

**Theorem 8.27.** If $\vdash N \parallel \mathcal{M} : G \parallel \mathcal{M}$, then $\mathcal{D}(\mathcal{S}^N(N \parallel \mathcal{M})) \simeq \mathcal{D}(\mathcal{S}^T(G \parallel \mathcal{M}))$.

**Proof:** Let $\omega = \text{otr}(\mathcal{M})$. We start by constructing a bijection between the proving sequences of the event structure $\mathcal{S}^N(N \parallel \mathcal{M})$ and the proving sequences of the event structure $\mathcal{S}^T(G \parallel \mathcal{M})$. By Theorem 8.11, if $\rho_1; \cdots; \rho_n \in \mathcal{C}(\mathcal{S}^N(N \parallel \mathcal{M}))$, then $N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}'$ where $\tau = i/o(\rho_1) \cdots i/o(\rho_n)$. By applying iteratively Subject Reduction (Theorem 3.18), we obtain

$$G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}' \text{ and } \vdash N' \parallel \mathcal{M}' : G' \parallel \mathcal{M}'$$

By Theorem 8.24, we get $\text{tec}(\omega, \tau) \in \mathcal{C}(\mathcal{S}^T(G \parallel \mathcal{M}))$.

By Theorem 8.25, if $\delta_1; \cdots; \delta_n \in \mathcal{C}(\mathcal{S}^T(G \parallel \mathcal{M}))$, then $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$, where $\tau = i/o(\delta_1) \cdots i/o(\delta_n)$. By applying iteratively Session Fidelity (Theorem 3.19), we obtain

$$N \parallel \mathcal{M} \xrightarrow{\tau} N' \parallel \mathcal{M}' \text{ and } \vdash N' \parallel \mathcal{M}' : G' \parallel \mathcal{M}'$$
By Theorem 8.10, we get nec(τ) ∈ C(SN (N || M)).

Therefore we have a bijection between D(SN (N || M)) and D(ST (G || M)), given by nec(τ) ↔ tec(ω, τ) for any τ generated by the (bisimilar) LTSs of N || M and G || M.

We now show that this bijection preserves inclusion of configurations.

By Lemma 8.26 it is enough to prove that if ρ₁;···;ρn ∈ C(SN (N || M)) is mapped to δ₁;···;δn ∈ C(ST (G || M)), then ρ₁;···;ρn;ρ ∈ C(SN (N || M)) iff δ₁;···;δn;δ ∈ C(ST (G || M)), where δ₁;···;δn;δ is the image of ρ₁;···;ρn;ρ under the bijection. So, suppose ρ₁;···;ρn ∈ C(SN (N || M)) and δ₁;···;δn ∈ C(ST (G || M)) are such that

$$ \rho_1; \dots; \rho_n = \mathrm{nec}(\tau) \leftrightarrow \mathrm{tec}(\omega, \tau) = \delta_1; \dots; \delta_n $$

Then i/o(ρ₁)···i/o(ρn) = τ = i/o(δ₁)···i/o(δn).

By Theorem 8.11, if ρ₁;···;ρn;ρ ∈ C(SN (N || M)) with i/o(ρ) = β, then

$$ N \parallel M \xrightarrow{\tau \cdot \beta} N' \parallel M' $$

By applying iteratively Subject Reduction (Theorem 3.18) we get

$$ G \parallel M \xrightarrow{\tau \cdot \beta} G' \parallel M' \text{ and } \vdash N' \parallel M' : G' \parallel M' $$

We conclude that tec(ω, τ · β) ∈ C(ST (G || M)) by Theorem 8.24.

By Theorem 8.25, if δ₁;···;δn;δ ∈ C(ST (G || M)) with i/o(δ) = β, then

$$ G \parallel M \xrightarrow{\tau \cdot \beta} G' \parallel M' $$

By applying iteratively Session Fidelity (Theorem 3.19) we get

$$ N \parallel M \xrightarrow{\tau \cdot \beta} N' \parallel M' \text{ and } \vdash N' \parallel M' : G' \parallel M' $$

We conclude that nec(τ · β) ∈ C(SN (N || M)) by Theorem 8.10.

# 9. Related Work and Conclusions

Session types, as originally proposed in [2, 4] for binary sessions, are grounded on types for the π-calculus. Early proposals for typing channels in the π-calculus include simple sorts [37], input/output types [38] and usage types [39]. In particular, the notion of progress for multiparty sessions [28, 29] is inspired by the notion of lock-freedom developed for the π-calculus in [40, 41]. The more recent work [42] provides further evidence of the strong relationship between binary session types and channel types in the linear π-calculus. The notion of lock-freedom for the linear π-calculus was also revisited in [43].

Multiparty sessions disciplined by global types were introduced in the keystone papers [3, 4]. These papers, as well as most subsequent work on multiparty session types (for a survey see [34]), were based on more expressive session calculi than the one we use here, where sessions may be interleaved and participants exchange pairs of labels and values. In that more general setting, global types are projected onto session types and in turn session types are assigned to processes. Here, instead, we consider only single sessions and pure label exchange: this allows us to project global types directly to processes, as in [44], where the considered global types are those of [4]. Possible extensions of our work to more expressive calculi are discussed at the end of this section.

Standard global types are too restrictive for typing processes which communicate asynchronously. A powerful typability extension is obtained by the use of the subtyping relation given in [21]. This subtyping allows inputs and outputs to be exchanged, stating that anticipating outputs is better. The rationale is that outputs are not blocking, while inputs are blocking in asynchronous
communication. Unfortunately, this subtyping is undecidable [22, 23], and thus type systems equipped with this subtyping are not effective. Decidable restrictions of this subtyping relation have been proposed [22, 23, 45]. In particular, subtyping is decidable when both internal and external choices are forbidden in one of the two compared processes [22]. This result is improved in [45], where both the subtype and the supertype can contain either internal or external choices. More interestingly, the work [46] presents a sound (though not complete) algorithm for checking asynchronous subtyping. A very elegant formulation of asynchronous subtyping is given in [47]: it allows the authors to show that any extension of this subtyping would be unsound. In the present paper we achieve a gain in typability for asynchronous networks by using a more fine-grained syntax for global types. Our type system is decidable, since projection is computable and the preorder on processes is decidable. Notice that there are networks that can be typed using the algorithm in [46] but cannot be typed in our system, like the running example of that paper.

We claim that our asynchronous types are more “prescribing” than the global types of [3, 4] equipped with asynchronous subtyping, since asynchronous types specify the order in which participants must do inputs and outputs in a more precise way. For instance, the asynchronous type $pq!\ell; qp!\ell'; pq?\ell; qp?\ell' \parallel \emptyset$ of Example 3.9 can type the network $p[q!\ell; q?\ell'] \parallel q[p!\ell'; p?\ell]$ of Example 2.4, but cannot type the network $p[q!\ell; q?\ell'] \parallel q[p?\ell; p!\ell']$. Instead, in the system of [3, 4] one needs the global type $p \to q : \ell; q \to p : \ell'$ and the subtyping $p!\ell'; p?\ell \le p?\ell; p!\ell'$ to type the network $p[q!\ell; q?\ell'] \parallel q[p!\ell'; p?\ell]$. The drawback is that the same global type can also type the network $p[q!\ell; q?\ell'] \parallel q[p?\ell; p!\ell']$.

More permissive variants of our asynchronous types, called “deconfined global types”, were subsequently considered in [26] and [48]. In [26] both projection and balancing are refined, the first one allowing the participants which are not involved in a choice to have different behaviours in the branches of the choice, and the second one allowing unbounded queues. The type system of [48] has global types that allow choices of inputs, and types the running example of [46] and also a network for which the algorithm of [46] fails. With the type systems of [26, 48], due to a more complex definition of balancing, one can type networks with queues that may grow unboundedly, which is not possible with the balancing of Figure 3. Since the focus of the present paper was on the event structure semantics, we decided to go for this simpler definition.

Since their introduction in [19, 20], Event Structures have been widely used to give semantics to process calculi. Several ES interpretations of Milner’s calculus CCS have been proposed, using various classes of ESs: Stable ESs [49], Prime ESs or variations of them [50, 51, 52], and Flow ESs [17, 53]. Other calculi such as TCSP [54, 55] and LOTOS have been provided respectively with a PES semantics [56, 57] and with a Bundle ES semantics [58, 59]. More recently, ES semantics have been investigated also for the $\pi$-calculus [60, 61, 62, 63, 64, 65]. A more extensive discussion on ES semantics for process calculi may be found in our companion paper [14].

It is noteworthy that all the above-mentioned ES semantics were given for calculi with synchronous communication. This is perhaps not surprising since ESs are generally equipped with a synchronisation algebra when modelling process calculi, and a communication is represented by a single event resulting from the synchronisation of two events. This is also the reason why, in our previous paper [14], we started by considering an ES semantics for a synchronous session calculus with standard global types.

An asynchronous PES semantics for finite synchronous choreographies was recently proposed in [66], where, like in the present paper, a communication is represented by two distinct events, one for the output and the other for the matching input. However, in our work the output and the matching input are already decoupled in the types, and their matching relation needs to be recon-
structed in order to obtain the cross-causality relation in the PES. Instead, in [66] the definition of cross-causality is immediate, since the standard synchronous type construct gives rises to a pair of events which are by construction in the cross-causality relation. Moreover, only types are interpreted as ESs in [66]. To sum up, while asynchrony is an essential feature of sessions in our calculus, and therefore it is modelled also in their abstract specifications (asynchronous types), asynchrony is rather viewed as an implementation feature of sessions in [66], and therefore it is not modelled in their abstract specifications (choreographies), which remain synchronous.

A denotational semantics based on concurrent games [67] has been proposed for the asynchronous π-calculus in [68]. Notice, however, that in the asynchronous π-calculus an output can never be a local cause of any other event, since the output construct has no continuation. Therefore the asynchrony of the asynchronous π-calculus is more liberal than that of our calculus and of session calculi in general, which adopt the definition of asynchrony of standard protocols such as TCP/IP, where the order of messages between any given pair of participants is preserved.

This work builds on the companion paper [14], where synchronous rather than asynchronous communication was considered. In that paper too, networks were interpreted as FESs, and global types, which were the standard ones, were interpreted as PESs. The key result was again an isomorphism between the configuration domain of the FES of a typed network and that of the PES of its global type. Thus, the present paper completes the picture set up in [14] by exploring the “asynchronous side” of the same construction.

An important feature of a denotational model such as Event Structures is abstraction. Clearly, our PES semantics for asynchronous types abstracts away from their syntax, by making explicit the concurrency relation between independent communications that is left implicit in the types: for instance, it maps to the same PES all the types given in Example 3.9 for the characteristic network of Example 2.4. Indeed, it can be shown that all well-formed asynchronous types that type the same network give rise to the same PES. Our FES semantics for networks also abstracts away from their syntax to some extent, via the narrowing operation which prunes off all the input events that are not justified by an output event or by a message in the queue, as well as all their successors. As a consequence, the (non typable) network $p[q?l; r!l'] \parallel r[p?l'] \parallel \emptyset$ is interpreted as the FES with an empty set of events, and so are other deadlocked networks of the same kind.

As future work, we shall try to devise semantic counterparts for our well-formedness conditions on asynchronous types, namely structural conditions characterising both the PESs of well-formed asynchronous types and the FESs of well-typed networks, along the lines of a previous proposal for binary sessions as Linear Logic proofs based on causal nets [69]. This would allow us to reason entirely on the semantic side, and in particular to establish the isomorphism of the configuration domains of a well-typed network FES and the PES of one its types in a more direct way. Such semantic characterisations of well-formedness would also help us to address the following synthesis problem: starting from an arbitrary Prime ES, is it possible (1) to verify that it represents a well-formed asynchronous type, and, if this is the case, (2) to reconstruct a network that behaves according to that asynchronous type? A step in this direction was recently made in [70], in the synchronous setting of [14].

Other possible directions for future work have already been sketched in [14]: they include the investigation of reversibility, which would benefit from previous work on reversible session calculi [71, 72, 73, 74, 75, 76] and Reversible Event Structures [77, 65, 78, 79, 80]. We also plan to investigate the extension of our asynchronous calculus with delegation. In the literature, delegation is usually modelled using the channel passing mechanism of the π-calculus, which requires interleaved sessions. Now, the extension of our event structure semantics to interleaved sessions