Luís Caires

Jorge A Pérez

Multiparty Session Types Within A Canonical Binary Theory, and Beyond

A widespread approach to software service analysis uses session types. Very different type theories for binary and multiparty protocols have been developed; establishing precise connections between them remains an open problem. We present the first formal relation between two existing theories of binary and multiparty session types: a binary system rooted in linear logic, and a multiparty system based on automata theory. Our results enable the analysis of multiparty protocols using a (much simpler) type theory for binary protocols, ensuring protocol fidelity and deadlock-freedom. As an application, we offer the first theory of multiparty session types with behavioral genericity. This theory is natural and powerful; its analysis techniques reuse results for binary session types.

Introduction

The purpose of this paper is to demonstrate, in a precise technical sense, how an expressive and extensible theory of multiparty systems can be extracted from a basic theory for binary sessions, thus developing the first formal connection between multiparty and binary session types. Our approach relies on a theory of binary session types rooted in linear logic and on medium processes that capture the behavior of global types.

Relating the global behavior of a distributed system and the components that implement it is a challenging problem in many scenarios. This problem is also important in the analysis of software services, where the focus is on message-passing programs with advanced forms of concurrency and distribution. Within language-based techniques, notable approaches include interface contracts (cf. [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF]) and behavioral types [START_REF] Huttel | Foundations of session types and behavioural contracts[END_REF]. Our interest is in the latter: by classifying behaviors (rather than values), behavioral types abstract structured protocols and enforce disciplined communication exchanges.

Session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF] are a much-studied class of behavioral types. They organize multiparty protocols as sessions, basic units of structured conversations. Several session typed frameworks have been developed (see [START_REF] Huttel | Foundations of session types and behavioural contracts[END_REF] for an overview). This diversity makes it hard to compare their associated techniques, and hinders the much desirable transfer of techniques between different typed models.

In this paper, we formally relate two distinct typed models for structured communications. By relying on a type theory of binary sessions rooted in linear logic [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF], we establish natural bridges between typed models for binary and multiparty sessions [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]. Our results reveal logically motivated justifications for key concepts in typed models of global/local behaviors, and enable the transfer of reasoning techniques from binary to multiparty sessions. In fact, our approach naturally enables us to define the first model of multiparty session types with parametric polymorphism, which in our setting means behavioral genericity (i.e., passing first-class behavioral interfaces in messages), not just datatype genericity. This new model is very powerful; we equip it with analysis techniques for behavioral genericity by reusing results for binary session types [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF].

Binary protocols [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] involve two partners, each abstracted by a behavioral type; correct interactions rely on compatibility, i.e., when one partner performs an action, the other performs a complementary one. Multiparty protocols may involve more than two partners: there is a global specification to which all of them, from their local perspectives, should adhere. In multiparty session types [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF], these visions are described by a global type and local types, respectively; a projection function relates the two. Previous research shows that type systems for multiparty protocols have a more involved theory than binary ones. For instance, the analysis of deadlock-freedom in multiparty protocols is challenging [START_REF] Coppo | Global progress for dynamically interleaved multiparty sessions[END_REF], and certainly harder than for binary protocols.

The question is then: could multiparty session types be reduced into binary ones? Defining such a reduction is far from trivial, as it should satisfy at least two requirements. First, the resulting collection of binary interactions must preserve crucial sequencing information among multiparty exchanges. Second, it should avoid undesirable behaviors: synchronization errors, deadlocks, non-terminating reductions.

This paper answers the above question in the affirmative. We tightly relate: (i) a standard theory of multiparty session types [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF], and (ii) the theory of deadlock-free binary session types proposed in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. The key device in our approach is the medium process of a multiparty protocol.

Given a global type G, its medium process M G is an entity that mediates in all communications. Therefore, M G extracts the semantics of G, uniformly capturing its sequencing information. Process M G is meant to interact with well-typed implementations for all participants declared in G. This way, for instance, given the global type G = p q:{l i U i .G i } i∈I (i.e., a labeled, directed exchange from p to q, indexed by I, which precedes execution of a protocol G i ), its medium M G first receives a label l j and message of type U j sent by p's implementation (with j ∈ I); then, it forwards these two objects to q's implementation; lastly, it executes process M G j .

Interestingly, our medium-based approach applies to global types with name passing, delegation, and parallel composition. To fully characterize a global type G, we determine the conditions under which M G may be well-typed using binary session types, with respect to its local types. A key ingredient here is the theory for binary session types introduced in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. Due to their logical foundations, typability in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] entails: fidelity (protocols are respected), safety (absence of communication errors), deadlockfreedom (processes do not get stuck), and termination (infinite internal behavior is ruled out). Most relevant for our approach is deadlock-freedom, not directly ensured by alternative type systems.

Here we present an analysis of multiparty session types using a theory of binary session types, ensuring fidelity and deadlock-freedom. Our technical contributions are:

• Characterization results relating (a) a global type that is well-formed (correct projectability) and (b) typability of its medium using binary session types (Thms. 4-5).

• Operational correspondence results relating (a) the behavior of a global type and (b) the behavior of its medium (instrumented in a natural way) composed with welltyped implementations for each local type (Thm. 7). These results confirm that our analysis does not introduce extra sequentiality in protocols. • A proof that behavioral transformations of global types [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF] can be justified by typed equalities for binary sessions [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF] expressed at the level of mediums (Thm. 6). This result offers a deep semantic justification of structural identities on global types, such as those capturing parallelism via interleaving of causally independent exchanges. • Transfer of techniques from binary to multiparty protocols. We define the first theory of multiparty session types with behavioral genericity; its analysis techniques reuse the binary session type theory with parametric polymorphism given in [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF].

Our results define the first formal relation between multiparty and binary session types. They highlight the fundamental character of the notions involved, since they can be independently explained by communicating automata (cf. [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]) and linear logic (cf. [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]).

Next, we collect definitions on multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF] and binary sessions [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. Our technical contributions are reported in § 3. In §4 we illustrate these contributions by means of an example that features non-trivial forms of replication and sharing. In § 5 we introduce multiparty session types with behavioral genericity, and in § 6 we illustrate our approach in the analysis of a multiparty protocol. § 7 concludes and discusses related works.

Preliminaries: Binary and Multiparty Session Types

Binary Session Types. We build upon the theory of binary session types of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Toninho | Corecursion and Non-Divergence in Session Types[END_REF], based on an interpretation of session types as linear logic propositions. We assume no background on linear logic from the reader; we refer to [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] for further details. The Process Model. We define a synchronous π-calculus [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF] with forwarding and nary labeled choice. We use l 1 , l 2 , . . . to range over labels. Given an infinite set Λ of names (x, y, z, u, v), the set of processes (P, Q, R) is defined by

P ::= 0 | P | Q | (νy)P | x y.P | x(y).P | !x(y).P | x l i ; P | x {l i : P i } i∈I | [x ↔ y]
Operators 0 (inaction), P | Q (parallel composition), and (νy)P (restriction) are standard. We have x y.P (send y on x, proceed as P ), x(y).P (receive a z on x, proceed as P with y replaced by z), and the replicated input !x(y).P . Operators x l ; P and x {l i :P i } i∈I define labeled choice [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF]. Forwarding [x ↔ y] equates x and y; it is a copycat process, similar to wires in [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF]. Also, x(y) denotes the bound output (νy)x y.

In restriction (νy)P and input x(y).P the occurrence of name y is binding, with scope P . The set of free names of a process P is denoted fn(P ). In a statement, a name is fresh if it is not among the names of the objects (processes, actions, etc.) of the statement. A process is closed if it does not contain free occurrences of names. We identify processes up to consistent renaming of bound names. The capture-avoiding substitution of x for y in P is denoted P { x /y}. Notation k denotes a finite sequence of pairwise distinct names k 1 , k 2 , • • • . We sometimes treat sequences of names as sets. Reduction expresses the internal behavior of processes. Closed under structural congruence (noted ≡, see [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]), it is the binary relation on processes defined by the rules:

x y.Q | x(z).P → Q | P { y /z} x y.Q | !x(z).P → Q | P { y /z} | !x(z).P (νx)([x ↔ y] | P ) → P { y /x} Q → Q ⇒ P | Q → P | Q P → Q ⇒ (νy)P → (νy)Q x l j ; P | x {l i : Q i } i∈I → P | Q j (j ∈ I)
The interaction of a process with its environment is defined by an early labeled transition system (LTS) for the π-calculus [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF], extended with labels and transition rules for choice and forwarding. Transition P λ -→ Q says that P may evolve to Q by performing the action represented by label λ, defined as:

λ ::= τ | x(y) | x l | x y | x(y) | x l .
Actions are the input x(y), the offer x l , and their co-actions: the output x y and bound output x(y) actions, and the selection x l , resp. The bound output x(y) denotes extrusion of y along x. Internal action is denoted τ . Session Types as Linear Logic Propositions. The type theory of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] connects session types as linear logic propositions. Main properties derived from typing, absent from other binary session type theories, are global progress (deadlock-freedom) and termination [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF]. The syntax of binary types is as follows:

Definition 1 (Binary Types). Types (A, B, C) are given by A, B ::

= 1 | !A | A ⊗ B | A B | {l i : A i } i∈I | ⊕{l i : A i } i∈I
We use A ⊗ B (resp. A B) to type a name that performs an output (resp. an input) to its partner, sending (resp. receiving) a name of type A, and then behaves as type B. Thus, A⊗B and A B represent the session types !A; B and ?A; B introduced in [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF].

We generalize [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] by considering n-ary offer and choice ⊕. Given a finite index set I, {l i :A i } i∈I types a name that offers a choice between an l i . Dually, ⊕{l i :A i } i∈I types the selection of one of the l i . Type !A types a shared channel, used by a server to spawn an arbitrary number of new sessions (possibly none), each one conforming to A. Type 1 is the terminated session; names of type 1 may be passed around as opaque values.

A type environment collects type assignments of the form x:A, where x is a name and A is a type, the names being pairwise disjoint. We consider two typing environments, subject to different structural properties: a linear part ∆ and an unrestricted part Γ , where weakening and contraction principles hold for Γ but not for ∆.

