Thomas Ehrhard
email: ehrhard@irif.fr

Jean Krivine
email: jkrivine@irif.fr

Ying Jiang

A Calculus of Branching Processes

CCS-like calculi can be viewed as an extension of classical automata with communication primitives. We are interested here to follow this principle, applied to tree-automata. It naturally yields a calculus of branching processes (CBP), where the continuations of communications are allowed to branch according to the arity of the communication channel. After introducing the calculus with a reduction semantics we show that CBP can be "implemented" by a fully compositional LTS semantics. We argue that CBP offers an interesting tradeoff between calculi with a fixed communication topology à la CCS and calculi with dynamic connectivity such as the π-calculus.

Introduction

The Calculus of Communicating Systems (CCS) [START_REF] Milner | Communication and Concurrency[END_REF] and Communicating Sequential Processes (CSP) [START_REF] Hoare | Communicating Sequential Processes[END_REF] are expressive formalisms that are widely used to model concurrent systems, in which processes synchronize by handshake. One can view concurrent runs in these calculi as computations of classical automata or Petri Nets in which transitions have to synchronize on complementary symbols. The starting point of the formalism we introduce in this paper is the following: what happens if instead of synchronizing classical transition systems, we were to allow more expressive automata to synchronize?

We introduce a Calculus of Branching Processes (CBP), that is obtained by adding synchronization to tree-automata [START_REF] Doner | Tree acceptors and some of their applications[END_REF]. We obtain a process calculus whose continuation scheme is branching according to the arity of the communication symbols. A CBP process of the form f (p, q) has communication symbol f and continuations p and q. Branching communication structure can only be achieved if the computations of p and q are not allowed to interact anymore. This leads naturally to a definition of a communication graph that connects processes and specifies which symbols are able to interact. In classical process algebra, the communication graph is left implicit since any two complementary symbols may synchronize. This explains, for instance, the difficulty to make concrete implementations of the π-calculus [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF]: in the absence of a network topology, one has to conceive of astute mechanisms to implement communications [START_REF] Peschanski | A stackless runtime environment for a pi-calculus[END_REF]. This has led to the definition of process calculi in which routing of communication is either trivially directed [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF][START_REF] Fournet | The join calculus: A language for distributed mobile programming[END_REF] or explicit [START_REF] Hennessy | A Distributed Pi-Calculus[END_REF][START_REF] Montanari | Network-conscious π-calculus -a model of pastry[END_REF][START_REF] Fehnker | A process algebra for wireless mesh networks[END_REF]]. An interesting aspect of CBP is that it comes with a structural operational semantics that makes explicit how the communication graph evolves over time.

Outline. In Section 2 we introduce the specification of CBP's operational semantics by means of (communication) graph rewriting rules. The syntax of processes involves two main constructs: parallel composition, as in CCS, and prefixing. As already suggested, this latter construct differs from CCS prefixing in that there can be more than one continuation. The number of continuations is determined by the label of the prefix which is a function symbol. For the sake of simplicity, we assume in the technical developments that this arity is always 2 (more general arities can easily be encoded in this setting).

The operational semantics of this calculus is mainly defined as a rewriting system. Our main design choice is summarized in Figure 1: when two processes p = f (p 1 , p 2 ) and q = f (q 1 , q 2 ) synchronize, the resulting configuration stipulates that p i can only communicate with q i (for i = 1, 2) and with the environment of p (and symmetrically for q). We can motivate this choice as follows:

• p 1 can synchronize only with q 1 , and not with q 2 (and similarly for p 2 ), to have CBP behave as a conservative extension of tree automata, as explained in Section 3.1.

• p 1 cannot synchronize with p 2 in order to obtain branching continuations in the style of process threads.

• Last, the fact that the continuations of a prefixed process p inherit the synchronization capabilities of p is inspired by the operational semantics of CCS and has the major effect of allowing the continuations of p to communicate by means of a common, shared, context (the context X in Fig. 1).

These restrictions on possible synchronizations are implemented by a graphical structure: a process graph Γ is an undirected simple graph, the vertices of which are labeled by processes. The edges of the process graph correspond to communication capabilities: two processes can synchronize if they are located on opposite ends of an edge of this graph. A process graph rewriting event corresponds to a synchronization that updates the process graph according to the three principles listed above and summarized in Figure 1. The corresponding rewriting relation on process graphs is presented in Section 2.4. Expressivity of CBP is discussed in Section 3. First we show, in Section 3.1, that CBP is a conservative extension of tree automata, in the sense that the recognition of a tree a by an automaton T can be expressed by the fact that a process representing the "parallel composition" of T and (the dual of) a reduces to an idle process. We then give an example, in Section 3.2, that illustrates the branching behavior of process continuations that are still able to interact by means of a shared environment. This is obtained by modeling a reader and a writer thread that have access to a common register process. Finally we explore, in Section 3.3, the graph self-assembly capabilities of CBP and we illustrate specifically that hexagones naturally arise from CBP rewriting, allowing for instance to implement a ternary version of dining philosophers. We consider this example as a local interaction based implementation of a distributed consensus, since the main feature of this sequence of reductions, presented in Figure 3, is that no interaction between the philosophers is possible before the final hexagonal configuration is reached.

The compositional semantics of CBP is introduced in Section 4. As usual, rewriting semantics is not compositional (the semantics of a process cannot be described in terms of the semantics of its subprocesses). Following a standard approach initiated by Milner with CCS, we present a labeled transition system for CBP. Unlike CCS where labels are simple letters or τ -symbols (for internal synchronizations), our labels involve also addresses in process trees, which are the syntactic objects our LTS deals with. These trees can be understood as process graphs enriched with further informations on the sequential construction steps of the underlying graph structure.

Thanks to the presence of addresses in our process tree LTS, we are able to prove in Section 5 that the two operational semantics presented in Section 2 and 4 are indeed equivalent through a translation from process trees to process graphs.

The calculus CBP and its reduction semantics

In this section we introduce the calculus CBP and its reduction semantics, which is a conservative extension of CCS [START_REF] Milner | Communication and Concurrency[END_REF]. This semantics describes the evolution of processes that are distributed on the vertices of a graph whose edges enable message exchange: two processes that are connected may interact if they communicate on complementary function symbols. Importantly, processes that are not connected by an edge cannot interact 1 .

