Chiara Bodei

Linda Brodo

Roberto Bruni

Open Multiparty Interaction

de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

An interaction is an action by which communicating processes can influence each other. Interactions in the time of the Web are something more than input and output between two entities. Actually, the word itself can be misleading, by suggesting a reciprocal or mutual kind of actions. Instead, interactions more and more often involve many parties and actions are difficult to classify under output and input primitives. We can imagine an interaction as a sort of puzzle in which many pieces have to be suitably combined together in order to work.

As networks have become part of the critical infrastructure of our daily activities (for business, social, health, government, etc.) and a large variety of loosely coupled processes have been offered over global networks, as services, more sophisticated forms of interactions have emerged, for which convenient formal abstractions are under study. For example, one important trend in networking is moving towards architectures where the infrastructure itself can be manipulated by the software, like in the Software Defined Networking approach, where the control plane is remotely accessible and modifiable by software clients, using open protocols such as OpenFlow, making it possible to decouple the network control from the network topology and to provide Infrastructure as a Service over data-centers and cloud systems. Another example is that of complex biological interactions as the ones emerging in bio-computing and membrane systems.

As a consequence, from a foundational point of view, it is strategic to provide the convenient formal abstractions and models to naturally capture these new communication patterns, by going beyond the ordinary binary form of communication. These models should be sufficiently expressive to faithfully describe the complex phenomena, but they have also to provide a basis for the formal analysis of such systems, by offering sufficient mathematical structure and tractability. We present here a process calculus, called link-calculus, which takes interaction as its basic ingredient. The described interactions are multiparty, i.e., they may involve more than two processes and are open, i.e., the number of involved processes is not known a priori. Communication actions are given in terms of links, that record the source and the target ends of each hop of interactions. Links can be indeed combined in link chains that route information across processes from a source to a destination. Despite the inherent complexity of representing more sophisticated forms of interaction, we show that the underlying synchronisation algebra and name handling primitives are quite simple and a straight generalisation of dyadic ones. This is witnessed by the operational semantics rules of our calculus, that in the simpler version (i.e., without message passing) resemble the rules of CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], while in the full one they resemble the rules of π-calculus [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF].

Finally, we address a more technical issue, by providing a natural encoding of Cardelli and Gordon's (pure) Mobile Ambients (MA) [START_REF] Cardelli | Mobile ambients[END_REF] in the link-calculus. We have chosen Mobile Ambients as one of the most representative examples of process calculi for compartmentalisation based on the principles of location mobility and location awareness, from which many other models originated as abstractions for global computing, for systems biology and membrane systems. Our encoding highlights the multi-party nature of interactions in MA and shows that the spatial aspects due to the ambient nesting can be dealt with in passing to a flat calculus such as our link-calculus. We prove a tight correspondence at the level of reduction semantics and we provide a new bisimilarity semantics for MA as a side result. We are confident that analogous results can be obtained for many descendants of MA, as e.g., the brane calculus [START_REF] Cardelli | Brane calculi[END_REF].

The paper, where we assume the reader has some familiarity with process calculi, is organised as follows. In Sections 1 and 2 we define the link-calculus, starting from introducing its fragment without name mobility, called Core Network Algebra. In Section 3, we recall the basics of MA. In Section 4, we define the encoding from MA to the link-calculus. In Section 5, we draw some final remarks, outline some future research avenues and point to some related works.

A Core Network Algebra

We start by defining a network-aware extension of CCS, called Core Network Algebra (CNA for short), whose communication actions are given in terms of links. A link is a pair that record the source and the target ends of a communication, meaning that the input available at the source end can be forwarded to the target one. Links are combined in link chains to describe how information can be routed across ends. Link chains also allow seamless realisation of multiparty synchronisations. While in this section we focus on the basic ideas of link interaction, we shall enhance the model with name mobility in the next section.

Links and Link Chains. Let C be the set of channels, ranged over by a, b, c, .... Let C ∪ { τ } ∪ { * } be the set of actions, ranged over by α, β, γ, ..., where the symbol τ denotes a silent action, and the symbol * denotes a non-specified action.

A link is a pair = α \ β ; it can be read as forwarding the input available on α to β, and we call α the source end of and β the target end of . A link = α \ β is valid if either α, β = * or = * \ * In the first case, the link is called solid. The link * \ * is called virtual. We let L be the set of valid links. Examples of non valid links are τ \ * and * \ a .

As it will be shortly explained, a virtual link is a sort of "missing link" inside a link chain, a non specified part that can be supplied, as a solid link, by another link chain, via a suitable composition operation.

A link chain is a finite sequence s = 1 ... n of (valid) links i = αi \ βi s.t.:

1. for any i ∈ [1, n -1], β i , α i+1 ∈ C implies β i = α i+1 β i = τ iff α i+1 = τ 2. if ∀i ∈ [1, n].α i , β i ∈ { τ, * }, then ∀i ∈ [1, n].α i = β i = τ .
The first condition says that any two adjacent solid links must agree on their ends: it also imposes that τ cannot be matched by * . The second condition disallows chains made of virtual links only.

The empty link chain is denoted by . A non-empty link chain is solid if all its links are so. A link chain is simple if it includes exactly one solid link (and one, none or many virtual links). For a solid link and s a simple link chain, we write ∈ s if is the only solid link occurring in s. We write |s| to denote the length of s, i.e., the number of links in s.

We say that an action a is matched in s if: 1) α 1 , β n = a, and 2) for any i ∈ [1, n -1], either β i = α i+1 = a or β i , α i+1 = a. Otherwise, we say that a is unmatched (or pending) in s. For instance, a is matched in the sequence τ \ a a \ τ , while it is not matched in the sequences τ \ * a \ * and in a \ a a \ a a \ a . We can rephrase usual communication primitives of process algebras as links.

-The output action a (resp. the input action a) of CCS can be seen as the link τ \ a (resp. a \ τ ) and the solid link chain τ \ a a \ τ as a CCS-like communication.

-The action a of CSP can be seen as the link a \ a and the solid link chain a \ a a \ a a \ a as a CSP-like communication among three peers over a.

The following basic operations over links and link chains are partial and strict, i.e., they may issue ⊥ (undefined) and the result is ⊥ if any argument is ⊥.

To keep the notation short: if one of the sub-expressions in the righthand side (RHS) of any defining equation is undefined, then we assume the result is ⊥; if none of the conditions in the RHS of any defining equation is met, then the result is ⊥.

Merge. Two link chains can be merged if they are to some extent "complementary", i.e., if they have the same length, each provides links that are not specified in the other and together they form a (valid) link chain. The virtual links in a chain can be seen as the part in the chain not yet specified, and possibly provided by another link chain after a merge. If there is a position where both link chains carry solid links, then there is a clash and the merge is not possible (undefined).

If the merge would result in a non valid sequence, then the merge is not possible. Formally, for s = 1 ... n and s = 1 ... n , with i = αi \ βi and i = α i \ β i for any i ∈ [1, n], we define s • s by letting:

3 s • s ( 1 • 1 )...( n • n ) α \ β • α \ β (α•α ) \ (β•β ) α • β α if β = * β if α = *
Roughly, the merge is defined element-wise on the actions of a link chain, by ensuring that whenever two actions are merged, (at least) one of them is * and that the result of the merge is still a link chain. Intuitively, we can imagine that s and s are two parts of the same puzzle separately assembled, where solid links are the pieces of the puzzle and virtual links are the holes in the puzzle and their merge s • s puts the two parts together, without piece overlaps.