A type judgment Γ ; ∆ P :: z:C asserts that P provides behavior C at channel z, building on "services" declared in Γ ; ∆. This way, e.g., a client Q that relies on external services and does not provide any is typed as Γ ; ∆ Q :: z:1. The domains of Γ, ∆ and z:C are required to be pairwise disjoint. We write dom(Γ ) (resp. dom(∆)) to denote (T L 2 ) Γ ; ∆, x: {l i :A i } i∈I P :: z:C k ∈ I Γ ; ∆, x: {l j :A j } j∈I∪{k} P :: z:C Fig. 2. The Type System for Binary Sessions (Excerpt). the domain of Γ (resp. ∆), a sequence of names. Empty environments are denoted ' • '. As π-calculus terms are considered up to structural congruence, typability is closed under ≡ by definition. We sometimes abbreviate Γ ; ∆ P :: z:1 as Γ ; ∆ P . Fig. 2 presents selected typing rules; see [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] for a full account. We have right and left rules: they say how to implement and use a session of a given type, respectively. We briefly comment on some of the rules. Rule (Tid) defines identity in terms of forwarding. Rule (Tcut) define typed composition via parallel composition and restriction. Implementing a session type {l i :A i } i∈I amounts to offering a choice between n sessions with type A i (Rule (T R)); its use on name x entails selecting an alternative, using prefix x l j (Rules (T L 1 ) and (T L 2 )). Type ⊕{l i : A i } i∈I has a dual interpretation.

We now recall some main results for well-typed processes. For any P , define live(P ) iff P ≡ (ν n)(π.Q | R), for some names n, a process R, and a non-replicated guarded process π.Q. Also, we write P ⇓, if there is no infinite reduction path from process P .

Theorem 1 (Properties of Well-Typed Processes).

1. Subject Reduction [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]: If Γ ; ∆ P :: x:A and P → Q then Γ ; ∆ Q::x:A. 2. Global Progress [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]: If •; • P ::z:1 and live(P ) then exists a Q such that P → Q. [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF]: If Γ ; ∆ P :: x:A then P ⇓.

Termination / Strong Normalization

Theorem 1 [START_REF] Bonelli | Correspondence assertions for process synchronization in concurrent communications[END_REF], key in our work, implies that our type discipline ensures deadlock freedom. Further properties of well-typed processes concern proof conversions and typed behavioral equivalences. The correspondence in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] is realized by relating proof conversions in linear logic with appropriate process equivalences. There is a group of commuting conversions that induces a behavioral congruence on typed processes, noted c . Process equalities justified by c include, e.g., (see [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF] for details):

Γ ; ∆, y:A ⊗ B (νx)(P | y(z).Q) c y(z).(νx)(P | Q) :: z:C Γ ; ∆, y:A B (νx)(P | y(z).(Q | R)) c y(z).(Q | (νx)(P | R)) :: T Γ ; ∆, y: {l i :A i } i∈I (νx)(P | y l i ; Q) c y l i ; (νx)(P | Q) :: T
These equalities reflect a behavioral equivalence over session-typed processes, called context bisimilarity (noted ≈) [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF]. Roughly, typed processes Γ ; ∆ P :: x:A and Γ ; ∆ Q :: x:A are context bisimilar if, once composed with their requirements (described by Γ, ∆), they perform the same actions on x (as described by A). Context bisimilarity is a congruence relation on well-typed processes. We have:

Theorem 2 ([19]). If Γ ; ∆ P c Q :: z:C then Γ ; ∆ P ≈ Q :: z:C.
Multiparty Session Types. Our syntax of global types includes constructs from [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]. With respect to [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF], we consider value passing in branching (cf. U below), fully supporting delegation and add parallel composition. Below, participants are ranged over by p, q, r, . . .; labels are ranged over by l 1 , l 2 , . . .. To streamline the presentation, we consider standard global types without recursion. Our approach extends to global types with recursion, exploiting the extension of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] with co-recursion [START_REF] Toninho | Corecursion and Non-Divergence in Session Types[END_REF]. Results for global types with recursion can be found in an online technical report [START_REF] Caires | A typeful characterization of multiparty structured conversations based on binary sessions[END_REF].

Definition 2 (Global/Local Types). Define global types (G) and local types (T ) as

G ::= end | p q:{l i U i .G i } i∈I | G 1 | G 2 U ::= bool | nat | str | . . . | T T ::= end | p?{l i U i .T i } i∈I | p!{l i U i .T i } i∈I
G denotes the above set of global types. Given a finite I and pairwise different labels, p q:{l i U i .G i } i∈I specifies that by choosing label l i , participant p may send a message of type U i to participant q, and then continue as G i . We decree p = q, so reflexive interactions are disallowed. The global type G 1 | G 2 allows the concurrent execution of G 1 and G 2 . We write end to denote the completed global type. The local type p?{l i U i .T i } i∈I denotes an offer of a set of labeled alternatives; the local type p!{l i U i .T i } i∈I denotes a behavior that chooses one of such alternatives. The terminated local type is end. Following [START_REF] Honda | Multiparty asynchronous session types[END_REF], there is no local type for parallel.

Example 1. Consider a global type G BS , a variant of the the two-buyer protocol in [START_REF] Honda | Multiparty asynchronous session types[END_REF], in which two buyers (B 1 and B 2 ) coordinate to buy an item from a seller (S):

G BS = B 1 S: send str .S B 1 :{rep int .S B 2 :{rep int . B 1 B 2 :{shr int .B 2 S:{ok 1 .end , quit 1 .end}}}}
Intuitively, B 1 requests the price of an item to S, who replies to B 1 and B 2 . Then B 1 communicates to B 2 her contribution in the transaction; finally, B 2 either confirms the purchase to S or closes the transaction.

We now define projection for global types. Following [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF], projection relies on a merge operator on local types, which in our case considers messages U . Definition 3 (Merge). We define as the commutative partial operator on base and local types such that: 1. bool bool = bool (and similarly for other base types); 2.

end end = end; 3. p!{l i U i .T i } i∈I p!{l i U i .T i } i∈I = p!{l i U i .T i } i∈I ; and 4. p?{l k U k .T k } k∈K p?{l j U j .T j } j∈J = p? {l k U k .T k } k∈K\J ∪ {l j U j .T j } j∈J\K ∪ {l l U l U l .(T l T l )} l∈K∩J
and is undefined otherwise. Therefore, for U 1 U 2 to be defined there are two options: (a) U 1 and U 2 are identical base, terminated or selection types; (b) U 1 and U 2 are branching types, but not necessarily identical: they may offer different options but with the condition that the behavior in labels occurring in both U 1 and U 2 must be mergeable. The set of participants of

(SW1) {p1, q1}#{p2, q2} p1 q1: li Ui .p2 q2:{l j U j .Gij}j∈J i∈I sw p2 q2: l j U j .p1 q1:{li Ui .Gij}i∈I j∈J (SW2) {p, q}#part(G1) ∀i, j ∈ I.G 1 i = G 1 j p q:{li Ui .(G 1 i | G 2 i )}i∈I sw G 1 1 | p q: li Ui .G 2 i }i∈I
G (part(G)) is defined as: part(end) = ∅, part(G 1 | G 2 ) = part(G 1 ) ∪ part(G 2 ), part(p q:{l i U i .G i } i∈I ) = {p, q} ∪ i∈I part(G i ).
Definition 4 (Projection [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]). Let G be a global type. The projection of G under participant r, denoted G r, is defined as: end r = end and

• p q:{l i U i .G i } i∈I r =      p!{l i U i .G i r} i∈I if r = p p?{l i U i .G i r} i∈I if r = q i∈I G i r otherwise ( as in Def. 3) • (G 1 | G 2 ) r = G i r if r ∈ part(G i ) and r ∈ part(G j ), i = j ∈ {1, 2} end if r ∈ part(G 1 ) and r ∈ part(G 2 )
When a side condition does not hold, the map is undefined.

Definition 5 (Well-Formed Global Types [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]). Global type G ∈ G is well-formed (WF) if for all r ∈ part(G), the projection G r is defined.

The last notion required in our characterization of multiparty session types as binary sessions is a swapping relation over global types [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF], which enables transformations among causally independent communications. Such transformations may represent optimizations that increase parallelism while preserving the intended global behavior.

Definition 6 (Global Swapping). The swapping relation sw is the smallest congruence on G which satisfies the rules in Fig. 3. (The symmetric of (SW2) is omitted.)

Relating Multiparty and Binary Session Type Theories

Our analysis of multiparty protocols as binary sessions relies on the medium process of a global type. Mediums offer a simple device for analyzing global types using the binary session types of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]. Mediums uniformly capture the sequencing behavior in a global type, for they take part in all message exchanges between local participants. After defining mediums (Def. 7), we establish their characterization results (Thms. 4 and 5). We then present a process characterization of global swapping (Def. 6) in terms of context bisimilarity (Thm. 6). Subsequently, we state operational correspondence results (Thm. 7), exploiting the auxiliary notions of instrumented mediums (Def. 10) and multiparty systems (Def. 11). We use the following conventions.

Convention 3 (Indexed/Annotated Names) We consider names indexed by participants p, q, . . ., noted c p , c q , . . . and names annotated by participants, noted k p , k q , . . .. Given p = q, indexed names c p and c q denote two different objects; in contrast, annotated names k p and k q denote the same name k with different annotations. Given a G with part(G) = {p 1 , . . . , p n }, we will write npart(G) to denote the set that contains a unique name c pj for every participant p j of G. We will occasionally use npart(G) as an unordered sequence of names.

Definition 7 (Mediums). The medium of G ∈ G, denoted M G , is defined as follows:

• M end = 0 • M G 1 | G 2 = M G 1 | M G 2 • M p q:{l i U i .G i } i∈I = c p l i : c p (u).c q l i ; c q (v).([u ↔ v] | M G i ) i∈I
The key case is M p q:{l i U i .G i } i∈I : note how the medium uses two prefixes (on name c p ) to mediate with p, followed by two prefixes (on name c q ) to mediate with q. We illustrate mediums by means of an example:

Example 2. The medium process for global type G BS in Example 1 is:

M G BS = c B1 send : c B1 (v).c S send ; c S (w).([w ↔ v] | c S {rep : c S (v).c B1 rep; c B1 (w).([w ↔ v] | c S {rep : c S (v).c B2 rep; c B2 (w).([w ↔ v] | c B1 {shr : c B1 (v).c B2 shr ; c B2 (w).([w ↔ v] | c B2 { ok : c B2 (v).c S ok ; c S (w).([w ↔ v] | 0) , quit : c B2 (v).c S quit; c S (w).([w ↔ v] | 0)})})})})
Intuitively, we expect that (well-typed) process implementations for B 1 , B 2 , and S should interact with M G BS through channels c B1 , c B2 , and c S , respectively.

We now move on to state our characterization results. We require two auxiliary notions, given next. Below, we sometimes write Γ ; ∆ M G instead of Γ ; ∆ M G :: z:1, when z ∈ fn(M G ).

Definition 8 (Compositional Typing). We say Γ ; ∆ M G ::

z:C is a compositional typing if: (i) it is a valid typing derivation; (ii) npart(G) ⊆ dom(∆); and (iii) C = 1.
A compositional typing says that M G depends on behaviors associated to each participant of G; it also specifies that M G does not offer any behaviors of its own. We relate binary session types and local types: the main difference is that the former do not mention participants. Below, B ranges over base types (bool, nat, . . .) in Def.

p!{l i U i .T i } i∈I = ⊕{l i : U i ⊗ T i } i∈I p?{l i U i .T i } i∈I = {l i : U i T i } i∈I

Characterization Results

Our characterization results relate process M G (well-typed with a compositional typing) and G p 1 , . . . , G p n (i.e., the local types of G transformed into binary session types via Def. 9). Our characterization results are in two directions, given by Thms. 4 and 5. The first direction says that well-formedness of global types (Def. 5) ensures compositional typings for mediums with (logic based) binary session types:

Theorem 4 (Global Types → Typed Mediums). Let G ∈ G. If G is WF with part(G) = {p 1 , . . . , p n } then Γ ; c p1 : G p 1 , . . . , c pn : G p n M G is a compositional typ- ing, for some Γ .
The second direction of the characterization is the converse of Thm. 4: compositional typings for mediums induce global types which are WF. Given local types T 1 , T 2 , below we write T 1 T 2 if there exists a local type T such that T 1 T = T 2 (cf. Def. 3). This notation allows us to handle the labeled alternatives silently introduced by rule (T L 2 ).

Theorem 5 (Well-Typed Mediums → Global Types). Let G ∈ G. If Γ ; c p1 :A 1 , . . . , c pn :A n M G is a compositional typing then ∃T 1 , . . . , T n such that G p j
T j and T j = A j , for all p j ∈ part(G).

Thms. 4 and 5 tightly connect (i) global types, local types and projection, and (ii) medium processes, and logic-based binary session types. They also provide an independent deep justification, through purely logical arguments, to the notion of projection.

A Behavioral Characterization of Global Swapping

Global swapping (Def. 6, Fig. 3) can be directly justified from more primitive notions, based on the characterizations given by Thms. 4 and 5. By abstracting a global type's behavior in terms of its medium we may reduce transformations on global types to typepreserving transformations on processes. This is the content of Thm. 6 below, which connects global swapping ( sw ) and context bisimilarity (≈). Hence, sequentiality of mediums can be relaxed in the case of causally independent exchanges captured by sw .

Theorem 6. Let G 1 ∈ G such that M G 1 has a compositional typing Γ ; ∆ M G 1 , for some Γ, ∆. If G 1 sw G 2 then Γ ; ∆ M G 1 ≈ M G 2 .
Since M G is a low-level representation of G, the converse of Thm. 6 is less interesting, for type-preserving transformations at the (low) level of mediums do not always correspond to behavior-preserving transformations at the (high) level of global types. That is, since M G implements each communication in G using several prefixes, swapping in G occurs only when all relevant prefixes in M G can be commuted via c .

Operational Correspondence Results

The results given so far focus on the static semantics of multiparty and binary systems, and are already key to justify essential properties such as absence of global deadlock.

p q:{li Ui .Gi}i∈I p l j ---→ p q: lj Uj .Gj (j ∈ I) p q: l U .G p -→ p q: l ((U )).G p q: l ((U )).G q l --→ p q: ((U )).G p q: ((U )).G q -→ G Fig. 4. LTS over Finite, Extended Global Types (Excerpt).

We now move on to dynamic semantics, and establish operational correspondence results between a global type and its medium process (Thm. 7).

We define the instrumented medium of a global type G, denoted M k G , as a natural extension of Def. 7. Process M k G exploits fresh sessions (denoted k), to emit a visible signal for each action of G. We use k as annotated names (cf. Conv. 3): each action on a k i contains the identity of the participant of G which performs it. Then, using M k G we define the set of systems associated to G (Def. 11), which collects process implementations for G mediated by M k G . Since interactions between local implementations and M k G are unobservable actions, Thm. 7 connects (i) the visible behavior of a system along annotated names k, and (ii) the visible behavior of G, defined by an LTS on global types (a variant of that in [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]). Below, k p .P stands for k p (x).P when x is not relevant in P . Also, k p .P stands for k p (v).(0 | P ) for some v.

Definition 10 (Instrumented Mediums). Let k be fresh, annotated names. The instrumented medium of G ∈ G with respect to k, denoted M k G , is defined as follows:

• M k end = 0 • M k1,k2 G 1 | G 2 = M k1 G 1 | M k2 G 2 • M k p q:{l i U i .G i } i∈I = c p l i : k p l i ; c p (u). k p . c q l i ; k q {l i : c q (v).([u ↔ v] | k q .M k G i )} {i} i∈I
The key case is M k p q:{l i U i .G i } i∈I . Each action of the multiparty exchange is "echoed" by an action on annotated name k: the selection of label l i by p is followed by prefix k p l i ; the output from p (captured by the medium by the input c p (u)) is echoed by prefix k p . This way, the instrumented process M k G induces a fine-grained correspondence with G, exploiting process actions with explicit participant identities. To state our operational correspondence result, we introduce extended global types and a labeled transition system (LTS) for (extended) global types. The syntax of extended global types is defined as

G ::= G | G 1 | G 2 with G ::= end | p q:{l i U i .G i } i∈I | p q: l U .G | p q: l ((U )).G | p q: ((U )).G
We consider parallel composition of sequential global types. We also have three auxiliary forms for global types, denoted with : they represent intermediate steps. Types p q: l U .G and p q: l ((U )).G denote the commitment of p to output and input along label l , resp. Type p q: ((U )).G represents the state just before the actual input action by q. We need the expected extension of Def. 10 for these types.

We adapt the LTS in [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF] to the case of (extended) global types. The set of observables is σ ::= p | p l | p | p l . Below, psubj(σ) denotes the participant in σ. This way, e.g., psubj(p l ) = p. The LTS over global types, noted G σ -→ G , is defined by rules including those in Fig. 4. Since Def. 10 annotates prefixes on k with participant identities, their associated actions will be annotated too; given a participant p, we may define the set of annotated visible actions as:

λ p ::= k p (y) | k p l | k p y | k p (y) | k p l .
We write k p and k p to denote actions k p (y) and k p (y), resp., whenever object y is unimportant. Also, psubj(λ p ) denotes the participant p which annotates λ. This way, e.g., psubj(k p ) = p and psubj(k q l ) = q. To relate labels for global types and process labels, given an annotated name k, we define mappings { {•} } k and || • || as follows:

{ {p} } k = k p { {p l } } k = k p l { {p } } k = k p { { p l } } k = k p l ||k p || = p ||k p l || = p l || k p || = p || k p l || = p l
Operational correspondence is stated in terms of the multiparty systems of a global type. Following Def. 8, we say that Γ ; ∆, ∆ M k G ::

z:C is an instrumented compositional typing if (i) it is a valid typing derivation; (ii) npart(G) ⊆ dom(∆); (iii) C = 1; (iv) dom(∆ ) = k:
Definition 11 (Systems). Let G ∈ G be a WF global type, with part(G) = {p 1 , . . . , p n }. Also, let Γ ; ∆, ∆ M k G be an instrumented compositional typing, with ∆ = c p1 : G p 1 , . . . , c pn : G p n , for some Γ . Let z = npart(G). The set of systems of G is defined as:

S k (G) = (ν z)(Q 1 | • • • | Q n | M k G ) | •; • Q j :: c pj : G p j , j ∈ 1 . . . n
Thus, given G, a multiparty system is obtained by composing M k G with well-typed implementations for each of the local projections of G. An R ∈ S k (G) is an implementation of the multiparty protocol G. By construction, its only visible actions are on annotated names: interactions between all the Q j and M k G will be unobservable.

Thm. 7 below connects global types and systems: it confirms that (instrumented) medium processes faithfully mirror the communicating behavior of extended global types. Below, we write G

σ[p] ---→ G if G σ -→ G
G σ[p] ---→ G then R λ[p] =⇒ R , for some λ, R , k ∈ k such that λ = { {σ} } k and R ∈ S k (G ). Moreover, if there is some R 0 s.t. R =⇒ R 0 λ[p] ---→ R then G σ[p] ---→ G , for some σ, G such that σ = ||λ|| and R ∈ S k (G ).

Example: Sharing in Multiparty Conversations

Here we further illustrate reasoning about global types in G by exploiting the properties given in § 3. In particular, we illustrate non-trivial forms of replication and sharing.

Let us consider the global type G BS , given in Example 1. The medium processes of G BS , denoted M G BS , has been detailed in Example 2; we proceed to examine its properties. Relying on Thms. 4 and 5, we have the compositional typing:

Γ ; c 1 :B1,
Γ ; • (νc 1 )(Buy1 | (νc 2 )(Sel | (νc 3 )(Buy2 | M G BS ))) (2)
The binary session types in § 2 allows us to infer that the multiparty system defined by ( 2) adheres to the declared projected types, is deadlock-free, and terminating. Just as we inherit strong properties for Buy1 , Sel , and Buy2 above, we may inherit the same properties for more interesting system configurations. In particular, local implementations which appeal to replication and sharing, admit also precise analyses thanks to the characterizations in § 3. Let us consider a setting in which the processes to be composed with the medium must be invoked from a replicated service (a source of generic process definitions). We may have •; • !u 1 (w).Buy1 w :: u 1 : !B1 and