CBP has essentially one reduction rule, which is informally described in Figure 1. The remainder of the present section is dedicated to the formal description of the reduction semantics, which should be understood as the specification of a distributed computation. Looking at Figure 1 the reader may wonder whether the new wiring of the right hand side of the reduction may be obtained by means of local rules since there are, a priori, many edges that may appear after a reduction (in particular for the full CBP calculus whose reduction scheme is shown on the right of Fig. 1). A solution to this problem is presented in Section 4, where a fully compositional semantics for CBP is introduced.

Syntax

For simplicity we restrict ourselves to binary CBP, where all function symbols have arity 2. Full CBP is obtained by relaxing this condition.

A process is a term built over the following grammar:

s ::= f (p, p) | 0 | D( f ) | s + s (sums) p ::= s | (p p) | p \ H (processes)
with f ∈ F a function symbol, H ⊆ F and D( f ) a (guarded) recursive definition with parameters f . We assume a definition set of the form Def = def i {D i ( fi ) := s i }, where fi are function symbols occurring free in s i (see fn function defined in Section 2.3). , and are connected by an edge. X (resp. Y ) denotes nodes in the context that are connected to x but not y (resp. y but not x). Z denotes nodes of the context of the reduction that are connected to both x and y. The reduction replaces nodes x and y by their continuations x 1 , x 2 and y 1 , y 2 . New edges connect nodes in X (resp. Y ) and Z to the continuations of x (resp. y). On the right, the reduction scheme for n-ary functions in the full CBP.

We let P = {p, q, . . . } denote the set of process terms. We also consider the involution . : F → F that will serve to denote dual function symbols 2 .

Let V = def {x, y, z, . . . } be a set of vertices. A process graph Γ = (V, E, π : V → P) is a tuple where V ⊆ V are the vertices of Γ, E ⊆ {{x, y} | x, y ∈ V } are its edges, and π : V → P is a labeling function that maps each vertex to a process. We use G = def {Γ, ∆, . . . } to denote the set of process graphs.

Update

Computations in CBP progress in the style of classical process algebra: complementary communication symbols are consumed conjunctly and their continuation is spawned. In the context of binary CBP, each function symbol comes with two continuation processes. Unlike the CCS term a.(p q) that has a unique continuation p q, the CBP term a(p, q) has two continuations that may not exchange messages in the future. 3 This is captured by a special form of substitution (described below) that substitutes a node by two continuation nodes, while taking care of the new edges that should appear.

We introduce the update functions that will be used to bring process graphs into a reducible form. These functions are defined respectively on V, E, π and eventually on Γ. For all V, E, π, with x ∈ V , x 1 , x 2 ∈ V and p, q ∈ P:

V [x 1 , x 2 /x] = def (V \ x) {x 1 , x 2 } (E {{z, t}})[x 1 , x 2 /x] = def {{x 1 , t}, {x 2 , t}} (E[x 1 , x 2 /x]) if x = z (E {{z, t}})[x 1 , x 2 /x] = def {{z, t}} (E[x 1 , x 2 /x]) if x ∈ {z, t} ∅[x 1 , x 2 /x] = def ∅ π[x 1 : p, x 2 : q/x] = def [y → π(y)] y∈V \{x} + [x 1 → p; x 2 → q]
where π = π + [y → p] is a labeling map with Dom(π ) = Dom(π) {y} and satisfying π (x) = π(x) for all x ∈ Dom(π) and π (y) = p.

Definition 2.1 (Process graph update). Let Γ = def (V, E, π) and Γ = def (V , E , π ). We define Γ{(x 1 : p, x 2 : q)/x | (y 1 : p , y 2 : q )/y} = Γ if:

V = V [x 1 , x 2 /x][y 1 , y 2 /y] E = (E \ {{x, y}})[x 1 , x 2 /x][y 1 , y 2 /y] ∪ {{x 1 , y 1 }, {x 2 , y 2 }} π = π[x 1 : p, x 2 : q/x][y 1 : p , y 2 : q /y]
Let x be a vertex and p be a process, we use {x : p} for the process graph (V, E, π) where V = {x}, E = ∅ and π(x) = p. We say that a process graph (V, E, π) is idle if π(x) = 0 for all x ∈ V .

Normalization

Process graph reduction can be blocked by processes that are not in a reducible form. This is due to three factors:

• Processes of the form p q need to be distributed as two processes connected by an edge.

• Restriction operators need to act as a fresh function symbol generators at the level of process graphs.

• Constants need to be replaced by their definitions.

Bringing process graphs to a reducible form is the job of the normalization procedure that we introduce now. For all p ∈ P, for all function symbols f, g ∈ F such that g does not occur in p, we write p{g/f } for the substitution of symbol f by g in p.

We define the function fn : P → V, which yields the free names of processes, as:

fn(f (p, q)) = def {f } ∪ fn(p) ∪ fn(q) fn(p + q) = def fn(p) ∪ fn(q) fn(p q) = def fn(p) ∪ fn(q) fn(D( f )) = def {f ∈ f } fn(0) = def ∅ fn(p \ H) = def fn(p) \ H
and, for all process graph (V, E, π), we define fn(π) = def x∈V fn(π(x)). Process normalization p ⊆ P × P is:

p (q \ H) p (p q) \ H if H ∩ fn(p) = ∅ (p \ H) q p (p q) \ H if H ∩ fn(q) = ∅ p \ H \ H p p \ (H ∪ H ) D( f ) p s{ f /g} if (D(g), s) ∈ Def
and is applied up-to α renaming of bound names. Normalization propagates at the level of process graphs. For all x ∈ V :

(V, E, π + [x → p]) g (V, E, π + [x → q]) if p p q (V, E, π + [x → p \ {g} H]) g (V, E, π + [x → (p{f /g}) \ H]) if f ∈ fn(π) ∪ fn(p) ∪ H (V, E, π + [x → p q]) g (V [x 1 , x 2 /x], E[x 1 , x 2 /x], π[x 1 : p, x 2 : q/x]) where x i , y i ∈ V .
Definition 2.2 (Normalized process graph). A process graph (V, E, π) is normalized if all its nodes are either idle or labeled by a function symbol, i.e. for all x ∈ V , π(x) = 0 or π(x) = f (p, q) for some f ∈ F and p, q ∈ P.

Process graph rewriting