Example 1. Let s 1 = τ \ * a \ * * \ * , s 2 = * \ a * \ * b \ * ,
s = s 1 • s 2 = ( τ \ a • * \ * )( * \ * • a \ b )( * \ * • * \ * ) = ( τ • * \ a• * )( * •a \ * •b )( * • * \ * • * ) = τ \ a a \ * b \ * .
Similarly, s and s 3 can then be merged to obtain:

s • s 3 = τ \ a a \ b b \ τ . Lemma 1. (i) If s is solid, then for any s we have s • s = ⊥.
(ii) The merge of link chains is a commutative and associative operation.

(iii) For any , :

• = * \ * if and only if = = * \ * .
Restriction. Certain actions of the link chain can be hidden by restricting the channel where they take place. Of course, restriction is possible only if this process does not introduce any unmatched communication, as in τ \ * a \ * . Formally, for s = 1 ... n , with i = αi \ βi with i ∈ [1, n], we define the restriction operation (ν a)s by letting

(ν a)s α1 \(ν a)( α2 β1 )\...\(ν a)( αn βn-1 )\ βn if α 1 , β n = a (ν a)( α β ) τ τ if α = β = a α β if α, β = a Lemma 2. (i) For any a, : (ν a) = * \ * if and only if = * \ * .
(ii) For any a, s, s such that a does not appear in s:

(ν a)(s • s ) = s • (ν a)s . (iii) For any a, b, s: (ν a)(ν b)s = (ν b)(ν a)s. Example 2. Let s = τ \ a a \ * b \ * and s = * \ * * \ b * \ τ . Then, (ν a)s = τ \(ν a)( a a )\(ν a)( * b )\ * = τ \ τ τ \ * b \ * . Similarly, (ν a)(s • s ) = τ \ τ τ \ b b \ τ = ((ν a)s) • s .
Process Syntax. The CNA processes are generated by the following grammar (for brevity, we omit the CCS-like renaming operator P [Φ] because it will be later subsumed by the syntax in Section 2):

P, Q ::= 0 | X | .P | P + Q | P |Q | (ν a)P | recX. P
where is a solid link (i.e., = α \ β with α, β = * ).