•; • !u 2 (w).Sel w :: u 2 : !S •; • !u 3 (w).Buy2 w :: u 3 : !B2
and the following "initiator processes" would spawn a copy of the medium's requirements, instantiated at appropriate names:

•; u 1 : !B1 u 1 (x).[x ↔ c 1 ] :: c 1 :B1 •; u 2 : !S u 2 (x).[x ↔ c 2 ] :: c 2 :S •; u 3 : !B2 u 3 (x).[x ↔ c 3 ] :: c 3 :B2
Let us write RBuy1 , RBuy2 , and RSel to denote the composition of replicated definitions and initiators above. Intuitively, they represent the "remote" variants of Buy1 , Buy2 , and RSel , respectively. We may then define the multiparty system:

Γ ; • (νc 1 )(RBuy1 | (νc 2 )(RSel | (νc 3 )(RBuy2 | M G BS )))
which, with a concise specification, improves (2) with concurrent invocation/instantiation of replicated service definitions. As (2), the revised composition above is correct, deadlock-free, and terminating.

Rather than appealing to initiators, a scheme in which the medium invokes and instantiates services directly is also expressible in our framework, in a type consistent way. Using (1), and assuming Γ = u 1 :B1, u 2 :S, u 3 :B2, we may derive:

Γ ; • u 1 (c 1 ).u 2 (c 2 ).u 3 (c 3 ).M G BS (3)
Hence, prior to engaging in the mediation behavior for G BS , the medium first spawns a copy of the required services. We may relate the guarded process in (3) with the multicast session request construct in multiparty session processes [START_REF] Honda | Multiparty asynchronous session types[END_REF]. Observe that (3) cleanly distinguishes between session initiation and actual communication behavior:

the distinction is given at the level of processes (cf. output prefixes on u 1 , u 2 , and u 3 ) but also at the level of typed interfaces. The service invocation (3) may be regarded as "eager": all required services must be sequentially invoked prior to executing the protocol. We may also obtain, in a typeconsistent manner, a medium process implementing a "lazy" invocation strategy that spawns services only when necessary. For the sake of example, consider process

Eager BS u 3 (c 3 ).M G BS
in which only the invocation on u 3 is blocking the protocol, with "open" dependencies on c 1 , c 2 . That is, we have Γ ; c 1 :B1, c 2 :S Eager BS :: z:1. It could be desirable to postpone the invocation on u 3 as much as possible. By combining the commutations on process prefixes realized by c [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF] and Thm. 2, we may obtain:

Γ ; c 1 :B1, c 2 :S Eager BS ≈ Lazy BS :: -:1
where Lazy BS is obtained from Eager BS by "pushing inside" prefix u 3 (c 3 ).

Multiparty Session Types with Behavioral Genericity

To illustrate the modularity of our approach, we conservatively extend, for the first time, multiparty session types with parametric polymorphism, developed for binary sessions in [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF][START_REF] Wadler | Propositions as sessions[END_REF]. Although expressed by second-order quantifiers on (session) types-in the style of the polymorphic λ-calculus-parametric polymorphism in our setting means behavioural genericity in multiparty conversations (i.e., passing first-class behavioral interfaces in messages), not just datatype genericity. In this section we describe how to extend the approach and results in § 3 to polymorphic, multiparty session types.

In [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF] we have extended the framework of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] with impredicative universal and existential quantification over session types, denoted with ∀X.A and ∃X.A, respectively. These two types are interpreted as the input and output of a session type, respectively. More precisely, ∀X.A is the type of a process that inputs some session type S (which we may as a kind of interface passing) and then behaves as prescribed by A{ S /X}. ∃X.A is the type of a process that sends some session type S and then behaves as prescribed by A{ S /X}. From the point of view of the receiver of such S, the protocol S is in a sense opaque; therefore, after inputting S the receiver behaves parametrically (in the sense of behavioral polymorphism) for any such S. In any case, any usage of S by the sender will necessarily be matched by some appropriate parties in the system. A relevant example of the phenomenon can be recovered from [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF]. Consider the type CloudServer : ∀X.(api X) X A session with this type will first input some session type X, say GMail, and then will input a session with type api GMail (that may be realized by a piece of code that will first receive a channel implementing the api behavior and will after-building on it-behave as specified by GMail) and then offers the behavior GMail. A system implementing the CloudServer type must somehow provide the api service internally and pass it to the channel of type api GMail (e.g., representing a piece of mobile code). Notice that after that the GMail service may be produced by copy-cating the resulting behavior to the cloud server client. The crucial point here is that the cloud server behaves uniformly for whatever session type X is requested for it to execute; its role in this case is to provide the suitable api. Of course, at runtime, all interactions at X will take place as prescribed by the concrete session type involved (in this example, GMail), which may be an arbitrarily complex (behaviorally generic) session type.

Binary Session Types with Parametric Polymorphism

We now recall key definitions from [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF]. The process model in § 2 is extended with processes x A.P (output type A, proceed as P ) and x(X).P (receive a type A, proceed as P { A /X}) and the reduction rule:

x A.Q | x(X).P → Q | P { A /X}, where { A /X}
is the substitution of type variable X with session type A. Thus, our process syntax allows terms such as, e.g., x A.Q | x(X).y X.P , where A is a session typed protocol. We extend binary types (cf. Def. 1) with existential and universal quantification:

A, B ::= 1 | !A | A ⊗ B |A B | {l i :A i } i∈I | ⊕{l i :A i } i∈I | X | ∃X.A | ∀X.A
Besides ∆ and Γ , the polymorphic type system uses environment Ω to record type variables. We have two judgments. Judgment Ω A type denotes that A is a wellformed type with free variables registered in Ω (see [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF] for well-formedness rules). Also, judgement Ω; Γ ; ∆ P :: x:A states that P implements a session of type A along channel x, provided it is composed with processes providing sessions linearly in ∆ and persistently in Γ , such that the types occurring in Ω are well-formed.

The required typing rules result by adding Ω in Fig. 2 and by considering rules in Fig. 5, which explain how to provide and use sessions of a polymorphic type. Rule (T∀R) types the offering of a session of universal type ∀X.A by inputing an arbitrary type, bound to X, and proceeding as A, which may bind the type variable X, regardless of what the received type is. Rule (T∀L) says that the use of type ∀X.A consists of the output of a type B (well-formed under Ω) which then warrants the use of the session as A{ B /X}. The existential type is dual: providing an existentially typed session ∃X.A is accomplished by outputting a type B and then providing a session of type A{ B /X} (Rule (T∃R)) . Using an existential session ∃X.A implies inputing a type and then using the session as A, regardless of the received session type (Rule (T∃L)).

Well-typed polymorphic processes satisfy Thm. 1 and relational parametricity [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF], a reasoning principle stated next. We require some notation, fully detailed in [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF]: ω:Ω denotes a type substitution that assigns a closed type to variables in Ω. Notation ω(P ) denotes the application of ω to type variables in P . Also, η:ω 1 ⇔ ω 2 is an equivalence candidate assignment (a typed relation on processes) between ω 1 and ω 2 . Moreover, ≈ L denotes a logical equivalence relation that coincides with barbed congruence.

Theorem 8 (Relational Parametricity [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF]). If Ω; Γ ; ∆ P :: z:A then, for all ω 1 :Ω, ω 2 :Ω, and η:ω 1 ⇔ ω 2 : Γ ; ∆ ω 1 (P ) ≈ L ω 2 (P ) ::

z:A[η:ω 1 ⇔ ω 2 ].
Thm. 8 entails behavioral genericity, a form of representation independence: it says that process P behaves the same independently from instantiations of its free type variables.

Multiparty Session Types with Polymorphism

We extend global types in G (Def. 2) with variables X, X , . . . and with a construct p q:{l [X].G }, which introduces parametric polymorphism (X is meant to occur in G ). To our knowledge, this is the first theory of its kind: Definition 12 (Polymorphic Session Types). Define global types and local types as

G ::= end | G 1 | G 2 | p q:{l i U i .G i } i∈I | p q:{l [X].G} | X U ::= bool | nat | str | . . . | T | (T ) † T ::= end | p?{l i U i .T i } i∈I | p!{l i U i .T i } i∈I | p!{l[X].T } | p?{l[X].T } | X Above (•) † denotes a function on local types that discards participant identities. E.g., (p?{l[X].T }) † =?{l[X].(T ) † } and (p?{l i U i .T i } i∈I ) † =?{l i U i .(T i ) † } i∈I .
We write G ∀∃ to denote the above global types. The global type p q:{l [X].G} signals that p sends to q an arbitrary local type (protocol), thus specifying q as a generic partner. Also, G is a generic global specification: its behavior will be depend on the type sent by p to q, which should be explicit in p's implementation. This new global type is related to local types p!{l[X].T } and p?{l[X].T }, which are to be understood as existential and universal quantification on local types, respectively-see below. The global type X should be intuitively understood as a behavior that remains "globally abstract", in the sense that it is determined by a concrete local type exchanged between two participants, namely, as a result of a (previous) communication of the form p q:{l [X].G}. As a result, the (global) communication behavior associated to local type exchanged between p and q should remain abstract (opaque) to other participants of the protocol.

The projection of G ∈ G ∀∃ onto participant r, denoted G r, extends Def. 4 by adding X r = X and by letting:

(p q:{l [X].G}) r =      p!{l[X].(G r)} if r = p p?{l[X].(G r)} if r = q G r otherwise
Well-formedness of global types in G ∀∃ is based on projectability but also on consistent uses of type variables: a participant can only communicate the types it knows. (This condition is similar to history-sensitivity, as in [START_REF] Bocchi | A theory of design-by-contract for distributed multiparty interactions[END_REF].) This way, e.g., an ill-formed type is p q:{l 1 [X].r s:{l 2 ?{l int .X} .end}}, since r, s do not know the type sent by p.

Mediums for Multiparty Session Types With Polymorphism

Mediums for global types in G ∀∃ are defined by extending Def. 7 as follows:

M p q:{l [X].G} = c p l : c p (X).c q l ; c q X.M G M X = 0

Observe that type variable X should not generate a mediator behavior, as we want to remain generic. The relation between local types and binary types extends Def. 9 with: G p = p q: l 1 bool .q r:{l [X].q r:{l 2 ?{l 3 api .X} .X}}