We are now in position to formally describe the reduction given in Fig. 1. Summation contexts are terms with exactly one hole of the form:

S[•] = def s + • | • + s | •
The process graph reduction semantics is the least relation satisfying derivations (1) and ( 2), for all Γ = def (V, E, π).

{x, y} ∈ E {x 0 , x 1 , y 0 , y 1 } ∩ V = ∅ π(x) = S[f (p 0 , p 1 )] π(y) = S [ f (q 0 , q 1 )] Γ → {x,y} Γ{(x 0 : p 0 , x 1 : p 1 )/x | (y 1 : q 0 , y 1 : q 1 )/y} (1)
Reduction of process graphs is performed up-to normalization steps:

Γ g ∆ → {x,y} ∆ g Γ Γ → {x,y} Γ (2)
We write also Γ → Γ when Γ → {x,y} Γ for some x, y. We use → * for the reflexivetransitive closure of this relation.

Expressivity

In this section we explore the expressivity of CBP. Although the formal treatment is restricted to binary CBP, in writing examples we will feel free to use the full calculus CBP. These examples can easily be encoded using the strict binary CBP, but this would be to the cost of readability.

Encoding tree automata

One major motivation of this work was to extend tree automata (considered from a top-down point of view) to an interactive setting, just as CCS can be understood as a natural interactive extension of ordinary word automata in the following sense. Given an automaton A, it is possible to define a process P A such that, for any word w = a 1 . . . a k , the automaton A recognizes w iff the CCS process w P A reduces to 0 (where we trivially see w as the process a 1 . • • • .a k .0), using the same method as in the definition of CCS testing semantics in [START_REF] De Nicola | Testing equivalences for processes[END_REF] (where one would probably have rather written w P A where w = ā1 . • • • . āk .0, but this is a pure matter of conventional choice in the definition of P A ). The object of this section is to prove a completely similar statement for tree automata and CBP.

A tree automaton is a tuple T = (Q, Θ, •) where Q is a finite set of states, • ∈ Q is a final state and Θ is a finite set of transitions. An element of Θ is a triple (q, f, (q 1 , q 2 )) where f ∈ F and q, q 1 , q 2 ∈ Q. For the sake of simplicity, and without loss of expressiveness, we assume that no element of Θ has the form (•, f, (q 1 , q 2 )) (no transitions from the final state).

Let * be a special symbol representing the empty tree. Trees are defined as follows:

a ::= * | f (a, a)
where f ∈ F. We use T to denote the set of trees.

Given an automaton T = (Q, Θ, •) and an element q of Q, we define a set of trees L(T, q) = L q where (L q ) q∈Q is the smallest element of (2 T ) Q such that

• * ∈ L • • if a i ∈ L qi for i = 1, 2 and (q, f, (q 1 , q 2 )) ∈ Θ, then f (a 1 , a 2 ) ∈ L q .
The set L(T, q) is the tree language recognized by T at state q.

Given a tree a, we can define a process a in the following straightforward way: * = 0 and f (a 1 , a 2 ) = f ( a 1 , a 2 ). Now we explain how to associate a process with a tree automaton, so assume T = (Q, Θ, •) to be a given tree automaton. Let f be a repetition-free list of all names which occur in Θ. With each q ∈ Q we associate injectively a process constant D q . We define a set Def T by

