Ilaria Castellani
email: ilaria.castellani@inria.fr

Mariangiola Dezani-Ciancaglini

Paola Giannini
email: paola.giannini@uniupo.it

Event Structure Semantics for Multiparty Sessions

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

We propose an interpretation of multiparty sessions as Flow Event Structures, which allows concurrency within sessions to be explicitly represented. We show that this interpretation is equivalent, when the multiparty sessions can be described by global types, to an interpretation of such global types as Prime Event Structures.

Introduction

Session types were proposed in the mid-nineties [START_REF] Takeuchi | An interaction-based language and its typing system[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], as a tool for specifying and analysing web services and communication protocols. They were first introduced in a variant of the π-calculus to describe binary interactions between processes. Such binary interactions may often be viewed as client-server protocols.

Subsequently, session types were extended to multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF], where several participants may interact with each other. A multiparty session is an interaction among peers, and there is no need to distinguish one of the participants as representing the server. All one needs is an abstract specification of the protocol that guides the interaction. This is called the global type of the session. The global type describes the behaviour of the whole session, as opposed to the local types that describe the behaviours of single participants. In a multiparty session, local types may be retrieved as projections from the global type.

Typical safety properties ensured by session types are communication safety (absence of communication errors), session fidelity (agreement with the protocol) and deadlock-freedom [START_REF] Honda | Multiparty asynchronous session types[END_REF]. When dealing with multiparty sessions, the type system is often enhanced so as to guarantee also the liveness property known as progress (no participant gets stuck) [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF].

Some simple examples of sessions not satisfying the above properties are: 1) a sender emitting a message while the receiver expects a different message (communication error); 2) two participants both waiting to receive a message from the other one (deadlock due to a protocol violation); 3) a three-party session where the first participant waits to receive a message from the second participant, which keeps interacting forever with the third participant (starvation).