We have participants p, q, and r. The intent is that r is a behaviorally generic participant, that provides a behavior of type api required by q. Crucially, r may interact with q independently of the local type sent by q. Such a local type is explicit in q's implementation (see below), rather than in the global type G p . In G p , participant p first sends a boolean value to q; then, q sends an unspecified protocol to r, say M , which is to be used subsequently in an exchange from q to r. Notice that M occurs in the value that r receives from q and influences the behavior after that exchange. Indeed, the value ?{l 3 api .X} denotes an unspecified session type that relies on the reception of a session of type api. The local projections for G p are G p p = p!{l 1 bool .end} and G p q = p? l 1 bool .q!{l [X].q!{l 2 ?{l 3 api .X} .X}} G p r = q? l [X].q?{l 2 ?{l 3 api .X} .X} Above, the occurrences of X at the end of both G p q and G p r may appear surprising, as they should represent dual behaviors. Notice that in each case, X should be interpreted according to the local type that "bounds" X (i.e., the output q!{l [X] . . .} in G p q and the input q?{l [X] . . .} in G p r). This dual perspective should become evident when looking at the binary session types associated to these projections. First, notice that we have that ?{l 3 api .X} = {l 3 :(api X)}. Writing (api X) to stand for {l 3 :(api X)}), we have the binary session types G p p = ⊕{l 1 : 1 ⊗ 1} and

G p q = {l 1 : 1 ⊕{l : ∃X. ⊕{l 2 : (api X) ⊗ X} G p r = {l : ∀X. {l 2 : (api X) X}}}}
The medium process for G p is then:

M G p = c p l 1 : c p (u).c q l 1 ; c q (v). [u ↔ v] | c q {l : c q (X).c r l ; c r X. c q {l 2 : c q (u).c r l 2 ; c r (v).([u ↔ v] | 0)}}
Using our extended characterization results, we may show that M G p can safely interact with implementations for p, q, and r whose types correspond to the projections of G p onto p, q, and r. Indeed, M G p can safely interact with any P , Q i , and R such that Ω; Γ ; ∆ 1 P :: c p : G p p and

Ω; Γ ; ∆ 3 R :: c r : G p r Ω; Γ ; ∆ 2 Q i :: c q : G p q Process (νc p , c q , c r )(M G p | P | R | Q i ) is a system for G p (cf. Def. 11). It is well- typed; we have Ω; Γ ; ∆ 1 , ∆ 2 , ∆ 3 (νc p , c q , c r )(M G p | P | R | Q i ) :: -: 1. Pro- cess c p l 1 ; c p (f ).(B f | 0
) is a concrete implementation for P , where name f stands for a boolean implemented by B f . As for R and Q i , we may have:

R = c r {l : c r (Y ).c r {l 2 : c r (y).y(a).(A a | [c r ↔ a])}} Q 1 = c q {l 1 : c q (b).c q l ; c q S.c q l 2 ; c q (w).(w(a).SMTP b w,a | [m ↔ c q ])}
Crucially, following the type G p r , process R is behaviorally generic: independently of the type received from Q i via the medium M G p (cf. the type input prefix c r (Y )), R enables process A a to provide the API along name a. Process Q 1 is just one possible implementation for q: it provides an implementation of a service SMTP b w,a that relies on behavior api along name a and a boolean along b to implement protocol S along w. A different implementation for q is process Q 2 below, which concerns session protocol I: Q 2 = c q {l 1 : c q (b).c q l ; c q I.c q l 2 ; c q (w).(w(a).IMAP b w,a | [m ↔ c q ])}

where IMAP b w,a uses api along a and boolean b to implement protocol I along w. Note that R and any Q i have limited interactions with M G p : to respect the genericity stipulated by G p , the polymorphic process M G p only mediates the exchange of the local type (S or I) and plugs the necessary connections; other exchanges are direct between R and Q 1 or Q 2 , and known to comply with the (dynamically passed protocol) specified by the session type S or I.

Both (νc p , c q , c r )(M G p | P | R | Q 1 ) and (νc p , c q , c r )(M G p | P | R | Q 2 )
are well-typed systems; hence, they satisfy fidelity and deadlock-freedom (Thm. 1). Using properties of well-typed processes together with relational parametricity (Thm. 8), we may further show that they are observationally equivalent, provided a typed relation between session types S and I. That is, Thm. 8 allows us to state the behavioral independence of the sub-system formed by M G p , P , and R with respect to any implementation Q i for participant q.

Concluding Remarks and Related Works

We developed the first analysis of multiparty protocols using binary session types. Our medium processes capture the semantics of multiparty session types and connect global types to well-typed implementations; this allows us to exploit properties for typed processes to reason about multiparty systems. Since mediums have a uniform definition, we may analyze global types with features such as delegation, which go beyond the scope of recent automata-based analyses of global types [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF][START_REF] Lange | From communicating machines to graphical choreographies[END_REF]. Our work thus complements such recent works. Our approach naturally supports the analysis of multiparty session types with behavioral genericity. This model, the first of its kind, is very powerful; it reuses techniques from binary sessions [START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF], notably relational parametricity. These features suggest that extensions of known multiparty sessions with behavioral genericity would be hard to obtain without following linear logic foundations, as done here.

Given a global type, our characterization results relate its medium and its local projections; these relations allow us to transfer properties of [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] (e.g., deadlock-freedom) to multiparty protocols. Our results stress the fundamental character of key notions in multiparty sessions (e.g., projections), and build on connections between two distinct session type theories based on linear logic [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] and on automata [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]. Our developments do not depend on the interpretation of session types in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF] being intuitionistic; clearly, its reasoning techniques (e.g., behavioral equivalences [START_REF] Pérez | Linear logical relations and observational equivalences for session-based concurrency[END_REF]) are important in our results. Our approach should extend also to interpretations based on classical linear logic [START_REF] Wadler | Propositions as sessions[END_REF]. Related Work. One challenge in decomposing a multiparty session type is preserving its sequencing information. The work [START_REF] Chen | Lightening global types[END_REF] shows how to decompose a global type into simpler, independent pieces: global types use an additional calls construct to invoke these pieces in the appropriate order, but connections with binary sessions are not established. Correspondence assertions [START_REF] Bonelli | Correspondence assertions for process synchronization in concurrent communications[END_REF] track data dependencies and detect unintended operations; they may allow to relate independent binary sessions. Using standard binary/multiparty session types, we capture sequencing information using a process extracted from a global type. Our approach relies on deadlock-freedom (not available in [START_REF] Bonelli | Correspondence assertions for process synchronization in concurrent communications[END_REF]) and offers a principled way of transferring it to multiparty systems.

To our knowledge, ours is the first formal characterization of multiparty session types using binary session types. Previous works have, e.g., compared different multiparty session types but without connecting to binary types [START_REF] Demangeon | On the expressiveness of multiparty session types[END_REF]. The work [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] (extended version) identifies a class of multiparty systems for which deadlock-freedom analysis can be reduced to the analysis of linear π-calculus processes. This reduction, however, does not connect with binary session types, nor exploits other properties of processes to analyze global types. The work [START_REF] Carbone | Multiparty session types as coherence proofs[END_REF] relates global types and a variant of classical linear logic; as in our work, a challenge in [START_REF] Carbone | Multiparty session types as coherence proofs[END_REF] is capturing sequencing information in global types. While [START_REF] Carbone | Multiparty session types as coherence proofs[END_REF] captures sequencing information in global types via role annotations in propositions/types (using an extra proof system, called coherence), our medium-based approach enables process reasoning on global types, uses standard linear logic propositions, and allows for conservative extensions with powerful reasoning techniques, notably behavioral genericity as enabled by parametric polymorphism.

Medium processes are loosely related to the concept of orchestrators in serviceoriented computing. The work [START_REF] Mcilvenna | Synthesis of orchestrators from service choreographies[END_REF] shows how to synthesize an orchestrator from a service choreography, using finite state machines. In contrast, we consider choreographies given as behavioral types; mediums are obtained directly from those types. Acknowledgments. Thanks to Bernardo Toninho for useful discussions. We are also grateful to the anonymous reviewers for their improvement suggestions. This work was partially supported by NOVA LINCS (Ref. UID/CEC/04516/2013) and COST Action IC1201 (Behavioural Types for Reliable Large-Scale Software Systems).