Def T = {D q ( f ) := (q,f,(q1,q2))∈Θ f (D q1 ( f ), D q2 ( f )) | q ∈ Q \ {•}} ∪ {(D • ( f ) := 0} .
Theorem 3.1. Let q ∈ Q and let a be a tree. Then a ∈ L(T, q) iff {x : ( a D q ( f ))} → * Γ 0 where Γ 0 is an idle process graph.

Proof. By induction on the tree a. Observe that {x : ( a D q ( f ))} g Γ = ({y, z}, {{y, z}}, [y → a, z → D q ( f )]).

Assume first that a = * . If a ∈ L(T, q) then we have q = • so that Γ is an idle process graph. Conversely, assume that Γ → * Γ 0 where Γ 0 is idle. Since a = 0, no f / f reduction can occur in Γ and hence Γ itself must be idle, meaning that q = • and hence a ∈ L(T, q). Assume now that a = f (a 1 , a 2 ). If a ∈ L(T, q) then there must exist q 1 , q 2 ∈ Q such that (q, f, (q 1 , q 2 )) ∈ Θ with a i ∈ L(T, q i ) for i = 1, 2. Setting

Γ i = ({y i , z i }, {{y i , z i }}, [y i → a i , z i → D qi ( f )])
for i = 1, 2 (with pairwise distinct vertices z i s and y i s), we know by inductive hypothesis that Γ i → * Γ i 0 where the Γ i 0 s are idle. Since (q, f, (q 1 , q 2 )) ∈ Θ we have D q ( f ) := f (D q1 ( f ), D q2 ( f )) + s ∈ Def T for some (possibly null) sum s. On the other hand a = f ( a 1 , a 2 ). Therefore Γ → {y,z} Γ = ({y 1 , y 2 , z 1 , z 2 }, {{y 1 , z 1 }, {y 2 , z 2 }}, π) where π(y i ) = a i and π(z i ) = D qi ( f ) for i = 1, 2 (up to some g steps). Since Γ i reduces to an idle process graph for i = 1, 2, it follows that Γ also reduces to an idle process graph.

If now Γ → * Γ 0 where Γ 0 is idle, since a = f ( a 1 , a 2 ), q cannot be the final state, and D q ( f ) must g normalize (by updating the value of this constant D q using Def T ) to a sum of the form f (p 1 , p 2 ) + s where the p i s are processes and s is a (possibly nil) sum. In view of the definition of Def T , this means that, for some q 1 , q 2 ∈ Q, one has (q, f, (q 1 , q 2 )) ∈ Θ and p i = D qi ( f ) for i = 1, 2 and moreover the reduction starting from Γ is of the form

Γ g ({y, z}, {{y, z}}, [y → f ( a 1 , a 2 ), z → f (D q1 ( f ), D q2 ( f )) + s]) → {y,z} ({y 1 , y 2 , z 1 , z 2 }, {{y 1 , z 1 }, {y 2 , z 2 }}, [y i → a i , z i → D qi ( f )] i∈1,2 )
and, calling Γ this latter graph process, we know that Γ → * Γ 0 . In view of the communications allowed by the graph structure of Γ , this implies that Γ i reduces to an idle process graph for i = 1, 2, where Γ i = ({y i , z i }, {{y i , z i }}, [y i → a i , z i → D qi ( f )]). Therefore, by inductive hypothesis, a i ∈ L(T, q i ) and hence a ∈ L(T, q) since (q, f, (q 1 , q 2 )) ∈ Θ.

Threads and shared memory

We illustrate here the fact that CBP naturally models thread-like synchronization, using shared memory, and process-like communication by means of remote procedure calls. We first model a simple one bit register4 :

Reg 0 = def r 0 (Reg 0 ) + w 0 (Reg 0 ) + w 1 (Reg 1 ) Reg 1 = def r 1 (Reg 1 ) + w 0 (Reg 0 ) + w 1 (Reg 1 )
Now a thread that attempts to read or write b ∈ {0, 1} from the register is simply

Read b = def rb (0) Write b = def wb (0)
Eventually we consider a server that may (indefinitely) spawn pairs of threads upon calling the function symbol sp: Spawn = def sp(0, 0, Spawn) Now consider the following process:

lnk (Reg 0 , Reg 0 ) | lnk (sp(Read 1 , Write 1 , 0), sp(Read 1 , Write 0 , 0)) | Spawn
its computation, which is depicted in Figure 2, proceeds as follows: two pairs of readerwriter threads are packed on the green node, guarded by two function symbols lnk and sp. The lnk function is called at step 1, and links both packs of threads to different registers (both initialized to 0). The first and second pairs of threads are then spawned using the function sp at steps 2 and 3. Because the two combinations of threads do not share the same register, and the second register does not hold the value expected by the associated reader thread, the second combination of threads is not able to terminate successfully.

Graph self-assembly

Consider a specification process graph Γ, which describes how a computation should be distributed, and in particular how processes that are located on the vertices of Γ should be topologically separated. The self-assembly challenge is to conceive of a process p (the implementation) that eventually produces the specification Γ, up-to garbage collection of idle nodes, as depicted in Figure 2. We finally show that CBP is able to realize non trivial assembly patterns. Definition 3.1 (Convergence). A process graph Γ weakly converges to Γ if there exists a trace of the form Γ → * Γ . We say that Γ strongly converges to Γ if all traces Γ → * Γ either factor through Γ , or Γ strongly converges to Γ .

Definition 3.2 (Homomorphism). Let Γ = def (V, E, π) and Γ = def (V , E , π ). A process graph homomorphism φ : Γ → Γ is an injective map φ : V → V that is: • Edge preserving : {x, y} ∈ E implies {φ(x), φ(y)} ∈ E . • Label preserving: π φ(x) = π(x), for all x ∈ V .
We say that a homomorphism φ : Γ → Γ is a quasi-iso if it is, in addition:

• Edge reflecting: {φ(x), φ(y)} ∈ E implies {x, y} ∈ E • Full: for all x ∈ V \ φ(V ), π (x ) = 0.
We write Γ φ Γ whenever there is a quasi-iso φ from Γ to Γ .

Proposition 3.2. The relation ≈ = def {(Γ, Γ ) | ∃φ : Γ φ Γ } is a bisimulation, i.e it is a symmetric relation that satisfies: Γ ≈ Γ =⇒ ∀Γ → Γ 0 , ∃Γ → Γ 1 such that Γ 0 ≈ Γ 1 .
Definition 3.3 (Assembly). A process p (strongly or weakly) assembles into Γ spec , with Γ spec = def (V s , E s , π s ), if {x : p} (strongly or weakly) converges to a graph Γ = (V, E, π) such that Γ spec φ Γ.

For simplicity, in the following example we consider only function symbols that are self dual, i.e f = f for all f . Consider the following process definitions and the process graph specification of the 3 dining philosophers: P = def take(take(Eat) + put(P)) Eat = def put(put(P)) F = def take(put(F))

Figure 3 illustrates the proof of p's assembly into Γ philo3 . We obtain the desired hexagon by transforming a triangle graph, which is the normalization of the process graph {x : p}, following the reductions of Fig. 3. Importantly the reduction Γ 3 → Γ 4 is enforced by symbol w which is positioned to prevent the reduction of symbol h before symbol i that would entail weak convergence only. Without symbol w, from Γ 2 , one may reduce symbol h to reach a state where two P processes have access to a single fork each. Now a philosopher may enter into infinite interactions with the fork by taking it and putting it back without letting the whole process ever reach the specification graph. Strong convergence requires that process p is able to assemble into the 3 dining philosophers in an atomic fashion: no philosopher may start taking forks before all philosophers are able to do so.

Compositional semantics

In this section, we introduce a labeled transition system (LTS) for CBP. It relies on a localization of top-level function symbols using a form of locality [START_REF] Boudol | A theory of processes with localities[END_REF][START_REF] Castellani | Observing distribution in processes: Static and dynamic localities[END_REF] or proof terms [START_REF] Boudol | A non-interleaving semantics for CCS based on proved transitions[END_REF][START_REF] Boudol | Permutation of transitions: an event structure semantics for CCS and SCCS, in: REXSchool/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency[END_REF]. The main idea behind the LTS is to "freeze" a process graph Γ into a tree t whose leaves correspond to nodes of and whose remaining nodes contain information allowing one to decide whether the leaves of the sub-tree are connected. The correspondence between CBP trees and CBP graphs is depicted in Figure 4. We formally address this correspondence in Section 5.

Syntax

Along with CBP processes, defined in Section 2:

s ::= f (p, p) | 0 | D( f ) | s + s p ::= s | (p p) | p \ H
we introduce CBP process trees, which provide an algebraic representation of graphs

t ::= p | (t ⊕ A t) | t \ H

labeled transition system

Let α ∈ F ∪ {τ } and θ ∈ {0, 1} * + ({0, 1} * × {0, 1} * ). For all (i, j), let b • (i, j) = def (b.i, b.j). The compositional semantics of CBP is induced by the following derivations:

f (p 1 , p 2 ) :f -→ p 1 ⊕ ∅ p 2 (act) (sum -left) s 1 :f -→ t s 1 + s 2 :f -→ t s 2 :f -→ t s 1 + s 2 :f -→ t (sum -right) s :f -→ t (D( h) := s{ h/g}) ∈ Def D(g) :f -→ t (link) t 0 i:f -→ t 0 t 1 j: f -→ t 1 (0.i, 1.j) ∈ E(A) B = upd(A, 0.i, 1.j) t 0 ⊕ A t 1 (0.i,1.j):τ -→ t 0 ⊕ B t 1 (synch) (res) t θ:α -→ t α ∈ H ∪ H t \ H θ:α -→ t \ H dist(p) θ:α -→ t p θ:α -→ t (dist) t θ:α -→ t t ⊕ A t 0•θ:α -→ t ⊕ A t (par -left) t θ:α -→ t t ⊕ A t 1•θ:α -→ t ⊕ A t (par -right)

Correctness of the labeled transition system

This section is dedicated to the proof of correctness of the LTS semantics of CBP introduced in Section 4. In Section 5.1 we show that any rigid process tree t can "thaw" into a process graph Γ. This "thawing" relation is defined by induction on the structure of t and produces eventually a bijective map that associates leaves of t to nodes of Γ. Theorem 5.1 then formalizes the correctness of the LTS as a bisimulation between the τ -transitions of CBP trees and the reductions that can be triggered from their thawed versions. The (main parts of the) proof of the theorem is split into Section 5.2, where we show that reductions can simulate the LTS, and Section 5.3 where the LTS is shown to simulate the reductions.

Thawing trees into graphs

For all t ∈ T define |t| ⊆ 2 {0,1} * as:

|p| = def { } |t ⊕ A t | = def 0 • |t| ∪ 1 • |t |
We define the thaw relation t φ (V, E, π), where φ is a bijective map φ : |t| → V , as the least relation satisfying:

p [ →x] {x : p} (3) t \ H φ Γ fresh(g) t \ (f H) φ (V, E, π{g/f }) (4)
-Suppose t = t 0 ⊕ A t 1 φ Γ. By derivation [START_REF] Boudol | A theory of processes with localities[END_REF] we have t 0 φ0 Γ 0 and t 1 φ1 Γ 1 . If x ∈ V 0 and y ∈ V 1 then we can apply Lemma 5.9, rule (synch) and derivation [START_REF] Boudol | A theory of processes with localities[END_REF] to obtain the derivation:

t 0 φ0 Γ 0 π 0 (x) = f (p, q) + s t 0 i:f -→ t 0 φ 0 Γ 0 [x 0 : p, x 1 : q/x] t 1 φ1 Γ 1 π 1 (y) = f (p , q ) + s t 1 j: f -→ t 1 φ 1 Γ 1 [y 0 : p , y 1 : q /y] t 0 ⊕ A t 1 (i,j):τ -→ t 0 ⊕ B t 1 ψ Γ with Γ = (V , E , π ) with V = V 0 [x 0 , x 1 /x] V 1 [y 0 , y 1 /y] E = E 0 [x 0 , x 1 /x] E 1 [y 0 , y 1 /y] E B π = π 0 [x 0 : p, x 1 : q/x] + π 1 [y 0 : p , y 1 : q /y]
We have t = t 0 ⊕ B t 1 and by derivation (5) we have:

E B = def {x , y } ∈ V 0 × V 1 | 0 • (φ -1 0 (x )), 1 • (φ -1 1 (y )) ∈ E(B) with V 0 = V 0 [x 0 , x 1 /x] and V 1 = V 1 [y 0 , y 1 /y].
Now, CBP reduction rule (1) produces Γ = def (V , E , π ), where according to Def. 2.1:

V = def V [x 0 , x 1 /x][y 0 , y 1 /y] E = def (E \ {{x, y}})[x i /x][ỹ i /y] ∪ {{x 0 , y 0 }, {x 1 , y 1 }} π = def π (V \ {x, y}) + [x 0 → p; x 1 → q; y 0 → p ; y 1 → q ]
We have V = V and π = π . It remains to verify that E = E . We decompose

E = E 0 E 1 E 01 where E 01 = {{z, t} ∈ V 0 × V 1 | {z, t} ∈ E}. Now we deduce: E \ {{x, y}} = (E 0 E 1 E 01 ) \ {{x, y}} = E 0 E 1 (E 01 \ {{x, y}}) since x ∈ V 0 and y ∈ V 1 .
We have:

E = (E 0 E 1 (E 01 \ {{x, y}}))[x i /x][ỹ i /y] ∪ {{x 0 , y 0 }, {x 1 , y 1 }} = E 0 [x i /x] E 1 [ỹ i /y] (E 01 \ {{x, y}} ∪ {{x 0 , y 0 }, {x 1 , y 1 }})
Since E 01 \ {{x, y}} ∪ {{x 0 , y 0 }, {x 1 , y 1 }} = E B we conclude that E = E and hence Γ = Γ .

• Suppose Γ → {x,y} Γ by application of the reduction rule (2). We summarize the inductive step in the diagram below.

Γ g / / ∆ {x,y} / / ∆ g / / Γ Eq. (2) Γ {x,y} / / Γ t φ O O Lem. 5.8 dnf(t) ψ O O H.R ψ -1 (x),ψ -1 (y) / / t Lem. 5.8 ψ O O dnf(t ) φ O O 18
We conclude that t i,j:τ -→ t , for i = ψ -1 (x) and j = ψ -1 (y), by Lemma 5.7. Since ψ(i) = φ(i) for all i in |t|, this terminates the proof.

Conclusion

We have introduced CBP, a calculus of branching processes, which is a generalization of CCS with branching continuations. Importantly, CBP is not conceived as an ad hoc calculus aiming at capturing a particular feature of concurrent systems. Yet, this arguably natural generalization of CCS provides powerful means to model a combination of distribution, thanks to non trivial communication graphs, and synchronization. Several theoretical investigations are suggested by the present work:

• A structural theory for process graphs. As pointed out in Section 3 we lack a theory of reachable process graphs in order to establish expressivity results. Being able to characterize whether a graph Γ can be obtained by successive reductions from a clique would characterize precisely which specification graphs are amenable to assembly from a purely local initial process.

• Self-assembly. More generally, techniques to produce a CBP implementation that converges to a specification need to be formally established. We conjecture that unlabeled process graph reductions, where one is interested in the assembly of a particular graph, without considering the way nodes are labeled, should play an important role. Also given weak convergence between {x : p} and Γ, it would be interesting to establish under which conditions one may automatically obtain strong convergence, by transformation of p.

• Other classes of automata. Following the CBP approach, one may wonder what class of concurrent systems corresponds to other types of communicating automata.

In particular, possible connections with pushdown automata [START_REF] Bouajjani | Reachability analysis of multithreaded software with asynchronous communication[END_REF] and final state machines [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] would be worth studying.

• Behavioral equivalences. CBP is a localized process calculus. Locality aware bisimulations [START_REF] Boudol | A theory of processes with localities[END_REF][START_REF] Bednarczyk | Hereditary History Preserving Bisimulations or What is the Power of the Future Perfect in Program Logics[END_REF] should naturally provide tools to compare branching processes.

Lemma 5.9. By induction on the derivation of t φ Γ.

• Base case is t = f (p, q) + s φ Γ = ({x}, ∅, [x → f (p, q) + s]). By rule (act), t :f -→ p ⊕ ∅ q. We apply derivation (3) to construct p φ0 ({x 0 }, ∅, [x 0 → p]) and q φ1 ({x 1 }, ∅, [x 1 → q]). By derivation (5) we build p ⊕ ∅ q φ ({x 0 , x 1 }, ∅, [x 0 → p; x 1 → q]) = def Γ . We can conclude since Γ = Γ[x 0 : p, x 1 : q/x].

• In the inductive step one assumes t = t 0 ⊕ A t 1 φ Γ and for all b ∈ {0, 1},

t b φ b Γ b . Since V = def V 0 V 1 ,
x is either in Γ 0 or Γ 1 . W.l.o.g., suppose x ∈ Γ 0 . We can derive by induction hypothesis: t 0 φ0 Γ 0 π 0 (x) = π(x) = f (p, q) + s i = φ -1 0 (x) t 0 i:f -→ t 0 ψ0 Γ 0 [x 0 : p, x 1 : q/x] = def Γ 0 By rule (par-left), we derive:

t 0 i:f -→ t 0 t = t 0 ⊕ A t 1 0.i:f -→ t 0 ⊕ A t 1 = t
Additionally, for derivation (5) we derive:

t 0 ψ0 Γ 0 t 1 φ1 Γ 1 t ψ (V 0 V 1 , E 0 E 1 E A , π 0 + π 1 ) = def Γ
with, for all i ∈ |t |, ψ (0.i) = ψ 0 (i) and ψ (1.i) = φ 1 (i).

It remains to verify that Γ = Γ[x 0 : p, x 1 : q/x]. By definition of the substitution operation we have:

V 0 = V 0 [x 0 , x 1 /
x] E 0 = E 0 [x 0 , x 1 /x] π 0 = π 0 [x 0 : p, x 1 : q/x] Since Γ = (V 0 V 1 , E 0 E 1 E A , π 0 + π 1 ) and x ∈ V 0 we do have Γ = Γ[x 0 : p, x 1 : q/x].

Figure 1 :

 1 Figure1: Binary CBP's reduction rule (left): the nodes x and y are ready to synchronize on symbols f and f (of arity 2), and are connected by an edge. X (resp. Y ) denotes nodes in the context that are connected to x but not y (resp. y but not x). Z denotes nodes of the context of the reduction that are connected to both x and y. The reduction replaces nodes x and y by their continuations x 1 , x 2 and y 1 , y 2 . New edges connect nodes in X (resp. Y ) and Z to the continuations of x (resp. y). On the right, the reduction scheme for n-ary functions in the full CBP.

Figure 2 :

 2 Figure 2: A computation of the threads processes (thick edges denote reduction redexes). Edges that connect two processes that have no complementary function symbols are dotted. Idle nodes are garbage collected.

Figure 3 :

 3 Figure 3: Proof of the assembly of p into the 3-dining philosophers. Nodes labeled with a nil process as well as edges connecting to them are faded out. Reductions are applied modulo quasi-iso.

Classical CCS terms may be denoted by processes distributed on the nodes of a clique, in this context.

Unlike CCS, self-dual function symbols, f = f , are also allowed.

However, the CCS process a.(p q) can be mimicked by the CBP process a(p q, 0), where p and q are in the same continuation and thus are able to interact.

Note that the encoding of the one-bit register is done in a fragment of CBP that coincides with CCS (unary CBP).

Acknowledgment

This work is supported by the Chinese Academy of Science-INRIA project Verification, Interactions and proofs, VIP GJHZ1844.

f (p 0 , q 0 ) < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > f (p 0 0 , q 0 0 )

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > ḡ(p 1 , q 1 ) < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > g(p 0 1 , q 0 1 )

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > (01,10) (0,1) (0,1) ⌧ < l a t e x i t s h a 1 _ b a s e 6 4 = " R h g 6 9 / g o B p 0 n / c D F G z r u Z k t r J B 4 = " > A A A D U 3 i c j V P L T t t A F D 1 J W g q h v J B r e 4 a / 5 q P r T 4 l V T S Z q O u W c C L 1 Z p 6 B P B I q 5 Q = < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " p M A l k R R q w u U M f W 3 Z u 6 F 9 Z z + h g v I = " > A A A D U 3 i c j V P L T t t A F D 1 J + k h D a Y E u U S W r E R K r y G k X b R d t I 9 F F l 6 n U F K Q E I d s M x M r 4 U X u M h K z 8 A l v 4 H / 4 B i T + A f + i C M 9 e O V I K q d q L Y 5 5 5 7 7 p l 7 x 7 a f 6 j A 3 r n v d a L Y e P X 7 y t P 2 s s /

X D 7 m p B m v y C W / 0 y w T 9 w / s G F p 2 5 K G J V h p k L S 5 5 5 7 7 q l 7 q y t h r u P S + P 5 T o 9 n 6 8 n V s f O J b e / L 7 1 P T p 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > p 0 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > ḡ(p 1 , q 1 ) < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > g(p 0

1 , q 0 1 )

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t >

(01,10) (00,10) (01,11) p 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > p 0 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > p 1

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 1

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > p 0 1 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0 1 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t >

X D 7 m p B m v y C W / 0 y w T 9 w / s G F p 2 5 K G J V h p k L S 5 5 5 7 7 q l 7 q y t h r u P S + P 5 t 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > t 1

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > t 2

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t >

(01,10) (00,10) (01,11) (0,1) p 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > p 0 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > q 0 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > ḡ(p 1 , q 1 ) < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > g(p 0 1 , q 0 1 )

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > 0 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > 1 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > t 1

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > 1 < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t >

2

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > t < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > t 0

< l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > < l a t e x i t s h a 1 _ b a s e 6 4 = " ( n u l l ) " > ( n u l l ) < / l a t e x i t > Figure 4: Representation of CBP graphs (Γ 0 , Γ 1 and Γ 2 ) as trees (t 0 , t 1 and t 2 ). Each leaf of the process tree t i contains a different vertex of the process graph Γ i (for i ∈ {0, 1, 2}). Roots of (sub)trees are labeled by a list of pairs of addresses (in the example: the blue, red and green rectangles, subtrees labeled by the empty list are pictured unlabeled). Addresses in these pairs are relative to the position of the root containing the list: 0 stands for the left subtree and 1 stands for the right subtree. The process graph Γ i denoted by the process tree t i is obtained by adding edges connecting two leaves (dotted in the picture) as indicated by the lists of address pairs in the root above them. For instance, the red router of process tree t 2 , associates address 01 to address 10, which point respectively to the subtrees t = p 0 ⊕ q 0 and t = p 1 ⊕ q 1 . This implies that all leaves of t and t should be pairwise connected in the corresponding process graph Γ 2 . Note that the leaves labeled by p 1 and q 1 in Γ 2 are not connected since the subtree t is labeled by the empty list.

where A ∈ 2 ({0,1} + ×{0,1} + ) . We use T to denote the set of process trees generated by non terminal symbol t. As presented in Fig 4, operators ⊕ A , that we call routers, act as "regulators" for communication. In the tree t 0 ⊕ A t 1 , a function symbol originating from the subtree t 0 will only be able to synchronize with a dual symbol in t 1 if the table A allows them to do so. Router table A is updated upon synchronization between t 0 and t 1 as shown in the next section.

In the meantime we introduce an important function that allows one to unfold a leaf labeled with p q into a tree. To do so, process trees are equipped with a distribution function, dist : P → T and that is defined as:

Router update

We consider addresses (meta-variables i, j, k, . . . ), which are words over the alphabet {0, 1}. For all addresses i, j, we write i ≤ j if j = i.k for some address k (j is more 12 precise than i). For all X ∈ 2 {0,1} * we define ↑ X = def {i ∈ {0, 1} * | ∃j ∈ X : j ≤ i}. Similarly, we use ↓ X to denote the set of addresses that are less precise than those in X.

For all A ∈ 2 ({0,1} + ×{0,1} + ) , the set of edges denoted by A is

After a synchronization has occurred, the table A needs to be updated to take into account the change in the topology of permissible communications, as specified in Fig. 1. We turn now to the formal description of this router update mechanism. For all I ∈ 2 {0,1} * and b ∈ {0, 1}, we use the meta operation b • I defined as b

For all b ∈ {0, 1} we write ¬b to denote (1b). We define . : {0, 1} * → 2 {0,1} * as:

For all i ≤ i we define i i as:

For instance, 10 1011 = def 10 • {0, 10}, which is {100, 1010}, and ↑{100, 1010} contains all addresses above 10 that are not above 1011.

For all i ∈ {0, 1} * and all I ⊆ ↓{i}, we write I i for i ∈I i i. Now, consider a set A ∈ 2 ({0,1} * ×{0,1} * ) and two addresses i, j ∈ {0, 1} * and let

One defines:

Theorem 4.2. The effect of δ i,j (A) is to prevent all synchronizations between localities that are more precise than (i, j) and to preserve all other previously possible communications, i.e.:

Definition 4.1 (Router update). For all i, j ∈ {0, 1} * , the router update is:

Corollary. For all A ∈ 2 {0,1} * ×{0,1} * and i, j ∈ {0, 1} * :

with:

is a bisimulation between process graphs reductions, and τ -transitions of process trees, i.e. for all φ, there exists a ψ that satisfies the following diagrams:

Process graph reductions simulate τ -transitions

Structural congruence for processes ≡ p ⊆ P×P is defined as

and structural congruence for process graphs is

Lemma 5.2. ≡ g is a bisimulation for process graph reduction semantics.

The above lemma insures that it is safe to consider process graphs up-to consistent substitution of function symbols. There is an equivalent proposition for process trees: Definition 5.1. Consider α ⊆ T × T that is the least relation satisfying:

The relation α is a bisimulation for CBP's labeled transition system. This lemma allows us to consider terms of CBP with restrictions occurring exclusively inside recursive definition bodies and to safely erase them upon definition unfolding. Note that this procedure is not needed for the operational semantics but simplifies greatly the proofs. Definition 5.2. Let t a process tree. For all i ∈ ↓ |t|, we define t@i by induction on i:

Lemma 5.4. For all transition t i:f -→ t , there exist p 0 , p 1 ∈ P such that t@i ≡ p f (p 0 , p 1 ) + s for some (possibly null) s.

Lemma 5.5. Let t φ Γ = def (V, E, π). For all i ∈ |t|, if t@i = p then π • φ(i) = p. Lemma 5.6. For all process tree t and process graph Γ = def (V, E, π), the following derivation holds ∀b ∈ {0, 1}:

Theorem 5.1, left diagram. We wish to show:

We proceed by induction on the derivation of the τ -transition.

• Base case is t (0.i,1.j):τ -→ t , for some i, j ∈ {0, 1} * , by application of rule (synch). We have:

Since t φ Γ we can use derivation [START_REF] Boudol | A theory of processes with localities[END_REF] to deduce:

for some

). We apply Lemma 5.4, to the premises of derivation [START_REF] Castellani | Observing distribution in processes: Static and dynamic localities[END_REF] and we obtain:

