{'fraction_non_alphanumeric': 0.0448148363242155, 'fraction_numerical': 0.007878893470391234, 'mean_word_length': 3.9216844512195124, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 1, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 29, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Formal Approach to Open Multiparty Interactions

We present a process algebra aimed at describing interactions that are multiparty, i.e. that may involve more than two processes and that are open, i.e. the number of the processes they involve is not fixed or known a priori. Here we focus on the theory of a core version of a process calculus, without message passing, called Core Network Algebra (CNA). In CNA communication actions are given not in terms of channels but in terms of chains of links that record the source and the target ends of each hop of interactions. The operational semantics of our calculus mildly extends the one of CCS. The abstract semantics is given in the style of bisimulation but requires some ingenuity. Remarkably, the abstract semantics is a congruence for all operators of CNA and also with respect to substitutions, which is not the case for strong bisimilarity in CCS. As a motivating and running example, we illustrate the model of a simple software defined network infrastructure.

Things (IoT) 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. This is a common situation when, e.g. a client interacts with a website that in turn invokes some services from other websites. At a certain level of abstraction it is important to know which are the involved services, while it is not important how they are contacted. This practice follows the "separation of concern" modelling style, where the modeller is not interested in the details of "how" (with how many synchronisations, for example) the interaction takes place as long as a specific phase of the overall procedure is concluded with success. Intuitively, we can imagine an interaction as the composition of a jigsaw puzzle: all partners provide different pieces that fit together to complete the picture.
Networks have become part of the critical infrastructure of our daily activities (for business, home, social, health, government, etc.) and a large variety of loosely coupled processes have been offered over global networks, as services. As a consequence, more sophisticated forms of interactions have become common, for which convenient formal abstractions are under investigation. In this regard, one important trend in networking is moving towards architectures where the infrastructure itself can be manipulated by the software, as in the Software Defined Networking (SDN) approach [1]. Software clients can remotely access and modify the control plane, by using standard open protocols such as OpenFlow. 1 In this case, it is therefore possible to decouple the network control from dataflow and from the network topology and to provide Infrastructure as a Service (IaaS) over data-centers, cloud systems and IoT.
Another example, coming from a completely different research field, is that of complex biological interactions as the ones emerging in bio-computing and membrane systems, where interactions typically involve several compounds and catalysts. 1 See, e.g. the Open Networking Foundation website http://www.opennetworking.org.  We present here a process algebra, called CNA, 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 the processes they involve is not fixed or known a priori. This is not to be confused with multiparty interactions represented as a global choreography [2,3], whose realisation is still based on dyadic interactions. Traditionally in process algebras, communication is based on synchronisation send/receive on specific channels. In CNA, instead, communication actions are given not in terms of channels but 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 in order to describe how information can be routed across processes before arriving at destination. Note that links can be combined if they are to some extent "complementary", i.e. if each process contributes with links that are compatible, if not necessary, with the chain of links provided by the other processes. According to the puzzle analogy, different parts of a chain can be composed separately, and, afterwards, assembled by superposition without overlays.
To help the intuition, we can see links as Z-shaped tetrominos that can be joined together along a line when the labels of the edges match (see Figure 1).
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, being a straight generalisation of dyadic ones. This is witnessed by the operational semantic rules of our calculus that, in their simpler version (i.e. without message passing), resemble the rules of CCS [4], while in the full one, not considered here (see [5]), they resemble the ones of π-calculus [6]. In this sense, CNA processes can be seen as running over a dedicated middleware that guarantees a proper handling of links, in the same way as CCS and π-calculus processes can be seen as running over a middleware that guarantees a proper handling of point-to-point messaging (e.g. messages are not lost).
Finally, we address a more technical issue, by providing a convenient abstract semantics, called network bisimilarity for CNA processes, which is the analogous of strong bisimilarity for CCS processes. Remarkably, network bisimilarity is a congruence w.r.t. all useful composition operators and also w.r.t. substitutions, a feature mostly missed in other frameworks.
Synopsis. In Section 2, we recall the basics of CCS, although we assume the reader has some familiarity with process algebras. Furthermore, we illustrate a simple scenario of a modular network infrastructure that will serve as a running example to demonstrate that the level of abstraction provided by CNA is much more convenient w.r.t. the one provided by processes with dyadic interactions.
In Section 3, we present the theory of link chains, to be used as labels in the operational semantics of CNA. The theory is quite rich, as it consists of several key operators for building and manipulating link chains. Some nice properties of the introduced operators are also proved, which later will turn out useful to assess semantics properties of CNA processes.
In Section 4, we introduce the syntax and operational semantics of CNA, together with some simple usage examples that should help the reader in understanding the driving principles behind our design choices. The key technical contribution in this section is the Accordion Lemma 25.
In Section 5, we close the loop by introducing network bisimilarity, the abstract semantics of CNA processes. We prove the main congruence results (see Theorem 43 and Proposition 48) and show how network bisimilarity fits well in the running example. Some variations are discussed by the end of Section 5.
Discussion of related work and some concluding remarks are in Section 6.
Some auxiliary results and the proofs of technical lemmata can be found in Appendix A.
Previous work. This article is the full version of the extended abstract in [5], where also the message passing version of CNA was presented, called linkcalculus. Here we focus on the core version of the framework and spell out its theory in full detail. It is worth mentioning that we have revised the definition of the equivalence on link chains that is the basis of network bisimilarity and introduced a finer equivalence that considerably simplifies the proofs of the main properties. The motivating and running example is completely original to this contribution. Finally, we give here all proofs at a good level of detail.
The main contribution in [5] was to show that the link-calculus can be used to encode Mobile Ambients (MA) [7] in such a way that there is a bijective correspondence between the reduction steps of MA processes and silent transitions of their encodings in the link-calculus. This was a much stronger operational correspondence than any available in the literature, such as the ones in [8,9].
In [10], following a similar line, we have provided an encoding of Brane Calculi [11] in the link-calculus. In particular, we have shown that biologically interactions that usually involve several compounds can be naturally rendered by multiparty interactions. Furthermore, locality can be easily handled, without introducing any specific operator, just encoding any membrane compartment as a separate process.

CCS: the Calculus of Communicating Systems
The Calculus of Communicating Systems (CCS) [4] was introduced by Turing Award winner Robin Milner in the early 1980s. It is based on the notion of processes that communicate on shared channels by executing actions and coactions over them. Without loss of generality, we can imagine them as input and output actions with synchronous dyadic interaction. Let C = {a, b, ...} be the set of channels and, by coercion, input actions. We denote by C = {a, b, ...} the set of co-actions (i.e. output actions), with C ∩ C = ∅ and let O = C ∪ C denote the set of observable actions ranged over by λ. We extend the bar-notation to observable actions, by letting λ = λ. We also fix a distinguished silent action τ ∈ O and let µ ∈ O ∪ {τ } denote a generic action. A channel relabelling is a function φ : C → C. It is extended to generic actions by letting φ(τ ) = τ and φ(λ) = φ(λ) for any observable action λ. It is called a renaming when it is bijective.
A CCS process is then a term generated by the following grammar: where φ is a channel relabelling function and A is any constant drawn from a set ∆ of possibly recursive definitions of the form A p.
Roughly the process 0 is the inactive process that cannot perform any action.
The action prefixed process µ.p can execute the action µ and then behaves as p. The operator + introduces nondeterminism: the composed process p + q can behave as p or as q, but once it performs an action as p the option q is discarded, and vice versa. The parallel composition of two processes, written p|q, allows p and q to interleave their actions or to interact by performing complementary actions a and a: if this is the case, the synchronisation is represented as a silent action τ and the channel where it takes places is not recorded. The restricted process (ν a)p can perform all actions that p can perform, except for actions a and a, which are blocked. The relabelled process p[φ] can perform all actions  In some cases we shall use constants A(x 1 , ..., x n ) that are parametric on a set of channel names x 1 , ..., x n , written more concisely as A( x), and that can be instantiated with actual names, as in A(a 1 , ..., a n ) or just A( a) for short.
Similarly, we write (ν a)p for (ν a 1 ) · · · (ν a n )p. To keep the notation compact, we write p µ1 −→ µ2 −→ · · · µn − − → q when there exist some processes p 1 , ...p n+1 that we do not need to mention such that p 1 = p, Recursive definitions can be used to account for infinite behaviour. For example, if (A a.A + b.0) ∈ ∆, then the process A can do any finite sequence of actions a terminated by an action b, as in A The main notion of equivalence for CCS processes is called strong bisimilarity and is denoted by ∼. It is defined as the largest strong bisimulation relation, i.e. as the largest binary relation R on CCS processes such that whenever p R q we have that: 1. for any µ, p such that p µ − → p there exists q such that q µ − → q and p R q ; 2. for any µ, q such that q µ − → q there exists p such that p µ − → p and p R q .
Notably, strong bisimilarity is a congruence w.r.t. all the operators of CCS.
Here we point out that it is not a congruence w.r.t. action substitution. For example, it is well-known that strong bisimilarity reduces concurrency to non-

Software Defined Infrastructures
In this sub-section we sketch four scenarios of increasing complexity together with their possible modelling in CCS. Once introduced CNA, in Sections 4 and 5, we will revisit these examples to show that they can be more conveniently accounted for in CNA.
The reference case study consists of a network infrastructure with n requestor agents A 1 , ..., A n , m servers S 1 , ..., S m and a routing infrastructure R that regulates which requestors are connected to which servers in a way that is out of the control of agents and requestors. For the sake of simplicity, in the following we let n = m = 2.
Example 1 (Blind routing). Initially, we keep the scenario as simple as possible: the idea is that a requestor can repeatedly request a service if there is a non-busy server connected to it via R. Let us suppose that R connects A 1 with S 1 and S 2 , while A 2 only with S 2 . In CCS, the system can be readily modelled by the following recursive processes that run in parallel.
For example we can let the system be defined as so that synchronisation is enforced for all the interactions between requestors and the infrastructure (on channels req 1 and req 2 ) and between the infrastructure and servers (on channels srv 1 and srv 2 ).
The routing depends on the state of the system. Suppose, for instance, that S 2 becomes busy and that A 2 sends a request to R, according to the transition This is perfectly admissible, but leaves A 2 thinking its request has been served, because the interaction with R has taken place, while the server S 2 has not even received it.
Example 2 (Acknowledged routing). To remedy the problem raised by the previous model, one can introduce some acknowledgement protocol, to ensure each agent that its request has been assigned to some server. The CCS model can thus be improved by redesigning the processes as follows: For example we can let the system be defined as where N is defined as before.
At a very abstract level, we can view an infrastructure as an oriented graph with n nodes on the left boundary and m nodes on the right boundary: the assignment of a request from A i to the server S j is possible if S j is available and if there is a connection between the ith node on the left boundary and the jth node on the right boundary. Graphically, M can be depicted as below: This time, when S 2 is busy and A 2 interacts with the infrastructure R on channel req 2 , the requestor A 2 blocks until the server S 2 becomes available and can accept the request by interacting on channel srv 2 with R. In fact, when this is the case, R sends the acknowledgment on channel ack 2 to A 2 .
Example 3 (Composite, acknowledged routing). Now suppose that the infrastructure R is not monolithic, and that it is instead obtained by composing some network infrastructures together, which is a necessity for complex systems.
To make the infrastructure compositional, we must make interaction symmetric on the two, left and right, boundaries, i.e. we must assume that servers also send some acknowledgement. Correspondingly, we set S j = srv j .sack j .exec.S j + busy.τ.S j for j ∈ [1, 2] Now the system can be depicted as below: Note that R does not forward any request coming from its first port. The resulting infrastructure is illustrated in the figure below: In general, an assignment of a request to a server is possible only if there is a path of connections in the graph associated with the infrastructure. In the example, the requests coming from A 1 and A 2 can only be assigned to S 2 , as there is no path towards S 1 .
Unfortunately, it may happen that the routing of the infrastructure comes to a dead point. In the example, R can forward the request from A 1 to R on s 1 , but then R is blocked because it will not be able to pass the request to R on s 1 .
To remedy this, either all dead paths must be removed before the infrastructure is deployed or some deadlock-detection and backtracking mechanism should be put in place, which requires some additional efforts.

A Theory of Link Chains
To address the challenges posed by the scenarios in Section 2, the idea is to move from dyadic interaction to multiparty one. Correspondingly, communication actions are given in terms of links and a single atomic interaction is possibly composed by more than one link. A link is a pair α \ β that records the source and the target sites of a communication, meaning that the input available at the source site α can be forwarded to the target one β. Links are suitably combined in link chains to describe how information can be routed across processes before arriving at their destination. Therefore, links are combined like pieces in a jigsaw puzzle, where each party contributes with its link. As ex- To achieve compositionality, we allow processes to provide link chains that are assembled just in part. Intuitively they correspond to puzzles where some, but not all, the pieces are present. As an example, Figure 3 shows a chain with a missing link from a to b.
In this section we present the underlying theory of links and link chains, posing the emphasis on the operations for combining them and on some relevant properties they satisfy.

Links
Let C be the set of channels, ranged over by a, b, c, ..., and let A = C ∪ { τ } ∪ { } be the set of actions, ranged over by α, β, γ, ..., where the symbol τ denotes a silent action, while the symbol denotes a virtual (non-specified) action (i.e. a missing piece of the puzzle according to the analogy proposed above).
Definition 5 (Links: solid, virtual, valid). A link is a pair = α \ β ; it can be read as forwarding the input available on α to β, and we call α the source site of and β the target site of . A link α \ β is solid if α, β = ; the link \ is called virtual. A link is valid if it is solid or virtual. We let L be the set of valid links.
Examples of non valid links are τ \ and \ a , while both τ \ a and a \ b are solid valid links. From now on, we only consider valid links.
As it will be shortly explained, the virtual link \ is a sort of "missing link" inside a link chain; it represents a needed link that can be supplied, as a solid link, by another link chain, via a suitable composition operation called merge (see below).

Link Chains
Links can be combined in link chains that record the source and the target sites of each hop of the interaction.
Definition 6 (Link Chain). A link chain is a finite sequence s = 1 ... n of (valid) links i = αi \ βi such that: The first condition says that any two adjacent solid links must match on their adjacent sites; it also imposes that, in particular, τ cannot be matched by . The second condition disallows chains made of virtual links only. A nonempty link chain is solid if all its links are so. For example, τ \ a a \ b is a solid link chain, while τ \ a \ b \ τ is not solid.
In counting links in a chain we may decide to ignore or not virtual links.
The following definition introduces an equivalence relation over link chains that equates two valid link chains if they only differ for the presence of virtual links only.

Definition 8 (Equivalence
). We let be the least equivalence relation over link chains closed under the axioms (whenever both sides are well defined link chains): and then taking its homomorphic extension to links and link chains: 2 Similarly, s and s 3 can then be merged to obtain: The merge operation enjoys some simple algebraic properties.
Lemma 11. For any , , s, s : (i) The merge of links and link chains is commutative and associative.
(iii) If s is solid, then for any s we have s • s = ⊥.
Finally, the following lemma about the composition of link chains will be exploited in Lemma 25 to prove that the operational semantics of CNA is insensitive w.r.t. the equivalence .
We say that an action a is matched in s if: 1. a = α 1 , β n , and Otherwise, we say that a is unmatched (or pending) in s.
It follows from the definition that we say that a is matched in s also when a does not appear at all in s.
For instance, a is matched in the sequence τ \ a a \ τ , while it is pending in the sequences τ \ a \ and in a \ a a \ a a \ a .
We define the restriction operation (ν a)s by letting Restriction on links enjoy properties similar to the usual structural congruence laws for processes.
Lemma 15. For any a, b, , s, s Finally, we prove a technical lemma, similar to Lemma 12 for the merge, that will be exploited in the proof of Lemma 25. Renaming. The last operation that we present is called renaming and allows us to change, in a uniform way, the channel names appearing in a link chain.
and φ be a channel renaming function. We define the renaming operation s[φ] by letting It can be readily checked that channel renaming functions enjoy the following properties.
Lemma 19. For any a, φ, ψ, , s, s We conclude this section by proving a last technical lemma that will be exploited in the proof of Lemma 25.

A Core Network Algebra
In this section we build on the theory of links and link chains to present the syntax and operational semantics of CNA.

Syntax
Definition 21. The CNA processes are generated by the following grammar: where is a solid link (i.e. = α \ β with α, β = ), φ is a channel renaming function, and A is a process identifier for which we assume a definition A P is available in a given set ∆ of (possibly recursive) process definitions.
As usual, we writeã for tuples of channels and we allow parametric process definitions of the form A(ã) P , whereã is the set of free channels of P . For brevity, in the examples, we sometimes write A P leaving implicit that the free channles of P are the parameters of A.

Remark 22.
The extension in which generic link chains are allowed as action prefixes instead of solid links is discussed in Section 5.3.
It is evident that processes are built over a CCS-like syntax, with inactive process 0, action prefix .P , choice P + Q, parallel P |Q, restriction (ν a)P , renaming P [φ] and constant definition A, but where the underlying synchronisation algebra [12] is based on link chains. This is made evident by the operational semantics that we present next.
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 processes are taken up to alpha-conversion of bound names. We shall sometimes omit trailing Example 23. CNA provides us with a natural way to rephrase the communication primitives of usual process calculi, such as CCS and CSP [13], in terms of links.
• Intuitively, 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 dyadic communication, analogous to the silent action τ of CCS.
• 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.

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 multi-party synchronisation is realised.
The operational semantics is defined in terms of a Labelled Transition System, in which states are CNA processes, labels are link chains, and transitions are generated by the SOS rules in Figure 5. Notice that the rules are very similar to the ones of CCS, 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 from the formal point of view.
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 can possibly be merged with other link chains. However, when s • s is solid, no further synchronisation is possible (by Lemma 11 (ii)).
cesses P 1 and P 2 . The process τ \ a .P 1 can perform an output on a, the process b \ τ .P 2 can perform an input from b; the process a \ b provides a one-shot link forwarder from a to b. Their links match along the sequence and a three-party interaction can take place. Together, these processes can indeed synchronise by agreeing to form the solid link chain τ \ a a \ τ τ \ τ of length three, as follows. 3 The following lemma, whose proof goes by rule induction, shows that labels provides a sort of name fusion, making a and b interchangeable.
An alternating forwarder A(a, b, c) from a to b first and then to c can be defined as A persistent non-deterministic forwarder C(a, c) (the C stands for choice), from a to c 1 , ..., c n can be written as C(a, c) a \ c1 .C(a, c) + · · · + a \ cn .C(a, c).
is a persistent non-deterministic forwarder, from b 1 , ..., b m to a.
By combining the two processes above as in we obtain a persistent forwarder from any of the b i 's to any of the c j 's. The only Example 27 (Blind routing in CNA). We have already observed that CCS processes can be transformed to CNA processes just by transforming action prefixes in link prefixes. Correspondingly, the blind routing example from Section 2 (Example 1) can be encoded in CNA just as follows, where for readability we have omitted the parameters from definitions.
For example, the following transitions can be derived from the SOS rules accounting for the case where a request from A 1 is assigned to S 2 : Note that, in the first two steps, interactions on channels req 1 and srv 2 are restricted and thus not observable, in fact (ν req 1 )( τ \ req 1 Example 28 (Acknowledged routing in CNA). The features of CNA become evident in our running example when we come to modelling acknowledged routing (Example 2). This is because the explicit acknowledgment is no longer necessary as it can be implicitly accounted for by the ability to construct a chain of links. 5 Correspondingly, we set Note that channels ack i are not needed and CNA processes A i and S j are defined as in the case of blind routing; only the syntax of R has been changed to link, in one single step, the requests from agents with the availability of servers.
For example, the following transitions can be derived from the SOS rules accounting for the case where a request from A 1 is assigned to S 2 : Note that, in the first step, the interaction on channels req 1 and srv 2 is restricted and thus not observable, in fact (ν req 1 )(ν srv 2 )( τ \ req 1 Example 29 (Composite, acknowledged routing in CNA). Notably, the infrastructure presented in the previous example is already designed in a mod-ular way: infrastructures can be composed without requiring any change and no dead path detection or backtracking mechanisms have to be put in place, because they are taken care by the CNA "middleware".
For instance, take the CNA versions of the infrastructures presented in Example 3: Besides looking considerably more concise than their CCS versions, they make evident that the delivery of any request to a server is atomic as any process executes one (link) action and reduces (recursively) to itself.
At a closer inspection, one may notice that the only possible transitions for R are the following ones (up to , as explained by the Accordion Lemma 25): As in the previous examples, note that, e.g. in the first step, the interaction on channels s 2 and s 2 is restricted and thus not observable, in fact . Therefore, at a suitable level of abstraction, in which routing details are omitted, we would like to relate the composite infrastructure R with the monolithic infrastructure R m defined as follows: In the next section we show how this can be formalised.

Abstract semantics
As usual, we can use the LTS semantics to define suitable behavioural equivalences over processes. We focus on bisimulation relations. The accordion lemma (Lemma 25) implies that it makes no sense to distinguish between two labels s and s such that s s , because if one process p can do s and reach p , then it can also do s and still reach p . However, when comparing two labels we would like to abstract away also from the number of hops performed and from the size (not just the length) of the chains, as the following example suggests.
Intuitively, we would like R(a, b) and T (a, b) to be interchangeable, as they offer the same routing service. If we were to compare R(a, b) and T (a, b) using plain bisimilarity, where labels must be matched syntactically, then they would not be equivalent. Also if we relax bisimulation by matching transition labels up-to , the two terms are not equivalent, as it is not true that a \ b a \ τ τ \ b (they have different sizes, i.e. they have a different number of solid links, and size is preserved by ).
To define a bisimilarity equivalence that relates processes such as R(a, b) and T (a, b) above, we introduce an equivalence coarser than , written , that we use to match labels in the bisimulation game, according to which e.g.
Definition 31 (Equivalence ). We let be the least equivalence relation over link chains closed under the following inference rules: The only difference between and is that the additional axiom of abstracts away from intermediate matched actions that are silent. The intuition is that such matched actions cannot be split and used to compose longer chains, because they are silent and therefore the matching was made on a restricted channel.
Remark 32. We invite the reader to check that the Accordion Lemma 25 is only concerned with and not with .
We now consider the equivalences classes given by and its representatives.
Definition 33 (Essential chain). A link chain is essential if it is composed by alternating solid and virtual links, with solid links at its extremes.
For example, the chain a \ τ The following lemma shows that each -equivalence class has a unique essential representative.
Lemma 34. All of the following properties hold for any link chain s.
(i) There exists an essential link chain s such that s s .
(ii) If s is essential, for any essential s such that s s , then s = s .
It is immediate to check that by orienting the axioms in Definitions 8 and 31 from left to right we have a procedure for transforming any link chain s to a unique essential link chain s such that s s . We write e(s) to denote such a unique representative.  Also the next lemma is introduced to prove the main Theorem 43. Definition 40 (Network bisimilarity ∼ ). We let ∼ denote the largest network bisimulation and we say that P is network bisimilar to Q if P ∼ Q.
It can be shown that network bisimulations are closed with respect to union and composition and that ∼ is an equivalence relation.
Example 41. Take the recursively defined processes R(a, b) a \ b .R(a, b) and T (a, b) (ν c)(R(a, c) | R(c, a)) from Example 30. It is straightforward to check that the relation R(a, b) and T (a, b) are network bisimilar.
Example 42. Consider the two processes P a \ b .P and Q (ν c)( a \ c | c \ b .Q).
We have that whenever P We are now ready to prove the first main result, i.e. that network bisimilarity is preserved by all the operators of CNA.
Theorem 43. Network bisimilarity is a congruence.
Proof. We show that network bisimilarity is preserved by all the operators. The proof uses standard arguments. The interesting cases are that of restriction, renaming and parallel composition, the others are just suitable rephrasing of the corresponding proofs in the CCS literature.
Prefix We want to prove that if P ∼ Q then for any we have .P ∼ .Q.
We define the relation R pre {( .P, .Q) | P ∼ Q} ∪ ∼ and show that R pre is a network bisimulation. The case when (P, Q) ∈ ∼ is obvious. Renaming We want to prove that if P ∼ Q then for any renaming function Choice We want to prove that if P ∼ Q then for any R we have P +R ∼ Q+R.
We define the relation R sum {(P + R, Q + R) | P ∼ Q}∪ ∼ and show that R sum is a network bisimulation. The case when (P, Q) ∈ ∼ is immediate. Take (P + R, Q + R) ∈ {(P + R, Q + R) | P ∼ Q}. Suppose • (Lsum), then it means that P s − → P for some P with T = P . By assumption, we know that P ∼ Q and therefore there exist s and Q such that Q s − → Q with e(s) = e(s ) and P ∼ Q . By applying the rule (Lsum), we obtain that Q + R s − → Q and we are done.
Parallel We want to prove that if P ∼ Q then for any R we have P |R ∼ Q|R.
We define the relation R par {(P |R, Q|R) | P ∼ Q} and show that R par is a network bisimulation. Suppose P ∼ Q and P |R Recursion Let E and F be two processes that invoke the process identifier X.
Let us denote with E{P/X} the process obtained by replacing in E every occurrence of the identifier X with the process P . Assume that for any process P we have E{P/X} ∼ F {P/X}. We want to prove that, given the process definitions A E{A/X}, B F {B/X}, then A ∼ B. The proof proceeds by showing that: 1. If A Q is a process definition, then A ∼ Q. Remark 44. As for CCS, it can be proved 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.

Semantics Closure with Respect to Substitutions
One relevant difference w.r.t. strong and weak bisimilarity in CCS is that network bisimilarity is also closed with respect to substitutions.
At the level of chains, name substitution is defined as the renaming (see Definition 18). Not to overload the notation, we denote substitution with {−/−}.
The first observation is that equivalence (but also ) is closed with respect to substitution, as stated by the next lemma.  Proof. We prove the two items separately.
1. The proof is straightforward by rule induction and thus omitted.

Composite and Dynamic Routing in CNA
By using CNA as a modelling framework, we can now revisit the example of composite routing and prove some interesting properties. We start by introducing the simplest possible algebra for building complex routing infrastructures starting from basic building blocks. As done in Section 2, we can imagine a routing infrastructure as a box with a left and right interface and with some connections from (some of) the left channels to (some of) the right channels.
Definition 50 (Basic infrastructure). Let a = a 1 , ..., a n and b = b 1 , ..., b m be two lists of channels. A basic routing infrastructure R from a to b, written R( a, b) is a CNA process of the form is either a basic infrastructure or the composition of two (composite) infrastructures Q( a, c) and S( c, b).
To each (composite) infrastructure R( a, b) we can associate a graph G (R( a, b)), whose nodes are the channels appearing in the definition 6 of the process R( a, b), and whose arcs are induced by the links appearing in the process, i.e. there is an arc x → y if the link x \ y appears as a prefix in the definition of R( a, b). We then have the following characterisation of the transitions admitted by R( a, b).
We recall that with ||s|| we denote the size of s, i.e. the number of solid links in the link chain s. Note that size is preserved by the equivalence , but not by .
Lemma 52. Let R( a, b) be a composite infrastructure.

If R( a, b)
s − → R then R = R( a, b) and there exist two nodes a i ∈ a and b j ∈ b of the graph G (R( a, b)) such that s ai \ bj and there is a path from a i to b j whose length is ||s|| in the graph G (R( a, b)).

2.
If there is a path of length n from a i to b j in the graph G (R( a, b)) then From the previous lemma, it follows that any composite infrastructure R( a, b) is network bisimilar to a basic infrastructure that has one link for each possible path in G (R( a, b)) from one of the a i s to one of the b j s.
Definition 53. Let R( a, b) be a composite infrastructure and G = G (R( a, b)) be its corresponding graph. We denote with P G ( a, b) the basic infrastructure that offers one link for any path in G, i.e.
where a → * b denotes the presence of a path from a to b.
Corollary 54. Any composite infrastructure R( a, b) is network bisimilar to the basic infrastructure P G(R( a, b)) ( a, b).
Example 55. Let us define the following basic infrastructures and combine them to form the composite infrastructures Q( req, s ) (ν s)(R ( req, s)|R ( s, s )) Assuming all of the tuples req, s, s and srv have length 2, the graph G(R) is depicted below Then, it is immediately evident that the admissible transitions for R are of the where, of course, many additional virtual links can be appended to the extremes of the labels (remember the Accordion Lemma 25). Consequently, R is network bisimilar to the basic infrastructure S( req, srv ) req 1 \ srv 2 .S( req, srv )+ req 2 \ srv 2 .S( req, srv ).
Finally, we show that CNA is particularly convenient to model programmable infrastructures, where links can be dynamically added and removed.
Given a = a 1 , ..., a n and b = b 1 , ..., b m let us consider the processes and their parallel composition where we use the shorthand n i=1 P i for the parallel composition P 1 | · · · | P n . The idea is that an interaction involving the link addi,j \ τ allows us to add one link from a i to b j and that an interaction involving the link remi,j \ τ allows us to remove one such link. Several links between a i and b j can be available at the same time, but no such link can be removed if it is not present. Initially, the process R makes no link available.
We believe that modelling infrastructures at this level of abstraction drastically improves the situation w.r.t other process algebras based on dyadic interaction, such as CCS. In fact imagine the situation where a composite programmable infrastructure is modelled in CCS: it can happen that a transfer of information is started along a viable path, but during the chain of interactions one or more of the hops are removed. As a consequence it is then impossible to deliver the request as well as acknowledge the failure. The CNA middleware guarantees that none of these troublesome scenarios can arise in the model.

Alternative Definitions
The theory of CNA is quite strong and stable and it can be extended in several directions without much efforts. Here we briefly discuss only three noteworthy possible variations of the presented framework.
Chain as prefixes. In the first variation, we could extend the syntax of CNA to allow essential chains instead of solid links as prefixes, i.e. the grammar production P ::= .P can be replaced by P ::= s.P with s essential. This change can increase the usability of the process algebra in modelling different scenarios. For example, we can write a process such as τ \ a \ b \ b \ c \ τ .P that requires an interaction from a to c via b. All of the results presented in the paper would carry over such an extension. Remarkably, network bisimilarity would still be a congruence.
Bisimilarity ∼ . In the second variation, in the bisimilarity game, we could decide to take into account the number of traversed (solid) links so to get a finer equivalence. This amounts to changing the definition of bisimulation by requiring that the matching label s is related to s by instead of . We can denote the corresponding bisimilarity as ∼ . Since ⊆ , it follows that ∼ is finer than ∼ , i.e. , it distinguishes more processes. However, as in the previous case, all the results presented in the paper would carry over this change.
Ordinary bisimilarity ∼= ∼ . In the third and last variation, we could take ordinary strong bisimilarity ∼, by requiring exact matching of labels. Then, because of the Accordion Lemma 25, the resulting equivalence would coincide with the equivalence ∼ from the second point.

Concluding Remarks and Related Works
In this paper we have presented CNA as a generalisation of traditional dyadic Concerning the taxonomy for multiparty languages proposed in [14], we can say that CNA is variable, i.e. the number of participants is not fixed a priori, and asynchronous, i.e. not all the processes in the systems are required to make a move at each step. In contrast, CNA adopts a multi-channel mechanism that does not work as a gate forcing all the involved processes to take part in the interaction. We can say that our interaction command, i.e. the command used to establish a multiparty interaction, only allows a multiparty interaction to happen. Thus, following this taxonomy we can classify CNA neither as conjunctive nor as disjunctive calculus.
As stated in Section 5.3, we intend to take CNA as a starting point for investigating more general forms of interaction and more advanced forms of equivalence. Several interesting directions are possible.
Some alternatives to network bisimilarity have been discussed in Section 5.3.
Weak variants of them can be readily defined by considering solid link chains as internal (silent) actions (as they represent completed interactions). As usual, the corresponding equivalences will not be congruences w.r.t. choice. However, we think that the multi-party interaction available in CNA offers already a more abstract mechanism than dyadic communication, so that weak equivalences are not needed for many applications. The name handling variant of CNA, called link-calculus, has been already considered in [5] and exploited in [10] to model biological interactions.
Due to space limitation, we decided to focus here on presenting the communication layer in full details and devote a companion paper to the name handling extension, which is currently under scrutiny. In particular, on the more applicative side, we think that the generalisation of link prefixes to link-chain prefixes can be very useful to encode some simple patterns of interaction directly in the action prefixes, thus enhancing the modelling power.
We plan to extend the theory to take into account some weights associated with each link, along the lines of [15]. For example, if weights are seen as costs, then processes can be compared on the basis of the overall cost of an interaction they offer, and the abstract equivalence can be refined to a preorder to reflect the fact that when two processes offer the same interactions, one is cheaper than the other. If costs are replaced with some logical information, e.g.
representing the knowledge associated with the link, then an interaction can be paired with deduction and thus compared with others on the basis of the amount of information it provides. Other quantitative extensions could exploit probabilities and stochastic rates.
Another direction for future work is concerned with the cross-fertilisation between computational sciences and biology. In [10] we have shown that membrane interactions are intrinsically multi-party, by providing a faithful encoding of Brane calculi [11] in terms of link-calculus. Brane calculi are compartmentbased calculi, introduced to model the behaviour of nested membranes in complex biological systems. We plan to include causality in the picture, so to study dependencies among interactions and track down sources of unwanted behaviours and consequences of biological reactions. Causality enriched models have already been used to study metabolic networks [16,17,18], e.g. for detecting incorrect behaviour that may depend on a particular ordering of certain events, sometimes difficult to predict. The idea is to define a causal semantics for CNA and exploit static analysis techniques for approximating the causal relationships among the interactions performed by a complex system, along the lines of the abstract causal semantics proposed in [19,20,21,22] for the Brane calculus and of the context dependent analysis presented in [23] for BioAmbients [24], another calculus for describing biological systems.
A further extension of our approach consists in the possibility of expressing non linear communication patterns in the prefixes, as allowing links of arity greater than 2 and combine them in trees, matrices or graphs.
Related Work. Among the recently presented network-aware extensions of classical calculi such as [25] (to handle explicit distribution, remote operations and process mobility), and [26] (to deal with permanent nodes crashing and links breaking), the closest proposal to ours is in [27], an extension of π-calculus, where links are named and are distinct from usual input/output actions, and there is one sender and one receiver (the output includes the final receiver name).
In the name-passing variant of CNA [5], links can carry message tuples, and each participant can play both the sender and the receiver rôle. This extended semantics recalls the concurrent semantics in [27], where concurrent 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 [28], the authors present a general framework to extend synchronisation algebras [29] with name mobility that could be easily adapted to many other high-level kinds of synchronisation, like the one we need, but with a more complex machinery. More sophisticated forms of synchronisations, with a fixed number of processes, are introduced in π-calculus in [30] (joint input) and in [31] (polyadic synchronisation). The focus of [32] 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 [33], and differently from our approach, participants can act either as senders or as receivers.
In [34], a conservative extension of CCS, called A 2 CCS, is studied that is able to model multi-party synchronisation. The mechanism is realised as an atomic sequence of dyadic synchronisations of arbitrary lengths, but imposes some constraints that make the parallel operator non associative and therefore more difficult to use as a model.
Finally, in [35], a distributed version of the π-calculus for handling names, (i) Trivial, by the fact that the underlying operation on actions α • β is commutative and associative.
(iii) Since s is solid, its length n = |s| is greater than zero. If |s | = n then   Then it must be s = s 1 \ s 2 for some s 1 and s 2 with (ν a)s 1 = s 0 and (ν a)s 2 = s 0 . We set s = s 1 \ \ s 2 , from which the thesis immediately follows.
As a cannot appear in (ν a)s, it must be the case that a = b and s = s 1 \ s 2 for some s 1 and s 2 with (ν a)s 1 = s 0 α \ b and (ν a)s 2 = b \ β s 0 . We set s = s 1 s 2 , from which the thesis immediately follows.
As a cannot appear in (ν a)s, it must be the case that a = b and s = s 1 s 2 for some s 1 and s 2 with (ν a)s 1 = s 0 α \ b and (ν a)s 2 = b \ β s 0 . We set s = s 1 \ s 2 , from which the thesis immediately follows.
We omit the remaining cases that are analogous.
We recall Lemma 19 (the original appears on p. 18).
Lemma 19. For any a, φ, ψ, , s, s Proof Since, for all i ∈ [1, n], (iv) The proof of (iv) derives from the compositionality of renaming functions, (v) To prove (v), we prove that the axioms, when applied in either direction, Proof.
(i) Take s and let • n be the number of adjacent solid links in s, • m be the number of adjacent virtual links in s, • k be the number of virtual links at the extremes of s. We prove the existence of s by induction on v(s) = n + m + k.
• For the base case, if v(s) = 0 then s is essential and we are done.
• For the inductive case, suppose v(s) > 0. Then at least one of n, m, k is greater than 0.
If n > 0, then there are two adjacent links in s such as α \ a a \ β or α \ τ τ \ β . In the former case, we can apply the last axiom of (Definition 8) to introduce a virtual link between the matched action a and decrement by one the number of adjacent solid links. In the latter case, we can apply the rightmost axiom of (Definition 31) to eliminate the matched τ actions and decrement by one the number of adjacent solid links.
If m > 0, then there are two adjacent virtual links in s and we can apply the top-right axiom of (Definition 8) to decrement by one the number of adjacent virtual links.
If k > 0 we can apply one of the leftmost axioms of ( We let s = s s and we are done, since (ν a)s = (ν a)s is defined by hypothesis.
We recall Lemma 37 (the original appears on p. 29).
Lemma 37. If s 1 s 1 , then for any s 2 such that s 2 • s 1 = ⊥ there exist two link chains s 2 s 2 and s 1 s 1 such that s 2 • s 1 = ⊥ and s 2 • s 1 s 2 • s 1 .
Proof. We prove that the property holds for the axioms of , then the fact that the property is preserved by the rules for equivalence is immediate. We prove only two cases, the remaining ones are similar.
Then, since s 2 • s 1 = ⊥ we infer that s 2 = s \ \ s for some s , s such that s • s = ⊥, and s • s = ⊥. Then we take s 2 = s \ s s 2 and s 1 = s 1 and we are done, since case [s α \ a \ a \ β s s α \ a a \ β s ] We have s 1 = s α \ a \ a \ β s and s 1 = s α \ a a \ β s . Then, there are two possibilities: either (a) s 2 = s \ \ \ s , or (b) s 2 = s \ a \ a \ s with s • s = ⊥, and s • s = ⊥. In the case (a), we take s 2 = s \ \ s s 2 and s 1 = s 1 and we are done, since s 2 • s 1 = (s • s) α \ a \ a \ β (s • s ) (s • s) α \ a a \ β (s • s ) = s 2 • s 1 . In the case (b) we take s 2 = s 2 and s 1 = s α \ a \ a \ β s s 1 and we are done, since s 2 •s 1 = (s •s) α \ a a \ a a \ β (s •s ) (s •s) α \ a a \ a a \ β (s •s ) = s 2 •s 1 .
We recall Lemma 38 (the original appears on p. 29).
Lemma 38. Let s and s be two link chains such that s s , then for any Proof. The proof is similar to the ones of Lemma 19 (point v) since, by definition φ(τ ) = τ and φ( ) = , then the equivalence relation is not affected by φ.
We recall Theorem 43 (the original appears on p. 30).
Theorem 43. Network bisimilarity is a congruence.
Proof. We complete here the proof outlined at p. 30, by giving the details of the case for recursion.
Recursion Let E and F be two processes that invoke the process identifier X.
Assume that for any process P we have E{P/X} ∼ F {P/X}. We want to prove that, given the process definitions A E{A/X}, B F {B/X}, then A ∼ B. The proof proceeds by showing that: 1. If A Q is a process definition, then A ∼ Q. Let R ctx {(G{A/X}, G{B/X}) | G is a process that possibly invokes X}.

Given the process definitions
Let R upto ∼ • R ctx • ∼ . Note that R ctx includes the identity relation when taking G with no occurrence of X. Moreover, R ctx ⊆ R upto , ∼ ⊆ R upto and R upto • ∼ = R upto because ∼ is an equivalence relation (and thus transitively closed). We prove that R upto is a network bisimulation. To this aim, it is enough to consider a generic pair of processes (G{A/X}, G{B/X}) in R ctx and prove that whenever G{A/X} We recall Lemma 52 (the original appears on p. 38).
Lemma 52. Let R( a, b) be a composite infrastructure.

If R( a, b)
s − → R then R = R( a, b) and there exist two nodes a i ∈ a and b j ∈ b of the graph G (R( a, b)) such that s ai \ bj and there is a path from a i to b j whose length is ||s|| in the graph G (R( a, b)).

2.
If there is a path of length n from a i to b j in the graph G (R( a, b)) then R( a, b) s − → R( a, b) with s ai \ bj and ||s|| = n.
Proof. We prove the two implications separately.
1. The proof is by structural induction on the composite infrastructure R( a, b).
If it is a basic infrastructure R( a, b) = 1 .R( a, b) + ... + k .R( a, b), then it must be the case that R = R( a, b) and s h = ai h \ bj h for some h ∈ [1, k]. Clearly ||s|| = 1 and in fact there is a path of length 1 from a i h to b j h in the graph G (R( a, b)).