(Fig. 1 .

 1 Fig. 1. LTS for Processes (Excerpt).

Fig. 1

 1 gives a selection of the rules that define P λ -→ Q. Weak transitions are as usual: =⇒ is the reflexive, transitive closure of τ -→. Notation λ =⇒ stands for =⇒ λ -→=⇒ (given λ = τ ) and τ =⇒ stands for =⇒.

Fig. 3 .

 3 Fig. 3. Swapping relation on global types (Def. 6). A#B denotes that sets A, B are disjoint.

2 . 9 (

 29 Definition Local Types → Binary Types). Mapping • from local types T (Def. 2) into binary types A (Def. 1) is inductively defined as end = B = 1 and

  and psubj(σ) = p. Also, we write P λ[p] ---→ P (resp. P λ[p] =⇒ P ) if P λ -→ P (resp. P λ =⇒ P ) holds and psubj(λ) = p. Theorem 7 (Operational Correspondence). Let G be an extended WF global type and R ∈ S k (G). We have: If

  c 2 :S, c 3 :B2 M G BS :: -:1 (1) for some Γ and with B1 = G BS B 1 , S = G BS S , and B2 = G BS B 2 . To implement the protocol, one may simply compose M G BS with type compatible processes •; • Buy1 :: c 1 :B1, •; • Sel :: c 2 :S, and •; • Buy2 :: c 3 :B2:

Fig. 5 .

 5 Fig. 5. Typing Rules for Polymorphic, Binary Session Types.

p

  !{l[X].T } = ⊕{l : ∃X. T } p?{l[X].T } = {l : ∀X. T } and by letting X = X and (T ) † = T . The characterization results in § 3.1 hold also for global types in G ∀∃ .

6

  Mediums At Work: A Behaviorally Generic Multiparty ProtocolWe illustrate our approach and results via a simple example. Consider the global type G p , inspired by the CloudServer from[START_REF] Caires | Behavioral polymorphism and parametricity in session-based communication[END_REF] already hinted to above. It features behavioral genericity (as enabled by parametric polymorphism); below, str, bool, denote basic data types, and api is a session type describing the cloud infrastructure API.

(Tid) Γ ; x:A [x ↔ z] :: z:A (T1R) Γ ; • 0 :: x:1 (Tcut) Γ ; ∆ P :: x:A Γ ; ∆ , x:A Q :: z:C Γ ; ∆, ∆ (νx)(P | Q) :: z:C (T L) Γ ; ∆ P :: y:A Γ ; ∆ , x:B Q :: z:C Γ ; ∆, ∆ , x:A B x(y).(P | Q) :: z:C (T⊗L) Γ ; ∆, y:A, x:B P :: z:C Γ ; ∆, x:A ⊗ B x(y).P :: z:C (T⊕L) Γ ; ∆, x:A 1 P 1 :: z:C • • • Γ ; ∆, x:A k P k :: z:C I = {1, . . . , k} Γ ; ∆, x: ⊕{l i : A i } i∈I x {l i : P i } i∈I :: z:C (T R) Γ ; ∆ P 1 :: x:A 1 • • • Γ ; ∆ P k :: x:A k I = {1, . . . , k} Γ ; ∆ x {l i : P i } i∈I :: x: {l i : A i } i∈I (T L 1 ) Γ ; ∆, x:A P :: z:C Γ ; ∆, x: {l i : A} {i} x l i ; P :: z:C


Laurent Reynaud
email: laurent.reynaud@orange.com

Isabelle Guérin-Lassous
email: isabelle.guerin-lassous@ens-lyon.fr

Physics-Based Swarm Intelligence for Disaster Relief Communications

Keywords: Controlled mobility, physics-based swarm intelligence, virtual forces, unmanned aerial vehicles, disaster relief communications

This study explores how a swarm of aerial mobile vehicles can provide network connectivity and meet the stringent requirements of public protection and disaster relief operations. In this context, we design a physics-based controlled mobility strategy, which we name the extended Virtual Force Protocol (VFPe), allowing self-propelled nodes, and in particular here unmanned aerial vehicles, to fly autonomously and cooperatively. In this way, ground devices scattered on the operation site may establish communications through the wireless multi-hop communication routes formed by the network of aerial nodes. We further investigate through simulations the behavior of the VFPe protocol, notably focusing on the way node location information is disseminated into the network as well as on the impact of the number of exploration nodes on the overall network performance.

Introduction

In the wake of disaster, communication systems play a key role for the support of appropriate response operations. During such times, when existing terrestrial networks may be damaged or even completely impaired, Public Protection and Disaster Relief (PPDR) teams need to lean on a reliable emergency communications infrastructure to be able to restore essential services and more generally to quickly provide an adequate assistance to the affected population [START_REF]Report 199: Public protection and disaster relief spectrum requirements[END_REF]. Regarding these requirements, multiple temporary network architectures relying on either terrestrial or satellite systems have been proposed [START_REF] Nelson | The Evolution of Hastily Formed Networks for Disaster Response: Technologies, Case Studies, and Future Trends[END_REF]. All these architectures were tailored to meet the specific PPDR requirements, including the need to support a scalable network provision for challenging environments (e.g. in terms of temperature, hygrometry, landforms, obstacles, etc.), with robust equipment to be operated while the user is in motion, able to achieve a rapid deployment of a temporary infrastructure and services to address network outages in the affected zone [START_REF]Radiocommunication Objectives and Requirements for Public Protection and Disaster Relief[END_REF]. In this regard, the European Electronic Communications Committee (ECC) defines broadband PPDR temporary additional capacity as the means to provide additional network coverage at the scene of the incident with equipment such as ad hoc networks [START_REF]Report 199: Public protection and disaster relief spectrum requirements[END_REF]. Over the last few years, airborne networking has also gained momentum to roll out rapidly deployable PPDR communication systems. In fact, aerial platforms, which can be designed to fly and operate at different altitudes, are increasingly valued for the multiple advantages they can offer in the context of disaster relief communications [START_REF] Reynaud | Deployable aerial communication networks: challenges for futuristic applications[END_REF]. Some of the expected benefits are favorable propagation conditions with frequent line-of-sight transmissions, low latency compared to satellite equipment, and communication payload modularity enabling mission versatility. Moreover, regulation bodies have started considering aerial platforms as a viable set of technologies to roll out an emergency response in the first hours after a disaster [START_REF]The Role of Deployable Aerial Communications Architecture in Emergency Communications and Recommended Next Steps, White Paper[END_REF], with many kinds and sizes of aerial platforms. Basically, each platform type displays distinct features best suited to different applicative perspectives: for instance, low altitude tethered balloons have been largely investigated in the context of disaster relief [START_REF] Qiantori | An Emergency Medical Communications System by Low Altitude Platform at the Early Stages of a Natural Disaster in Indonesia[END_REF], [START_REF] Reynaud | An integrated Aerial Telecommunications Network that supports emergency traffic[END_REF], [START_REF] Gomez | Aerial Base Stations with Opportunistic Links for Next Generation Emergency Communications[END_REF] for their cost-efficiency, low complexity of operation and ability to rapidly lift a telecommunication payload and act as temporary cell towers as long as response operations are required. Other initiatives investigate the use of high altitude, long endurance platforms in the context of disaster relief communications [START_REF] Deaton | High altitude platforms for disaster recovery: capabilities, strategies, and techniques for emergency telecommunications[END_REF]. Although still facing multiple technical challenges, such solutions should provide large network coverages from the low stratosphere during weeks or months.

In this work, we take a particular interest in low altitude platforms with high mobility dynamics, also known as unmanned aerial vehicles, for their aptitude to self-propel and quickly bring small telecommunication payloads where and when needed. Further, we consider autonomous and distributed mobility control mechanisms for these platforms: those mechanisms, when they also enable neighboring nodes to cooperatively adapt their respective trajectories and behavior via local information exchange, are known under the name of swarming (or flocking) strategies [START_REF] Varela | Swarm intelligence based approach for real time UAV team coordination in search operations[END_REF], [START_REF] Daniel | A Communication Aware Steering Strategy Avoiding Self-Separation of Flying Robot Swarms[END_REF]. In this regard, we investigate how to design an efficient swarming strategy based on virtual force principles, with the objective to deploy steerable nodes that are able to form a temporary wireless network and support disaster relief communications. This paper is organized as follows: Section 2 presents the disaster relief scenario as well as the network topology that are considered in the context of this study. Section 3 details prominent works and principles related to virtual force-based mobility control mechanisms and explains the design choices made for the extended Virtual Force Protocol (VFPe), which builds upon our previous study [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF] by generalizing the force system and enabling node location dissemination in the network via extended multi-purpose beacon messages. Further, we analyze in Section 4 the performance of VFPe through representative network simulations, and finally conclude in Section 5.

Scenario

Regarding disaster relief scenarios, the main chronology events generally encompass three distinct phases: preparedness, response and recovery. We propose a network architecture which targets the response stage in this time line, with the specific objective to offer as quickly as possible a reliable and efficient communication environment to the public protection staff, rescue teams and other end users located at the scene of the considered incident or emergency. To this end, we specify four types of network nodes, as Fig. 1 Regarding node movements, two mobility patterns can be distinguished:

-S-and T-type nodes roam the exploration zone Z e in a similar fashion, at random, however T-type nodes possess a slower pedestrian-like velocity compared to the other nodes. -R-and P-type nodes enforce a cooperative mobility strategy which we present and study in this work. With this mobility pattern, the considered R-and P-type nodes exert mutual virtual forces which result into node movement.

These mobility schemes are further detailed in the rest of this study, and nodes are in particular given specific mobility patterns in Section 4. Moreover, in terms of network deployment, we explain in the next section how nodes use the VFPe protocol to cooperatively create a communication chain between a user traffic (source, destination) pair through local information exchange.

3 Protocol design

Related works

With regard to swarming concepts applied to network communications, two prominent approaches have been pursued, based on either the principles of stigmergic collaboration or physicomimetics:

-Stigmergy, dating back to studies on social insects performed in the late 1950s [START_REF] Grassé | La reconstruction du nid et les coordinations interindividuelles; la théorie de la stigmergie[END_REF], refers to the ability, for a swarm of nodes, to adopt an emergent behavior via cooperation and traces left in the environment, with the example of virtual pheromones. These messages intrinsically embed the location of their emission and may allow the creation of gradients based on pheromone additivity and decay [START_REF] Brambilla | Swarm robotics: a review from the swarm engineering perspective[END_REF]. Stigmergy can therefore be used to design path planning or obstacle avoidance strategies and more generally support collective node behavior. Yet, the implementation of pheromones requires either a centralized entity to act as the environment or an exchange system of incomplete views of the environment, which can both prove impractical in actual deployments.

-Physicomimetics, also known as physics-based swarm intelligence, applies to controlled mobility principles for which the local interactions between neighboring nodes allow nodes to reach an emergent cooperative behavior [START_REF] Spears | Distributed, Physics-Based Control of Swarms of Vehicles[END_REF]. In this respect, many works investigated the use of virtual forces, often derived from analogies with gravitational or electromagnetic forces [START_REF] Spears | Distributed, Physics-Based Control of Swarms of Vehicles[END_REF], [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF], [START_REF] Yu | A node deployment algorithm based on van der Waals force in wireless sensor networks[END_REF] or other physics-based phenomena [START_REF] Le | VirFID: A Virtual Force (VF)-based Interest-Driven moving phenomenon monitoring scheme using multiple mobile sensor nodes[END_REF]. Despite differences in the way virtual forces are defined, such solutions share a similar approach in the way nodes evaluate, via local sensing or information exchange, the resulting virtual forces exerted by their neighbors.

In this study, our Virtual Force Protocol design proposal also relies on the principles of physicomimetics. However, the general approach in the literature related to virtual forces presupposes swarms made of a large number of nodes, and incurs the formation of large-scale and steady topologies such as vast grids [START_REF] Spears | Distributed, Physics-Based Control of Swarms of Vehicles[END_REF], lattices or hexagonal distributions [START_REF] Yu | A node deployment algorithm based on van der Waals force in wireless sensor networks[END_REF]. Recent works investigate more dynamic and interest-driven topology formations [START_REF] Le | VirFID: A Virtual Force (VF)-based Interest-Driven moving phenomenon monitoring scheme using multiple mobile sensor nodes[END_REF] yet still address mesh topologies with many redundant communication links, best suited for mobile sensor networks. In contrast, we seek to address deployment scenarios in which the number of network nodes is constrained. In this challenging environment, our solution can steer a limited number of relay nodes to form suitable multihop routes between nodes in need to establish a communication. To meet this requirement, two classes of VFPe core mechanisms were designed: i) a virtual force system exerted on all intermediary nodes of a communication chain, providing the means to control their mobility pattern and ii) a beacon-based mechanism to create and maintain communication chains made of P-and R-type intermediary nodes between the user traffic endpoints. Beacons are also used to discover neighboring nodes and disseminate their positions, thereby allowing chain nodes to accurately match the desired topology. The following subsections detail both mechanisms.