t 0 @i ≡ p f (p 0 , p 1 ) + s t 1 @j ≡ p f (p 0 , p 1 ) + s

We apply Lemma 5.5 to deduce π 0 • φ 0 (i) ≡ p f (p 0 , p 1 ) + s and π 1 • φ 1 (j) ≡ p f (p 0 , p 1 ) + s . Now according to the premises of derivation (5), φ(0.i) = φ 0 (i) and φ(1.j) = φ 1 (j). Hence we have:

It remains to verify that φ(0.i) and φ(1.j) are connected in Γ. The only possibility is to verify that {φ(0.i), φ(1.j)} ∈ E A . It is indeed the case if:

which is equivalent to:

and reduces to (0.i, 1.j) ∈ E(A) which holds by the premises of derivation [START_REF] Castellani | Observing distribution in processes: Static and dynamic localities[END_REF]. We can conclude that Γ → {φ(0.i),φ(1.j)} Γ since all preconditions to trigger a reduction 16 of the process graph Γ hold. It remains to verify that t = t 0 ⊕ B t 1 ψ Γ for some ψ. We apply Lemma 5.6 to the premises of

and derivation (5) applied to t 0 ⊕ A t 1 φ Γ, and we obtain t 0 φ 0 Γ 0 and t

• We conclude by applying a straightforward induction for the contextual rules in the particular case of a τ -transition.