Roughly, processes are built over a CCS-like syntax (with nil process 0, prefix .P , sum P + Q, parallel P |Q, restriction (ν a)P and recursion recX. P , for X a process variable, but where the underlying synchronisation algebra is based on link chains. This is made evident by the operational semantics, presented below.

As usual, (ν a)P binds the occurrences of a in P , the sets of free and of bound names of a process P are defined in the obvious way and denoted, respectively, by fn(P ) and bn(P ), processes are taken up to alpha-conversion of bound names, and we shall often omit trailing 0, e.g. by writing a \ b instead of a \ b .0 Operational Semantics. The idea is that communication can be routed across several processes by combining the links they make available to form a link chain. Since the length of the link chain is not fixed a priori, an open multiparty synchronisation is realised.

The operational semantics is defined in terms of a Labelled Transition System (LTS) whose states are CNA processes, whose labels are link chains and whose transitions are generated by the SOS rules in Fig. 1. Notice that the SOS rules are very similar to the CCS ones, apart from the labels that record the link chains involved in the transitions: moving from dyadic to linked interaction does not introduce any complexity burden. We comment in details the rules (Act), (Res), and (Com). In rules (Res) and (Com) we leave implicit the side conditions (ν a)s = ⊥ and s • s = ⊥, respectively (they can be easily recovered by noting that otherwise the label of the transition in the conclusion would be undefined).

The rule (Act) states that .P s -→ P for any simple link chain s whose unique solid link is . Intuitively, .P can take part in any interaction, in any (admissible) position. To join in a communication, .P should suitably enlarge its link to a simple link chain s including it, whose length is the same for all participants in order to proceed with the merge operation. Following the early style, the suitable length can be inferred at the time of deducing the input transition. Note that if one end of is τ , then can only appear at one extreme of s.

In the (Res) rule, the operator (νa) applied to s, can serve different aims: floating, if a does not appear in s, then (ν a)s = s; hiding, if a is matched in s (i.e., a appears as ends already matched by adjacent links), then all occurrences of a in s are renamed to τ in (ν a)s; blocking, if a is pending in s (i.e., there is a 'nonmatched' occurrence of a in s), then (ν a)s = ⊥ and the rule cannot be applied.

In the (Com) rule the link chains recorded on both the premises' transitions are merged in the conclusion's transition. This is possible only if s and s are to some extent "complementary". Contrary to CCS, the rule (Com) can be applied several times to prove that a transition is possible, because s • s can still contain virtual links (if s and s had a virtual link in the same position). However, when s • s is solid, no further synchronisation is possible (by Lemma 1 (ii)). Example 3.

Let P = τ \ a .P 1 |(ν b)Q and Q = b \ τ .P 2 | a \ b .
The process τ \ a .P 1 can output on a, while b \ τ .P 2 can input from b; the process a \ b provides a one-shot link forwarder from a to b. Together, they can synchronise by agreeing to form a solid link chain of length 3, as follows, where (νb

) * \ a * \ b b \ τ = * \ a * \ τ τ \ τ . (Act) τ \a.P1 τ \ * a \ * * \ * ------→ P1 (Act) b \τ .P2 * \ * * \ b * \τ ------→ P2 (Act) a \ b .0 ------→ 0 (Com) Q * \ a * \ b b \τ ------→ P2|0 (Res) (ν b)Q * \ a * \ τ τ \τ ------→ (ν b)(P2|0) (Com) P τ \ a a \ τ τ \τ -------→ P1|(ν b)(P2|0)
The following lemma, whose proofs go by rule induction, shows that labels behave like an accordion. Any label s in a transition is interchangeable or replaceable with any chain having one or more * \ * either on the left or on the right or on both sides of s. It is also replaceable with any composition where each * \ * inside s is replaced by one or more * \ * . This fact can be exploited later, when the abstract semantics is given.

Lemma 3. (i) If P s -→ P and s * \ * (resp. * \ * s) is valid, then P s * \ * ---→ P (resp. P * \ * s ---→ P ). Vice versa, if P s -→ P and s = s * \ * or s = * \ * s, then P s -→ P . (ii) If P s1 * \ * s2 -----→ P then P s1 * \ * * \ * s2 ------→ P . Vice versa, if P s1 * \ * * \ * s2
------→ P then

P s1 * \ * s2 -----→ P . (iii) If P s1 α \ a a \ β s2 -------→ P then P s1 α \ * a \ a * \ β s2 --------→ P . Vice versa, if P s1 α \ * a \ a * \ β s2 --------→ P then P s=s1 α \ a a \ β s2 --------→ P . Note that if P a \ τ τ \ b
----→ P , then it is not the case that a virtual link can be inserted in the middle of the chain, because the τ 's may represent a communication on a restricted channel and a \ * τ \ τ * \ b is not a valid link chain anyway.

Routing examples. We give a few examples to show how flexible is CNA for defining "routing" policies. We have already seen a one-shot, one-hop forwarder from a to b, that can be written as a \ b .0. Its persistent version is just written as P a b recX. a \ b .X. Moreover, with P a b |P b a we obtain a sort of name fusion between a and b, i.e., a and b can be interchangeably used. An alternating forwarder from a to b first and then to c can be defined as

A a b,c recX. ( a \ b . a \ c .X).
A persistent non-deterministic forwarder, from a to c 1 ...c n can be written, e.g., as

P a c1...cn recX. ( a \ c1 .X + • • • + a \ cn .X). Similarly, P b1...bm a recX. ( b1 \ a .X + • • • + bm \ a .X) is a persistent non-deterministic forwarder, from b 1 ...b m to a.
By combining the two processes as (ν a)(P b1...bm a |P a c1...cn ), then we obtain a persistent forwarder from any of the b i 's to any of the c j 's.

Abstract semantics. As usual, we can use the LTS semantics to define suitable behavioural equivalences over processes. We are interested in bisimilarity. However, when comparing two labels we abstract away from the number and identities of hops performed and from the size of the sequences of virtual links. Definition 1. We let be the least equivalence relation over link chains closed under the following axioms (remind that α, β, γ

∈ C ∪ { τ, * }): * \ * s s s 1 α \ γ γ \ β s 2 s 1 α \ β s 2 s * \ * s
A link chain is essential if it is composed by alternating solid and virtual links, and has solid links at its ends. An essential link chain has minimal length with respect to equivalent link chains and concisely represent the missing "paths" of interactions between those already completed. For example, we have that It is immediate to check that by orienting the axioms in Def. 1 from left to right we have a procedure to transform any link chain s to a unique essential link chain s such that s s . We write e(s) to denote such unique representative, which enjoys the following nice properties, useful in the proof of the following Proposition 1. The first part of the lemma says that e(•) induces an equivalence over link chains that is a congruence with respect to juxtaposition of link chains (when it is well-defined). The second part says that taken two link chains s 1 and s 2 in the same equivalence class, and given any sequence s that can be merged with s 1 , then it is possible to find a link chain s , in the same equivalence class as s, such that it can be merged with s 2 and the result is equivalent to s • s 1 .

* \ a * \ τ τ \ * b \ * * \ c * \ d d \ * a \ * is equivalent to the essential chain a \ * b \ c * \ a

Lemma 5.

(i) If e(s 1 ) = e(s 2 ), then for any s such that s 1 s (resp. ss 1 ) is a link chain we have that also s 2 s (resp. ss 2 ) is a link chain and e(s 1 s) = e(s 2 s) (resp. e(ss 1 ) = e(ss 2 )).

(ii) If e(s 1 ) = e(s 2 ), then for any s such that s • s 1 = ⊥ there exists a link chain s s such that s • s 2 = ⊥ and e(s • s 1 ) = e(s • s 2 ).

In the following, we write P → P when P s -→ P for some s s.t. e(s) = τ \ τ .

Definition 2. A network bisimulation R is a binary relation over CNA processes such that, if P R Q then:

-P s -→ P , then ∃ s , Q such that e(s) = e(s ), Q s -→ Q , and P R Q ; -if Q s -→ Q , then ∃ s , P
such that e(s) = e(s ), P s -→ P , and P R Q .

We let ∼ n denote the largest network bisimulation and we say that P is network bisimilar to

Q if P ∼ n Q. Example 4. Consider the two processes P recX. a \ b .X and Q recX. (ν c) ( a \ c | c \ b .X).
We have that whenever P s -→ P , then P = P and e(s)

= a \ b . Similarly, whenever Q s -→ Q , then Q = (ν c)(0|Q
) and e(s) = a \ b . Then we prove that P ∼ n Q by showing that the relation R below:

R {(P, R) | ∃n.R = C n [Q]} is a network bisimulation, where C n [Q] is inductively defined by letting C 0 [Q] Q and C n+1 [Q] C[C n [Q]] for C[•] the context (ν c)(0|•) Proposition 1. Network bisimilarity is a congruence.
Proof. The proof uses standard arguments. The only non-trivial case is that of parallel composition. We want to prove that if P ∼ n Q then for any R we have -→ Q with e(s 1 ) = e(s 1 ) and P ∼ n Q . Now it may be the case that s 1 • s 2 is not defined, but by the previous technical lemmata, we know that s 1 and s 2 can be stretched resp. to s 1 and s 2 by inserting enough virtual links to have that

P |R ∼ n Q|R.
s 1 • s 2 is defined, e(s 1 • s 2 ) = e(s 1 • s 2 ), Q s 1 -→ Q and R s 2 -→ R . We conclude by applying rule (Com): Q|R s -→ Q |R with P |R R | Q |R by definition of R | .
Analogously to CCS, it is immediate to check that several useful axioms over processes hold up to network bisimilarity, like the commutative monoidal laws for | and +, the idempotence of + and the usual laws about restriction.

The calculus of linked interactions

We can now enhance the algebra to deal with name passing and call it the calculus of linked interactions (link-calculus for short), by extending, in the syntax, link prefixes with tuples of arguments, where each link in the whole chain simply carries the same list of arguments, but with different (send/receive) capabilities.

P, Q ::= • • • | t.P
In this way, we keep apart the interaction mechanism from the name-passing one that eventually fit together in synchronisations. We have just borrowed from πcalculus the name handling machinery (and liberated it from dyadic interaction legacy), still having input, output and extrusion mechanisms.

In the tuple t = w , names can be used either as values or as variables. To be distinguished, variables are underlined. During communication, variables are instantiated by values, while values are used for matching arguments, as in [START_REF] Bodei | Detecting and preventing type flaws at static time[END_REF].

Example 5. Consider e.g., the tuples in the two "complementary" prefixes like τ \ a id, n, x .P and a \ τ id, y, m .Q, where x is an input for P , y is an input for Q, and id is a name known by both processes: the two links can be merged, the first parameters must match exactly, n is assigned to y, while m is assigned to x. This mechanism allows, e.g., a form of multi-way communication, where all peers involved in the chain link can express arguments to be matched and provide actual arguments to replace the formal ones of other peers. For a tuple t, we let vals(t) and vars(t) denote the set of values and the set of variables of t, respectively. We say that a tuple t is ground if vars(t) = ∅.

We assume action names are admissible values, i.e., as in π-calculus we have the possibility to communicate (names of) means of communication. Similarly to (ν a), the prefix t.P binds the occurrences of the variables vars(t) in P (and the notions of free names fn(P ), bound names bn(P ) and alpha-conversion are updated accordingly). In the following, given two sets of names S and T , we write S#T as a shorthand for S ∩ T = ∅.

Operational semantics. The operational semantics is defined in terms of an LTS whose states are link-calculus processes, whose labels are pairs sg of link chains and tuples and whose transitions are generated by the SOS rules in Fig. 2.

In a label of the form sg, with s solid, g must be the empty tuple , i.e., it is not possible to observe the arguments of a completed communication. We let s abbreviate s .

We denote by σ = [x 1 → v 1 , ..., x n → v n ] the substitution that replaces each x i with v i , and is the identity otherwise, and set vars(σ) = { x 1 , ..., x n }. For a tuple t = w 1 , ..., w n , a link = α \ β , and a substitution σ = [x 1 → v 1 , ..., x n → v n ] we define tσ and σ element-wise as:

tσ w1σ, ..., wnσ σ ασ \ βσ aσ vi if a = xi for some i ∈ [1, n] a otherwise aσ vi if a = xi for some i ∈ [1, n] a otherwise
The application of σ on processes is defined as below (note that, as processes are taken up to alpha-conversion of bound names, it is always possible to find suitable representatives of t.P and (ν a)P , such that ( t.P )σ and ((ν a)P )σ are well-defined): We say that g is a full instance of t and write g σ t if vars(σ) = vars(t)∧g = tσ.

Like in the π-calculus, names in the tuple can be extruded during the communication. In the labels of transitions, we need to annotate positions in the tuple to distinguish between arguments that are taken in input (i.e., they are guessed instances), or that are extruded. We underline the former and overline the latter. A name can be extruded when it is not already annotated; after the extrusion, it will be overlined. Formally, given a (annotated) tuple g, we define (ν a)sg and (ν a)g as follows: We let ex (g) denote the set of extruded (i.e., overlined) names appearing in g.

We write a ∈ g if the name a appears in the tuple g (with or without annotation). Two annotated tuples can be merged when they list exactly the same values in the same order, and if the values in matching positions are annotated in some compatible way. Formally, if w = w 1 , ..., w n and w = w 1 , ..., w n :

sg • s g (s • s )(g • g ) w • w w1 • w 1 , ..., wn • w n w • w    w if (w = w = v) ∨ (w = w = v) v if (w = v ∧ w = v) ∨ (w = v ∧ w = v) v if (w = v ∧ w = v) ∨ (w = v ∧ w = v) Example 6. Back to Ex. 5, τ \ * a \ * id, n, m • * \ a * \ τ id, n, m = ( τ \ * a \ * • * \ a * \ τ ) ( id, n, m • id, n, m ) = τ \ a a \ τ id • id, n • n, m • m = τ \ a a \ τ id, n, m .
Recall that in the early-style (Act) rule the values to be received are guessed and so the prefix variables y and x are replaced by n and m, respectively.

Lemma 7. If g • g = ⊥, then vars(g • g ) ⊆ vars(g) ∩ vars(g ).
A close look at the SOS rules in Fig. 2 shows that they resemble the early semantic rules of π-calculus. The main difference is that we are dealing with a multi-party form of communication, hence the "close" rule must be applied when the communication has been completed. Let us briefly comment on the rules. (ν a)P Rule (Act) allows the process t.P to offer the tuple t in a communication on the link . More precisely, following an early style, the actual tuple to be communicated must be a full instance of t (see the condition g σ t): the communication is that of sg, where variables appearing in t are replaced in g = tσ by actual parameters. must hold. The substitution σ is also applied to the continuation, after the transition (P σ).

(ν a)sg ----→ P P sg -→ P Q s g --→ Q ex (g)#fn(Q) ex (g )#fn(P ) s • s is not solid (Com) P |Q sg•s g -----→ P |Q P sg -→ P Q s g --→ Q ex (g)#fn(Q) ex (g )#fn(P ) s • s is solid g • g is ground (Close) P |Q s•s --→ (ν ex (g • g ))(P |Q )
In rules (Res) and (Open) we leave implicit the side condition (ν a)sg = ⊥. Rule (Res) is applicable whenever a ∈ g, in which case (ν a)g = g = ⊥ and thus (ν a)(sg) = ((ν a)s)g. Rule (Open) models the extrusion of a. Note that, since (ν a)sg = ⊥ and a ∈ g, we have that the only possibility for a to appear in g is without annotations (otherwise (ν a)g = ⊥). Then, by definition of (ν a)g, all occurrences of a within g are overlined in (ν a)g (to denote the name extrusion).

In rule (Com), the annotated tuples are "complementary" and can be merged, by merging the link chains and the two tuples. Note that we leave implicit the side condition sg •s g = ⊥, because the sg •s g annotates the label of the conclusion transition. In addition, rule (Com) checks that extruded names of one process do not clash with the free names of the other process (like in ordinary π-calculus) and finally that the communication is not completed yet (s • s not solid).

Rule (Close) checks differ from (Com) one, because (Close) is applicable only when the communication has been fully completed and cannot be further extended (s•s is solid), in which case we must close, i.e., put back the restriction of all names extruded in the communication ((ν ex (g • g ))). Still, we need to make sure that g • g has no unresolved input, i.e., that all requested values have been issued (g • g is ground). Moreover, the observed label is just s • s , as explained before. This is similar to the π-calculus mechanism, according to which the synchronisation of e.g., a x and a x yields τ and not τ x .

While rules (Lsum), (Rsum) and (Rec) are straightforward, rules (Lpar) and (Rpar) need just to check that extruded names of one process do not clash with free names of the other process (like in ordinary π-calculus).

Note that if the only used tuples are the empty ones , then the semantics rules coincide with the ones of CNA.

Example 7. Consider the following restricted process, built on the processes in Ex. 5, S (ν a)( τ \ a id, n, x .P |(ν m) a \ τ id, y, m .Q). In one step, S can reduce to S (ν a)(ν m)(P [x → m]|Q[y → n]), via the communication τ \ τ τ \ τ id, n, m , where the restriction on a hides the matched occurrences of a in τ \ a a \ τ and the restriction on m causes the extrusion of the name m (to process P ). Moreover, since the chain link τ \ τ τ \ τ is solid (i.e., it cannot be extended further) and the tuple id, n, m is ground, we remove the tuple from the observed label, i.e.,

S τ \ τ τ \τ ----→ S .
No other interaction is possible.

Abstract semantics By analogy with the early bisimilarity of the π-calculus, we extend the notion of network bisimilarity to consider the tuples of names.

Definition 3. A linked bisimulation R is a binary relation over link-calculus processes such that, if P R Q then:

if P sg -→ P with ex (g)#fn(P ), then there exists s and Q such that e(s) = e(s ), Q s g --→ Q , and P R Q ; if Q sg -→ Q with ex (g)#fn(Q), then there exists s and P such that e(s) = e(s ), P s g --→ P , and P R Q .

We let ∼ l denote the largest linked bisimulation and we say that P is linked bisimilar to Q if P ∼ l Q.

The following result may look surprising, since early bisimilarity is not a congruence in the case of π-calculus, due to the input prefix context. The classic counterexample is P = x|y being bisimilar to Q = x.y + y.x but a(y).P being not bisimilar to a(y).Q (when the name received on y is x, a τ move is available for P [y → x] but not for Q[y → x]). The fact is that the SOS semantics of the link-calculus can collect the ready set of prefixes concurrently available to be executed (e.g., by separating them through virtual links); thus the above P and Q are not considered as bisimilar. In other words, virtual links allow to establish an interaction between different ends, as if a substitution was available to rename one end into the other, i.e., the semantics is already substitution closed. Proposition 2. Linked bisimilarity is a congruence.

(In) n[ in m.P | Q ] | m[ R ] → m[ n[ P | Q ] | R ] (Out) m[ n[ out m.P | Q ] | R ] → n[ P | Q ] | m[ R ] (Open) open n.P | n[ Q ] → P | Q P → Q (Res) (ν n)P → (ν n)Q P → Q (Amb) n[ P ] → n[ Q ] P → Q (Par) P | R → Q | R P ≡ P P → Q Q ≡ Q (Cong) P → Q P ≡ P Q ≡ P ⇒ P ≡ Q P ≡ Q, Q ≡ R ⇒ P ≡ R P | 0 ≡ P P | Q ≡ Q | P (P | Q) | R ≡ P | (Q | R) (ν n)0 ≡ 0 (ν n)(ν m)P ≡ (ν m)(ν n)P P ≡ Q ⇒ P |R ≡ Q|R (ν n)(P | Q) ≡ P | (ν n)Q, if n ∈ fn(P ) P ≡ Q ⇒ (ν n)P ≡ (ν n)Q !P ≡ P | !P (ν n)(m[ P ]) ≡ m[ (ν n)P ], if n = m P ≡ Q ⇒ n[ P ] ≡ n[ Q ]

Background on Mobile Ambients

In this section, we briefly recall Mobile Ambients (MA) syntax and semantics, in order to show the encoding of MA in the link-calculus, in the next section. Mobile Ambients (MA) [START_REF] Cardelli | Mobile ambients[END_REF] is a calculus for mobility that includes both mobile agents and mobile computational ambients in which agents interact. Ambients are bounded locations, such as a web page or a virtual address space, that can be moved as a whole. Each ambient has a name and can include sub-ambients to form a hierarchical structure, that can be dynamically modified by agents.

We focus here on the so-called pure MA, i.e., disregarding communication primitives and variables for brevity. However our results in Section 4 can be easily extended to the more general case.

Let n range over the numerable set of names N . The set of mobile ambient processes P M A (with metavariable P ) and the set of capabilities Cap (with metavariable M) are defined below:

P ::= 0 | (ν n)P | P |Q | !P | n[ P ] | M.P M ::= in n | out n | open n
The first four constructs are quite standard in process calculi, while the other ones are specific to ambients: n[ P ] denotes the ambient n in which the process P runs; M.P executes an action depending on the capability M and then behaves as P . There are three kinds of capabilities: one for entering, one for exiting and one for opening up an ambient. In the process in m.P the entry capability allows the immediately surrounding ambient n (if any) to find a sibling ambient named m where to enter (i.e., to become a child of m). Similarly, in the process out m.P the exit capability allows the immediately surrounding ambient n to exit its parent ambient (if named m) and to become a sibling of m. Finally, in open m.P the open capability allows the boundary of an ambient m located in parallel to be dissolved. Each interaction involves more than two parties.

The only binder is (ν n) and the sets of free names and of bound names of a process P are defined in the obvious way and denoted, respectively, by fn(P ) and bn(P ). As usual, the restriction of a sequence of names m = {m 1 , ..., m k } for a process P is denoted as (ν m)P and stands for (νm 1 )...(νm k )P . We shall denote by σ = [n → m] the (capture-avoiding) substitution that replaces n by m, and by P σ the process obtained by applying σ to P to replace all free occurrences of n in P by m. Processes are taken up to alpha-conversion of restricted names, i.e., (ν n)P denotes the same process as (ν m)(P [n → m]) whenever m ∈ fn(P ).

The semantics of the MA is given by the reduction and the structural congruence rules in Fig. 3. Besides the one-step reduction rules for movement capabilities ((In), (Out) and (Open)) and the usual reduction rule for congruence (Cong), the other rules propagate reductions across scopes (Res), ambient nesting (Amb) and parallel composition (P ar).

Example 8. Consider the process

P m[ s[ in n.R ] | T ] | open m.Q | n[ G ] (for suitable R, T, Q, G) that can
execute an open m followed by an in n:

P → s[ in n.R ] | T | Q | n[ G ] → T | Q | n[ s[ R ] | G ]
We write P ↓ n , and say that P has barb n, if P ≡ (ν m)(n[P 1 ]|P 2 ) for some names m and processes P 1 and P 2 with n ∈ m. We say that P has weak barb n, written P ⇓ n if there exists P such that P → * P and P ↓ n , for → * the reflexive and transitive closure of the (immediate) reduction relation →. Let R a binary relation on processes. We say that:

-R is preserved by contexts if P R Q implies C[P ] R C[Q] for any context C[•]; -R is closed under reductions (or reduction closed ) if whenever P R Q and P → P then there exists Q such that Q → * Q and P R Q ; -R is barb preserving if P R Q and P ↓ n implies Q ⇓ n .
Definition 4. Reduction barbed congruence, written ∼ =, is the largest relation over processes, which is reduction closed, barb preserving, and preserved by all contexts.

Encoding Mobile Ambients

We are now ready to show our encoding of MA in the link-calculus, that follows the idea developed in [START_REF] Brodo | On the expressiveness of the pi-calculus and the mobile ambients[END_REF]. We pick MA as an interesting case because ambient interactions are inherently multi-party, even when they apparently involve only two parties. Each movement involves an ambient and the process exercising the corresponding capability, but the resulting reconfiguration of the hierarchical structure also impacts on the ambients and processes of the context. Rule (In) requires a three-party interaction (at least), involving: 1) the process in m.P with the capability to enter the ambient m; 2) its parent ambient n[ • ] to be moved; 3) the ambient m[ • ] to be entered. The rule can be successfully applied only when all the three entities are available. Any encoding based on binary interactions must deal with atomicity issues in the completion of the move, with conflicting, concurrent operations on the same ambient and with the possibility of retract/roll-back in case only two peers out of three are available.