Virtual force-based system

With VFPe, three types of virtual forces are applied on the network nodes. The first two forces are based on physicomimetics precepts [START_REF] Spears | Distributed, Physics-Based Control of Swarms of Vehicles[END_REF], respectively impersonating physics-based attraction-repulsion and friction forces. As specified in our earlier works [START_REF] Reynaud | Mobilité contrôlée pour la poursuite de frelons[END_REF], [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF], both forces can be used to maintain neighboring nodes at a required distance by means of local distance-based interactions and without the need to interact with a centralized mobility planning entity.

An attraction-repulsion force f is defined so that any node N located in either the attractive or repulsive zone of another node P is under the influence of P's force f , collinear with vector P N , as illustrated by Fig. 2: P's repulsive zone is the disc centered on P with a radius d r, while P's attractive zone is the annular surface positioned at a distance d f ≤ d ≤ d a from P. Further, f 's intensity can be defined so that it depends on the distance between N and P, Fig. 2 outlining two exemplary intensity profiles for f . In the context of this work, we consider the simple piecewise-defined function such that f = f = I in the repulsive area, f = -I in the attractive area and f = 0 otherwise. A friction force f f r is exerted on a node which is located in the friction zone of a nearby node. Retaining the previous notations, P's friction zone is the annular surface positioned at a distance d r ≤ d ≤ d f . If N were located in P's friction zone (which is not the case in the example of Fig. 2), a friction force f f r , collinear with N's velocity vector, would be applied on N, so that f f r = f f r = -Cx. The use of a friction zone here is essential since it allows a neighboring node to decelerate and stop its motion within the boundaries of the considered zone. In this context, its absence would result into undesirable oscillating motion patterns for VFPe-enabled nodes, and be detrimental to the formation of the target chain topology.

It is worth highlighting that in [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF], we conducted a in-depth study of the aforementioned parameters I and Cx and in particular sought optimal values. Consequently, key VFPe parameters in Section 4 were valued accordingly. However, the referenced study considered specific deployment environments in which the position of the user traffic destination is known and where communications chains are formed in a straight line. In contrast, as previously delineated by Section 2, our current work addresses more general deployment scenarios where no assumption is made on the knowledge regarding the location and movement patterns of the user traffic sources or destinations. In this challenged environment, the simple combination of attraction-repulsion and friction forces only ensures an acceptable distance between successive intermediate nodes in a communication chain, but does not guarantee that those chains are correctly directed towards the traffic endpoints. We therefore added a third component in the VFPe virtual force system.

An alignment force f a is used to ensure that in a communication chain, successive intermediate nodes actually direct the chain towards the user traffic destination. As again depicted by the left part of Fig. 2, force f a tends to steer an intermediate node N of a communication chain towards the line between the user traffic endpoints S and D. Since all intermediate nodes are under the effect of f a , the whole chain tends to eventually form a straight line between S and D. Note that normally, f a steers N towards its orthogonal projection Np on line (SD), unless this position is farther away from D, compared to the projection Pp of N's predecessor, P, on (SD). In this latter case, to make sure that N is closer from D compared to its predecessor P, f a steers N towards the symmetric point of Np about Pp on (SD). That way, f a not only allows aligning and orienting a chain towards its user traffic destination, but also triggers the repositioning of intermediate nodes if their order in the chain does not match their respective distance with destination D.

Beacon-based protocol design

A realistic implementation of a distributed force-based scheme requires the local exchange of information between neighboring nodes, which can be achieved via the emission by each node at regular time intervals of a specific beacon message over the radio communication links. With VFPe, we designed a beacon containing information about the emitting node, in order to enable the creation and maintenance of communication chains between user traffic sources and destinations [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF]. In essence, the beacon entries relate to the emitting node identifier and type, position and velocity vectors. Also, if the considered node is a relay in a chain, it contains information about successor, predecessor, destination identifiers and whether a new nearby node should be inserted in the chain as an additional relay. On this basis, VFPe is able to contextually insert S-type nodes into a chain, or on the contrary remove intermediary P-or R-type nodes, which then revert back to their S-type state.

Compared to [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF], we extended the VFPe beacon specification in order to meet our PPDR scenario requirements where the position of user traffic endpoints is initially unknown, must be discovered, and varies with time. Our additions are twofold:

-Supplementary fields were added to account for both source and destination position discovery. A time-related field was also inserted to time-stamp the whole entry and be able to assess position errors with respect to time, as well as to allow the implementation of a VFPe scheme where beacons optionally use the freshest entries, as will be seen in the next section. -As illustrated by Fig. 3, the VFPe structure was extended to allow multiple node entries, the first entry always relating to the beacon emitting node. Additional entries are used to more quickly disseminate network node position and status. The number of entries in the beacon as well as the way entries are sorted is tunable, and is investigated further in the rest of this work. As previously mentioned, VFPe entails both an exploration phase as well as a chain formation and maintenance phase. Since we were particularly interested to evaluate the impact of the exploration schemes on the overall VFPe performance, we designed the set of simulations accordingly. All (P, R, S and T)-type node mobility schemes were implemented within the release 3.23 of the ns-3 network simulator. Network nodes embed an IEEE 802.11b/g network interface card configured for High-Rate Direct Sequence Spread Spectrum (HR-DSSS) at 11 Mb/s. Moreover, the Optimized Link State Routing protocol (OLSR) [START_REF] Clausen | RFC3626, Optimized Link State Routing Protocol (OLSR)[END_REF] supports here multi-hop communication capability, and lossless radio propagation are assumed for the communication devices. Two T-type nodes constitute a user traffic (source, destination) pair and are initially scattered at random within the exploration area Z e . Other nodes start with the S-type status and are initially located at the center of Z e . Moreover, regarding the controlled mobility of the R-type and P-type nodes, VFPe is configured so that each node exerts a virtual force with key parameters valued as shown in Table I. On this matter, it is worth noting that the description of these force-based parameters, as well as the justification for the chosen values, which allow an efficient use of the VFPe protocol, can be found in [START_REF] Reynaud | Lassous: Design of a force-based controlled mobility on aerial vehicles for pest management[END_REF]. Likewise, mobility patterns are valued in Table I, and the Random Waypoint Model (RWP) is mentioned when relevant. Furthermore, each point of the simulated performance curves illustrated and analyzed in the rest of this section results from averaging 2000 independent simulations. The same applies for the measure of contact times between nearby S-type nodes mentioned hereafter. Additionally, the handling of error margins is such that confidence intervals are constructed at a confidence level of 95%. Error bars are shown accordingly for each performance curve in the subsequent figures. Finally, results are analyzed based on the following performance metrics:

-Packet Delivery Ratio (PDR) is defined here with respect to the user traffic flow exchanged between the (S, D) T-type node pair. In that regard, we model this traffic with a constant bitrate (CBR) flow at 10 Kb/s, which is relevant when considering added-value, narrow band PPDR traffic such as predefined status messages and short messages, point-to-point voice communications, vehicle status and transfer of location information, and access to databases in small volumes [START_REF]Radiocommunication Objectives and Requirements for Public Protection and Disaster Relief[END_REF]. More precisely, the PDR here defined by the ratio of the number of CBR packets received by destination node D over the number of CBR packets sent by source node S. -End-to-end delay measures the delay difference between the time of reception by node D of the CBR packets at the application layer and the time of emission of these packets by node S, still at the application layer.

Simulation results

We first took interest in how the performance of the controlled mobility-based VFPe protocol evolves with the way VFPe beacon messages are disseminated by the S-type nodes, when roaming the exploration area Z e . As described in Section 3, VFPe-enabled nodes regularly emit a beacon message, which contains a maximum of cs entries related to previously discovered nodes. Besides the first entry which is related to the emitting node itself, we purposely did not specify at the design stage how the remaining entries should be chosen and prioritized by the emitting node. Instead, we implemented 3 variants of the VFPe protocol, in terms of how VFPe-enabled nodes broadcast their beacon messages:

-VFPe with random contacts: according to this scheme, a VFPe-enabled node chooses the remaining entries at random, irrespectively of the time elapsed since the local information related to these nodes was first generated. -VFPe with fresh contacts: this strategy, unlike the previous scheme, selects the remaining entries to insert in the VFPe beacon by prioritizing the freshest entries (i.e. which were added or updated last in the node local database). -VFPe with ideal node knowledge: we also designed a VFPe extension in which the knowledge of other nodes' coordinates is not approximate and based on the disseminated VFPe beacons, but is assumed to be perfectly known at all times. We considered this ideal strategy to handle an upper range performance as a reference ; however, this theoretical extension does not address how, and at what cost in terms of signalization overhead, these exact positions could be realistically retrieved in an actual network deployment.

In addition, we sought to complement the simulations by evaluating the performance of a RWP-only mobility scheme that does not make use of the VFPe controlled mobility. No VFPe beacons are in this case disseminated and therefore, S-type nodes are never turned into relay nodes. As a consequence, communication chains between the T-type (S,D) pair are never constructed and nodes, whether S-or T-type nodes, only rely on a RWP mobility pattern and on the underlying Mobile Ad Hoc Networks (MANET) OLSR routing protocol.