τ -transitions simulate process graph reductions

In order to prove the right diagram of Theorem 5.1 we need a couple of definitions and lemmas. Definition 5.3 (dist-normal form). We define the dist-normalization function dnf : T → T as:

Note that dnf(t) returns after exactly |t| calls to dist.

Lemma 5.7. Let D= def {(t, t ) | dnf(t) = dnf(t )}. The relation D is a bisimulation for CBP's labeled transition system.

Lemma 5.8. For all Γ, Γ ∈ G and all t ∈ T satisfying Γ g Γ and t φ Γ, there exists ψ such that dnf(t) ψ Γ .

Lemma 5.9. For all t and Γ = (V, E, π), the following derivation holds:

We have now everything in place to prove the final part of the theorem.

Theorem 5.1, right diagram. We need to show

We prove this derivation by induction on the derivation of the reduction Γ → {x,y} Γ .

• Suppose Γ → {x,y} Γ by application of reduction rule (1). We show statement [START_REF] De Nicola | Testing equivalences for processes[END_REF] by induction on the derivation of t φ Γ.

-Base case: if t = p then no reduction is possible from Γ through reduction rule (1).

Appendix

Missing proofs of important lemmas are listed here.

Lemma 5.4. By induction on the derivation of t i:f -→ t

• (act) we have t@ = f (p 0 , p 1 ) which is readily of the desired form.