What makes session types particularly attractive is that they offer several advantages at once: 1) static safety guarantees, 2) automatic check of protocol implementation correctness, based on local types, and 3) a strong connection with linear logics [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Toninho | Dependent session types via intuitionistic linear type theory[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF][START_REF] Caires | Linear logic propositions as session types[END_REF], and with concurrency models such as communicating automata [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF], graphical choreographies [START_REF] Lange | From communicating machines to graphical choreographies[END_REF][START_REF] Tuosto | Semantics of global view of choreographies[END_REF] and message-sequence charts [START_REF] Honda | Multiparty asynchronous session types[END_REF].

In this paper we further investigate the relationship between multiparty session types and concurrency models, by focussing on Event Structures [START_REF] Winskel | An introduction to event structures[END_REF]. We consider a standard multiparty session calculus where sessions are described as networks of sequential processes [START_REF] Dezani-Ciancaglini | Precise subtyping for synchronous multiparty sessions[END_REF]. Each process implements a participant in the session. We propose an interpretation of such networks as Flow Event Structures (FESs) [START_REF] Boudol | Permutation of transitions: an event structure semantics for CCS and SCCS[END_REF][START_REF] Boudol | Flow models of distributed computations: three equivalent semantics for CCS[END_REF] (a subclass of Winskel's Stable Event Structures [START_REF] Winskel | An introduction to event structures[END_REF]), which allows concurrency between session communications to be explicitly represented. We then introduce global types for these networks, and define an interpretation of them as Prime Event Structures (PESs) [START_REF] Winskel | Events in Computation[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF]. Since the syntax of global types does not allow all the concurrency among communications to be expressed, the events of the associated PES need to be defined as equivalence classes of communication sequences up to permutation equivalence. We show that when a network is typable by a global type, the FES semantics of the former is equivalent, in a precise technical sense, to the PES semantics of the latter. To prove this equivalence, we exploit the bisimilarity of their Labelled Transition Systems, as expressed by the Subject Reduction and Session Fidelity theorems (Theorem 6.10 and Theorem 6.11). An alternative approach would have been to compare the two ESs directly, thus conducting the whole reasoning within the denotational model itself. However, while one side of the comparison (mapping the PES of the type to the FES of the network, which can be viewed as a synthesis problem) would be very direct, the other side (reconstructing the PES of the type from the FES of the network) would be more involved, as it would require a structural characterisation of the FESs that represent typable networks, which is far from obvious and therefore is left for future work. This issue will be discussed at length at the end of Section 7.

Event Structures have been used to give semantics to process calculi ever since their introduction at the beginning of the eighties [START_REF] Winskel | Events in Computation[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF] (see Section 9 for an extensive historical discussion). A specific feature of our proposed FES semantics for networks is that we impose strong semantic constraints on the construction of the events themselves (like duality of the histories of their components) in order to reduce the number of events from the very beginning, and to enforce already at the syntactic level some of the expected semantic properties. This allows us to obtain more compact FESs, with fewer events, which is an advantage when displaying their graphical representations 3 , as well as handling examples and carrying out proofs.

In a companion paper [START_REF] Castellani | Global types and event structure semantics for asynchronous multiparty sessions[END_REF], we investigated a similar Event Structure semantics for a session calculus with asynchronous communication, which led to a quite different treatment as it made use of a new notion of asynchronous global type. A detailed comparison with [START_REF] Castellani | Global types and event structure semantics for asynchronous multiparty sessions[END_REF] will be given in Section 9. This paper is an expanded and amended version of [START_REF] Castellani | Event structure semantics for multiparty sessions[END_REF]. The main novelty is that we use a coinductive definition for processes and global types, which simplifies several definitions and proofs, and a more stringent definition for network events. This definition relies on the new notion of causal set, which is crucial for the correctness of our ES semantics. Finally, the present paper includes the proofs of all results, some of which require ingenuity.

The paper is organised as follows. Section 2 introduces our multiparty session calculus. In Section 3 we recall the definitions of PESs and FESs, which will be used to interpret processes (Section 4) and networks (Section 5), respectively. PESs are also used to interpret global types (Section 7), which are defined in Section 6. In Section 8 we prove the equivalence between the FES semantics of a network and the PES semantics of its global type. Section 9 discusses related work and sketches directions for future work.

The proofs of all theorems and propositions are given in the main paper, except for those of Subject Reduction (Theorem 6.10) and Session Fidelity (Theorem 6.11), which are standard and thus deferred to Appendix B. The proofs of lemmas, when not trivial, are collected in Appendices A, B, C, D and E. To help the reader, Appendix F contains a glossary of the symbols used and a table of the notations with their meaning and a reference to where they are defined.

A Core Calculus for Multiparty Sessions

We now formally introduce our calculus, where multiparty sessions are represented as networks of processes. We assume the following base sets: session participants, ranged over by p, q, r, . . . and forming the set Part, and messages, ranged over by λ, λ ′ , . . . and forming the set Msg.

Let π ∈ {p!λ, p?λ | p ∈ Part, λ ∈ Msg} denote an action. The action p!λ represents an output of message λ to participant p, while the action p?λ represents an input of message λ from participant p. The participant of an action, pt(π), is defined by pt(p!λ) = pt(p?λ) = p. Definition 2.1 (Processes). Processes are defined by: P ::= coind i∈I p!λ i ; P i | Σ i∈I p?λ i ; P i | 0 where I is non-empty and λ h λ k for all h, k ∈ I, h k, i.e. messages in choices are all different.

Processes of the shape i∈I p!λ i ; P i and Σ i∈I p?λ i ; P i are called output and input processes, respectively.

other kinds of stable ESs.

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 [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF]. So, when writing processes, we shall use (mutually) recursive equations. When I is a singleton, i∈I p!λ i ; P i will be rendered as p!λ; P and Σ i∈I p?λ i ; P i will be rendered as p?λ; P. When I contains only two elements, as it will be the case in most of our examples, we shall feel free to use the binary choices p!λ 1 ; P 1 ⊕ p!λ 2 ; P 2 and p!λ 1 ; P 1 + p!λ 2 ; P 2 , where the branches p!λ i ; P i should be viewed as being parenthesised (since the connector ; is not an operator of our calculus, but an integral part of the guarded sum operators).

Trailing 0 processes will be omitted.

Processes may be viewed as trees whose internal nodes are decorated by p! or p?, leaves by 0, and edges by messages λ.

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

Definition 2.2 (Networks).

Networks are defined by:

N = p[[ P ]] | p[[ P ]] ∥ N
We assume the standard structural congruence ≡ on networks, stating that parallel composition is associative and commutative and has neutral element p[[ 0 ]] for any fresh p. Given the associativity of ∥, we shall feel free to write networks in We say that a network is unary if it has a unique participant 4 and binary if it has exactly two participants.

the form N = p 1 [[ P 1 ]] ∥ • • • ∥ p n [[ P n ]]
To express the operational semantics of networks, we use an LTS whose labels record the message exchanged during a communication together with its sender and receiver. The set of communications, ranged over by α, α ′ , is defined to be {pqλ | p, q ∈ Part, λ ∈ Msg}, where pqλ represents the transmission of a message λ from participant p to participant q.

p[[ i∈I q!λ i ; The LTS semantics of networks is specified by the unique rule [Com] given in Figure 1. Notice that rule [Com] is symmetric with respect to input and output choices. In a well-typed network (see Section 6) it will always be the case that I ⊆ J, ensuring that participant p can freely choose an output, since participant q offers all corresponding inputs. Note also that a unary network has no transitions.

P i ]] ∥ q[[ Σ j∈J p?λ j ; Q j ]] ∥ N pqλ k ---→ p[[ P k ]] ∥ q[[ Q k ]] ∥ N where k ∈ I∩J [Com]
Note that we could have given first the (standard) LTS semantics for processes, and then derived the LTS for networks from it. However, the syntax of our calculus is so simple that the LTS for networks can be defined directly. Thus we chose to omit the LTS for processes, which would anyway be of no use in the sequel.

In the following we will make an extensive use of finite (and possibly empty) sequences of communications. As usual we define them as traces.

Definition 2.3 (Traces).

(Finite) traces σ ∈ Traces are defined by:

σ ::= ϵ | α • σ
We use |σ| to denote the length of the trace σ.

The set of participants of a trace, notation part(σ), is defined by part(ϵ) = ∅ and

part(pqλ • σ) = {p, q} ∪ part(σ). When σ = α 1 • . . . • α n (n ≥ 1) we write N σ - → N ′ as short for N α 1 -→ N 1 • • • α n --→ N n = N ′ .

Event Structures

We recall now the definitions of Prime Event Structure (PES) from [START_REF] Winskel | Events in Computation[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF] and Flow Event Structure (FES) from [START_REF] Boudol | Permutation of transitions: an event structure semantics for CCS and SCCS[END_REF]. The class of FESs is more general than that of PESs: for a precise comparison of various classes of event structures, we refer the reader to [START_REF] Boudol | Flow models of distributed computations: event structures and nets[END_REF]. As we shall see in Sections 4 and 5, while PESs are sufficient to interpret processes, the greater generality of FESs is needed to interpret networks.

Definition 3.1 (Prime Event Structure).

A prime event structure (PES) is a tuple S = (E, ≤, # ) where:

1. E is a denumerable set of events;

2. ≤ ⊆ (E × E) is a partial order relation, called the causality relation; 1. E is a denumerable set of events; 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. Moreover, 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, ≤, # ) may be regarded as a FES, with ≺ given by < (the strict ordering) or by the covering relation of ≤.

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 X 1 ⊂ X 2 means that S may evolve from X 1 to X 2 .

Definition 3.3 (PES configuration)

. Let S = (E, ≤, # ) be a prime event structure. A configuration of S is a finite subset X of E such that:

1. X is downward-closed: e ′ ≤ e ∈ X ⇒ e ′ ∈ X; 2. X is conflict-free: ∀e, e ′ ∈ X, ¬(e # e ′ ).
The definition of configuration for FESs is slightly more elaborated. For a subset X of E, let ≺ X be the restriction of the flow relation to X and ≺ * X be its transitive and reflexive closure.

Definition 3.4 (FES configuration)

. Let S = (E, ≺, # ) be a flow event structure. A configuration of S is a finite subset X of E such that:

1. X is downward-closed up to conflicts: e ′ ≺ e ∈ X, e ′ X ⇒ ∃ e ′′ ∈ X. e ′ # e ′′ ≺ e;

2. X is conflict-free: ∀e, e ′ ∈ X, ¬(e # e ′ );

3. X has no causality cycles: the relation ≺ * 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 [START_REF] Baldan | Domains and event structures for fusions[END_REF] 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: We recall from [START_REF] Boudol | Flow models of distributed computations: event structures and nets[END_REF] a useful characterisation for configurations of FESs, which is based on the notion of proving sequence, defined as follows:

Definition 3.6 (Proving sequence). Given a flow event structure S = (E, ≺, # ), a proving sequence in S is a sequence e 1 ; • • • ; e n of distinct non-conflicting events (i.e. i j ⇒ e i e j and ¬(e i # e j ) for all i, j) satisfying:

∀i ≤ n ∀e ∈ E : e ≺ e i ⇒ ∃j < i . either e = e j or e # e j ≺ 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 3.7 (Representation of FES configurations as proving sequences [9]).

Given a flow event structure S = (E, ≺, # ), a subset X of E is a configuration of S if and only if it can be enumerated as a proving sequence e To conclude this section, we recall from [START_REF] Castellani | Parallel product of event structures[END_REF] the definition of downward surjectivity (or downward-onto, as it was called there), a property that is required for partial functions between two FESs in order to ensure that they preserve configurations.

We will make use of this property in Section 5.

Definition 3.8 (Downward surjectivity).

Let S i = (E i , ≺ i , # i ), be a flow event structure, i = 0, 1. Let e i , e ′ i range over E i , i = 0, 1. A partial function f : E 0 → * E 1 is downward surjective if it satisfies the condition:

e 1 ≺ 1 f (e 0 ) =⇒ ∃e ′ 0 ∈ E 0 . e 1 = f (e ′ 0 )

Event Structure Semantics of Processes

In this section, we define an event structure semantics for processes, and show that the obtained event structures are PESs. This semantics will be the basis for defining the ES semantics for networks in Section 5. We start by introducing process events, which are non-empty sequences of actions.

Definition 4.1 (Process event)

. Process events η, η ′ , also called p-events, are defined by: η

::= π | π • η π ∈ {p!λ, p?λ | p ∈ Part, λ ∈ Msg}
We denote by PE the set of p-events, and by |η| the length of the sequence of actions in the p-event η.

Let ζ denote a (possibly empty) sequence of actions, and ⊑ denote the prefix ordering on such sequences. Each p-event η may be written either in the form

η = π • ζ or in the form η = ζ • π.
We shall feel free to use any of these forms. When a p-event is written as η = ζ • π, then ζ may be viewed as the causal history of η, namely the sequence of past actions that must have happened in the process for the last action π to be able to happen.

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

act(ζ • π) = π
Definition 4.2 (Causality and conflict relations on process events). The causality relation ≤ and the conflict relation # on the set of p-events PE are defined by:

1. η ⊑ η ′ ⇒ η ≤ η ′ ; 2. π π ′ ⇒ ζ • π • ζ ′ # ζ • π ′ • ζ ′′ .
Definition 4.3 (Event structure of a process). The event structure of process P is the triple S P (P) = (PE(P), ≤ P , # P )

where:

1. PE(P) ⊆ PE is the set of non-empty sequences of labels along the nodes and edges of a path from the root to an edge in the tree of P;

2. ≤ P is the restriction of ≤ to the set PE(P);

3. # P is the restriction of # to the set PE(P).

It is easy to see that # P = (PE(P) × PE(P)) \ (≤ P ∪ ≥ P ). In the following we shall feel free to drop the subscript in ≤ P and # P .

Note that the set PE(P) may be denumerable, as shown by the following example.

Example 4.4. If P = q!λ; P ⊕ q!λ ′ , then

PE(P) = {q!λ • . . . • q!λ n | n ≥ 1} ∪ {q!λ • . . . • q!λ n •q!λ ′ | n ≥ 0}
Theorem 4.5. Let P be a process. Then S P (P) is a prime event structure.

Proof We show that ≤ and # satisfy Properties 2 and 3 of Definition 3.1. Reflexivity, transitivity and antisymmetry of ≤ follow from the corresponding properties of ⊑.

As for irreflexivity and symmetry of # , they follow from Clause 2 of Definition

ζ ′′ such that π π ′ and η = ζ • π • ζ ′ and η ′ = ζ • π ′ • ζ ′′ . From η ′ ≤ η ′′ we derive that η ′′ = ζ • π ′ • ζ ′′ • ζ 1 for some ζ 1 .
Therefore η # η ′′ , again from Clause 2.

Event Structure Semantics of Networks

In this section we define the ES semantics of networks and show that the resulting ESs, which we call network ESs, are FESs. We also show that when the network is binary, then the obtained FES is a PES. The formal treatment involves defining the set of potential events of network ESs, which we call network events, as well as introducing the notion of causal set of a network event and the notion of narrowing of a set of network events. This will be the subject of Section 5.1.

In Section 5.2, we first prove some properties of the conflict relation in network

ESs. Then, we come back to causal sets and we show that they are always finite and that each configuration includes a unique causal set for each of its network events.

We also discuss the relationship between causal sets and prime configurations, which are specific configurations that are in 1-1 correspondence with network events in ESs. Finally, we define a notion of projection of network events on participants, yielding p-events, and prove that this projection (extended to sets of network events) is downward surjective and preserves configurations.

The proofs omitted in this section can be found in Appendix A.

Definitions and Main Properties

We start by defining network events, the potential events of network ESs. Since these events represent communications between two network participants p and q, they should be pairs of dual p-events, namely, of p-events emanating respectively from p and q, which have both dual actions and dual causal histories.

Formally, to define network events we need to specify the location of p-events, namely the participant to which they belong: Definition 5.1 (Located event). We call located event a p-event η pertaining to a participant p, written p :: η.

As hinted above, network events should be pairs of dual located events p :: ζ • π and q :: ζ ′ • π ′ with matching actions π and π ′ and matching histories ζ and ζ ′ .

To formalise the matching condition, we first define the projections of p-events on participants, which yield sequences of undirected actions of the form !λ and ?λ, or the empty sequence ϵ. Then we introduce a notion of duality between located events, based on a notion of duality between undirected actions.

Let ϑ range over !λ and ?λ, and Θ range over (possibly empty) sequences of ϑ's.

Definition 5.2 (Projection of p-events on participants).

The projection of a p-event η on a participant p, written η ↱ p , is defined by:

q!λ ↱ p =        !λ if p = q ϵ otherwise q?λ ↱ p =        ?λ if p = q ϵ otherwise (π • η) ↱ p = π ↱ p • η ↱ p
ϵ ϵ Θ Θ ′ ⇒ !λ • Θ ?λ • Θ ′
Definition 5.4 (Duality of located events). Two located events p :: η, q :: η ′ are dual, written p :: η q :: η ′ , if η ↱ q η ′ ↱ p and pt(act(η)) = q and pt(act(η ′ )) = p.

Dual located events may be sequences of actions of different length. For instance p :: q!λ • r!λ ′ r :: p?λ ′ and p :: q!λ q :: r!λ ′ • p?λ.

Definition 5.5 (Network event). Network events ν, ν ′ , also called n-events, are unordered pairs of dual located events, namely:

ν ::= {p :: η, q :: η ′ } where p :: η q :: η ′

We denote by NE the set of n-events.

We define the communication of the event ν, notation cm(ν), by cm(ν) = pqλ if ν = {p :: ζ • q!λ, q :: ζ ′ • p?λ} and we say that the n-event ν represents the communication pqλ. We also define the set of locations of an n-event to be loc({p :: η, q :: η ′ }) = {p, q}.

It is handy to have a notion of occurrence of a located event in a set of network events:

Definition 5.6. A located event p :: η occurs in a set E of n-events, notation p :: η ∈∈ E, if p :: η ∈ ν and ν ∈ E for some ν.

We define now the flow and conflict relations on network events. While the flow relation is the expected one (a network event inherits the causality from its constituent processes), the conflict relation is more subtle, as it can arise also between network events with disjoint sets of locations.

In the following definition we use |Θ| to denote the length of the sequence Θ.

Definition 5.7 (Flow and conflict relations on n-events).

The flow relation ≺ and the conflict relation # on the set of n-events NE are defined by:

1. ν ≺ ν ′ if p :: η ∈ ν & p :: η ′ ∈ ν ′ & η < η ′ ; 2. ν # ν ′ if (a) either p :: η ∈ ν & p :: η ′ ∈ ν ′ & η # η ′ ; (b) or p :: η ∈ ν & q :: η ′ ∈ ν ′ & p q & |η ↱ q | = |η ′ ↱ p | & ¬(η ↱ q η ′ ↱ p ).
Two n-events are in conflict if they share a participant with conflicting p-events (Clause (2a)) or if some of their participants have communicated with each other in the past in incompatible ways (Clause (2b)), as illustrated by the n-events ν and ν ′ in Example 5.8 (Point 3). Observe that in Clause (2b) the condition |η

↱ q | = |η ′ ↱ p |
is needed if we want to check duality of the two projections. Without this condition we could get unwanted conflicts, for instance between ν = {p :: q!λ, q :: p?λ} and ν ′ = {p :: q!λ • q!λ ′ , q :: p?λ • p?λ ′ }. Removing this condition and checking duality only up to the length of the shortest projection would yield more conflicting events, as discussed in Example 5.8 (Point 3). Note also that the two clauses (2a) and (2b)

are not exclusive, as shown in Example 5.8 (Point 4).

Example 5.8. This example illustrates the use of Definition 5.7 in various cases. It also shows that the flow and conflict relations may be overlapping on n-events.

1. Let ν = {p :: q!λ 1 • r!λ, r :: p?λ} and ν ′ = {p :: q!λ 2 , q :: p?λ 2 }. Then ν # ν ′ by Clause (2a) since q!λ 1 • r!λ # q!λ 2 . Note that ν # ν ′ can be also deduced by Clause (2b), since

(q!λ 1 • r!λ) ↱ q = !λ 1 and p?λ 2 ↱ p = ?λ 2 and |!λ 1 | = |?λ 2 | and ¬(!λ 1 ?λ 2 ).
2. Let ν be as in (1) and ν ′ = {p :: q!λ 2 • q!λ, q :: p?λ 2 • p?λ}. Again, we can deduce ν # ν ′ using Clause (2a), since q!λ 1 • r!λ # q!λ 2 • q!λ. On the other hand, Clause (2b)

does not apply in this case, since (q!λ 1 • r!λ) ↱ q = !λ 1 and (p?λ 2 • p?λ) ↱ p = ?λ 2 •?λ

and thus |!λ 1 | |?λ 2 •?λ|.
3. Let ν be as in (1) and ν ′ = {q :: p?λ 2 • s!λ, s :: q?λ}. Here loc(ν) ∩ loc(ν ′ ) = ∅, so clearly Clause (2a) does not apply. On the other hand, ν # ν ′ can be deduced by

Clause (2b), since (q!λ 1 • r!λ) ↱ q = !λ 1 and (p?λ 2 • s!λ) ↱ p = ?λ 2 and |!λ 1 | = |?λ 2 |
and ¬(!λ 1 ?λ 2 ). Consider now ν ′′ = {q :: p?λ 2 • p?λ ′ • s!λ, s :: q?λ}. Then we cannot deduce ν # ν ′′ in the same way because the two projections do not have the same length. However, we can deduce ν # ν ′′′ ≺ ν ′′ , where ν ′′′ = {p :: q!λ 2 , q :: p?λ 2 }.

In other words, ν and ν ′′ are in semantic conflict, as Proposition 5.22 shows, but not in the syntactic conflict # (the fact that semantic conflict is in general larger than syntactic conflict is common to all classes of ESs except PESs). We could have chosen to make the syntactic conflict larger by replacing Clause (2b) by the following alternative clause, where Θ, Θ ′ are as in Definition 5.3 and ⊑ is the prefix ordering:

Clause (2b') or p :: η ∈ ν & q :: η ′ ∈ ν ′ & p q & (∃ Θ ⊑ η ↱ q , ∃ Θ ′ ⊑ η ′ ↱ p . |Θ| = |Θ ′ | & ¬(Θ Θ ′ ))
With this alternative clause, we could deduce the syntactic conflict ν # ν ′′ . However, in Definition 5.7 we chose to keep our definition of # stricter in order to have fewer syntactic conflicts to handle in examples and proofs.

4. Let ν be as in (1) and ν ′ = {p :: q!λ 2 • r!λ • r!λ ′ , r :: p?λ • p?λ ′ }. In this case we have both ν ≺ ν ′ by Clause (1) and ν # ν ′ by Clause (2a), namely, causality is inherited from participant r and conflict from participant p.

We introduce now the notion of causal set of an n-event ν in a given set of events

Ev. Intuitively, a causal set of ν in Ev is a complete set of non-conflicting direct causes of ν which is included in Ev.

Definition 5.9 (Causal set)

. Let ν ∈ Ev ⊆ NE. A set of n-events E is a causal set of ν in Ev if E is a minimal subset of Ev such that 1. E ∪ {ν} is conflict-free and 2. p :: η ∈ ν and η ′ < η imply p :: η ′ ∈∈ E.
Note that in the above definition, the conjunction of minimality and Clause [START_REF] Baier | The connection between an event structure semantics and an operational semantics for TCSP[END_REF] implies that, if ν ′ ∈ E, then ν ′ ≺ ν. Thus E is a set of direct causes of ν. Moreover, a causal set of an n-event cannot be included in another causal set of the same nevent, as this would contradict the minimality of the larger set. Hence, Definition 5.9

indeed formalises the idea that causal sets should be complete sets of compatible direct causes of a given n-event.

Example 5.10. Let ν 1 = {p :: q!λ 1 • r!λ, r :: p?λ} and ν 2 = {p :: q!λ 2 • r!λ, r :: p?λ}. Then both {ν 1 } and {ν 2 } are causal sets of ν = {r :: p?λ • s!λ ′ , s :: r?λ ′ } in Ev = {ν 1 , ν 2 , ν}. Note that ν 1 # ν 2 and that neither ν 1 nor ν 2 has a causal set in Ev.

Let us now consider also ν ′ 1 = {p :: q!λ 1 , q :: p?λ 1 } and ν ′ 2 = {p :: q!λ 2 , q :: p?λ 2 }.

Then ν still has the same causal sets {ν 1 } and

{ν 2 } in Ev ′ = {ν ′ 1 , ν ′ 2 , ν 1 , ν 2 , ν}, while each ν i , i = 1, 2, has the unique causal set {ν ′ i } in Ev ′ , and each ν ′ i , i = 1, 2, has the empty causal set in Ev ′ .
Finally, ν has infinitely many causal sets in NE. For instance, if for every natural number n we let ν n = {p :: q!λ n • r!λ, r :: p?λ}, then each {ν n } is a causal set of ν in NE. Symmetrically, a causal set may cause infinitely many events in NE. For instance, the above causal sets {ν 1 } and {ν 2 } of ν could also act as causal sets for any n-event ν ′′ n = {r :: p?λ • s!λ n , s :: r?λ n } or, assuming the set of participants to be denumerable, for

any event ν ′′′ n = {r :: p?λ • s n !λ ′ , s n :: r?λ ′ }.
When defining the set of events of a network ES, we want to prune out all the n-events that do not have a causal set in the set itself. The reason is that such n-events should not happen in the event structure of a network, although, when projected on their locations (see Definition 5.25), they would always give rise to p-events occurring in a configuration 5 . Example 5.14 should further clarify this point. This pruning is achieved by means of the following narrowing function.

Definition 5.11 (Narrowing of a set of n-events).

The narrowing of a set E of n-events, denoted by n(E), is the greatest fixpoint of the function f E on sets of n-events defined by:

f E (X) = {ν ∈ E | ∃E ′ ⊆ X. E ′ is a causal set of ν in X }
Note that we could not have taken n(E) to be the least fixpoint of f E rather than its greatest fixpoint. Indeed, the least fixpoint of f E would be the empty set.

Example 5.12. The following two examples illustrate the notions of causal set and narrowing. Let

ν 1 = {r :: s?λ 1 , s :: r!λ 1 } ν 2 = {r :: s?λ 2 , s :: r!λ 2 } ν 3 = {p :: r?λ 1 , r :: s?λ 1 • p!λ 1 } ν 4 = {q :: s?λ 2 , s :: r!λ 2 • q!λ 2 } ν 5 = {p :: r?λ 1 • q!λ, q :: s?λ 2 • p?λ}
Then n({ν 1 , . . . , ν 5 }) = {ν 1 , . . . , ν 4 }, because a causal set for ν 5 would need to contain both ν 3 and ν 4 , but this is not possible, since ν 3 # ν 4 by Clause (2b) of Definition 5.7. In fact

(s?λ 1 • p!λ 1 ) ↱ s = ?λ 1 and (r!λ 2 • q!λ 2 ) ↱ r = !λ 2 and |?λ 1 | = |!λ 2 | and ¬(?λ 1 !λ 2 ). Let ν 1 = {r :: s?λ 1 , s :: r!λ 1 } ν 2 = {r :: s?λ 2 , s :: r!λ 2 } ν 3 = {p :: r?λ 1 , r :: s?λ 1 • p!λ 1 } ν 4 = {p :: r?λ 1 • s?λ 2 , s :: r!λ 2 • p!λ 2 } ν 5 = {p :: r?λ 1 • s?λ 2 • q!λ, q :: p?λ}
Here n({ν 1 , . . . , ν 5 }) = {ν 1 , ν 2 , ν 3 }. Indeed, a causal set for ν 4 would need to contain both ν 2 and ν 3 , but this is not possible, since ν 2 # ν 3 by Clause (2a) of Definition 5.7. In fact s?λ 2 # s?λ 1 • p!λ 1 . Then, ν 5 will also be pruned by the narrowing, since any causal set for ν 5 should contain ν 4 .

We can now finally define the event structure associated with a network. The intuition is that the events appearing in some configuration of the event structure should correspond exactly to the transitions executable in some state of the network.

Definition 5.13 (Event structure of a network).

The event structure of network N is the triple

S N (N) = (NE(N), ≺ N , # N )
where:

1. NE(N) = n(CE(N)) with CE(N) = {{p :: η, q :: η ′ } | p[[ P ]]∈N, q[[ Q ]]∈N, η∈PE(P), η ′ ∈PE(Q), p :: η q :: η ′ } 2. ≺ N is the restriction of ≺ to the set NE(N); 3. # N is the restriction of # to the set NE(N).
The set of n-events of the ES associated with a network N is the narrowing of its set of candidate n-events, CE(N), which contains all pairs of dual located events that may be constructed from two different components of N. We give now a simple example that justifies the use of the narrowing function for building the set of events of a network ES.

Example 5.14.

Let N = p[[ q?λ • r!λ ′ ]] ∥ r[[ p?λ ′ ]]. Then CE(N) contains the unique n-event ν = {p :: q?λ • r!λ ′ ,
p?λ; Q + p?λ ′ and N = p[[ P ]] ∥ q[[ Q ]]. Then NE(N) = {{p :: q!λ • . . . • q!λ n , q :: p?λ • . . . • p?λ n } | n ≥ 1} ∪ {{p :: q!λ • . . . • q!λ n •q!λ ′ , q :: p?λ • . . . • p?λ n •p?λ ′ } | n ≥ 0}
A simple variation of this example shows that even within the events of a network ES, an n-event ν may have an infinite number of causal sets. Let ν = {r :: p?λ • s!λ ′ , s :: r?λ ′ } be as in Example 5.10. Consider the network

N ′ = p[[ P ′ ]] ∥ q[[ Q ]] ∥ r[[ R ]] ∥ s[[ S ]]
, where P ′ = q!λ; P ′ ⊕ q!λ ′ ; r!λ, Q is as above, R = p?λ; s!λ ′ and S = r?λ ′ . Then ν has an infinite number of causal sets E n = {ν n } in NE(N ′ ), where

ν n = {p :: q!λ • . . . • q!λ n • q!λ ′ • r!λ, r :: p?λ}
On the other hand, a causal set may only cause a finite number of events in a network ES, since the number of branches in any choice is finite, as well as the number of participants in the network.

Theorem 5.16. Let N be a network. Then S N (N) is a flow event structure with an irreflexive conflict relation.

Proof

The relation ≺ N is irreflexive since η < η ′ implies ν ν ′ , where η, η ′ , ν, ν ′ are as in Definition 5.7 (1). As for the conflict relation, note first that a conflict between an n-event and itself could not be derived by Clause (2b) of Definition 5.7, since the two located events of an n-event are dual by construction. Lastly, symmetry and irreflexivity of the conflict relation follow from the corresponding properties of conflict between p-events.

The fact that the conflict relation is irreflexive in our network FESs means that we do not exploit the possibility of self-conflicts offered by general FESs. This is due to the way we defined the set of events of our network FESs, using the narrowing function as discussed previously. We could have chosen an alternative definition, introducing additional self-conflicting events of a more liberal form 6 which would have disappeared when building configurations (together with their successors having no other possible causes), as it was done for CCS in [START_REF] Boudol | Flow models of distributed computations: three equivalent semantics for CCS[END_REF]. However, this would have resulted in much larger sets of events for network FESs, leading to more cumbersome examples and proofs. Our design choice here was to reduce the set of events of network FESs by introducing already some semantic constraints on their events (like duality and the existence of causal sets). It should be stressed, however, that the narrowing function does not exclude all non executable events, as shown by the FES in Example 5.20, which has three events, each of which has a causal set but none of which is executable.

Although they have an irreflexive conflict relation like PESs, our network FESs exhibit two important features which are not shared by PESs, namely non-hereditary conflict (as shown by the FES given in Figure 5, where the two conflicting events ν ′ 1 and ν ′ 2 have a common successor ν) and causality cycles (as shown by the FES in Example 5.20, where there is a circular dependency among the three events ν 1 , ν 2 and ν 3 ).

Note that n-events with disjoint sets of locations may be related by the transitive closure of the flow relation, as illustrated by the next example, which also shows how n-events inherit the flow relation from the causality relation of their p-events.

Example 5.17. Let N be the network

p[[ q!λ 1 ]] ∥ q[[ p?λ 1 ; r!λ 2 ]] ∥ r[[ q?λ 2 ; s!λ 3 ]] ∥ s[[ r?λ 3 ]]
Then S N (N) has three network events ν 1 ={p :: q!λ 1 , q :: p?λ 1 } ν 2 ={q :: p?λ 1 • r!λ 2 , r :: q?λ 2 } ν 3 ={r :: q?λ 2 • s!λ 3 , s :: r?λ 3 }

The flow relation obtained by Definition 5.13 is: ν 1 ≺ ν 2 and ν 2 ≺ ν 3 . These two flows are inherited from the causality relations within the process ESs associated with participants q and r, respectively. The non-empty configurations are {ν 1 }, {ν 1 , ν 2 } and {ν 1 , ν 2 , ν 3 }. Note that S N (N) has only one proving sequence per configuration (which is the one given by the numbering of events).

Clearly, if a network is unary, then the set of events of its FES is empty. If a network is binary, then its FES may be turned into a PES by replacing ≺ with its reflexive and transitive closure ≺ * . To prove this result, we first show a property of n-events of binary networks. We say that an n-event ν is binary if the participants occurring in the p-events of ν are contained in loc(ν).

Lemma 5.18. Let ν and ν ′ be binary n-events with loc(ν) = loc(ν ′ ). Then ν # ν ′ iff p :: η ∈ ν and p ::

η ′ ∈ ν ′ imply η # η ′ . Proposition 5.19. Let N = p 1 [[ P 1 ]] ∥ p 2 [[ P 2 ]] and S N (N) = (NE(N), ≺ N , # ). Then n(CE(N)) = CE(N) and the structure S N * (N)= def (NE(N), ≺ * N , # ) is a prime event structure.
Proof We first show that n(CE(N)) = CE(N). By Definition 5.13( 1)

CE(N) = {{p 1 :: η 1 , p 2 :: η 2 } | η 1 ∈ PE(P 1 ), η 2 ∈ PE(P 2 ), p 1 :: η 1 p 2 :: η 2 }
Let {p 1 :: η 1 , p 2 :: η 2 } ∈ CE(N). Since p 1 :: η 1 p 2 :: η 2 and all the actions in η 1 involve p 2 and all the actions in η 2 involve p 1 , we know that η 1 and η 2 have the same length n ≥ 1 and for each i, 1 ≤ i ≤ n, the prefixes of length i of η 1 and η 2 , written η i 1 and η i 2 , must themselves be dual. Then {p 1 ::

η i 1 , p 2 :: η i 2 } ∈ CE(N) for each i, 1 ≤ i ≤ n, hence {p 1 :: η 1 , p 2 :: η 2 } has a causal set in CE(N).
We prove now that the reflexive and transitive closure ≺ * N of ≺ N is a partial order.

Since by definition ≺ * N is a preorder, we only need to show that it is antisymmetric.

Define the length of an n-event ν = {p 1 :: η 1 , p 2 ::

η 2 } to be length(ν)= def | η 1 | + | η 2 | (where | η | is the length of η). Let now ν, ν ′ ∈ NE(N), with ν = {p 1 :: η 1 , p 2 :: η 2 } and ν ′ = {p 1 :: η ′ 1 , p 2 :: η ′ 2 }. By definition ν ≺ N ν ′ implies η i < η ′ i for some i = 1, 2, which in turn implies | η i | < | η ′ i | .
As observed above, η 1 and η 2 must have the same length, and so must η ′ 1 and

η ′ 2 . This means that if ν ≺ N ν ′ then length(ν) = | η 1 | + | η 2 | < | η ′ 1 | + | η ′ 2 | = length(ν ′ ). From this we can conclude that if ν ≺ * N ν ′ and ν ′ ≺ * N ν, then necessarily ν = ν ′ .
Finally we show that the relation # satisfies the required properties. By Theorem 5.16 we only need to prove that # is hereditary. Let ν and ν ′ be as above. If

ν # ν ′ , then by Lemma 5.18 η 1 # η ′ 1 and η 2 # η ′ 2 . Let now ν ′′ = {p 1 :: η ′′ 1 , p 2 :: η ′′ 2 }. If ν ′ ≺ * N ν ′′ , this means that there exist ν 1 , . . . , ν n such that ν ′ ≺ N ν 1 . . . ≺ N ν n = ν ′′ . We
prove by induction on n that ν # ν ′′ . For n = 1 we have ν ′ ≺ N ν ′′ . Then by Clause

(1) of Definition 5.13 we have η ′ j < η ′′ j for some j ∈ {1, 2}. Since

η i # η ′ i for all i ∈ {1, 2}
and # is hereditary on p-events, we deduce η j # η ′′ j , which implies ν # ν ′′ . Suppose now n > 1. By induction ν # ν n-1 . Since ν n-1 ≺ N ν n = ν ′′ we then obtain ν # ν ′′ by the same argument as in the base case.

If a network has more than two participants, then the duality requirement on its n-events is not sufficient to ensure the absence of circular dependencies 7 . For instance, in the following ternary network (which may be viewed as representing the 3-philosopher deadlock) the relation ≺ * is not a partial order.

Example 5.20. Let N be the network

p[[ r?λ; q!λ ′ ]] ∥ q[[ p?λ ′ ; r!λ ′′ ]] ∥ r[[ q?λ ′′ ; p!λ ]]
Then S N (N) has three n-events ν 1 = {p :: r?λ, r :: q?λ ′′ • p!λ} ν 2 = {p :: r?λ • q!λ ′ , q :: p?λ ′ } ν 3 = {q :: p?λ ′ • r!λ ′′ , r :: q?λ ′′ } By Definition 5.13 (1) we have

ν 1 ≺ ν 2 ≺ ν 3 and ν 3 ≺ ν 1 . The only configuration of S N (N)
is the empty configuration, because the only set of n-events that satisfies downward-closure up to conflicts is X = {ν 1 , ν 2 , ν 3 }, but this is not a configuration because ≺ * X is not a partial order (recall that ≺ X is the restriction of ≺ to X) and hence the condition (3) of Definition 3.4

is not satisfied.

Further Properties

In this subsection, we first prove two properties of the conflict relation in network

ESs: non disjoint n-events are always in conflict, and conflict induced by Clause (2b) of Definition 5.7 is semantically inherited. We then discuss the relationship between causal sets and prime configurations and prove two further properties of causal sets, which are shared with prime configurations8 : finiteness, and the existence of a causal set for each event in a configuration. Finally, observing that the FES of a network may be viewed as the product of the PESs of its processes, we proceed to prove a classical property for ES products, namely that their projections on their components preserve configurations. To this end, we define a projection function from n-events to participants, yielding p-events, and we show that configurations of a network ES project down to configurations of the PESs of its processes.

Let us start with the conflict properties. By definition, two n-events intersect each other if and only if they share a located event p :: η. Otherwise, the two n-events are disjoint. Note that if p ::

η ∈ (ν ∩ ν ′ ), then loc(ν) = loc(ν ′ ) = {p, q},
where q = pt(act(η)). The next proposition establishes that two distinct intersecting n-events in NE are in conflict.

Lemma 5.21 (Sharing of located events implies conflict

). If ν, ν ′ ∈ NE and ν ν ′ and (ν ∩ ν ′ ) ∅, then ν # ν ′ .
Although conflict is not hereditary in FESs, we prove that a conflict due to incompatible mutual projections (i.e., a conflict derived by Clause (2b) of Definition 5.7) is semantically inherited. Let ϑ ↘ n denote the prefix of length n of ϑ.

Proposition 5.22 (Semantic conflict hereditariness). Let p :: η ∈ ν and q ::

η ′ ∈ ν ′ with p q. Let n = min{|η ↱ q |, |η ′ ↱ p |}. If ¬((η ↱ q ) ↘ n (η ′ ↱ p ) ↘ n), then there exists no configuration X such that ν, ν ′ ∈ X.
Proof Suppose ad absurdum that X is a configuration such that ν, ν ′ ∈ X. there exists a non-empty causal set E ν of ν such that E ν ⊆ X. Let η 0 < η be such that

If | η ↱ q | = | η ′ ↱ p | then ν # ν ′ by
| η 0 ↱ q | = | η ′ ↱ p | = n.
By definition of causal set, there exists ν 0 ∈ E ν such that p :: η 0 ∈ ν 0 . By Definition 5.7(2b) we have then ν 0 # ν ′ , contradicting the fact that X is conflict-free.

We prove now two further properties of causal sets. For the reader familiar with

ESs, the notion of causal set may be reminiscent of that of prime configuration [START_REF] Winskel | Events in Computation[END_REF],

which similarly consists of a complete set of causes for a given event 9 . However, there are some important differences: the first is that a causal set does not include the event it causes, unlike a prime configuration. The second is that a causal set only contains direct causes of an event, and thus it is not downward-closed up to conflicts, as opposed to a prime configuration. The last difference is that, while a prime configuration uniquely identifies its caused event, a causal set may cause different events, as shown in Example 5.10.

A common feature of prime configurations and causal sets is that they are both finite. For causal sets, this is implied by minimality together with Clause (2) of Definition 5.9, as shown by the following proposition.

Proposition 5.23. Let ν ∈ Ev ⊆ NE. If E is a causal set of ν in Ev, then E is finite.
Proof Suppose ν = {p :: η, q :: η ′ }. We show that

| E | ≤ | η | + | η ′ | -2,
where

| E | is the cardinality of E.
By Condition (2) of Definition 5.9, for each η 0 < η and η ′ 0 < η ′ there must be ν 0 , ν ′ 0 ∈ E such that p :: η 0 ∈ ν 0 and q :: η ′ 0 ∈ ν ′ 0 . Note that ν 0 and ν ′ 0 could possibly coincide. Moreover, there cannot be ν ′ ∈ E such that p :: η 0 ∈ ν ′ ν 0 or q :: η ′ 0 ∈ ν ′ ν ′ 0 , since this would contradict the minimality of E (and also its conflict-freeness, since by Lemma 5.21 we would have either ν ′ # ν 0 or

ν ′ # ν ′ 0 )
. Hence the number of events in E is at most (|η| -1) + (|η ′ | -1).

A key property of causal sets, which is again shared with prime configurations, is that each configuration includes a unique causal set for each n-event in the configuration.

Lemma 5.24. If X is a configuration of S N (N) and ν ∈ X, then there is a unique causal set E of ν such that E ⊆ X.

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 on participants, which yields p-events, and showing that it is downward surjective.

Definition 5.25 (Projection of n-events on participants)

.

pro j p (ν) =        η if p :: η ∈ ν, unde f ined otherwise.
The projection function pro j p (•) is extended to sets of n-events in the obvious way: pro j p (X) = {η | ∃ν ∈ X . pro j p (ν) = η} Example 5.26. Let {ν 1 , ν 2 , ν 3 } be the configuration defined in Example 5.17. We get

pro j q ({ν 1 , ν 2 , ν 3 }) = {p?λ 1 , p?λ 1 • r!λ 2 }
Example 5.27. Let N and ν be as in Example 5.14. As observed there, if we did not apply narrowing the set of events of S N (N) would be the singleton {ν}, which would also be a configuration of S N (N). However, pro j p (ν) = {q?λ • r!λ ′ } would not be a configuration in S P (P), since it would contain the event q?λ • r!λ ′ without its cause q?λ.

Narrowing ensures that each projection of the set of n-events of a network FES on one of its participants is downward surjective (according to Definition 3.8).

Proposition 5.28 (Downward surjectivity of projections).

Let S N (N) = (NE(N), ≺ N , # N ) and S P (P) = (PE(P), ≤ P , # P ) and p[[ P ]] ∈ N. Then the partial function pro j p : NE(N) ⇀ PE(P) is downward surjective.

Proof As mentioned already in Section 3, any PES S = (E, ≤, # ) may be viewed as a FES, with ≺ given by < (the strict ordering underlying ≤). Let η ∈ PE(P) and ν ∈ NE(N). Then the property we need to show is:

η < P pro j p (ν) =⇒ ∃ν ′ ∈ NE(N) . η = pro j p (ν ′ ) Note that η < P pro j p (ν) implies pro j p (ν) = η • η ′ for some η ′ . Recall that NE(N) = n(CE(N)),

Theorem 5.29 (Projection of n-events preserves configurations). If p[[

P ]] ∈ N, then X ∈ C(S N (N)) implies pro j p (X) ∈ C(S P (P)).
Proof Clearly, pro j p (X) is conflict-free. We show that it is also downward-closed.

If ν ∈ X, by Lemma 5.24 there is a causal set E of ν such that E ⊆ X. If p :: η ∈ ν and η ′ < η, by Definition 5.9 there is ν ′ ∈ E such that p :: η ′ ∈ ν ′ . We conclude that ν ′ ∈ X, and therefore η ′ ∈ pro j p (X).

Notice that the reverse of Theorem 5.29 is not true, namely p[[ P ]] ∈ N does not imply that each configuration of C(S P (P)) can be obtained by projecting some configuration of C(S N (N)) on p. Consider for instance the network N = p[[ q?λ ]].

Then {q?λ} ∈ C(S P (P)), while C(S N (N)) = ∅.

The reader may wonder why our ES semantics for sessions is not cast in categorical terms, like classical ES semantics for process calculi [START_REF] Winskel | Events in Computation[END_REF][START_REF] Castellani | Parallel product of event structures[END_REF], where process constructions arise as categorical constructions (e.g., parallel composition arises as a categorical product). In fact, a categorical formulation of our semantics would not be possible, due to our two-level syntax for processes and networks, which does not allow networks to be further composed in parallel. However, it should be clear that our construction of a network FES from the process PESs of its components is a form of parallel composition, and the properties expressed by Proposition 5.28 and Theorem 5.29 give some evidence that this construction satisfies the conditions usually required for a categorical product of ESs.

Global Types

This section is devoted to our type system for multiparty sessions. Global types describe the communication protocols involving all session participants. Usually, global types are projected into local types and typing rules are used to derive local types for processes [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]. The simplicity of our calculus allows us to project directly global types into processes and to have exactly one typing rule, see Figures 2 and3. This section is split in two subsections.

The first subsection presents the projection of global types onto processes, together with the proof of its soundness. Moreover it introduces a boundedness condition on global types, which is crucial for our type system to ensure progress.

The second subsection presents the type system, as well as an LTS for global types.

Lastly, the properties of Subject Reduction, Session Fidelity and Progress are shown.

The omitted proofs can be found in Appendix B.

Well-formed Global Types

Global types are built from choices among communications. Definition 6.1 (Global types). Global types G are defined by:

G ::= coind p → q : ⊞ i∈I λ i ; G i | End
where I is not empty, λ h λ k for all h, k ∈ I, h k, i.e. messages in choices are all different.

As for processes, ::= coind indicates that global types are defined coinductively.

Again, we focus on regular terms. Since also processes are defined coinductively this allows for a simpler definition of projection, see Figure 2.

The type p → q : ⊞ i∈I λ i ; G i formalises a protocol which starts with the communication of a message λ k from p to q, for some k ∈ I, and then, depending on which λ k was chosen by p, continues as G k .

When I is a singleton, a choice p → q : ⊞ i∈I λ i ; G i will be rendered simply as p λ → q ; G. When I contains only two elements, as for processes we will use the binary choice notation p → q : (λ 1 ; G 1 ⊞ λ 2 ; G 2 ). Trailing End types will be omitted.

G ↾ r = 0 if r part(G) (p → q : ⊞ i∈I λ i ; G i ) ↾ r =                  Σ i∈I p?λ i ; G i ↾ r if r = q, i∈I q!λ i ; G i ↾ r if r = p, G 1 ↾ r if r {p, q} and r ∈ part(G 1 )
and The set of participants of a global type G, part(G), is defined to be the union of the sets of participants of all its traces, namely

G i ↾ r = G 1 ↾ r for all i ∈ I
part(G) = σ∈Tr + (G) part(σ)
Note that the regularity assumption ensures that the set of participants is finite.

The projection of a global type onto participants is given in Figure 2. As usual, projection is defined only when it is defined on all participants. Because of the simplicity of our calculus, the projection of a global type, when defined, is simply a process. The definition is coinductive, so a global type with an infinite (regular) tree produces a process with a regular tree. The projection of a choice type on the sender produces an output process, i.e. a process sending one of its possible messages to the receiver and then acting according to the projection of the corresponding branch.

Similarly for the projection on the receiver, which produces an input process.

Projection of a choice type on the other participants is defined only if it produces the same process for all the branches of the choice. This is a standard condition for multiparty session types [START_REF] Honda | Multiparty asynchronous session types[END_REF].

Our coinductive definition of global types is more permissive than that based on the standard µ-notation used in [START_REF] Honda | Multiparty asynchronous session types[END_REF], because it allows more global types to be projected, as shown by the following example.

Example 6.2. The global type G = p → q : (λ 1 ; q λ 3 → r ⊞ λ 2 ; G) is projectable and

• G ↾ p = P = q!λ 1 ⊕ q!λ 2 ; P • G ↾ q = Q = p?λ 1 ; r!λ 3 + p?λ 2 ; Q • G ↾ r = q?λ 3
On the other hand, the corresponding global type based on the µ-notation

G ′ = µt. p → q : (λ 1 ; q λ 3 → r ⊞ λ 2 ; t)
is not projectable because G ′ ↾ r is not defined.

However, this additional permissiveness will not be exploited in the present paper. Indeed, the global type G of Example 6.2 will be ruled out by the condition of boundedness, introduced next, which aims at forbidding starvation. On the other hand, such permissiveness could be of interest whenever starvation is not a concern.

To achieve progress, we need to ensure that each network participant occurs in every computation, whether finite or infinite. This means that each type participant must occur in every path of the tree of the type. Projectability already ensures that each participant 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 participant occurs at some finite depth in this path, or this path crosses infinitely many branching points in which the participant occurs in all branches. In the latter case, since the depth of the participant increases when crossing each branching point, there is no bound on the depth of the participant over all paths of the type. Hence, to ensure that all type participants occur in all paths, it is enough to require the existence of such bounds.

This motivates the following definition of depth and boundedness.

Definition 6.3 (Depth and boundedness).

Let the two functions depth(σ, p) and depth(G, p) be defined by: If depth(G, p) is finite, then there are no paths in the tree of G in which p is delayed indefinitely. Note that if depth(G, p) is finite, G may have subtrees G ′ for which depth(G ′ , p) is infinite as the following example shows.

depth(σ, p) =        n if σ = σ 1 • α • σ
Example 6.4. Consider G ′ = q λ → r; G where G is as defined in Example 6.2. Then we have:

depth(G ′ , p) = 2 depth(G ′ , q) = 1 depth(G ′ , r) = 1 whereas depth(G, p) = 1 depth(G, q) = 1 depth(G, r) = ∞ since Tr + (G) = {pqλ 2 • • • pqλ 2 n •pqλ 1 • qrλ 3 | n ≥ 0} ∪ {pqλ 2 • • • pqλ 2 • • • } and sup{2, 3, . . .} = ∞.
The depths of the participants in G which are not participants of its root communication decrease in the immediate subtrees of G. The proof is trivial since, if

G = p → q : ⊞ i∈I λ i ; G i , then σ ∈ Tr + (G) implies σ = pqλ i • σ ′ and σ ′ ∈ Tr + (G i ) for some i ∈ I.
Lemma 6.5. If G = p → q : ⊞ i∈I λ i ; G i and r ∈ part(G)\{p, q}, then depth(G, r) > depth(G i , r) for all i ∈ I.

We can now show that the definition of projection given in Figure 2 is sound for bounded global types.

Lemma 6.6. If G is bounded, then G ↾ r is a partial function for all r.

Boundedness and projectability single out the global types we want to use in our type system. Definition 6.7 (Well-formed global types). We say that the global type G is well formed if G is bounded and G ↾ p is defined for all p.

Clearly it is sufficient to check that G ↾ p is defined for all p ∈ part(G), since otherwise G ↾ p = 0. The definition of well-typed networks is given in Figure 3. We first define a preorder on processes, P ≤ Q, meaning that process P can be used where we expect process Q. More precisely, P ≤ Q if either P is equal to Q, or we are in one of two situations: either both P and Q are output processes with the same receiver and choice of messages, and their continuations after the send are two processes P ′ and Q ′ such that P ′ ≤ Q ′ ; or they are both input processes with the same sender and choice of messages, and P may receive more messages than Q (and thus have more behaviours) but whenever it receives the same message as Q their continuations are two processes P ′ and Q ′ such that P ′ ≤ Q ′ . The rules are interpreted coinductively, since the processes may have infinite (regular) trees.

Type System

0 ≤ 0 [ ≤ -0] P i ≤ Q i i ∈ I
P i ≤ G ↾ p i i ∈ I part(G) ⊆ {p i | i ∈ I} ⊢ Π i∈I p i [[ P i ]] : G [Net]
A network is well typed if all its participants have associated processes that behave as specified by the projections of a global type. In Rule [Net], the condition part(G) ⊆ {p i | i ∈ I} ensures that all participants of the global type appear in the

p → q : ⊞ i∈I λ i ; G i pqλ j ---→ G j j ∈ I [Ecomm] G i α - → G ′ i for all i ∈ I part(α) ∩ {p, q} = ∅ [Icomm] p → q : ⊞ i∈I λ i ; G i α - → p → q : ⊞ i∈I λ i ; G ′ i
G = p → q : (λ; G ⊞ λ ′ ) G ′ = p λ 1 → q; q λ 2 → r; r λ 3 → s
It is handy to define the LTS for global types given in Figure 4. Rule [Icomm] is justified by the fact that in a projectable global type p → q : ⊞ i∈I λ i ; G i , the behaviours of the participants different from p and q are the same in all branches, and hence they are independent from the choice and may be executed before it.

This LTS respects well-formedness of global types, as shown by Lemma 6.9. Given this lemma, we will focus on well-formed global types from now on.

We end this section with the expected results of Subject Reduction, Session Fidelity [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF] and Progress [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF][START_REF] Padovani | Type reconstruction for the linear π-calculus with composite regular types[END_REF]. The proof of Progress relies on Session Fidelity. Both Subject Reduction and Session Fidelity will be used in Section 8 to show the isomorphism between the configuration domains of the FES of a typable network and the PES of its global type (Theorem 8.18).

Theorem 6.10 (Subject Reduction

). If ⊢ N : G and N α - → N ′ , then G α - → G ′ and ⊢ N ′ : G ′ .

Theorem 6.11 (Session Fidelity

). If ⊢ N : G and G α - → G ′ , then N α - → N ′ and ⊢ N ′ : G ′ .
We are now able to prove that in a typable network, every participant whose process is not terminated may eventually perform a communication. This property is generally referred to as progress.

σ i • α i ---→ G ′ i with p ∈ part(α i ) for all i ∈ I. We conclude G qrλ i •σ i • α i -------→ G ′ i for all i ∈ I.
The proof of the progress theorem shows that the execution strategy which uses

G ′′ = p → q : (λ; G ′′ ⊞ λ ′ ; p λ → r; r λ ′ → s)
is not bounded, given that depth(G ′′ , r) and depth(G ′′ , s) are not finite.

Moreover we cannot define a global type whose projections are greater than or equal to the processes associated with the network of Example 5.20.

Event Structure Semantics of Global Types

We define now the event structure associated with a global type, whose events are equivalence classes of particular traces, and we show that it is a PES.

The unique omitted proof can be found in Appendix C.

We recall that a trace σ ∈ Traces is a finite sequence of communications (see Definition 2.3). We will use the following notational conventions:

• We denote by σ[i] the i-th element of σ, i > 0.

• If i ≤ j, we define σ[i ... j] = σ[i] • • • σ[ j]
to be the subtrace of σ consisting of the ( ji + 1) elements starting from the i-th one and ending with the j-th one. If i > j, we convene σ[i ... j] to be the empty trace ϵ.

If not otherwise stated we assume that σ has n elements, so

σ = σ[1 ... n].
We start by defining an equivalence relation on Traces which allows swapping of communications with disjoint participants.

Definition 7.1 (Permutation equivalence). The permutation equivalence on Traces is the least equivalence

∼ such that σ • α • α ′ • σ ′ ∼ σ • α ′ • α • σ ′ if part(α) ∩ part(α ′ ) = ∅
We denote by [σ] ∼ the equivalence class of the trace σ, and by Traces/∼ the set of equivalence classes on Traces. Note that [ϵ] ∼ = {ϵ} ∈ Traces/∼, and [α] ∼ = {α} ∈ Traces/∼ for any α.

Moreover |σ ′ | = |σ| for all σ ′ ∈ [σ] ∼ .
The events associated with a global type, called g-events and denoted by γ, γ ′ , are equivalence classes of particular traces that we call pointed. Intuitively, in a pointed trace all communications but the last one are causes of some subsequent communication. Formally:

Definition 7.2 (Pointed trace). A trace σ = σ[1 ... n] is said to be pointed if for all i, 1 ≤ i < n, part(σ[i]) ∩ part(σ[(i + 1) ... n]) ∅
Note that the condition of Definition 7.2 must be satisfied only by the σ[i] with i < n, thus it is vacuously satisfied by any trace of length 1.

Example 7.3. Let α 1 = pqλ 1 , α 2 = rsλ 2 and α 3 = rpλ 3 . Then σ 1 = α 1 and σ 3 = α 1 • α 2 • α 3 are pointed traces, while σ 2 = α 1 • α 2 is not a pointed trace.
We use last(σ) to denote the last communication of σ. We denote by GE the set of g-events.

Notice that cm(γ) is well defined due to Lemma 7.4.

We now introduce an operator of prefixing of a g-event γ by a communication α, which acts as follows: if α is a cause of some communication in the trace of γ, then α is added at the beginning of the trace, otherwise γ is left unchanged. This ensures that the operator always transforms a g-event into another g-event. We call this operator "retrieval of a g-event before a communication", because it yields the g-event obtained from γ if we were to execute the communication α before γ. This operator is the counterpart of the "residual of a g-event after a communication", which yields the g-event obtained from γ after executing the communication α from γ, see Definition 8.9.

Definition 7.6 (Retrieval of g-events before communications).

1. The retrieval operator • applied to a communication and a g-event is defined by:

α • [σ] ∼ =        [α • σ] ∼ if part(α) ∩ part(σ) ∅ [σ] ∼ otherwise 2.
The operator • naturally extends to traces:

ϵ • γ = γ (α • σ) • γ = α • (σ • γ)
Using the retrieval, we can define the mapping ev(•) which, applied to a trace σ, gives the g-event representing the communication last(σ) prefixed by its causes occurring in σ.

Definition 7.7. The g-event generated by a non-empty trace is defined by:

ev(σ • α) = σ • [α] ∼
Clearly cm(ev(σ)) = last(σ).

Example 7.8. A trace of the global type p

λ 1 → q; q λ 2 → r; s λ 3 → p is pqλ 1 • qrλ 2 • spλ 3 , and
ev(pqλ 1 • qrλ 2 • spλ 3 ) = pqλ 1 • qrλ 2 • {spλ 3 } = pqλ 1 • {spλ 3 } = {pqλ 1 • spλ 3 }
We proceed now to define the causality and conflict relations on g-events. To define the conflict relation, it is handy to define the projection of a trace on a participant, which gives the sequence of the participant's actions in the trace. The result is a p-event. In this way we can define the conflict between g-events using the conflict between p-events.

Definition 7.9 (Projection of traces on participants).

1. The projection of α onto r, α@r , is defined by:

pqλ@r =            q!λ if r = p p?λ if r = q ϵ if r {p, q} 2.
The projection of a trace σ onto r, σ@r , is defined by: ϵ@r = ϵ (α • σ)@r = α@r • σ@r Definition 7.10 (Causality and conflict relations on g-events). The causality relation ≤ and the conflict relation # on the set of g-events GE are defined by:

1. γ ≤ γ ′ if γ = [σ] ∼ and γ ′ = [σ • σ ′ ] ∼ for some σ, σ ′ ; 2. [σ] ∼ # [σ ′ ] ∼ if σ@p # σ ′ @p for some p. If γ = [σ • α • σ ′ • α ′ ] ∼ , then the communication α must be done before the com- munication α ′ . This is expressed by the causality [σ • α] ∼ ≤ γ. An example is [pqλ] ∼ ≤ [rsλ ′ • pqλ • sqλ ′′ ] ∼ .
As regards conflict, note that if σ ∼ σ ′ then σ@p = σ ′ @p for all p, because ∼ does not swap communications which share some participant. Hence, conflict is well defined, since it does not depend on the trace chosen in the equivalence class.

The condition σ@p # σ ′ @p states that participant p does the same actions in both traces up to some point, after which it performs two different actions in σ and

σ ′ . For example [pqλ • rpλ 1 • qpλ ′ ] ∼ # [pqλ • rpλ 2 ] ∼ , since (pqλ • rpλ 1 • qpλ ′ )@p = q!λ • r?λ 1 • q?λ ′ # q!λ • r?λ 2 = (pqλ • rpλ 2 )@p .
G (G) = (GE(G), ≤ G , # G )
where:

1. GE(G) = {ev(σ) | σ ∈ Tr + (G)}
2. ≤ G is the restriction of ≤ to the set GE(G);

3. # G is the restriction of # to the set GE(G).

Note that, in case the tree of G is infinite, the set GE(G) is denumerable.

Example 7.12.

Let G 1 = p λ 1 → q; r λ 2 → s; r λ 3 → p and G 2 = r λ 2 → s; p λ 1 → q; r λ 3 → p. Then GE(G 1 ) = GE(G 2 ) = {γ 1 , γ 2 , γ 3 } where γ 1 = {pqλ 1 } γ 2 = {rsλ 2 } γ 3 = {pqλ 1 • rsλ 2 • rpλ 3 , rsλ 2 • pqλ 1 • rpλ 3 }
with γ 1 ≤ γ 3 and γ 2 ≤ γ 3 . The configurations are {γ 1 }, {γ 2 }, {γ 1 , γ 2 } and {γ 1 , γ 2 , γ 3 }, and the proving sequences are

γ 1 γ 2 γ 1 ; γ 2 γ 2 ; γ 1 γ 1 ; γ 2 ; γ 3 γ 2 ; γ 1 ; γ 3 If G ′ is as in Example 6.8, then GE(G ′ ) = {γ 1 , γ 2 , γ 3 }
where Reflexivity and transitivity of ≤ follow from the properties of concatenation and of permutation equivalence. As for antisymmetry, by Definition 7.10(1

γ 1 = {pqλ 1 } γ 2 = {pqλ 1 • qrλ 2 } γ 3 = {pqλ 1 • qrλ 2 • rsλ 3 } with γ 1 ≤ γ 2 ≤ γ 3 .
) [σ] ∼ ≤ [σ ′ ] ∼ implies σ ′ ∼ σ • σ 1 for some σ 1 and [σ ′ ] ∼ ≤ [σ] ∼ implies σ ∼ σ ′ • σ 2 for some σ 2 . Hence σ ∼ σ • σ 1 • σ 2 , which implies σ 1 = σ 2 = ϵ.
Irreflexivity and symmetry of # follow from the corresponding properties of # on p-events.

As for conflict hereditariness, suppose that

[σ] ∼ # [σ ′ ] ∼ ≤ [σ ′′ ] ∼ . By Definition 7.10(1)
and ( 2) we have respectively that σ ′ • σ 1 ∼ σ ′′ for some σ 1 and σ@p # σ ′ @p for some p. Hence also σ@p # (σ ′ • σ 1 )@p , whence by Definition 7.10(2) we conclude that

[σ] ∼ # [σ ′′ ] ∼ .
Observe that, while our interpretation of networks as FESs exactly reflects the concurrency expressed by the syntax of networks, our interpretation of global types as PESs exhibits more concurrency than that given by the syntax of global types.

We conclude this section with two pictures that summarise the features of our ES semantics and illustrate the difference between the FES of a network and the PES of its type. In general these two ESs are not isomorphic, unless the FES of the network is itself a PES.

N = p[[ q!λ 1 ; r!λ ⊕ q!λ 2 ; r!λ ]] ∥ q[[ p?λ 1 ; s!λ ′ + p?λ 2 ; s!λ ′ ]] ∥ r[[ p?λ; s!λ ′′ ]] ∥ s[[ q?λ ′ ; r?λ ′′ ]] ν 1 = {p :: q!λ 1 , q :: p?λ 1 } ν ′′ 1 = {q :: p?λ 1 • s!λ ′ , s :: q?λ ′ } ν = {r :: p?λ • s!λ ′′ , s :: q?λ ′ • r?λ ′′ } ν 2 = {p :: q!λ 2 , q :: p?λ 2 } ν ′′ 2 = {q :: p?λ 2 • s!λ ′ , s :: q?λ ′ } ν ′ 1 = {p :: q!λ 1 • r!λ, r :: p?λ} ν ′ 2 = {p :: q!λ 2 •r!λ , r :: p?λ} # c c • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •
G = p → q : (λ 1 ; p λ → r; q λ ′ → s; r λ ′′ → s ⊞ λ 2 ; p λ → r; q λ ′ → s; r λ ′′ → s) γ 1 = [pqλ 1 ] ∼ γ ′′ 1 = [pqλ 1 • qsλ ′ ] ∼ γ = [pqλ 1 • prλ • qsλ ′ • rsλ ′′ ] ∼ γ ′ = [pqλ 2 • prλ • qsλ ′ • rsλ ′′ ] ∼ γ 2 = [pqλ 2 ] ∼ γ ′ 1 = [pqλ 1 • prλ] ∼ γ ′′ 2 = [pqλ 2 • qsλ ′ ] ∼ γ ′ 2 = [pqλ 2 • prλ] ∼
Consider the network FES pictured in Figure 5, where the arrows represent the flow relation and all the n-events on the left of the dotted line are in conflict with all the n-events on the right of the line. In particular, notice that the conflicts between n-events with a common location are deduced by Clause (2a) of Definition 5.7, while the conflicts between n-events with disjoint sets of locations, such as ν ′ 1 and ν ′′ 2 , are deduced by Clause (2b) of Definition 5.7. Observe also that the n-event ν has two different causal sets in NE(N), namely {ν ′ 1 , ν ′′ 1 } and {ν ′ 2 , ν ′′ 2 }. The reader familiar with

ESs will have noticed that there are also two prime configurations whose maximal element is ν, namely {ν 1 , ν ′ 1 , ν ′′ 1 , ν} and {ν 2 , ν ′ 2 , ν ′′ 2 , ν}. It is easy to see that the network N can be typed with the global type G shown in Figure 6.

Consider now the PES of the type G pictured in Figure 6, where the arrows represent the covering relation of the partial order of causality and inherited conflicts are not shown. Note that while the FES of N has a unique maximal n-event ν, the PES of its type G has two maximal g-events γ and γ ′ . This is because an n-event only records the computations that occurred at its locations, while a g-event records

the global computation and keeps a record of each choice, including those involving locations that are disjoint from those of its last communication. Indeed, g-events correspond exactly to prime configurations.

Note that the FES of a network may be easily recovered from the PES of its global type by using the following function gn(•) that maps g-events to n-events:

gn(γ) = {p :: σ@p , q :: σ@q } if γ = [σ] ∼ with part(cm(γ)) = {p, q}
On the other hand, the inverse construction is not as direct. First of all, an n-event in the network FES may give rise to several g-events in the type PES, as shown by the n-event ν in Figure 5, which gives rise to the pair of g-events γ and γ ′ in Figure 6. Moreover, the local information contained in an n-event is not sufficient to reconstruct the corresponding g-events: for each n-event, we need to consider all the prime configurations that culminate with that event, and then map each of these configurations to a g-event. Hence, we need a function ng(•) that maps n-events to sets of prime configurations of the FES, and then maps each such configuration to a g-event. We will not explicitly define this function here, since we miss another important ingredient to compare the FES of a network and the PES of its type, namely a structural characterisation of the FESs that represent typable networks. Indeed, if we started from the FES of a non typable network, this construction would not be correct. Consider for instance the network N ′ obtained from N by omitting the output r!λ from the second branch of the process of p. Then the FES of N ′ would not contain the n-event ν ′ 2 and the event ν would have the unique causal set {ν ′ 1 , ν ′′ 1 }, and the unique prime configuration culminating with ν would be {ν 1 , ν ′ 1 , ν ′′ 1 , ν}. Then our construction would give a PES that differs from that of type G only for the absence of the g-events γ ′ 2 and γ ′ . However, the network N ′

is not typable and thus we would expect the construction to fail. Note that in the FES of N ′ , the n-event ν ′′ 2 is a cause of ν but does not belong to any causal set of ν. Thus a possible well-formedness property to require for FESs to be images of a typable network would be that each cause of each n-event belong to some causal set of that event. However, this would still not be enough to exclude the FES of the non typable network N ′′ obtained from N ′ by omitting the output s!λ ′ from the second branch of the process of q.

To conclude, in the absence of a semantic counterpart for the well-formedness properties of global types, which eludes us for the time being, we will follow another approach here, namely we will compare the FESs of networks and the PESs of their types at a more operational level, by looking at their configuration domains and by relating their configurations to the transition sequences of the underlying networks and types.

Equivalence of the two Event Structure Semantics

ν 1 ; . . . ; ν n = nec(σ)
Th.8.8

u u N σ = cm(ν 1 ) • . . . • cm(ν n ) SR / / Th.8.7 j j N ′ G Th.8. 15
)

) σ = cm(γ 1 ) • . . . • cm(γ n ) / / SF O O G ′ gec(σ) = γ 1 ; . . . ; γ n
Th.8.16

5 5

Figure 7: Isomorphism proof in a nutshell.

In this section we establish our main result for typable networks (Theorem 8.18), namely the isomorphism between the domain of configurations of the FES of a typable network and the domain of configurations of the PES of its global type.

To do so, we first relate the transition sequences of networks and global types to the configurations of their respective ESs. Then, we exploit our results of Subject Reduction (Theorem 6.10) and Session Fidelity (Theorem 6.11), which relate the transition sequences of networks and their global types, to derive a similar relation between the configurations of their respective ESs. The schema of our proof is described by the diagram in Figure 7. Here, SR stands for Subject Reduction and SF for Session Fidelity, and ν 1 ; . . . ; ν n and γ 1 ; . . . ; γ n are proving sequences of S N (N) and S G (G), respectively. Finally, nec(σ) and gec(σ) denote the proving sequences of nevents and g-events which correspond to the trace σ (as given by Definition 8.3 and Definition 8.13). Theorem 8.8 says that, if

ν 1 ; • • • ; ν n is a proving sequence of S N (N), then N σ - → N ′ , where σ = cm(ν 1 ) • . . . • cm(ν n ). By Subject Reduction (Theorem 6.10) G σ - → G ′ .
This implies that gec(σ) is a proving sequence of S G (G) by Theorem 8.15.

Dually, Theorem 8.16 says that, if

γ 1 ; • • • ; γ n is a proving sequence of S G (G), then G σ - → G ′ , where σ = cm(γ 1 ) • . . . • cm(γ n ). By Session Fidelity (Theorem 6.11) N σ - → N ′ .
Lastly, nec(σ) is a proving sequence of S N (N) by Theorem 8.7. The equalities in the top and bottom lines are proved in Lemmas 8.4(1a) and 8.14(1).

This section is divided in two subsections: Section 8.1, which handles the upper part of the above diagram, and Section 8.2, which handles the lower part of the diagram and then connects the two parts using both SR and SF within Theorem 8.18, our closing result. The omitted proofs of Sections 8.1 and 8.2 can be found in Appendices D and E, respectively.

Relating Transition Sequences of Networks and Proving Sequences of their ESs

The aim of this subsection is to relate the traces that label the transition sequences of networks with the configurations of their FESs. We start by showing how network communications affect n-events in the associated FES. To this end we define two partial operators ♢ and ♦, which applied to a communication α and an n-event ν yield another n-event ν ′ (when defined), which represents the event ν before the communication α or after the communication α, respectively. We call "retrieval" the ♢ operator (in agreement with Definition 7.6) and "residual" the ♦ operator.

Formally, the operators ♢ and ♦ are defined as follows.

Definition 8.1 (Retrieval and residual of n-events with respect to communications).

1. The retrieval operator ♢ applied to a communication and a located event returns the located event obtained by prefixing the p-event by the projection of the communication:

α ♢ (p :: η) = p :: (α@p ) • η 2.
The residual operator ♦ applied to a communication and a located event returns the located event obtained by erasing from the p-event the projection of the communication (if possible): α ♦ (p :: η) = p ::

η ′ if η = (α@p ) • η ′ 3.
The operators ♢ and ♦ naturally extend to n-events and to traces:

α ♢ ({p :: η, q :: η ′ }) = {α ♢ (p :: η), α ♢ (q :: η ′ )} α ♦ ({p :: η, q ::

η ′ }) = {α ♦ (p :: η), α ♦ (q :: η ′ )} ϵ ♢ ν = ν (α • σ) ♢ ν = α ♢ (σ ♢ ν) ϵ ♦ ν = ν (α • σ) ♦ ν = σ ♦ (α ♦ ν)
Note that the operator ♢ is always defined. Instead pqλ ♦ r :: η is undefined if r ∈ {p, q} and either η is just one atomic action or pqλ@r is not the first atomic action of η. For example pqλ ♦ p :: q!λ and pqλ ♦ p :: q!λ ′ • η with λ λ ′ are undefined for any η.

The retrieval and residual operators are inverse of each other. Moreover they preserve the flow and conflict relations.

Lemma 8.2 (Properties of retrieval and residual for n-events).

1. If α ♦ ν is defined, then α ♢ (α ♦ ν) = ν; 2. α ♦ (α ♢ ν) = ν; 3. If ν ≺ ν ′ , then α ♢ ν ≺ α ♢ ν ′ ; 4. If ν ≺ ν ′ and both α ♦ ν and α ♦ ν ′ are defined, then α ♦ ν ≺ α ♦ ν ′ ; 5. If ν # ν ′ , then α ♢ ν # α ♢ ν ′ ; 6. If ν # ν ′ and both α ♦ ν and α ♦ ν ′ are defined, then α ♦ ν # α ♦ ν ′ ; 7. If α ♢ ν # α ♢ ν ′ , then ν # ν ′ .
Starting from the trace σ ϵ that labels a transition sequence in a network, one can reconstruct the corresponding sequence of n-events in its FES. Recall that σ[1 ... i] is the prefix of length i of σ and σ[i ... j] is the empty trace if i > j.

Definition 8.3 (Building sequences of n-events from traces). If σ is a non-empty trace with σ[i] = p i q i λ i , 1 ≤ i ≤ n, we define the sequence of n-events corresponding to σ by

nec(σ) = ν 1 ; • • • ; ν n where ν i = σ[1 ... i -1] ♢ {p i :: q i !λ i , q i :: p i ?λ i } for 1 ≤ i ≤ n.
It is immediate to see that, if σ = pqλ, then nec(σ) is the event {p :: q!λ, q :: p?λ}.

We show now that σ can be recovered from nec (σ), and that two n-events occurring in nec(σ) cannot be in conflict. Moreover, the n-event obtained by applying nec to a communication cannot be in conflict with the n-event obtained by applying the retrieval to the same communication and an arbitrary n-event.

Lastly, we relate the sequences of n-events generated by two traces one of which is a suffix of the other. Given that the mapping nec is based on the retrieval operator, this relation is naturally expressed using the retrieval and residual operators.

Lemma 8.4 (Properties of nec(•)).

1. Let nec(σ) = ν 1 ; • • • ; ν n . Then (a) cm(ν i ) = σ[i] for all i, 1 ≤ i ≤ n; (b) If 1 ≤ h, k ≤ n, then ¬(ν h # ν k ).
2. ¬(nec(α) # α ♢ ν) for all ν.

3. Let σ = α • σ ′ and σ ′ ϵ. If nec(σ) = ν 1 ; • • • ; ν n and nec(σ ′ ) = ν ′ 2 ; • • • ; ν ′ n , then α ♢ ν ′ i = ν i and α ♦ ν i = ν ′ i for all i, 2 ≤ i ≤ n.
Notice that if α ♦ ν is undefined and ν is an n-event of a network with communication α, then either ν = nec(α) or ν # nec(α). We may now prove the correspondence between the traces labelling the transition sequences of a network and the proving sequences of its FES. Inductive case.

Let σ = α • σ ′ . From N σ - → N ′ we get N α - → N ′′ σ ′ -→ N ′ for some N ′′ . Let nec(σ) = ν 1 ; • • • ; ν n and nec(σ ′ ) = ν ′ 2 ; • • • ; ν ′ n . By induction nec(σ ′ ) is a proving sequence in S N (N ′′ ).
We show that nec(σ) is a proving sequence in S N (N). By Lemma 8.4(1b) nec(σ ′ ) is conflict free. By Lemma 8.4(3) ν i = α ♢ ν ′ i for all i, 2 ≤ i ≤ n. This implies ν i ∈ NE(N) for all i, 2 ≤ i ≤ n by Lemma 8.6(1) and ¬(ν 1 # ν j ) for all i, j, 2 ≤ i, j ≤ n by Lemma 8.2 [START_REF] Boudol | On the semantics of concurrency: partial orders and transition systems[END_REF]. Finally, since ν 1 = nec(α), by Lemma 8.4(2) we obtain ¬(ν 1 # ν i ) for all i, 2 ≤ i ≤ n. We conclude that nec(σ) is conflict-free and included in NE(N).

Let ν ∈ NE(N) and ν ≺ ν k for some k, 1 ≤ k ≤ n. This implies k > 1 since nec(α) has no causes. Hence ν k = α ♢ ν ′ k . By Lemma 8.5, we know that ν = nec(α) or ν # nec(α)

or α ♦ ν is defined. We consider the three cases. Let part(α) = {p, q}.

Case ν = nec(α). In this case we conclude immediately since nec(α) = ν 1 and 1 < k. Case α ♦ ν defined. We get α ♦ ν ≺ ν ′ k by Lemma 8.2(4). Since nec(σ ′ ) is a proving sequence in S N (N ′′ ), there is (1). In the second case: Lemma 8.2(5), which implies ν # ν h by Lemma 8.2(1), and

Case ν # nec(α). Since nec(α) = ν 1 , if ν 1 ≺ ν k we are done. If ν 1 ⊀ ν k , then loc(ν k ) ∩ {p, q} = ∅ otherwise ν 1 # ν k . We get ν k = α ♢ ν ′ k = ν ′ k . Since ν ≺ ν k ,
h < k such that either α ♦ ν = ν ′ h or α ♦ ν # ν ′ h ≺ ν ′ k . In the first case ν = α ♢ (α ♦ ν) = α ♢ ν ′ h = ν h by Lemma 8.2
• from α ♦ ν # ν ′ h we get (α ♢ (α ♦ ν)) # (α ♢ ν ′ h ) by
• from ν ′ h ≺ ν ′ k we get (α ♢ ν ′ h ) ≺ (α ♢ ν ′ k ) by Lemma 8.2(3), namely ν h ≺ ν k . Theorem 8.8. If ν 1 ; • • • ; ν n is a proving sequence in S N (N), then N σ - → N ′ , where σ = cm(ν 1 ) • • • cm(ν n ).

Proof

The proof is by induction on n.

Case n = 1. Let ν 1 = {p :: ζ • q!λ, q :: ζ ′ • p?λ}. Then cm(ν 1 ) = pqλ. We first show that ζ = ζ ′ = ϵ. Assume ad absurdum that ζ ϵ or ζ ′ ϵ. By narrowing, this implies that there is ν ∈ NE(N) such that ν ≺ ν 1 , contradicting the fact that ν 1 is a proving sequence.

Lemma 8.10 (Properties of retrieval and residual for g-events).

1. If α • γ is defined, then α • (α • γ) = γ; 2. α • (α • γ) = γ; 3. If γ 1 < γ 2 , then α • γ 1 < α • γ 2 ; 4. If γ 1 < γ 2 and both α • γ 1 and α • γ 2 are defined, then α • γ 1 < α • γ 2 ; 5. If γ 1 # γ 2 , then α • γ 1 # α • γ 2 ; 6. If γ < α • γ ′ , then either γ = [α] ∼ or α • γ < γ ′ ; 7. If part(α 1 ) ∩ part(α 2 ) = ∅, then α 1 • (α 2 • γ) = α 2 • (α 1 • γ); 8. If part(α 1 )∩part(α 2 ) = ∅ and both α 2 •(α 1 • γ), α 2 •γ are defined, then α 1 •(α 2 • γ) = α 2 • (α 1 • γ).
The next lemma relates the retrieval and residual operator with the global types in the branches of choices.

Lemma 8.11. The following hold:

1. If γ ∈ GE(G), then pqλ • γ ∈ GE(p → q : ⊞ i∈I λ i ; G i ), where λ = λ k and G = G k for some k ∈ I; 2. If γ ∈ GE(p → q : ⊞ i∈I λ i ; G i ) and pqλ k • γ is defined, then pqλ k • γ ∈ GE(G k ),
where k ∈ I.

The following lemma plays the role of Lemma 8.6 for n-events.

Lemma 8.12.

Let G α - → G ′ . 1. If γ ∈ GE(G ′ ), then α • γ ∈ GE(G); 2. If γ ∈ GE(G) and α • γ is defined, then α • γ ∈ GE(G ′ ).
Each non-empty trace gives rise to a sequence of g-events, compare with Definition 8.3.

Definition 8.13 (Building sequences of g-events from traces). We define the sequence of g-events corresponding to a non-empty trace σ by

gec(σ) = γ 1 ; • • • ; γ n where γ i = ev(σ[1 ... i]) for all i, 1 ≤ i ≤ n.
We show that gec(•) has similar properties as nec(•), see Lemma 8.4(1). The proof is straightforward.

Lemma 8.14. Let gec(σ) = γ 1 ; • • • ; γ n . 1. cm(γ i ) = σ[i] for all i, 1 ≤ i ≤ n. 2. If 1 ≤ h, k ≤ n, then ¬(γ h # γ k );
We Proof By induction on σ.

Base case. Let σ = α, then gec(α) = [α] ∼ . We use a further induction on the inference

of the transition G α - → G ′ . Let G = p → q : ⊞ i∈I λ i ; G i , G ′ = G h and α = pqλ h for some h ∈ I. By Defini- tion 7.11(1) [pqλ h ] ∼ ∈ GE(G). Let G = p → q : ⊞ i∈I λ i ; G i and G ′ = p → q : ⊞ i∈I λ i ; G ′ i and G i α - → G ′ i for all i ∈ I and part(α) ∩ {p, q} = ∅. By induction [α] ∼ ∈ GE(G i
) for all i ∈ I. By Lemma 8.11( 1)

pqλ i • [α] ∼ ∈ GE(G) for all i ∈ I. By Definition 7.11(1) pqλ i • [α] ∼ = [α] ∼ , since part(α)∩{p, q}=∅. We conclude [α] ∼ ∈ GE(G). Inductive case. Let σ = α • σ ′ with σ ′ ϵ. From G σ - → G ′ we get G α - → G ′′ σ ′ -→ G ′ for some G ′′ . Let gec(σ) = γ 1 ; • • • ; γ n and gec(σ ′ ) = γ ′ 2 ; • • • ; γ ′ n . By induction gec(σ ′ ) is a
proving sequence in S G (G ′′ ). By Definitions 8.13 and 7.6

γ i = α • γ ′ i , which implies α • γ i = γ ′ i by Lemma 8.10(2) for all i, 2 ≤ i ≤ n.
We can show that γ 1 = [α] ∼ ∈ GE(G) as in the proof of the base case. By Lemma 8.12(1) γ i ∈ GE(G) since γ ′ i ∈ GE(G ′′ ) and α • γ i = γ ′ i for all i, 2 ≤ i ≤ n. We prove that gec(σ) is a proving sequence in S G (G). Let γ < γ k for some k, 1 ≤ k ≤ n.

Note that this implies

k > 1. Since γ k = α • γ ′ k by Lemma 8.10(6) either γ = [α] ∼ or α•γ < γ ′ h . If γ = [α] ∼ = γ 1 we are done. Otherwise α•γ ∈ GE(G ′′ ) by Lemma 8.11(2). Since gec(σ ′ ) is a proving sequence in S G (G ′′ ), there is h < k such that α • γ = γ ′ h and this implies γ = α • (α • γ) = α • γ ′ h = γ h by Lemma 8.10(1). Theorem 8.16. If γ 1 ; • • • ; γ n is a proving sequence in S G (G), then G σ - → G ′ , where σ = cm(γ 1 ) • • • • • cm(γ n ).
Proof The proof is by induction on the length n of the proving sequence. Let cm(γ 1 ) = α and {p, q} = part(α).

Case n = 1. Since γ 1 is the first event of a proving sequence, we have γ 1 = [α] ∼ . We show this case by induction on d = depth(G, p) = depth(G, q).

Case d = 1. Let α = pqλ and G = p → q : ⊞ i∈I λ i ; G i and λ = λ h for some h ∈ I.

- → N 0 α - → N ′
and ⊢ N ′ : G ′ . By Theorem 8.7 nec(σ • α) is a proving sequence of S N (N).

Related Work and Conclusions

Event Structures (ESs) were introduced in Winskel's PhD Thesis [START_REF] Winskel | Events in Computation[END_REF] and in the seminal paper by Nielsen, Plotkin and Winskel [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF], roughly in the same frame of time as Milner's calculus CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. It is therefore not surprising that the relationship between these two approaches for modelling concurrent computations started to be investigated very soon afterwards. The first interpretation of CCS into ESs was proposed by Winskel in [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF]. This interpretation made use of Stable ESs, because PESs, the simplest form of ESs, appeared not to be flexible enough to account for CCS parallel composition. Indeed, since CCS parallel composition allows for two concurrent complementary actions to either synchronise or occur independently in any order, each pair of such actions gives rise to two forking computations: this requires duplication of the same continuation process for these forking computations in PESs, while the continuation process may be shared by the forking computations in Stable ESs, which allow for disjunctive causality. Subsequently, ESs (as well as other nonsequential "denotational models" for concurrency such as Petri Nets) have been used as the touchstone for assessing noninterleaving operational semantics for CCS: for instance, the pomset semantics for CCS by Boudol and Castellani [START_REF] Boudol | On the semantics of concurrency: partial orders and transition systems[END_REF][START_REF] Boudol | Permutation of transitions: an event structure semantics for CCS and SCCS[END_REF] and the semantics based on "concurrent histories" proposed by Degano, De Nicola and Montanari [START_REF] Degano | Concurrent histories: A basis for observing distributed systems[END_REF][START_REF] Degano | On the consistency of truly concurrent operational and denotational semantics[END_REF][START_REF] Degano | A partial ordering semantics for CCS[END_REF], were both shown to agree with an interpretation of CCS processes into some class of ESs (PESs for [START_REF] Degano | On the consistency of truly concurrent operational and denotational semantics[END_REF][START_REF] Degano | A partial ordering semantics for CCS[END_REF], PESs with non-hereditary conflict for [START_REF] Boudol | On the semantics of concurrency: partial orders and transition systems[END_REF], and FESs for [START_REF] Boudol | Permutation of transitions: an event structure semantics for CCS and SCCS[END_REF]). Among the early interpretations of process calculi into ESs, we should also mention the PES semantics for TCSP (Theoretical CSP [START_REF] Brookes | A theory of communicating sequential processes[END_REF][START_REF] Olderog | TCSP: theory of communicating sequential processes[END_REF]), proposed by Goltz and Loogen [START_REF] Loogen | Modelling nondeterministic concurrent processes with event structures[END_REF] and later generalised by Baier and Majster-Cederbaum [START_REF] Baier | The connection between an event structure semantics and an operational semantics for TCSP[END_REF], and the Bundle ES semantics for LOTOS, proposed by Langerak [START_REF] Langerak | Bundle event structures: a non-interleaving semantics for LO-TOS[END_REF] and extended by Katoen [START_REF] Katoen | Quantitative and qualitative extensions of event structures[END_REF]. Like FESs, Bundle ESs are a subclass of Stable ESs. We recall the relationships between the above classes of ESs (the reader is referred to [START_REF] Boudol | Flow models of distributed computations: three equivalent semantics for CCS[END_REF] for separating examples):

Prime ESs ⊂ Bundle ESs ⊂ Flow ESs ⊂ Stable ESs ⊂ General ESs
More sophisticated ES semantics for CCS, based on FESs and designed to be robust under action refinement [1,[START_REF] Darondeau | Refinement of actions in event structures and causal trees[END_REF][START_REF] Goltz | Comparing syntactic and semantic action refinement[END_REF], were subsequently proposed by Goltz and van Glabbeek [START_REF] Van Glabbeek | Well-behaved flow event structures for parallel composition and action refinement[END_REF]. Importantly, all the above-mentioned classes of ESs, except General ESs, give rise to the same prime algebraic domains of configurations, from which one can recover a PES by selecting the complete prime elements.

More recently, ES semantics have been investigated for the π-calculus by Crafa, Varacca and Yoshida [START_REF] Crafa | Compositional event structure semantics for the internal π-calculus[END_REF][START_REF] Varacca | Typed event structures and the linear π-calculus[END_REF][START_REF] Crafa | Event structure semantics of parallel extrusion in the π-calculus[END_REF] and by Cristescu, Krivine and Varacca [START_REF] Cristescu | Operational and denotational semantics for the reversible πcalculus[END_REF][START_REF] Cristescu | Rigid families for CCS and the π-calculus[END_REF][START_REF] Cristescu | Rigid families for the reversible π-calculus[END_REF].

Previously, other causal models for the π-calculus had already been put forward by Jategaonkar and Jagadeesan [START_REF] Jategaonkar | Causality and true concurrency: A data-flow analysis of the π-calculus[END_REF], by Montanari and Pistore [START_REF] Montanari | Concurrent semantics for the π-calculus[END_REF], by Cattani and Sewell [START_REF] Luca | Models for name-passing processes: interleaving and causal[END_REF] and by Bruni, Melgratti and Montanari [START_REF] Bruni | Event structure semantics for nominal calculi[END_REF]. The main new issue, when addressing causality-based semantics for the π-calculus, is the implicit causality induced by scope extrusion. Two alternative views of such implicit causality had been proposed in early work on noninterleaving operational semantics for the πcalculus, respectively by Boreale and Sangiorgi [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF] and by Degano and Priami [START_REF] Degano | Non-interleaving semantics for mobile processes[END_REF].

Essentially, in [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF] an extruder (that is, an output of a private name) is considered to cause any action that uses the extruded name, whether in subject or object position, while in [START_REF] Degano | Non-interleaving semantics for mobile processes[END_REF] it is considered to cause only the actions that use the extruded name in subject position. Thus, for instance, in the process P = νa (b⟨a⟩ | c⟨a⟩ | a), the two parallel extruders are considered to be causally dependent in the former approach, and independent in the latter. All the causal models for the π-calculus mentioned above, including the ES-based ones, take one or the other of these two stands. Note that opting for the second one leads necessarily to a non-stable ES model, where there may be causal ambiguity within the configurations themselves: for instance, in the above example the maximal configuration contains three events, the extruders b⟨a⟩, c⟨a⟩ and the input on a, and one does not know which of the two extruders enabled the input. Indeed, the paper [START_REF] Crafa | Event structure semantics of parallel extrusion in the π-calculus[END_REF] uses non-stable ESs. The use of non-stable ESs (General ESs) to express situations where a computational step can merge parts of the state is advocated for instance by Baldan, Corradini and Gadducci in [START_REF] Baldan | Domains and event structures for fusions[END_REF]. These ESs give rise to configuration domains that are not prime algebraic, hence the classical representation theorems have to be adjusted.

In our simple setting, where we deal only with single sessions and do not consider session interleaving nor delegation, we can dispense with channels altogether, and therefore the question of parallel extrusion does not arise. In this sense, our notion of causality is closer to that of CCS than to the more complex one of the π-calculus. However, even in a more general setting, where participants would be paired with the channel name of the session they pertain to, the issue of parallel extrusion would not arise: indeed, in the above example b and c should be equal, because participants can only delegate their own channel, but then they could not be in parallel because of linearity, one of the distinguishing features enforced by session types. Hence we believe that in a session-based framework the two above views of implicit causality should collapse into just one. We now briefly discuss our design choices.

• The calculus considered in the present paper uses synchronous communication -rather than asynchronous, buffered communication -because this is how communication is classically modelled in ESs, when they are used to give semantics to process calculi. We should mention however that after first proposing the present study in [START_REF] Castellani | Event structure semantics for multiparty sessions[END_REF], we also considered a calculus with asynchronous communication in the companion paper [START_REF] Castellani | Global types and event structure semantics for asynchronous multiparty sessions[END_REF]. In that work too, networks are interpreted as FESs, and their associated global types, which we called asynchronous types as they split communications into outputs and inputs, are interpreted as PESs. The key result is again an isomorphism between the configuration domain of the FES of a typed network and that of the PES of its type.

• Concerning the choice operator, we adopted here the basic (and most restrictive) variant for it, as it was originally proposed for multiparty session calculi in [START_REF] Honda | Multiparty asynchronous session types[END_REF]. This is essentially a simplifying assumption, and we do not foresee any difficulty in extending our results to a more general choice operator, where the projection is rendered more flexible through the use of a merge operator [START_REF] Deniélou | Dynamic multirole session types[END_REF].

• As regards the preorder on processes, which is akin to a subtyping relation, we envisaged to use the standard subtyping, in which a process with fewer outputs can be used in place of a process with more outputs. However, in that case Session Fidelity would become weaker, since a transition in the LTS of a global type would only ensure a transition in the LTS of the corresponding network, but not necessarily with the same labelling communication. The main drawback would be that Theorem 8.18 would no longer hold: more precisely, the domains of network configurations would only be embedded in (and not isomorphic to) the domains of their global type configurations.

Notably, typability is independent from the use of our preorder or of the standard one, as proved in [START_REF] Barbanera | Composition and decomposition of multiparty sessions[END_REF].

As regards future work, we plan to define an asynchronous transition system (ATS) [START_REF] Bednarczyk | Categories of Asynchronous Systems[END_REF] for our calculus, along the lines of [START_REF] Boudol | Flow models of distributed computations: three equivalent semantics for CCS[END_REF], and show that it provides a noninterleaving operational semantics for networks that is equivalent to their FES semantics. This would enable us also to investigate the issue of reversibility, jointly on our networks and on their FES representations, since the ATS semantics would give us the handle to unwind networks, while the corresponding FESs could be unrolled following one of the methods proposed in existing work on reversible event structures [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF][START_REF] Cristescu | Rigid families for the reversible π-calculus[END_REF][START_REF] Graversen | Towards a categorical representation of reversible event structures[END_REF][START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF][START_REF] Graversen | Event Structure Semantics of Reversible Process Calculi[END_REF].

As mentioned at the end of Section 7, the quest for a semantic counterpart of our well-formedness conditions on global types -namely, for properties that characterise the FESs obtained from typable networks -is still open. By way of comparison, such semantic well-formedness conditions have been proposed in [START_REF] Tuosto | Semantics of global view of choreographies[END_REF] for graphical choreographies, a truly concurrent graphical model for global specifications with two kinds of forking nodes, representing respectively choice and parallel composition. In [START_REF] Tuosto | Semantics of global view of choreographies[END_REF], those well-formedness conditions, called wellsequencing and well-branchedness, were shown to be sufficient to ensure projectability on local specifications. In our case, the property corresponding to well-sequencing is automatically ensured by our ES semantics, and we conjecture that the wellbranchedness condition for choice nodes (corresponding to projectability) could amount in our simpler setting 10 This condition would allow us to rule out the FESs of both networks N ′ and N ′′ discussed at the end of Section 7. However, it should be completed with a condition corresponding to boundedness, and the conjunction of these two conditions might

Proof (1). The proof is by induction on d = depth(G, p).

If d = 1, then by definition of projection (see Figure 2) G ↾ p = i∈I q!λ i ; P i implies G = p → q : ⊞ i∈I λ i ; G i with G i ↾ p = P i . By the same definition G ↾ q = Σ j∈J p?λ ′ j ; Q j implies J = I and λ ′ j = λ j and Q j = G j ↾ q for all j ∈ J. Moreover G (2). The proof is by induction on the transition rules of Figure 4.

The interesting case is:

G h pqλ ---→ G ′ h h ∈ H {p,
G h ↾ p =
i∈I q!λ i ; P i , G h ↾ q = Σ i∈I p?λ i ; Q i , λ = λ k for some k ∈ I and G ′ h ↾ r = G h ↾ r for all r {p, q} and all h ∈ H. By definition of projection G ↾ p = G h ↾ p and G ↾ q = G h ↾ q for all h ∈ H. For r {p, q, s, t} we get G ↾ p = i∈I q!λ i ; P ′ i with P i ≤ P ′ i for all i ∈ I, from Rule [ ≤ -Out] of Figure 3, and 2. G ↾ q = Σ j∈J ′ p?λ j ; Q ′ j with Q j ≤ Q ′ j for all j ∈ J ′ ⊆ J, from Rule [ ≤ -In] of

G ′ ↾ r = G ′ h ↾ r = G h ↾ r = G ↾ r . Moreover G ′ ↾ s = h∈H t!λ ′ h ; G ′ h ↾ s = h∈H t!λ ′ h ; G h ↾ s = G ↾ s and G ′ ↾ t = Σ h∈H t?λ ′ h ; G ′ h ↾ t = Σ h∈H s?λ ′ h ; G h ↾ s = G ↾ t .
σ 0 = σ 1 • α • α ′ • σ 2 ∼ σ 1 • α ′ • α • σ 2 = σ ′ and part(α) ∩ part(α ′ ) = ∅
By induction hypothesis σ 0 is a pointed trace and last(σ) = last(σ 0 ). Therefore σ 2 ϵ since otherwise α ′ would be the last communication of σ 0 and it cannot be part(α) ∩ part(α ′ ) = ∅. This implies last(σ) = last(σ ′ ).

To show that σ ′ is pointed, since all the communications in σ 1 and σ 2 have the same successors in σ 0 and σ ′ , all we have to prove is that the required property holds for the two swapped communications α ′ and α in σ ′ , namely: The last two statements are known to hold since σ 0 is pointed by induction hypothesis.

  in the sequel. If P 0 we write p[[ P ]] ∈ N as short for N ≡ p[[ P ]] ∥ N ′ for some N ′ . We define the set of participants of N to be {p | ∃P. p[[ P ]] ∈ N}.

Figure 1 :

 1 Figure 1: LTS for networks.

3 .Definition 3 . 2 (

 332 # ⊆ (E×E) is an irreflexive symmetric relation, called the conflict relation, satisfying the property: ∀e, e ′ , e ′′ ∈ E : e # e ′ ≤ e ′′ ⇒ e # e ′′ (conflict hereditariness). Flow Event Structure). A flow event structure (FES) is a tuple S = (E, ≺, # ) where:

2 .

 2 ≺ ⊆ (E × E) is an irreflexive relation, called the flow relation; 3. # ⊆ (E × E) is a symmetric relation, called the conflict relation.

Definition 3 . 5 (

 35 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)= def (C(S), ⊆).

Definition 5 . 3 (

 53 Duality of undirected action sequences).The duality of undirected action sequences, written Θ Θ ′ , is the symmetric relation induced by:

Example 5 . 15 .

 515 r :: p?λ ′ }. If we did not apply the narrowing function to CE(N), namely if we took CE(N) as the set of n-events for S N (N), then {ν} would be a possible configuration of S N (N), which is clearly wrong, since the network N does not have a corresponding transition. Instead, by applying the narrowing function to CE(N) we obtain NE(N) = n(CE(N)) = ∅, since the n-event ν has no causal set in CE(N), which is what we expect. The set of n-events of a network ES can be infinite, as shown by the following example. Let P be as in Example 4.4, Q =

  Definition 5.7(2b) and we reach immediately a contradiction. So, assume | η ↱ q | > | η ′ ↱ p | = n. This means that | η | > 1 and thus

  where n(•) is the narrowing function (Definition 5.11). By definition of narrowing, p :: η • η ′ ∈∈ NE(N) implies that there is E ⊆ NE(N) such that E is a causal set of ν in NE(N). Therefore p :: η • η ′ ∈ ν implies p :: η ∈∈ E and so p :: η ∈∈ NE(N), which is what we wanted to show.

Figure 2 :

 2 Figure 2: Projection of global types onto participants.

2 and |σ 1 |

 1 = n -1 and p part(σ 1 ) and p ∈ part(α) 0 otherwise Then depth(G, p) = sup{depth(σ, p) | σ ∈ Tr + (G)} We say that a global type G is bounded if depth(G ′ , p) is finite for all subtrees G ′ of G and for all participants p.

Σ

  i∈I∪J p?λ i ; P i ≤ Σ i∈I p?λ i ; Q i = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =[ ≤-In] P i ≤ Q i i ∈ I i∈I p!λ i ; P i ≤ i∈I p!λ i ; Q i = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =[ ≤-Out]

Figure 3 :

 3 Figure 3: Preorder on processes and network typing rule.

Figure 4 :Example 6 . 8 .

 468 Figure 4: LTS for global types.

Lemma 6 . 9 .

 69 If G is a well-formed global type and G pqλ ---→ G ′ , then G ′ is a well-formed global type.

Theorem 6 . 12 (

 612 Progress). If ⊢ N : G and p[[ P ]] ∈ N, then N σ•α --→ N ′ and p ∈ part(α). Proof We prove by induction on d = depth(G, p) that: if ⊢ N : G and p[[ P ]] ∈ N, then G σ • α ---→ G ′ with p ∈ part(α). This will imply N σ • α ---→ N ′ by Session Fidelity (Theorem 6.11). Case d = 1. In this case G = q → r : ⊞ i∈I λ i ; G i and p ∈ {q, r} and G qrλ h ---→ G h for some h ∈ I by Rule [Ecomm]. Case d > 1. In this case G = q → r : ⊞ i∈I λ i ; G i and p {q, r}. By Lemma 6.5 this implies depth(G i , p) < d for all i ∈ I. Using Rule [Ecomm] we get G qrλ i ---→ G i for all i ∈ I. By Session Fidelity, N qrλ i ---→ N i and ⊢ N i : G i for all i ∈ I. Moreover, since p {q, r} we also have p[[ P ]] ∈ N i for all i ∈ I. By induction G i

Lemma 7 . 4 .Definition 7 . 5 (

 7475 Let σ be a pointed trace. If σ ∼ σ ′ , then σ ′ is a pointed trace and last(σ) = last(σ ′ ). Global event). Let σ = σ ′ • α be a pointed trace. Then γ = [σ] ∼ is a global event, also called g-event, with communication α, notation cm(γ) = α.

Definition 7 . 11 (

 711 Event structure of a global type). The event structure of the global type G is the triple S

Theorem 7 . 13 .

 713 The configurations are {γ 1 }, {γ 1 , γ 2 } and {γ 1 , γ 2 , γ 3 }, and there is a unique proving sequence corresponding to each configuration. Let G be a global type. Then S G (G) is a prime event structure.Proof We show that ≤ and # satisfy Properties (2) and (3) of Definition 3.1.

Figure 5 :

 5 Figure 5: FES of the network N.

Figure 6 :

 6 Figure 6: PES of the type G.

Lemma 8 . 5 .

 85 If N α -→ N ′ and ν ∈ NE(N), then ν = nec(α) or ν # nec(α) or α ♦ ν is defined.The following lemma, which is technically quite challenging as it involves reasoning about the fixpoint properties of the set of n-events of a network FES (as defined by the narrowing function), relates the sets of n-events of two network FESs, where one network is a one-step derivative of the other, by means of the retrieval and residual operators.Lemma 8.6. Let N α -→ N ′ . Then 1. {nec(α)} ∪ {α ♢ ν | ν ∈ NE(N ′ )} ⊆ NE(N);2. {α ♦ ν | ν ∈ NE(N) and α ♦ ν defined} ⊆ NE(N ′ ).

Theorem 8 . 7 .

 87 If N σ -→ N ′ , then nec(σ) is a proving sequence in S N (N). Proof The proof is by induction on σ. Base case. Let σ = α. From N α -→ N ′ and Lemma 8.6(1) nec(α) ∈ NE(N). Since nec(α) has no causes, by Definition 3.6 we conclude that nec(α) is a proving sequence in S N (N).

  there exists r :: η ∈ ν and r ::η ′ ∈ ν k = ν ′k such that η < η ′ , where r {p, q} because r ∈ loc(ν k ).Since nec(σ ′ ) is a proving sequence in S N (N ′′ ), by Lemma 5.24 there is ν ′ h ∈ NE(N ′′ ) such that r :: η ∈ ν ′ h . Since α ♢ r :: η = r :: η we get r :: η ∈ ν h . This implies ν h ≺ ν k , where ν h # ν by Lemma 5.21.

4 . 8 . 15 .

 4815 may now prove the correspondence between the traces labelling the transition sequences of a global type and the proving sequences of its PES. Let us stress the difference between the set of traces Tr + (G) of a global type G as defined at page 20 and the set of traces that label the transition sequences of G, which is a larger set due to the internal Rule [Icomm] of the LTS for global types given in Figure Theorem If G σ -→ G ′ , then gec(σ) is a proving sequence in S G (G).

  to the following semantic condition:Let ν 1 , ν 2 ∈ NE(N) and p :: ζ • π ∈ ν 1 and p :: ζ • π ′ ∈ ν 2 with π π ′ and q = pt(π) = pt(π ′ ). If ν 1 ≺ * ν ′ 1 for some ν ′ 1 ∈ NE(N) such that r ∈ loc(ν ′ 1 ) with r {p, q}, then ν 2 ≺ * ν ′ 2 for some ν ′ 2 ∈ NE(N) such that r ∈ loc(ν ′ 2 ).

  pqλ i ---→ G i by Rule[Ecomm] for all i ∈ I.If d > 1, then G = r → s : ⊞ h∈H λ ′′ h ; G ′ h with {p, q} ∩ {r, s} = ∅. By definition of projection G ↾ p = G ′ h ↾ p and G ↾ q = G ′ h ↾ q for all h ∈ H. By Lemma 6.5 depth(G, p) > depth(G ′ h , p) for all h ∈ H. Then by induction I = J, λ i = λ ′ i , → G i h , G i h ↾ p = P i and G i h ↾ q = Q i for all i ∈ I and all h ∈ H. Let G i = r → s : ⊞ h∈H λ ′′ h ; G i h . By Rule [Icomm] G pqλ i ---→ G i for all i ∈ I. By defini-tion of projection G i ↾ p = P i and G i ↾ q = Q i for all i ∈ I.

Lemma 6 . 9 Lemma B. 3 (Theorem 6 . 10 (

 693610 If G is a well-formed global type and G pqλ ---→ G ′ , then G ′ is a well-formed global type. Proof If G pqλ ---→ G ′ , by Lemma B.1(1) and (2) G ′ ↾ r is defined for all r. The proof that depth(G ′′ , r) is finite for all r and G ′′ subtree of G ′ is easy by induction on the transition rules of Figure4.The proofs of Subject Reduction and Session Fidelity rely on the Inversion andCanonical Form lemmas whose proofs are immediate.Lemma B.2 (Inversion). If⊢ N : G, then P ≤ G ↾ p for all p[[ P ]] ∈ N. Canonical Form). If ⊢ N : G and p ∈ part(G), then p[[ P ]] ∈ N and P ≤ G ↾ p . Subject Reduction) If ⊢ N : G and N α -→ N ′ , then G α -→ G ′ and ⊢ N ′ : G ′ . Proof Let α = pqλ. By Rule [Com] of Figure 1, N ≡ p[[ P ]] ∥ q[[ Q ]] ∥ N ′′ where P = i∈I q!λ i ; P i and Q = Σ j∈J p?λ j ; Q j and N ′ ≡ p[[ P h ]] ∥ q[[ Q h ]] ∥ N ′′ and λ = λ hfor some h ∈ I ∩ J. From Lemma B.2 we get 1.

Figure 3 , and 3 .Theorem 6 . 11 (C. Proofs of Section 7 Lemma 7 . 4

 33611774 Figure 3, and 3. R ≤ G ↾ r for all r[[ R ]] ∈ N ′′ . By Lemma B.1(1) G pqλ h ---→ G h and G h ↾ p = P ′ h and G h ↾ q = Q ′ h . By Lemma B.1(2)G h ↾ r = G ↾ r for all r {p, q}. We can then choose G ′ = G h . Theorem 6.11 (Session Fidelity) If ⊢ N : G and G α -→ G ′ , then N α -→ N ′ and ⊢ N ′ : G ′ .

  part(α ′ ) ∩ (part(α) ∪ part(σ 2 )) ∅ part(α) ∩ part(σ 2 ) ∅ Since part(α) ∩ part(α ′ ) = ∅,these two statements are respectively equivalent to:part(α ′ ) ∩ part(σ 2 ) ∅ part(α) ∩ (part(α ′ ) ∪ part(σ 2 )) ∅

  1

  only Rule [EComm] is fair, since there are no infinite transition sequences where some participant is stuck. This is due to the boundedness condition on global types. The second network of Example 5.15 and the network of Example 5.20 cannot be typed because they do not enjoy progress. Notice that the candidate global type for the second network of Example 5.15:

	Example 6.13.

  Case d > 1. Let G = r → s : ⊞ i∈I λ i ; G i and {r, s} ∩ {p, q} = ∅. By Definition 8.9(1)rsλ i • γ 1 is defined for all i ∈ I since {r, s} ∩ {p, q} = ∅. This implies rsλ i • γ 1 ∈ GE(G By Theorem 8.8, if ν 1 ; • • • ; ν n ; ν is a proving sequence of S N (N), then N ′ : G ′ . By Theorem 8.15 gec(σ • α) is a proving sequence of S G (G).By Theorem 8.16, if γ 1 ; • • • ; γ n ; γ is a proving sequence of S G (G), then G ′ . By applying iteratively Session Fidelity (Theorem 6.11) N

	N ′ . By applying iteratively Subject Reduction (Theorem 6.10) G	σ -→ G 0	σ -→ N 0 → G ′ and α -→ α -
	⊢ N σ -→
	G 0	α -→ G σ
	G	α -→ G h by rule [Ecomm].	Then

i ) for all i ∈ I by Lemma 8.11(2). By induction hypothesis G i α -→ G ′ i for all i ∈ I. Then we can apply rule [Icomm] to derive G α -→ r → s : ⊞ i∈I λ i ; G ′ i .

  q} ∩ {s, t} = ∅ [Icomm] s → t : ⊞ h∈H λ ′

h ; G h pqλ ---→ s → t : ⊞ h∈H λ ′ h ; G ′ h with G = s → t : ⊞ h∈H λ ′ h ; G h and G ′ = s → t : ⊞ h∈H λ ′ h ; G ′ h . By induction

Both FESs and PESs enjoy a graphical representation (see Figure5and Figure6), as opposed to

Unary networks will not be typable, and therefore, by Subject Reduction, a typable network will never evolve to a unary network. On the other hand, this will be possible for non typable networks.

In fact, every event of a PES occurs in a configuration.

For instance, we could have allowed events of the form {p :: η, * } to represent incomplete communications, and then prevented them from occurring by putting them in conflict with themselves. In this case, the event ν of Example 5.14 would have also been prevented from occurring because of its unique self-conflicting cause {p :: q?λ, * }, and we would not have needed the narrowing function.

This is a well-known issue in multiparty session types, which motivated the introduction of global types in[START_REF] Honda | Multiparty asynchronous session types[END_REF], see Section 6.

A prime configuration is a configuration with a unique maximal element, its culminating event.

In PESs, the prime configuration associated with an event is unique, while it is not unique in FESs and more generally in Stable ESs, just like a causal set.

Our choice operator for global types is less general than that of[START_REF] Tuosto | Semantics of global view of choreographies[END_REF].

Acknowledgment. We are strongly indebted to the anonymous referees for their constructive remarks, which helped us improve the submitted version of the paper.

This work was partially funded by the ANR17-CE25-0014-01 CISC project. 2 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).

By Definition 5.13 (1) we have N = p[[ P ]] ∥ q[[ Q ]] ∥ N 0 with q!λ ∈ PE(P) and p?λ ∈ PE(Q). Whence by Definition 4.3 (1) we get P = i∈I q!λ i ; P i and Q = Σ j∈J p?λ j ; Q j where λ = λ k for some k ∈ I ∩ J. Therefore

Case n > 1. Let ν 1 and N be as in the basic case, N ′′ = p[[ P k ]] ∥ q[[ Q k ]] ∥ N 0 and α = pqλ. Since ν 1 ; • • • ; ν n is a proving sequence, we have ¬(ν l # ν l ′ ) for all l, l ′ such that 1 ≤ l, l ′ ≤ n. Moreover, for all l, 2 ≤ l ≤ n we have ν l ν 1 = nec(α), thus α ♦ ν l is defined by Lemma 8.5. Let ν ′ l = α ♦ ν l for all l, 2 ≤ l ≤ n, then ν ′ l ∈ NE(N ′′ ) by Lemma 8.6 [START_REF] Baier | The connection between an event structure semantics and an operational semantics for TCSP[END_REF].

We show that ν ′ 2 ; • • • ; ν ′ n is a proving sequence in S N (N ′′ ). First notice that for all l, Lemma 8.2(5) and (1). Let now ν ≺ ν ′ h for some h, 2 ≤ h ≤ n. By Lemma 8.2(3) and (1) α ♢ ν ≺ α ♢ (α ♦ ν h ) = ν h . This implies by Definition 3.6 that there is

Therefore, since ν ′ l is defined for all l, 2 ≤ l ≤ n, we get either ν = ν ′ h ′ by Lemma 8.2 [START_REF] Baier | The connection between an event structure semantics and an operational semantics for TCSP[END_REF] or ν # ν ′ h ′ ≺ ν ′ h by Lemma 8.2 [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF] and [START_REF] Barbanera | Composition and decomposition of multiparty sessions[END_REF].

By induction

is the required transition sequence.

Relating Transition Sequences of Global Types and Proving Sequences of their ESs

In this subsection, we relate the traces that label the transition sequences of global types with the configurations of their PESs. As for n-events, we need retrieval and residual operators for g-events. The first operator was already introduced in Definition 7.6, so we only need to define the second one, which is given next. Definition 8.9 (Residual of g-events after communications).

1. The residual operator • applied to a communication and a g-event is defined by:

The operator • naturally extends to traces:

The operator •, applied to a communication and a g-event, gives the g-event obtained by erasing the communication, if it occurs in head position (modulo ∼) in the given g-event, and leaves the g-event unchanged if its participants are disjoint from those of the communication. Note that the operator α • [σ] ∼ is undefined whenever either [σ] ∼ = {α} or one of the participants of α occurs in σ but the first communication of σ is different from α. For example pqλ • [pqλ] ∼ and pqλ • [pqλ ′ • σ] ∼ with λ λ ′ are undefined for any σ.

The following lemma gives some simple properties of the retrieval and residual operators for g-events. The first five statements correspond to those of Lemma 8.2

for n-events. The last three statements give properties that are relevant only for the operators • and •.

Case n > 1. Let G α -→ G ′′ be the transition as obtained from the base case. We show that α • γ j is defined for all j, 2 ≤ j ≤ n. If α • γ k were undefined for some k, 2 ≤ k ≤ n, then by Definition 8.9(1) either

In the second case α @ p # σ @ p or α @ q # σ @ q, which implies γ k # γ 1 . So both cases are impossible. If α • γ j is defined, by Lemma 8.12(2) we get

We show that γ ′ 2 ;

2 ≤ j ≤ n. By Lemma 8.10(1) γ j = α • γ ′ j for all j, 2 ≤ j ≤ n. Then by Lemma 8.10(5) no two events in the sequence γ ′ 2 ;

The last ingredient required to prove our main theorem is the following separation result from [START_REF] Boudol | Flow models of distributed computations: event structures and nets[END_REF] (Lemma 2.8 p. 12):

Lemma 8.17 (Separation [START_REF] Boudol | Flow models of distributed computations: event structures and nets[END_REF]). Let S = (E, ≺, # ) be a flow event structure and X, X ′ ∈ C(S) be such that X ⊂ X ′ . Then there exist e ∈ X ′ \X such that X ∪ {e} ∈ C(S).

We may now finally show the correspondence between the configurations of the FES of a network and the configurations of the PES of its global type. Let ≃ denote isomorphism on domains of configurations. Proof By Theorem 8.8 if

By applying iteratively Session Fidelity (Theorem 6.11)

Therefore we have a bijection between D(S N (N)) and D(S G (G)), given by nec(σ) ↔ gec(σ) for any σ generated by the (bisimilar) LTSs of N and G.

We show now that this bijection preserves inclusion of configurations. By Lemma 8.17 it is enough to prove that if

where

) and α = cm(ν) = cm(γ) by Lemmas 8.4 and 8.14.

still not be sufficient in general to ensure typability. We plan to further investigate this question in the near future.

Appendices A. Proofs of Section 5

This section contains the proofs of Lemmas 5.18, 5.21 and 5.24.

Lemma 5.18 Let ν and ν ′ be binary n-events with loc(ν) = loc(ν ′ ). Then ν # ν ′ iff p :: η ∈ ν and p ::

Proof The "if" direction holds by Definition 5.7(2a). We show the "only-if" direction. First observe that for any n-event ν = {p :: η 1 , q :: η 2 } the condition p :: η 1 q :: η 2 of Definition 5.5 implies η 1 ↱ q η 2 ↱ p by Definition 5.4, which in turn implies |η 1 ↱ q | = |η 2 ↱ p | by Definition 5.3. If ν is a binary event, we also have

2, since all the actions of η 1 involve q and all the actions of η 2 involve p, and thus the projections do not erase actions.

Assume now ν ′ = {p :: η ′ 1 , q :: η ′ 2 }. We consider two cases (the others being symmetric):

-

the above remark about binary events, we get

Then we may conclude, Proof Let p :: η ∈ (ν ∩ ν ′ ) and loc(ν) = loc(ν ′ ) = {p, q}. Then there must exist η 0 , η ′ 0 such that q :: η 0 ∈ ν and q :: η ′ 0 ∈ ν ′ . From p :: η q :: η 0 and p :: η q :: η ′ 0 it follows that η 0 ↱ p = η ′ 0 ↱ p . This, in conjunction with the fact that pt(act(η 0 )) = pt(act(η ′ 0 )) = p, implies that neither η 0 < η ′ 0 nor η ′ 0 < η 0 . Thus η 0 # η ′ 0 and therefore ν # ν ′ by Definition 5.7.

Lemma 5. [START_REF] Cristescu | Rigid families for CCS and the π-calculus[END_REF] If X is a configuration of S N (N) and ν ∈ X, then there is a unique causal set E of ν such that E ⊆ X.

Proof By Definition 5.11, if ν ∈ NE(N), then ν has at least one causal set included

Moreover, if p :: η ∈ ν and η ′ < η, then by Lemma 5.21 there is at most one ν ′′ ∈ E ′ such that p :: η ′ ∈ ν ′′ . Therefore, E ′ ⊆ E for some causal set E of ν by Definition 5.9.

We show that E ⊆ E ′ . Assume ad absurdum that ν 0 ∈ E\E ′ . By definition of causal set, ν 0 ≺ ν. By definition of E ′ , ν 0 E ′ implies ν 0 X. By Definition 3.4 this implies

Then ν 1 ∈ E ′ by definition of E ′ , and thus ν 1 ∈ E. Hence ν 0 , ν 1 ∈ E and ν 0 # ν 1 , contradicting Definition 5.9.

B. Proofs of Section 6

This section contains the proofs of Lemmas 6.6, 6.9, Theorems 6. Proof We redefine the projection ↓ r as the largest relation between global types and processes such that (G, P) ∈↓ r implies:

The equality E of processes is the largest symmetric binary relation R on processes such that (P, Q) ∈ R implies:

It is then enough to show that the relation

satisfies Clauses (a) and (b) (with R replaced by R r ), since this will imply R r ⊆ E.

Note first that (0, 0) ∈ R r because (End, 0) ∈↓ r , and that (0, 0) ∈ E because Clauses (a)

and (b) are vacuously satisfied by the pair (0, 0). The proof is by induction on d = depth(G, r). We only consider Clause (b), the proof for Clause (a) being similar.

So, assume (P, Q) ∈ R r and P = Σ i∈I p?λ i ; P i .

Case d = 1. In this case G = p → r : ⊞ i∈I λ i ; G i and P = Σ i∈I p?λ i ; P i and (G i ,

Hence Q has the required form and (P i , Q i ) ∈ R r for all i ∈ I.

Case d > 1. In this case G = p → q : ⊞ j∈J λ ′ j ; G j and r {p, q} and (G j , P) ∈↓ r for all

We need a lemma relating the projections of a well-formed global type with its transitions.

Lemma B.1.

Let G be a well-formed global type.

D. Proofs of Subsection 8.1

This section contains the proofs of Lemmas 8.2, 8.4, 8.5 and 8.6.

Lemma 8.2 (Properties of retrieval and residual for n-events).

Proof For ( 1) and ( 2) it is enough to show the corresponding properties for located events.

(1) Since α ♦ (p :: η) is defined, we have η = (α@p ) • η ′ and α ♦ (p :: η) = p ::

(2) Since α ♢ (p :: η) = p :: (α@p ) • η is always defined, we immediately get

(3) Let ν ≺ ν ′ . By Definition 5.7(1), there are p :: η ∈ ν and p ::

(4) As in the previous case, there are p :: η ∈ ν and p ::

Since both α ♦ ν and α ♦ ν ′ are defined, there exist η 0 and η ′ 0 such that η = (α@p ) • η 0 and η ′ = (α@p ) • η ′ 0 and α ♦ (p :: η) = p :: η 0 and α ♦ (p ::

(5) Let ν # ν ′ . If Clause (2a) of Definition 5.7 applies, then there are p :: η ∈ ν and p ::

If Clause (2b) of Definition 5.7 applies, then there are p :: η ∈ ν and q ::

The proof is similar to that of Point [START_REF] Bednarczyk | Categories of Asynchronous Systems[END_REF], considering that α ♦ ν and α ♦ ν ′ are defined.

(7) Let α ♢ ν # α ♢ ν ′ . If Clause (2a) of Definition 5.7 applies, then there are p :: η ∈ ν and p ::

Clause (2b) of Definition 5.7 applies, then there are p ::

It follows that η 0 = (α@p ) • η and η ′ 0 = (α@q ) • η ′ and p :: η ∈ ν and q ::

{p, q}, then (α@p ) ↾ q = ϵ = (α@q ) ↾ p and thus

In both cases we conclude that ν # ν ′ .

Lemma 8.4 (Properties of nec(•))

2. ¬(nec(α) # α ♢ ν) for all ν.

Proof (1a) Immediate from Definition 8.3, since cm(σ ♢ ν) = cm(ν) for any event ν.

(1b) We show that neither Clause (2a) nor Clause (2b) of Definition 5.7 can be used to derive ν h # ν k . Notice that ν i = {p i :: σ[1 ... i]@p i , q i :: σ[1 ... i]@q i }. So if p :: η ∈ ν h and p :: η ′ ∈ ν k with h < k, then either η < η ′ or η = η ′ . Therefore Clause (2a) does not apply. If p :: η ∈ ν h and q :: η ′ ∈ ν k and p q and |η ↾ q

) cannot be used.

(2) We show that neither Clause (2a) nor Clause (2b) of Definition 5.7 can be used to derive nec(α) # α ♢ ν. Let part(α) = {p, q}. Then nec(α) = {p :: α@p , q :: α@q }.

Note that p :: η ∈ α ♢ ν iff η = (α@p ) • η ′ and p :: η ′ ∈ ν. Since α@p < (α@p ) • η ′ , Clause (2a) of Definition 5.7 cannot be used. Now suppose r :: η ∈ α ♢ ν for some r {p, q}. In this case (α@p ) ↾ r = (α@q ) ↾ r = ϵ. Therefore, since ϵ ϵ, Clause (2b) of Definition 5.7 does not apply.

(

Then, by Definition 8.3

Proof Let nec(α) = {p :: α@p , q :: α@q } and ν = {r :: η, s ::

There are 2 possibilities:

• {r, s} ∩ {p, q} = ∅. Then α@r = α@s = ϵ and α ♦ ν = ν;

• {r, s} ∩ {p, q} ∅. Suppose r = p. There are three possible subcases:

1. η = π • ζ with π α@p . Then r :: η # p :: α@p and thus ν # nec(α);

2. η = α@p . Then either η ′ = α@q and ν = nec(α), or η ′ α@q and ν # nec(α) by Lemma 5.21;

3. η = (α@p ) • η 0 . Then α ♦ p :: η = p :: η 0 . Now, if s q we have α ♦ s :: η ′ = s :: η ′ , and thus α ♦ ν = {p :: η 0 , s :: η ′ }. Otherwise, ν = {p :: (α@p ) • η 0 , q :: η ′ }. By Definition 5.5 p :: (α@p ) • η 0 q :: η ′ , which implies η ′ = (α@q ) • η ′ 0 for some η ′ 0 .

where for some k ∈ (I ∩ J) we have λ k = λ and

We first show that RT ⊆ CE(N). • {r, s} ∩ {p, q} ∅. Suppose r = p. Then η ∈ PE(P k ) and p :: q!λ k • η ∈ α ♢ ν and q!λ k • η ∈ PE( i∈I q!λ i ; P i ). There are two subcases:

By

s = q. Then η ′ ∈ PE(Q k ) and q :: p?λ k • η ′ ∈ α ♢ ν and q!λ k • η ′ ∈ PE(Σ j∈J p?λ j ; Q j ). We have α ♢ ν = {p :: q!λ k • η, q :: p?λ k • η ′ } ∈ CE(N); -s q. Then α ♢ s :: η ′ = s :: η ′ , and thus α ♢ ν = {p :: q!λ k • η, s ::

Therefore in all cases RT ⊆ CE(N). We want now to show that RT ⊆ NE(N).

Recall from Section 5 that NE(N) is the greatest fixed point of the function

Then NE(N) is also the greatest post-fixed point of f CE(N) (X), namely the greatest X such that X ⊆ f CE(N) (X). Therefore, to show that RT ⊆ NE(N), it is enough to show that RT is also a post-fixed point of f CE(N) (X), namely that RT ⊆ f CE(N) (RT).

Consider first the event nec(α). Since the only causal set of nec(α) in any set is ∅, it is immediate that nec(α) ∈ f CE(N) (RT). Consider now α ♢ ν ∈ RT for some ν ∈ NE(N ′ ) with loc(ν) = {r, s}. Define

We show that pre(α, E, ν) is a causal set of α ♢ ν in RT, namely that it is a minimal subset of RT satisfying Conditions (1) and (2) of Definition 5.9.

Condition (1) If nec(α) ∈ pre(α, E, ν), then {r, s} ∩ {p, q} ∅. A conflict between nec(α) and any other event of pre(α, E, ν) ∪ {α ♢ ν} can only be derived by Clause (2a) of Definition 5.7, since nec(α) = {p :: q!λ, q :: p?λ} and (α@p ) ↾ t = (α@q ) ↾ t = ϵ for all t {p, q}. Suppose r = p. Then p :: q!λ • η ∈ α ♢ ν. Since q!λ < q!λ • η, Clause (2a) cannot be used to derive a conflict nec(α) # α ♢ ν. Similarly, if α ♢ ν 1 ∈ pre(α, E, ν) and p :: [START_REF] Boudol | On the semantics of concurrency: partial orders and transition systems[END_REF].

We show that if η 0 < (α@r ) • η, then r :: η 0 ∈ ν 0 for some ν 0 ∈ pre(α, E, ν). From

, then it must be η 0 = α@r ϵ and thus r ∈ {p, q}.

In this case {nec(α)} ∈ pre(α, E, ν) and thus r :: η 0 ∈∈ pre(α, E, ν).

As for minimality , we first show that

Assume that r :: η ′ r ∈ ν ′ with η ′ r < η r (the proof is similar for s). By Condition (2), there is ν ′′ ∈ E ′ such that r :: η ′ r ∈ ν ′′ . But then ν ′ # ν ′′ by Lemma 5.21, contradicting the fact that pre(α, E, ν) verifies Condition (1). Therefore pre(α, E, ν) is minimal.

( • {r, s} ∩ {p, q} ∅. Suppose r = p. Then η ∈ PE( i∈I q!λ i ; P i ) and since α ♦ ν is defined we have that η = q!λ k • η k where η k ∈ PE(P k ). There are two subcases:

In this case we have α ♦ ν = {p ::

s q. Then α ♦ s :: η ′ = s :: η ′ , and thus α ♦ ν = {p :: η k , s ::

Therefore in all cases RS ⊆ CE(N ′ ). We want now to show that RS ⊆ NE(N ′ ).

We proceed as in the proof of Statement (1). We know that NE(N ′ ) is the greatest post-fixed point of the function

We show that post(α, E, ν) is a causal set of α ♦ ν in RS, namely that it is a minimal subset of RS satisfying Conditions (1) and (2) of Definition 5.9. Lemma 8.2(5) and (1).

Condition (2) Since ν = {r :: η, s :: η ′ } and α ♦ ν is defined, we have η = (α@r ) • η r and η ′ = (α@s ) • η s and α ♦ ν = {r :: η r , s ::

As for minimality, we first show that

of Definition 5.9 for α ♦ ν.

Assume that r ::

there is ν ′′ ∈ E ′ such that r :: η ′ r ∈ ν ′′ . But then ν ′ # ν ′′ by Lemma 5.21, contradicting the fact that post(α, E, ν) verifies Condition (1). Therefore post(α, E, ν) is minimal.

E. Proofs of Subsection 8.2

This section contains the proofs of Lemmas 8.10, 8.11 and 8.12.

Lemma 8.10 (Properties of retrieval and residual for g-events).

(2) By Definition 7.6 either α

∅, and we have α

(

for some σ 1 by Definition 7.6 (1). Then this case is impossible.

(8) Let γ = [σ] ∼ . By Definitions 7.6(1) and 8.9(1) we have four cases:

Lemma 8.11

The following hold:

where k ∈ I.

Proof (2) By Definition 7.11(1) γ ∈ GE(p → q : ⊞ i∈I λ i ; G i ) implies γ = ev(σ) for some

) by Definition 8.9(1). In the first case

In the second case σ ′′ ∈ Tr + (G k ) for some σ ′′ ∼ σ ′ by definition of projection, which prescribes the same behaviours to all participants different from p, q, see Figure 2. We conclude pqλ k • γ ∈ GE(G k ) by Definition 7.11 (1).

Proof Both proofs are by induction on the inference of the transition

(1) For rule [Ecomm] we get G = p → q : ⊞ i∈I λ i ; G i and G ′ = G k and α = pqλ k for some k ∈ I. We conclude α • γ ∈ GE(G) by Lemma 8.11 (1).

For rule [Icomm] we get G = p → q : ⊞ i∈I λ i ; G i and G ′ = p → q : ⊞ i∈I λ i ; G ′ is defined unless σ 0 = pqλ k by Definition 8.9(1). We consider two cases.

(2) For rule [Ecomm] we get G = p → q : ⊞ i∈I λ i ; G i and G ′ = G k and α = pqλ k for some k ∈ I. We conclude α • γ ∈ GE(G ′ ) by Lemma 8.11(2).

For rule [Icomm] we get G = p → q : ⊞ i∈I λ i ; G i and G = p → q : ⊞ i∈I λ i ; G ′ We first show that α • γ ′ is defined. Since α • γ and pqλ k • γ are defined, by Definition 8.9(1) we have four cases:

(a) σ 0 ∼ α • σ 1 for some σ 1 and σ

In case (a)

pqλ k • γ ′ = γ. Therefore from α • γ defined we have α • (pqλ k • γ ′ ) defined.

Since α • γ ′ is also defined and part(α) ∩ {p, q} = ∅, by Lemma 8.10(8) we get

F. Glossary of Symbols and