Incidence of the contact size. As previously mentioned, we define the contact size as cs, the maximum number of entries contained by a VFPe beacon. In this first series of simulations, we studied impact of the number of node information exchanged during a contact between nodes in direct range able to exchange VFPe beacon messages. To this end, we carried out simulations with different values 1 ≤ cs ≤ 20 and measured the PDR of the CBR flow between the (S, D) T-type node pair, as well as the average end-to-end delay taken by flow. As illustrated by Fig. 4 (left), the RWP-only and VFPe-cs-ideal schemes give a low and high performance range with a respective PDR of about 4% and 39%, which both remain constant with cs. At this stage in the analysis, it must be stressed that in the context of the considered network scenario, a maximum PDR value below 40% does not imply here a performance issue and is the expected consequence of the incompressible time needed for unmanned vehicles to move and for the desired chain topology to be established and allow the transmission of user traffic. Regarding the VFPe schemes with beacon messages containing either random entries (VFPe-cs-random) or fresh entries (VFPe-cs-fresh), it can be observed that the PDR is about 14% for cs = 1 (i.e. when nodes only disseminate their own information in the VFPe beacons) and increases with cs, converging towards a similar PDR value around 34%. Further, the random scheme exhibits a significantly steeper increase, since the PDR is already approaching 32% for cs = 2, while the PDR of the fresh scheme is still below 22%. Although this behavior may seem counter-intuitive at first, it can however be explained with the scenario assumptions. As an illustration, with our parameter values and setting cs = 5, we measured for the random scheme an average contact time of 15.4 s between the nearby S-type nodes, which is much larger than the VFPe beacon emission interval. More generally, several successive beacons are likely to be exchanged during such contact times, and the random will offer more diversity in terms of disseminated node entries. As a result, even with low cs values, nodes will handle more accurate coordinates with the random scheme and will be steered towards positions more likely to create the desired communication chains between the (S, D) T-type node pair.

In terms of end-to-end delay, Fig. 4 (right) shows the performance of the considered four schemes. The RWP-only scheme does not use VFPe beacons, hence exhibiting a delay which remains constant with cs. In contrast, the VFPe-cs-ideal scheme increases with cs despite a constant PDR on the whole range of cs, as previously seen. To explain this, it is worth highlighting that in the implementation of our 3 VFPe-enabled schemes, each node entry takes 36 bytes in a VFPe beacon message. Besides, although all simulations rely on a HR-DSSS modulation at 11 Mb/s, the VFPe frame payload is transmitted at a lower bitrate of 1 Mb/s, since the considered beacons are broadcast. As a result, each additional node entry (and therefore incrementation of cs) incurs an increase of about 0.29 ms, which in turns impacts the CBR queued traffic awaiting transmission on the wireless shared medium. Moreover, the delays for both VFPe-cs-random and VFPe-cs-random schemes are lower than 9.5 ms for the whole range of cs values and remain compatible with the low-latency requirements of interpersonal communications, for instance. In that light, the use of the VFPe-cs-random scheme may be preferred since the PDR approaches its maximum value with only a low contact size value (e.g. cs = 4), that is with a small-sized beacon.

Incidence of the number of nodes. For any given deployment scenario, the number of rolled-out systems has a strong impact on the workability of operations and on the overall cost of the solution. We therefore thought to assess how the performance of a controlled mobility scheme like VFPe evolves with the number of network nodes, and in particular with N , the initial number of S-type nodes. Fig. 5 (left) gives a representation of the PDR results for each of the four considered mobility strategies, with 1 ≤ N ≤ 30. In this set of simulations as well, the RWP-only scheme gives a reference, and a low performance range, regarding what can be expected from a simple MANET protocol here: overall, the PDR slightly increases with N , ranging from 3% up to 4.5%. Assuming here a constant value cs = 10, the three VFPe-enabled schemes give PDR results which are consistent with the previous set of simulations: the ideal scheme yields the best results for all values of N in the considered interval, while VFPe-cs-random outperforms VFPe-cs-fresh for N ≥ 10. Besides, all three schemes show a steep PDR increase, then a maximum PDR value for N around 16 to 18, followed by a regular PDR decrease in the rest of the considered interval for N . Moreover, Fig. 5 (right) allows stressing that the end-to-end delays for the three VFPe-enabled schemes, although still acceptable since they remain below 15 ms for all considered values of N , sharply increase with N . As a whole, this set of simulations shows that a limited set N max of S-type nodes (such that 16 ≤ N max ≤ 18 with our assumptions) is needed to reach the best network performance. At this point, in order to properly apprehend those results, it is important to recall that the speed range of exploration S-type nodes, which is [START_REF]The Role of Deployable Aerial Communications Architecture in Emergency Communications and Recommended Next Steps, White Paper[END_REF][START_REF] Daniel | A Communication Aware Steering Strategy Avoiding Self-Separation of Flying Robot Swarms[END_REF] m/s, exceeds the standard speed conditions normally found in pedestriantype scenarios, where MANET protocols, and in particular link-state protocol like OLSR, behave best. As a result, when N = 16, enough S-nodes are initially available so that VFPe induces the best possible chain topologies. As a result, above that threshold for N , no additional S-type node is statistically expected to be converted into a relay (P, R)-type node to extend the communication chains, and the extra S-type nodes will be used by VFPe for exploration purposes only. When N increases above that threshold, the beneficial effects of adding S-type nodes in the network, and therefore increasing link diversity for the underlying multi-hop routing protocol, are severely hindered by the detrimental effects of high-velocity S-type nodes crossing the communication chains. In effect, the underlying MANET protocol will detect those transient and unstable links and try to exploit the corresponding routes, which is in turn likely to result into CBR packet losses, the time for OLSR to detect the link failures and to rebuild its routes accordingly. Further, an in-depth analysis of the simulation traces confirms the increasing amount of OLSR route losses due to the temporary presence of unneeded nearby S-type nodes, when N increases above the aforementioned threshold. In this regard, corrective steps could be taken to prevent the routing protocol from exploiting those suboptimal routes or even to repel S-type nodes (through an extra repulsion force effect, for instance) from an established communication chain. However, it is important to highlight that marginally improving the overall network performance via an increase of additional nodes is not desirable in the context of disaster relief deployment scenarios, for which we seek a limited number of deployed communication systems. With that requirement in mind, the implications from this analysis are threefold: first, VFPe allows reaching a satisfying network performance with a limited number N max of nodes, then that this number N max can be precisely defined, and lastly, that N max remains sufficiently low (16 ≤ N max ≤ 18 with the given assumptions) to offer the perspective of cost-efficient network deployments in real conditions.

Conclusion

In this work, we presented the VFPe protocol, which, by the use of virtual force principles, allows a swarm of mobile network nodes to fly cooperatively, to rapidly form wireless multi-hop communication routes and to efficiently transmit end-user traffic flows. After describing our network architecture proposal and explaining the design choices made for VFPe, notably in terms of force system and beacon-based information dissemination in the network, we analyzed a series of simulation results to assess the impact of the exploration schemes on the overall VFPe performance. We first analyzed how VFPe behaves with the way its beacon messages are disseminated by the network nodes in their exploration phase, and verified that our proposals for realistic VFPe scheme implementations compare satisfyingly with an ideal strategy. We then scrutinized the progression of VFPe performance with respect to the number of network nodes and identified, in the specific context of high mobility underpinning our applicative scenarios, that a maximum efficiency can be obtained with a limited set of nodes. Those results lead us to conclude that VFPe is able to provide an adapted solution for the rapid deployment of temporary networks, notably suited to the demanding context of disaster relief and cost-efficient emergency communications where in particular the amount of communication systems, and in this case the number of mobile network nodes, is constrained. Currently, we are planning to embed a VFPe implementation on quad-rotors to further evaluate the solution through experimentation. In the future, we intend to study the benefits of jointly using a virtual force-based protocol with disruption-and delay-tolerant schemes.

  shows: -Traffic (T-type) nodes impersonate consumer devices and subsequent traffic requirement on the disaster site. A pair (source, destination) is arbitrarily chosen from this set and in the subsequent simulations, we monitor the user traffic from source to destination. -Surveillance (S-type) nodes roam the exploration zone Z e , discover nodes in physical proximity and record their location for later use and dissemination. -Relay (R-type) nodes are former S-type nodes which became intermediate nodes in a communication chain between a (source, destination) T-type pair. When no longer useful in the chain, those nodes can revert to the S-type. -A prospection (P-type) node is physically located at the apex of a forming communication chain. It not only has the role of intermediate node like regular R-type nodes, but is also in charge to evaluate which neighboring S-type node should be changed into a R-type node to further extend the communication chain. When no longer legitimate in this role, a P-type node switches to the R-type or S-type, depending on the context.

Fig. 1 .

 1 Fig. 1. Outline of the network equipment in the considered Disaster Relief scenario.

Fig. 2 .

 2 Fig. 2. Virtual forces f (attraction/repulsion) and fa (alignment) exerted on a node.

Fig. 3 .

 3 Fig. 3. Multi-entry structure of a VFPe beacon

Table 1 .

 1 Main simulation parameters Exploration zone Ze = 1000 m × 1000 m Mobility patterns T-type Position initially uniformly distributed on Ze, RWP, velocity ∈ [0.25, 1] m/s S-type Position initially at center of Ze, RWP, velocity ∈ [5, 10] m/s P-and R-type VFPe-based mobility, velocity ∈ [0, 10] m/s Nodes Number of T-type nodes = 2 Number of (P+R+S)-type nodes = N , node mass = 1 kg When fixed, N = 15. Otherwise, 1 ≤ N ≤ 30. Network 802.11b/g, HR-DSSS at 11 Mb/s, radio range = 100 m, constant speed propagation delay model Routing OLSR protocol with default parameter values [19] VFPe parameters Beacon emission interval = 1 s VFPe forces Interaction f d r = 50 m, d f = 75 m, d a = 100 m, T h dmin = 40 m, T h dmax = 75 m, I = 1 N [15] Friction ffr Cx = 2 [15] Alignment fa fa = 2 N if node is getting closer to the target realignment position, fa = 4 N otherwise User traffic CBR flow at 10 Kb/s between the T-type node pair, CBR packet size = 100 bytes

Fig. 4 .

 4 Fig.[START_REF] Reynaud | An integrated Aerial Telecommunications Network that supports emergency traffic[END_REF]. PDR (left) and end-to-end delay (right) related to the CBR packets received by destination node D, with the number cs of node entries contained in beacon messages.

Fig. 5 .

 5 Fig. 5. PDR (left) and end-to-end delay (right) related to the CBR packets received by destination node D with N, the initial number of S-type nodes.