• (sum-left) by induction hypothesis, we have s 1 @ ≡ p f (p 0 , p 1 )+s so t = (f (p 0 , p 1 )+ s) + s 2 and t ≡ p f (p 0 , p 1 ) + (s + s 2 ), which is in the desired form. The symmetric argument applies for (sum-right).

• (link) we have t@ = D(g). Since Def contains only guarded sums, we have D(g) ≡ p f (p 0 , p 1 ) + s and one proceeds as before.

• (dist) The interesting case is whenever p = def p 0 p 1 . We have dist(p) = p 0 ⊕ {(0,1)} p 1 and dist(p)

-Suppose i = 0.i for some i . The only rule that has:

in its conclusion is (parleft). Therefore we have p 0 i :f -→ t 0 (by the premises of the rule) and t = t 0 ⊕ {(0,1)} p 1 . By induction hypothesis we have p 0 @i ≡ p f (p , q )+s. One deduces that dist(p)@0.i ≡ p f (p , q )+s or written otherwise dist(p)@i ≡ p f (p , q ) + s, which is the desired form.

-The case i = 1.i for some i is treated likewise using the (parright) rule.

-The case where i = is not applicable because no rule having t ⊕ A t on the left hand side has label with an address.

• (synch) This rule may not produce a transition of the correct form.