Similarly, rule (Out) requires a three-party interaction (at least), involving: 1) the process out m.P with the capability to leave the ambient m; 2) its parent ambient n[ • ] to be moved; 3) the "grand-parent" ambient m[ • ] (where n[ • ] is enclosed) to be exited.

Rule (Open) apparently requires a two-party interaction only, but as a matter of fact it is more complex than the other two rules, as it introduces the need of multi-party interactions with an unbounded number of peers. This is because when the ambient n[ Q ] is dissolved, its content Q must be relocated, which may consist of an unbounded (and not known a priori) number of parallel processes: they all participate to the interaction! We adopt here a syntactic solution with no semantic impact on the rest: we replace n[ • ] with some sort of blind forwarder that leaves Q unaware of the deletion of n[ • ]. However, the presence of forwarders complicates the interactions needed by rules (In) and (Out), because the three parties can now be connected via chains of forwarders of arbitrary length. Our forwarders are reminiscent of forwarders in π-calculus [START_REF] Gardner | Linear forwarders[END_REF], inspired by [START_REF] Wischik | Explicit fusions[END_REF].

Roughly, the idea is to define an encoding assigning to any MA process P a corresponding link-calculus process P ã (the role of names ã will be made clear later) such that:

for any reduction P → P there is a step P ã → P ã; and vice versa, for any silent step P ã → Q there is an MA process P such that Q = P ã and P → P .