• (par-left,par-right) one applies induction hypothesis on the premises of the rules.

Lemma 5.6. We proceed by induction on the derivation of t i:f -→ t .

• Case (act). We have t = f (p 0 , p 1 ) and Γ = ({x}, ∅, p 0 ⊕ ∅ p 1 ψ ({x 0 , x 1 }, ∅, [x 0 → q 0 ; x 1 → q 1 ]) ≡ g Γ[x 0 : p 0 , x 1 : p 1 /x] since q b ≡ p p b .

• Cases (sum-left/right). We have t = s 0 +s 1 φ Γ and we apply induction hypothesis to s 0 Applying derivation (5) and derivation (3), we have:

dist(p) φ ({x, y}, {{x, y}}, [x → q 0 ; y → q 1 ]) = def Γ with q b ≡ p p b .

-Suppose i = 0.i . We apply inductive step to deduce: t ψ ({x 0 , x 1 , y}, {{x 0 , y}, {x 1 , y}}, [x b → t @i.b; y → q 1 ]) = def Γ Since Γ = Γ [x 0 , x 1 /x] and Γ ≡ g Γ we may conclude.

-The case i = 1.i follows a symmetric argument.

• Cases (par-left/right). Let t = t 0 ⊕ A t 1 0.i :f -→ t 0 ⊕ A t 1 . By the premises of (par-left)

and derivation [START_REF] Boudol | A theory of processes with localities[END_REF] we have t 0 i :f -→ t 0 and t b φ b Γ b for all b ∈ {0, 1}. We apply induction hypothesis to deduce: t 0 ψ Γ 0 [x 0 : t 0 @i .0, x 1 : t 0 @i .1/φ 0 (i )] with Γ 0 ≡ g Γ 0 .

Let p b = t 0 @i .b and Γ 0 [x 0 : p 0 , x 1 : p 1 /φ 0 (i )] = (V 0 , E 0 , π 0 ). We use the fact that t 1 φ1 Γ 1 = def (V 1 , E 1 , π 1 ) to obtain, thanks to derivation (5):

We verify now that Γ ≡ g Γ[x 0 , x 1 /φ(i)]. Since t = t 0 ⊕ A t 1 we know, by derivation (5) that Γ = (V 0 V 1 , E 0 E 1 , π 0 ). Since V 0 is the set of vertices of Γ 0 [x 0 : p 0 , x 1 : p 1 /φ 0 (i )] with Γ 0 ≡ g Γ 0 we have:

π 0 = π 0 [x 0 : t 0 @i .0, x 1 : t 0 @i .1/φ 0 (i )] Since φ 0 (i ) = φ(0.i ) = φ(i) and t 0 @i .b = (t 0 ⊕ A t 1 )@0.i .b = t @i.b we can conclude.

• The case (res) is straightforward.