Unfortunately, a direct encoding has to deal with the presence of forwarders, so that in general:

for any reduction P → P we can find a step P ã → Q but Q can differ from P ã because of the presence of forwarders; and vice versa, for any silent step P ã → Q we can find an MA process P such that P → P but, again, Q can differ from P ã because of the presence of forwarders.

One possible turnaround is to show that the correspondence holds up to some suitable abstract equivalence instead of strict equality. Instead, we provide a tighter correspondence that introduces forwarders in the syntax of MA, with no effect whatsoever on the semantics and expressiveness, and that allows us to recover the stronger correspondence result sketched above, with exact matching between the reductions of MA and the silent steps of the link-calculus (modulo some standard structural laws imposed by the MA structural congruence).

Ambients within Brackets

We just extend the syntax of MA with the possibility to enclose a process P within a pair of parentheses:

P ::= • • • | P
making the presence of parentheses inessential w.r.t the behaviour of the process.

To this aim, we introduce the additional structural congruence axioms:

(ν n)P ≡ (ν n) P P ≡ Q ⇒ P ≡ Q
Finally, we define the notion of passive context C, to adjust the basic reduction rules to deal with the presence of an arbitrary number of balanced parentheses.

C, D, E ::= • | C | C|P | P |C
and write C(P ) to denote the process obtained by replacing the hole • in C with P . Thus we add the suitable reduction rules:

(In) D(n[ C(in m.P ) ]) | E(m[ R ]) → D(0) | E(m[ n[ C(P ) ] | R ]) (Out) m[ D(n[ C(out m.P ) ]) ] → n[ C(P ) ] | m[ D(0) ] (Open) C(open n.P ) | D(n[ Q ]) → C(P ) | D( Q ) P → Q (Brac) P → Q Structural Encoding
The encoding of a (possibly parenthesised) MA process is defined by delegating the management of an ambient n[ • ] to a suitable linkcalculus process. The multi-party interaction between capabilities and ambients is regulated via communication on dedicated ports. Informally, a process P "resides" in some location, to which it addresses all its requests about the next actions to perform. The process that simulates the ambient n[ • ] also resides in some location p: it also defines an inner location ã, where its content resides. A location ã denotes the 5-tuple of ports a in , a [in] , a out , a [out] , a opn , where:

1. a in is used for the interaction between the capability "in m" to enter the ambient m and the ambient n[ • ] where it is contained; 2. a [in] for the interaction between the ambient n[ • ] that contains the capability "in m" and the ambient m[ • ] to be entered; 3. a out for the interaction between the capability "out m" to exit the ambient m and the ambient n[ • ] where it is contained; 4. a [out] for the interaction between the ambient n[ • ] that contains the capability "out m" and the ambient m[ • ] (that contains both) to be exited; 5. a opn for the interaction between the capability "open n" to open the ambient n and the sibling ambient n[ • ] to be dissolved.

In the encoding, dissolving ambients amounts to resorting to forwarders, located between the dissolved locations and the "parent" ones, that redirect all the interactions that involve the processes originally inside the dissolved ambient. Forwarders need to forward requests through arbitrarily long chains of indirection. These are requests arriving from "below" (i.e., from the processes inside the

0 ã 0 n[ P ] ã (ν b)(Amb(n, b, ã)| P b ) P |Q ã P ã| Q ã in m.P ã τ \a in m, x . P ã (ν n)P ã (ν n) P ã out m.P ã τ \a out m, x . P ã !P ã recX. ( P ã|X ) open n.P ã τ \a opn n . P ã P ã (ν b)(Fwd ( b, ã)| P b Amb(n, ã, p) a in \p [in] m, z .Amb(n, ã, z) + p [in] \τ n, ã .Amb(n, ã, p) + a out \p [out] m, z .Amb(n, ã, z) + a [out] \τ n, p .Amb(n, ã, p) + popn \τ n .Fwd (ã, p) Fwd (ã, p) a in \p in n, x .Fwd (ã, p) + a [in] \p [in] n, x .Fwd (ã, p) + p [in] \a [in] n, x .Fwd (ã, p) + a out \p out n, x .Fwd (ã, p) + a [out] \p [out] n, x .Fwd (ã, p) +
aopn \p opn n .Fwd (ã, p) + popn \a opn n .Fwd (ã, p) Fig. 4. Structural encoding of MA in link-calculus dissolved ambient) to be forwarded up and requests arriving from "above" (i.e., from the processes that want to interact with the processes inside the dissolved ambient) that must be forwarded down: the former case applies to all ports, whereas the second case applies only to ports a [in] and a opn . The encoding P ã of P is parametric with respect to its location, i.e., the tuple of ports to be used to communicate with the enclosing ambient (or forwarders). Name passing is used to match the name of the ambient for which the capability is applicable with the name of the ambient where we would like to apply it. Moreover, in the case of enter/exit capabilities, name passing is necessary to inform the ambient that moves about the location where it is relocated.

We implicitly assume that all restricted names introduced by the encoding are (globally) "fresh". The encoding is defined by straightforward structural induction in Fig. 4, where the processes Amb(n, ã, p) and Fwd (ã, p) represent, respectively, an ambient n located at p and providing its content with location ã, and a forwarder between the dissolved location ã and the "parent" location p.

As said above, applying the rule (In) to a process n[ in m.P | Q ] | m[ R ] requires at least a three-party interaction, whose corresponding encodings are commented below. To help intuition, we can represent ambients as graphs, that reflect the hierarchical structure of nested ambients and that record the locations of ambients reside and the inner locations where ambients contents reside. We now illustrate how the encoding works in Fig. 5, where the labels to be merged are in correspondence with the processes that issued them, and the processes are arranged according to the hierarchy of processes:

(i) The process in m.P with the capability to enter the ambient m is encoded by τ \ ain m, x . P ã, where the emphasis is on the name m (variables in x are not important) and a in is the port for the entering interaction.

• b • b Amb(n, ã, b) * \ a in * \ * b [in] \ * m, c Amb(m, c, b) * \ * * \ b [in] * \τ m, c Amb(m, c, b) • a • c lab i / / • c in m.P ã τ \ * a in \ * * \ * m, c Q ã R c Amb(n, ã, c) R c • a P ã Q ã
Fig. 5. Three party interaction for entering an ambient, where labi stands for b [in] \ τ (by the application of the rule (Res) when (ν a) is encountered) and the tuple records the extrusion of c, i.e., it becomes m, c (by the application of the rule (Open) when (ν c) is encountered). In the end, the whole transition is just labelled by

(ν ã)(ν c) τ \ a in a in \ b [in] b [in] \τ = τ \ τ τ \ b [in] b [in] \τ (
τ \ τ τ \ b [in]
b [in] \ τ , because the link chain is solid, and thus the (ground) tuple m, c is discarded by rule (Close) (that also restores the restriction on the extruded location c that was removed by the (Open) rule).

Similarly, as described in Fig. 6, the rule (Out) requires the encodings for: 1) the process out m.P capable to leave the ambient m; 2) its parent ambient n[ • ] to be moved; 3) the "grand-parent" ambient m[ • ] (enclosing n[ • ]) to be exited.

Finally (see Fig. 6), in the rule (Open) besides the encodings for the processes open n.P and n[ Q ], we should take care of the relocation of all processes included in the ambient n. We obtain this by using a forwarder, as explained below. \ τ n = τ \ bopn bopn \ τ n that is a solid link chain (in this case there are no extruded names in the tuple). In the following, t stands for the topmost location in which the ambients reside. Definition 5. We let ≡ l be the structural congruence on link-calculus processes induced by the axioms:

• b • b Amb(m, c, b) * \ * * \ c [out] * \τ m, b Amb(n, ã, b) Amb(m, c, b) • c τ \ τ τ \ τ τ \τ / / • a • c Amb(n, ã, c) * \ a out * \ * c [out] \ * m, b R c P ã Q ã R c • a out m.P ã τ \ * a out \ * * \ * m, b Q ã • b • b open n.P b τ \ * bopn \ * n Amb(n, ã, b) * \ bopn * \τ n P b Fwd (ã, b) • a τ \ bopn bopn \τ / / • a Q ã Q ã
P | 0 ≡ l P P | Q ≡ l Q | P (P | Q) | R ≡ l P | (Q | R) (ν n)0 ≡ l 0 (ν n)(ν m)P ≡ l (ν m)(ν n)P (ν n)(P | Q) ≡ l P | (ν n)Q, if n ∈ fn(P )
recX.P ≡ l P {recX.P/P } Lemma 8. P ≡ l Q implies P ∼ l Q.

Proposition 3. The encoding in Fig. 4 is well-defined, in the sense that if

P ≡ Q then P t ≡ l Q t.
Without loss of generality, in the following we will consider link-calculus processes as taken up to the structural congruence ≡ l .

Example 9. Take again the MA process P

m[ s[ in n.R ] | T ] | open m.Q | n[ G ]
in Ex. 8 for putting our encoding at work. Let

Pπ P t = m[ s[ in n.R ] | T ] t| open m.Q t| n[ G ] t = (ν ã)(Amb(m, ã, t)| s[ in n.R ] | T ã)| open m.Q t| n[ G ] t = (ν ã)(Amb(m, ã, t)|( T ã|((ν b)(Amb(s, b, ã)| τ \ b in n, x . R b))| τ \t opn m . Q t|(ν c)(Amb(n, c, t)| G c)
be its encoding. Here we will recall the two transitions of process P , described in Ex. 8. The only difference is that the dissolved ambient is surrounded by . , in order to record the content of the opened ambient. The process P can execute an "open m" followed by a in n one:

P ≡ m[ s[ in n.R ] | T ] | open m.Q | n[ G ] → s[ in n.R ]|T | Q | n[ G ] → T | Q | n[ s[ R ]|G ] ≡ P
We will show that we can directly encode any derivatives on an MA process P obtaining a process which is congruent to a derivative of P t. If we encode the target process

P ≡ T | Q | n[s[R]|G]
of the two MA transitions, we obtain:

P t = T t| Q t| n[s[R]|G] t = (ν b)(Fwd ( b, t)| T b)| Q t|(ν c)(Amb(n, c, t)| G c|(ν b)(Amb(s, b, c)| R b)) ≡ l (ν b)(ν c)(ν ã)(Fwd ( b, t)| T b| Q t|(Amb(n, c, t)| G c|Amb(s, b, c)| R b) (1)
where in the last step, we rearrange all the restrictions at the left end. By following instead the derivatives of P π , we have that the first transition, as illustrated below, corresponding to the "open m" capability, derived by involving the two subprocesses Amb(m, ã, t)| T ã and τ \ topn m . Q t is:

(Act) τ \t opn m .Qπ τ \t opn m -------→ Qπ (Act)
Amb(m, ã, t)

topn \τ m -------→ Fwd (ã, t) (Close) τ \t opn m .Qπ|Amb(m, ã, t) τ \ topn topn \τ ------→ Qπ|Fwd (ã, t) (Par) τ \t opn m .Qπ|Amb(m, ã, t))|Tπ τ \ topn topn \τ ------→ Qπ|Fwd (ã, t)|Tπ (Res) (ν a)( τ \t opn m .Qπ|Amb(m, ã, t)|Tπ) τ \ topn topn \τ ------→ (ν a)(Qπ|Fwd (ã, t)|Tπ) (Par) (ν a)( τ \t opn m .Qπ|Amb(m, ã, t)|Tπ)|Cπ τ \ topn topn \τ ------→ (ν a)(Qπ|Fwd (ã, t)|Tπ)|Cπ where C π ≡ (ν b)(Amb(s, b, ã)| τ \ bin n, x . R b|(ν c)(Amb(n, c, t) | G c), Q π ≡ Q t and T π ≡ T ã.
The next transition (not reported for the sake of brevity) performs the corresponding "in n" capability, leading to the target process:

(ν ã)(ν b)(ν c)( R b|Amb(s, b, c)|Fwd (ã, t)|Amb(n, c, t)| T ã| G c| Q t) (2)
In our case also the Fwd (ã, t) process is involved, as the process Amb(s, b, ã) refers to the ambient name ã that does not exist any longer. It is easy to see that (1) differs from (2) only for bound names and variables.

Operational Correspondence We can filter out non solid transitions (representing partial interactions) of encoded processes by letting: P (ν t) P t We say that a link chain s is silent if it consists of τ actions only, and write P τ -→ Q if P s -→ Q for some silent s. (Note that any silent link chain is solid.)

Lemma 9. If P s -→ Q, then s is silent.
Proof. The proof is by cases on the type of capability simulated by the encoded process P (open n.Q, in n.Q, out n.Q). The proof of each case is, in turn, by induction on the length of the derivation of the transition.

Theorem 1. Let P be a MA process, then P → P if and only if there exists Q such that P s -→ Q, and Q ≡ P .

The only if part can be proved by induction on the proof of reduction P → P . The idea underlying the proof of the if part goes as follows. At the extremities of the step a silent action τ should appear and the only actions able to perform τ on the left are the movement capabilities (offering the links τ \ ain , τ \ aout , τ \ aopn ), while on the right we need an ambient offering the corresponding links a [in] \ τ , a [out] \ τ , a opn \ τ . An ambient is needed to pass from the action a in (resp. a out ) to the action a [in] (resp. a [out] ), while the forwarders do not change the type of actions. Participants to the action can be arranged in parallel, according to their position in s, thanks to the ≡ l . By induction on the proof, we can rebuild the tree of the bracketed ambients involved in the reduction. Working modulo the structural congruence we can always build the synchronisation, starting from one of the extremities, thus rebuilding the reduction under analysis.

Linked bisimilarity induces a behavioural equivalence on MA processes via our encoding: two MA processes can be retained as equivalent if their encodings are so. We conjecture that linked bisimilarity is finer than barbed congruence, since it would distinguish e.g., (ν n)n[in m.0] from 0. Moreover, link bisimilarity has a 'strong' flavour (silent moves are matched exactly), as opposed to the 'weak' flavour of barbed congruence. We can define a weak version of linked bisimilarity in the standard way, but then the weak version would not be preserved by sum and still it would distinguish e.g., (ν n)n[in m.0] from 0. We think the mismatch is mostly due to the quite arbitrary choice of barbs to be observed in MA, i.e., the names of the topmost ambients: in our encoding, an ambient is just an interacting process, and its name is just a piece of information among others used to match capabilities requests.

Concluding Remarks and Related Works

We have presented the link-calculus as a lightweight enrichment of traditional dyadic process calculi able to deal with open multiparty interactions. We consider the link-calculus as a basis to investigate more general forms of interaction. An important field of application of our calculus is that of Systems Biology, where biological interactions are often multi-party. We would like to generalise link prefixes to link-chain prefixes, to encode some simple pattern of interaction directly, and also to express non linear communication patterns in the prefixes.

Among the recently presented network-aware extensions of classical calculi such as [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF] (to handle explicit distribution, remote operations and process mobility), and [START_REF] Nicola | Basic observables for a calculus for global computing[END_REF] (to deal with permanent nodes crashing and links breaking), the closest proposal to ours is in [START_REF] Montanari | Network conscious pi-calculus: a concurrent semantics[END_REF], an extension of π-calculus, where links are named and are distinct from usual I/O actions, and there is one sender and one receiver (the output includes the final receiver name). In our calculus, links can carry message tuples, and each participant can play both the sender and the receiver rôle. Our semantics recalls their concurrent semantics, where transmissions can be observed in the form of a multi-set of routing paths. In our case the collected links are organised in a link chain. In [START_REF] Bruni | Parametric synchronizations in mobile nominal calculi[END_REF] the authors present a general framework to extend synchronisation algebras [START_REF] Winskel | Synchronization trees[END_REF] with name mobility, that could be easily adapted to many other high-level kinds of synchronisation, like ours, but with a more complex machinery. More sophisticated forms of synchronisations, with a fixed number of processes, are introduced in π-calculus in [START_REF] Nestmann | On the expressive power of joint input[END_REF] (joint input) and in [START_REF] Carbone | On the expressive power of polyadic synchronisation in pi-calculus[END_REF] (polyadic synchronisation). The focus of [START_REF] Laneve | The expressive power of synchronizations[END_REF] is instead on the expressiveness of an asynchronous CCS equipped with joint inputs allowing the interactions of n processes, proving that there is no truly distributed implementation of operators synchronising more than three processes. As in the join-calculus [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF], and differently from our approach, participants can act either as senders or as receivers. In [START_REF] Gorrieri | An operational petri net semantics for A 2 CCS[END_REF], a conservative extension of CCS, with multiparty synchronisation is introduced. The mechanism is realised as a sequence of dyadic synchronisations and, furthermore, puts some constraints that make the parallel operator non associative. Our approach also recalls the asynchronous semantics of CCS-like process calculi (see e.g. [START_REF] Vaandrager | On the relationship between process algebra and input/output automata[END_REF][START_REF] De Boer | On the asynchronous nature of communication in concurrent logic languages: A fully abstract model based on sequences[END_REF]). In both cases, the idea is that one process decides which interaction to try, and the other processes have to match. We introduce the capability of creating chains of links, useful to model communication patterns and information routing. Finally, [START_REF] Bodei | Names of the π-calculus agents handled locally[END_REF] introduces a distributed version of the π-calculus for names to be exported, where names are equipped with the information needed to point back to its local environment, thus keeping track of the origin of mobile agents in a multi-hop travel.

Several approaches, among which we recall [START_REF] Ferrari | A LTS semantics of ambients via graph synchronization with mobility[END_REF][START_REF] Merro | Behavioral theory for mobile ambients[END_REF][START_REF] Rathke | Deriving structural labelled transitions for mobile ambients[END_REF][START_REF] Bonchi | Labelled transitions for mobile ambients (as synthesized via a graphical encoding)[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], are specifically devoted to provide an LTS semantics to MA, as a basis for bisimulation congruence. A contextual equivalence for MA is instead presented in [START_REF] Gordon | Equational properties of mobile ambients[END_REF]. While, in all these works ad hoc semantics are introduced, our proposed encoding is just an illustrative example of application of our network-aware calculus. Our link labels naturally accommodate the encoding. Furthermore, their LTSs are higher-order, since they can move processes (e.g., in [START_REF] Merro | Behavioral theory for mobile ambients[END_REF], a transition can lead from a process to a context, while in [START_REF] Bonchi | Labelled transitions for mobile ambients (as synthesized via a graphical encoding)[END_REF] contexts are used as labels). A different approach is in [START_REF] Hausmann | A coalgebraic approach to the semantics of the ambient calculus[END_REF], where a coalgebraic denotational semantics for the MA is presented.

  and s 3 = * \ * * \ b * \ τ three link chains of the same length. Then s 1 and s 2 can be merged to obtain

Fig. 1 .

 1 Fig. 1. SOS semantics of the CNA (rules ((Rsum) and (Rpar ) omitted).

Lemma 4 .

 4 (i) Let s and s be two essential link chains s.t. s s , then s = s . (ii) Let s be an essential link chain. For any s s we have |s | ≥ |s|.

  We define the relation R | {(P |R, Q|R) | P ∼ n Q} and show that R | is a bisimulation. Suppose P ∼ n Q and P |R s -→ T . We want to prove that Q|R s -→ T with T R | T . There are three cases to be considered, depending on the last SOS rule used to prove P |R s -→ T . If the used rule is -(Rpar), then it means that R s -→ R for some R with T = P |R . But then, by using (Rpar) we have Q|R s -→ Q|R and P |R R | Q|R by definition of R | . -(Lpar), then it means that P s -→ P for some P with T = P |R. By assumption we know that P ∼ n Q and therefore there exists s , Q s.t. Q s -→ Q with e(s) = e(s ) and P ∼ n Q . By applying the rule (Lpar) we have that Q|R s -→ Q |R and we have done because P |R R | Q |R by definition of R | . -(Com), then it means that P s1 -→ P , R s2 -→ R , for some s 1 , s 2 , P , R with s = s 1 • s 2 and T = P |R . By assumption we know that P ∼ n Q and therefore there exists s 1 , Q s.t. Q s 1

  P )σ ( σ)(tσ).(P σ), if vars(t)#(vars(σ) ∪ vals(σ)) (P + Q)σ P σ + Qσ (P |Q)σ P σ|Qσ ((ν a)P )σ (νa)P σ, if {a}#(vars(σ) ∪ vals(σ)) Xσ X (recX. P )σ recX. (P σ)

(

  ν a)(sg) ((ν a)s)((ν a)g) (ν a) w1, ..., wn (ν a)w1, ..., (ν a)wn (ν a)w w if w = a, a, a a if w = a

Lemma 6 .

 6 If (ν a)g = ⊥, then vars((ν a)g) = vars(g).

Fig. 2 .

 2 Fig. 2. SOS semantics of the link-calculus (rules (Rsum) and (Rpar ) omitted)

Fig. 3 .

 3 Fig. 3. Reduction and Structural Congruence Rules for the Mobile Ambients

  ii) The parent ambient n[ • ] to be moved is encoded by the restricted process (ν ã)(Amb(n, ã, b)| P ã| Q ã), where Amb(n, ã, b) includes the sub-process ain \ b [in] y, z .Amb(n, ã, z) as a choice. (iii) The ambient m[ • ] to be entered is encoded by (ν c)(Amb(m, c, b)| R c), where Amb(m, c, b) includes the process b [in] \ τ m, c .Amb(m, c, b) as a choice, where m must match with the first field of the message in the first item. The three process prefixes fit together: b is the parent location of both ambients n and m, whose content reside respectively at the sub-locations ã and c; the messages agree on the first value m (variable y is instantiated by m) and the links can be merged to form a valid link chain. Similarly, the variables x and z are instantiated by the location c. Intuitively, the complete interaction can be described as τ \ ain ain \ b [in] b [in] \ τ m, c . However, names ã and c are restricted, hence the link chain becomes τ \ τ τ \ b [in]

Fig. 6 .

 6 Fig. 6. (Top part) Three party interaction for exiting an ambient, (bottom part) three party interaction for opening an ambient.

As anticipated, we remark that in the defining equations for merge it is implicitly understood that:if i • i = ⊥ for some i, then s • s = ⊥; if the sequence ( 1 • 1 )...( n • n ) is not a link chain, then s • s = ⊥; if α • α = ⊥ or β • β = ⊥, then α \ β • α \ β = ⊥; if α, β = * , then α • β = ⊥.


Min-Ji Cho

-The Void's fonctions in the Korean contemporary Art

teaching and research institutions in France or abroad, or from public or private research centers.