Andrés Aristizábal

Filippo Bonchi

Catuscia Palamidessi

Frank Luis Pino

Frank D Valencia

LIX Valencia Comète

Deriving Labels and Bisimilarity for Concurrent Constraint Programming

published or not. The documents may come

L'archive ouverte

Introduction

Concurrency is concerned with systems of multiple computing agents, usually called processes, that interact with each other. Process calculi treat processes much like the λcalculus treats computable functions. They provide a language in which processes are represented by terms, and computational steps are represented as transitions between them. These formalisms are equipped with equivalence relations that determine what processes are deemed indistinguishable.

Bisimilarity is one of the main representative of these process equivalences. It captures our intuitive notion of process equivalence; two processes are equivalent if they can match each other's moves. Furthermore, it provides an elegant co-inductive proof technique based on Park's notion of bisimulation.

Concurrent Constraint Programming (ccp) [START_REF] Saraswat | Concurrent constraint programming[END_REF] is a well-established formalism that combines the traditional algebraic and operational view of process calculi with a declarative one based upon first-order logic. In ccp, processes interact by adding (or telling) and asking information (namely, constraints) in a medium (the store). Ccp is parametric in a constraint system indicating interdependencies (entailment) between constraints and providing for the specification of data types and other rich structures. The above features have recently attracted a renewed attention as witnessed by the works [START_REF] Palamidessi | On the expressiveness of linearity vs persistence in the asychronous pi-calculus[END_REF][START_REF] Buscemi | Open bisimulation for the concurrent constraint picalculus[END_REF][START_REF] Bengtson | Psi-calculi: Mobile processes, nominal data, and logic[END_REF][START_REF] Bartoletti | A calculus of contracting processes[END_REF] on calculi exhibiting data-types, logic assertions as well as tell and ask operations.

Despite the relevance of bisimilarity, there have been few attempts to define a notion of bisimilarity for ccp. The ones we are aware of are those in [START_REF] Saraswat | Concurrent constraint programming[END_REF] and [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF] upon which we build. These equivalences are not completely satisfactory: We shall see that the first one may tell apart processes with identical observable behaviour, while the second quantifies over all possible inputs from the environment, and hence it is not clear whether it can lead to a feasible proof technique.

The goal of this paper is to define a notion of bisimilarity for ccp which will allow to benefit of the feasible proof and verification techniques typically associated with bisimilarity. Furthermore, we aim at studying the relationship between this equivalence and other existing semantic notions for ccp. In particular, its elegant denotational characterization based on closure operators [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] and the connection with logic [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF]. Labels and Bisimilarity from Reductions. Bisimilarity relies on labelled transitions: each evolution step of a system is tagged by some information aimed at capturing the possible interactions of a process with the environment. Nowadays process calculi tend to adopt reduction semantics based on unlabelled transitions and barbed congruence [START_REF] Milner | Barbed bisimulation[END_REF]. The main drawback of this approach is that to verify barbed congruences it is often necessary to analyze the behaviour of processes under every context.

This scenario has motivated a novel stream of research [START_REF] Sewell | From rewrite to bisimulation congruences[END_REF][START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF][START_REF] Ehrig | Deriving bisimulation congruences in the dpo approach to graph rewriting[END_REF][START_REF] Sassone | Reactive systems over cospans[END_REF][START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Rathke | Deconstructing behavioural theories of mobility[END_REF][START_REF] Gianantonio | Rpo, second-order contexts, and lambdacalculus[END_REF],5] aimed at defining techniques for "deriving labels and bisimilarity" from unlabeled reduction semantics. The main intuition is that labels should represent the "minimal contexts allowing a process to reduce". The theory of reactive systems by Leifer and Milner [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF] provides a formal characterization (by means of a categorical construction) of such "minimal contexts" and it focuses on the bisimilarity over transition systems labeled as: P C -→ P ′ iff C[P ] -→ P ′ and C is the minimal context allowing such reduction.

In [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], it is argued that the above bisimilarity is often too fine grained and an alternative, coarser, notion of bisimilarity is provided. Intuitively, in the bisimulation game, each move (transition) P C -→ P ′ , has to be matched it with a move C[Q] -→ Q ′ . Labels and Bisimilarity for ccp. The operational semantics of ccp is expressed by reductions between configurations of the form P, d -→ P ′ , d ′ meaning that the process P with store d may reduce to P ′ with store d ′ . From this semantics we shall derive a labeled transition system for ccp by exploiting the intuition of [START_REF] Sewell | From rewrite to bisimulation congruences[END_REF][START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF]. The transition P, d e -→ P ′ , d ′ means that e is a "minimal constraint" (from the environment) that needs to be added to d to reduce from P, d into P ′ , d ′ .

Similar ideas were already proposed in [START_REF] Saraswat | Concurrent constraint programming[END_REF] but, the recent developments in [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF] enlighten the way for obtaining a fully abstract equivalence. Indeed, the standard notion of bisimilarity defined on our labeled semantics can be seen as an instance of the one proposed in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF]. As for the bisimilarity in [START_REF] Saraswat | Concurrent constraint programming[END_REF], it is too fine grained, i.e., it separates processes which are indistinguishable. Instead, the notion of bisimulation from [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF] (instantiated to the case of ccp) is fully abstract with respect to the standard observational equivalence given in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Our work can therefore be also regarded as a compelling application of the theory of reactive systems. Contributions. We provide a labelled transition semantics and a novel notion of labelled bisimilarity for ccp by building upon the work in [START_REF] Saraswat | Concurrent constraint programming[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]. We also establish a strong correspondence with existing ccp notions by providing a fully-abstract characterization of a standard observable behaviour for infinite ccp processes: The limits of fair computations. From [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] this implies a fully-abstract correspondence with the closure operator denotational semantics of ccp. Therefore, this work provides ccp with a new co-inductive proof technique, coherent with the existing ones, for reasoning about process equivalence. We shall confine ourselves to the summation free-fragment of ccp [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Our notion of bisimilarity is orthogonal to this issue, however this restriction allows us to obtain the fully-abstract characterization mentioned above.

Background

In this section we recall the syntax, the operational semantics and the observational equivalence of concurrent constraint programming (ccp). We begin with the notion of constraint system. We presuppose some basic knowledge of domain theory (see [START_REF] Abramsky | Domain theory[END_REF]).

Constraint Systems

The ccp model is parametric in a constraint system specifying the structure and interdependencies of the information that processes can ask and tell. Following [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF], we regard a constraint system as a complete algebraic lattice structure in which the ordering ⊑ is the reverse of an entailment relation (c ⊑ d means that d contains "more information" than c, hence c can be derived from d). The top element false represents inconsistency, the bottom element true is the empty constraint, and the least upper bound (lub) ⊔ represents the join of information. Definition 1. A constraint system C is a complete algebraic lattice (Con, Con 0 , ⊑ , ⊔, true, false) where Con (the set of constraints) is a partially ordered set w.r.t. ⊑, Con 0 is the subset of finite elements of Con, ⊔ is the lub operation, and true, false are the least and greatest elements of Con, respectively.

Recall that C is a complete lattice iff every subset of Con has a least upper bound in Con. An element c ∈ Con is finite iff for any directed subset D of Con, c ⊑ D implies c ⊑ d for some d ∈ D. C is algebraic iff each element c ∈ Con is the least upper bound of the finite elements below c.

In order to model hiding of local variables and parameter passing, in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] the notion of constraint system is enriched with cylindrification operators and diagonal elements, concepts borrowed from the theory of cylindric algebras (see [START_REF] Henkin | Cylindric Algebras (Part I)[END_REF]).

Let us consider a (denumerable) set of variables Var with typical elements x, y, z, . . . Define ∃ Var as the family of operators ∃ Var = {∃ x | x ∈ Var } (cylindric operators) and D Var as the set D Var = {d xy | x, y ∈ Var } (diagonal elements).

A cylindric constraint system over a set of variables Var is a constraint system whose support set Con ⊇ D Var is closed under the cylindric operators ∃ Var and satisfying the axioms in Def. 11 in Appendix A.1. For our purposes, it is enough to think the operator ∃ x as existential quantifier and the constraint d xy as the equality x = y.

Different notions of free variables and variables substitution for constraints have been given in literature (see e.g. [START_REF] Villanueva | Model Checking for the Concurrent Constraint Paradigm[END_REF]). Here, we do not rely on any specific definition, but we just assume that they satisfy the following conditions, where c[y/x] is the constraint obtained by substituting x by y in c and fv (c) is the set of free variables of c:

(1) if y / ∈ fv (c) then (c[y/x])[x/y] = c; (2) (c ⊔ d)[y/x] = c[y/x] ⊔ d[y/x]; (3) x / ∈ fv (c[y/x]); (4) fv (c ⊔ d) = fv (c) ∪ fv (d).
We now define the cylindric constraint system that will be used in all the examples. We assume the reader is familiar with basic concepts of Model Theory [START_REF] Chang | Model theory[END_REF].

Example 1 (The S Constraint System). Let S = (ω + 1, 0, ∞, =, <, succ) be a firstorder structure whose domain of interpretation is ω + 1 def = ω ∪ {∞}, i.e., the natural numbers extended with a top element ∞. The constant symbols 0 and ∞ are interpreted as zero and infinity, respectively. The symbols =, < and succ are all binary predicates on ω + 1. The symbol = is interpreted as the identity relation. The symbol < is interpreted as the set of pairs (n, m) s.t., n ∈ ω, m ∈ ω + 1 and n strictly smaller than m. The symbol succ is interpreted as the set of pairs (n, m) s.t., n, m ∈ ω and m = n + 1.

Let Var be an infinite set of variables. Let L be the logic whose formulae φ are:

φ ::= t | φ 1 ∧ φ 2 | ∃ x φ t ::= e 1 = e 2 | e 1 < e 2 | succ(e 1 , e 2 )
where e 1 and e 2 are either 0 or ∞ or variables in V ar. Note that formulas like x = n or x < n (for n = 1, 2, . . . ) do not belong to L. A useful abbreviation to express them is succ n (x, y) def = ∃y 0 . . . ∃y n ( 0<i≤n succ(y i-1 , y i ) ∧ x = y 0 ∧ y = y n ). We use x = n as shorthand for succ n (0, x) and x < n as shorthand for ∃ y (x < y ∧ y = n).

A variable assignment is a function µ : Var -→ ω + 1. We use A to denote the set of all assignments; P(X) to denote the powerset of a set X, ∅ the empty set and ∩ the intersection of sets. We use M(φ) to denote the set of all assignments that satisfy the formula φ, where the definition of satisfaction is as expected.

We can now introduce a constraint system as follows: the set of constraints is P(A), and define c ⊑ d iff c ⊇ d. The constraint false is ∅, while true is A. Given two constraints c and d, c ⊔ d is the intersection c ∩ d. By abusing the notation, we will often use a formula φ to denote the corresponding constraint, i.e., the set of all assignments satisfying φ. E.g. we use

1 < x ⊑ 5 < x to mean M(1 < x) ⊑ M(5 < x).
From this structure, let us now define the cylindric constraint system S as follows. We say that an assignment µ ′ is an x-variant of µ if ∀y = x, µ(y) = µ ′ (y). Given x ∈ Var and c ∈ P(A), the constraint ∃ x c is the set of assignments µ such that exists µ ′ ∈ c that is an x-variant of µ. The diagonal element d xy is x = y.

⊓ ⊔

Before introducing the syntax of ccp, we need to make an extra-assumption that will be pivotal in Section 2. Given a partial order (C, ⊑), we say that c is strictly smaller than d (written c ⊏ d) if c ⊑ d and c = d. We say that (C, ⊑) is well-founded if there exists no infinite descending chains

• • • ⊏ c n ⊏ • • • ⊏ c 1 ⊏ c 0 .
For a set A ⊆ C, we say that an element m ∈ A is minimal in A if for all a ∈ A, a ⊏ m. We shall use min(A) to denote the set of all minimal elements of A. Well-founded order and minimal elements are related by the following result.

Lemma 1. Let (C, ⊑) be a well-founded order and

A ⊆ C. If a ∈ A, then ∃m ∈ min(A) s.t., m ⊑ a.
In spite of its being a reasonable assumption, well-foundedness of (Con, ⊑) is not usually required in the standard theory of ccp. We require it because the above lemma is fundamental for proving the completeness of labeled semantics (Lemma 5).

Syntax

Concurrent constraint programming (ccp) was proposed in [START_REF] Saraswat | Concurrent Constraint Programming[END_REF] and then refined in [START_REF] Saraswat | Concurrent constraint programming[END_REF][START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. We restrict ourselves to the summation-free fragment of ccp. The distinctive confluent nature of this fragment is necessary for showing that our notion of bisimilarity coincides with the observational equivalence for infinite ccp processes given in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF].

Definition 2. Assume a cylindric constraint system C = (Con, Con 0 , ⊑, ⊔, true, false) over a set of variables Var . The ccp processes are given by the following syntax:

P, Q . . . ::= tell(c) | ask(c) → P | P Q | ∃ x P | p(z)
where c ∈ Con 0 , x ∈ Var , z ∈ Var * . We use Proc to denote the set of all processes. Finite processes. Intuitively, the tell process tell(c) adds c to the global store. The addition is performed regardless the generation of inconsistent information. The ask process ask(c) → P may execute P if c is entailed from the information in the store. The process P Q stands for the parallel execution of P and Q; ∃ x is a hiding operator, namely it indicates that in ∃ x P the variable x is local to P . The occurrences of x in ∃ x P are said to be bound. The bound variables of P , bv (P ), are those with a bound occurrence in P , and its free variables, fv (P ), are those with an unbound occurrence.

Infinite processes. To specify infinite behaviour, ccp provides parametric process definitions. A process p(z) is said to be a procedure call with identifier p and actual parameters z. We presuppose that for each procedure call p(z 1 . . . z m ) there exists a unique procedure definition possibly recursive, of the form p(x 1 . . . x m ) def = P where fv (P ) ⊆ {x 1 . . . x m }. Furthermore we require recursion to be guarded: I.e., each procedure call within P must occur within an ask process. The behaviour of p(z 1 . . . z m ) is that of P [z 1 . . . z m /x 1 . . . x m ], i.e., P with each x i replaced with z i (applying αconversion to avoid clashes). We shall use D to denote the set of all process definitions.

Although we have not defined yet the semantics of processes, we find it instructive to illustrate the above operators with the following example. Recall that we shall use S in Ex. 1 as the underlying constraint system in all examples.

Example 2. Consider the following (family of) process definitions.

up n (x) def = ∃ y (tell(y = n) ask (y = n) → up(x, y)) up(x, y) def = ∃ y ′ (tell(y < x∧succ 2 (y, y ′ )) ask(y < x∧succ 2 (y, y ′ )) → up(x, y ′ ))
Intuitively, up n (x), where n is a natural number, specifies that x should be greater than any natural number (i.e., x = ∞ since x ∈ ω + 1) by telling (adding to the global store) the constraints y i+1 = y i + 2 and y i < x for some y 0 , y 1 , . . . with y 0 = n. The process up 0 (x) ask(42 < x) → tell(z = 0), can set z = 0 when it infers from the global store that 42 < x. (This inference is only possible after the 22 nd call to up.) ⊓ ⊔

Reduction semantics

To describe the evolution of processes, we extend the syntax by introducing a process stop representing successful termination, and a process ∃ e x P representing the evolution of a process of the form ∃ x Q, where e is the local information (local store) produced during this evolution. The process ∃ x P can be seen as a particular case of ∃ e

x P : it represents the situation in which the local store is empty. Namely,

∃ x P = ∃ true x P . R1 tell(c), d -→ stop, d ⊔ c R2 c ⊑ d ask (c) → P, d -→ P, d R3 P, d -→ P ′ , d ′ P Q, d -→ P ′ Q, d ′ R4 P, e ⊔ ∃xd -→ P ′ , e ′ ⊔ ∃xd ∃ e x P, d -→ ∃ e ′ x P ′ , d ⊔ ∃xe ′ R5 P [z/x], d -→ γ ′ p(z), d -→ γ ′
where p(x)

def = P is a process definition in D Table 1.
Reduction semantics for ccp (The symmetric Rule for R3 is omitted)

A configuration is a pair P, d representing the state of a system; d is a constraint representing the global store, and P is a process in the extended syntax. We use Conf with typical elements γ, γ ′ , . . . to denote the set of configurations. The operational model of ccp can be described formally in the SOS style by means of the transition relation between configurations -→ ⊆ Conf × Conf defined in Table 1.

Rules R1-R3 and R5 are easily seen to realize the above process intuitions. Rule R4 is somewhat more involved. Here, we show an instructive example of its use, a detailed description of this standard ccp rule is in Appendix A.2.

Example 3. We obtain the following reduction of P = ∃ e x (ask (y > 1) → Q) where the local store is e = x < 1, and the global store

d ′ = d ⊔ α with d = y > x, α = x > 1. R2 R4 (y > 1) ⊑ e ⊔ ∃ x d ′ ask (y > 1) → Q, e ⊔ ∃ x d ′ -→ Q, e ⊔ ∃ x d ′ P, d ′ -→ ∃ e x Q, d ′ ⊔ ∃ x e
Note that the x in d ′ is hidden, by using existential quantification in the reduction obtained by Rule R2. This expresses that the x in d ′ is different from the one bound by the local process. Otherwise an inconsistency would be generated (i.e., (e⊔d ′ ) = false). Rule R2 applies since (y > 1) ⊑ e ⊔ ∃ x d ′ . Note that the free x in e ⊔ ∃ x d ′ is hidden in the global store to indicate that is different from the global x.

⊓ ⊔

Observational equivalence

The notion of fairness is central to the definition of observational equivalence for ccp.

To define fair computations, we introduce the notions of enabled and active processes, following [START_REF] Falaschi | Confluence in concurrent constraint programming[END_REF]. Observe that any transition is generated either by a tell(c) or by an ask (c) → P . We say that a process is active in a transition, if it generates such transition. Moreover, we say that a process is enabled in a configuration γ if it is active in a transition γ -→ γ ′ .

Definition 3. A computation γ 0 -→ γ 1 -→ . . . -→ γ n .
. . is said to be fair if for each process enabled in some γ i there exists j ≥ i such that the process is active in γ j .

Note that a finite fair computation is guaranteed to be maximal, namely no outgoing transitions are possible from its last configuration. The standard notion of observables for ccp are the results computed by a process for a given initial store. The result of a computation is defined as the least upper bound of all the stores occurring in the computation, which, due to the monotonic properties of ccp, form an increasing chain. More formally, given a finite or infinite computation ξ of the form

Q 0 , d 0 -→ Q 1 , d 1 -→ ... -→ Q i , d i -→ ..., the result of ξ, denoted by Result(ξ), is the constraint i d i .
Note that for a finite computation the result coincides with the store of the last configuration.

The following theorem from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] states that all the fair computations of a configuration have the same result (due to fact that summation-free ccp is confluent).

Theorem 1 (from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]). Let γ be a configuration and let ξ 1 and ξ 2 be two computations of γ. If

∼ o Q, iff O(P ) = O(Q).
Example 4. Consider the processes P = up 0 (x) up 1 (y) and Q = ∃ z (tell(z = 0) ask(z = 0) → fairup(x, y, z)) with up 0 and up 1 as in Ex. 2 and fairup(x, y, z)

def = ∃ z ′ (tell(z < x ∧ succ(z, z ′ )) ask ((z < x) ∧ succ(z, z ′ )) → fairup(y, x, z ′ )))
Let s(γ) denote the store in the configuration γ. For every infinite computation ξ : P, true = γ 0 -→ γ 1 -→ . . . with (1 < y) ⊑ s(γ i ) for each i ≥ 0, ξ is not fair and Result(ξ) = (x = ∞). In contrast, every infinite computation ξ : Q, true = γ 0 -→ γ 1 -→ . . . is fair and Result(ξ) = (x = ∞ ∧ y = ∞). Nevertheless, under our fair observations, P and Q are indistinguishable, i.e., O(P ) = O(Q). ⊓ ⊔

Saturated Bisimilarity for ccp

We introduce a notion of bisimilarity in terms of (unlabelled) reductions and barbs and we prove that this equivalence is fully abstract w.r.t. observational equivalence.

Saturated Barbed Bisimilarity

Barbed equivalences have been introduced in [START_REF] Milner | Barbed bisimulation[END_REF] for CCS, and have become the standard behavioural equivalences for formalisms equipped with unlabeled reduction semantics. Intuitively, barbs are basic observations (predicates) on the states of a system.

The choice of the "right" barbs is a crucial step in the barbed approach, and it is usually not a trivial task. For example, in synchronous languages like CCS or π-calculus both the inputs and the outputs are considered as barbs, (see e.g. [START_REF] Milner | Barbed bisimulation[END_REF][START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF]), while in the asynchronous variants only the outputs (see e.g. [START_REF] Amadio | On bisimulations for the asynchronous picalculus[END_REF]). Even several works (e.g. [START_REF] Rathke | Semantic barbs and biorthogonality[END_REF][START_REF] Honda | On reduction-based process semantics[END_REF]) have proposed abstract criteria for defining "good" barbs.

We shall take as barbs all the finite constraints in Con 0 . This choice allows us to introduce a barbed equivalence (Def. 7) that coincides with the standard observational equivalence (Def. 4). It is worth to note that in ∼ o , the observables are all the constraints in Con and not just the finite ones.

We say that γ = P, d satisfies the barb c, written γ ↓ c , iff c ⊑ d; γ weakly satisfies the barb c, written γ ⇓ c , iff γ -→ * γ ′ and γ ′ ↓ c . 1Definition 5. (Barbed bisimilarity) A barbed bisimulation is a symmetric relation R on configurations such that whenever (γ 1 , γ 2 ) ∈ R:

(i) if γ 1 ↓ c then γ 2 ↓ c , (ii) if γ 1 -→ γ ′ 1 then there exists γ ′ 2 such that γ 2 -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are barbed bisimilar, written γ 1 ∼b γ 2 , if there exists a barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R. We write P ∼b Q iff P, true ∼b Q, true .

Congruence characterization. One can verify that ∼b is an equivalence. However, it is not a congruence; i.e., it is not preserved under arbitrary contexts. A context C is a term with a hole ⊓ ⊔

An elegant solution to modify bisimilarity for obtaining a congruence has been introduced in [START_REF] Montanari | Dynamic congruence vs. progressing bisimulation for ccs[END_REF] for the case of weak bisimilarity in CCS. This work has inspired the introduction of saturated bisimilarity [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF] (and its extension to the barbed approach [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]). The basic idea is simple: saturated bisimulations are closed w.r.t. all the possible contexts of the language. In the case of ccp, it is enough to require that bisimulations are upward closed as in condition (iii) below.

Definition 6. (Saturated barbed bisimilarity). A saturated barbed bisimulation is a symmetric relation R on configurations such that whenever

(γ 1 , γ 2 ) ∈ R with γ 1 = P, d and γ 2 = Q, e : (i) if γ 1 ↓ c then γ 2 ↓ c , (ii) if γ 1 -→ γ ′ 1 then there exists γ ′ 2 such that γ 2 -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R, (iii) for every a ∈ Con 0 , ( P, d ⊔ a , Q, e ⊔ a ) ∈ R.
We say that γ 1 and γ 2 are saturated barbed bisimilar, written γ 1 ∼sb γ 2 , if there exists a saturated barbed bisimulation R s.t. (γ 1 , γ 2 ) ∈ R. We write P ∼sb Q iff P, true ∼sb Q, true . Since ∼sb is itself a saturated barbed bisimulation, it is obvious that it is upward closed. This fact also guarantees that it is a congruence w.r.t. all the contexts of ccp: a context C can modify the behaviour of a configuration γ only by adding constraints to its store. The same holds for ≈sb .

Correspondence with Observational Equivalence

We now show that ≈sb coincides with the observational equivalence ∼ o . From [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] it follows that ≈sb coincides with the standard denotational semantics for ccp.

First, we recall some basic facts from domain theory central to our proof. Two (possibly infinite) chains

d 0 ⊑ d 1 ⊑ • • • ⊑ d n ⊑ . . . and e 0 ⊑ e 1 ⊑ • • • ⊑ e n ⊑ .
. . are said to be cofinal if for all d i there exists an e j such that d i ⊑ e j and, viceversa, for all e i there exists a d j such that e i ⊑ d j . In the proof, we will show that the stores of any pairs of fair computations of equivalent processes form pairs of cofinal chains. First, the following result relates weak barbs and fair computations. Proof. If P 0 , d 0 ⇓ c , then P 0 , d 0 -→ * P ′ , d ′ with c ⊑ d ′ (by definition of barb). If P ′ , d ′ belongs to the above computation (i.e., there exists an i such that P i = P ′ and d i = d ′ ) then the result follows immediately. If P ′ , d ′ does not belong to the computation, it holds that there exists P i , d i (in the computation above) such that P ′ , d ′ -→ * P i , d i , because (summation-free) ccp is confluent and the computation is fair. Since the store is preserved, d ′ ⊑ d i and then c ⊑ d i .

Lemma 2. Let d 0 ⊑ d 1 ⊑ • • • ⊑ d n ⊑ . . .
⊓ ⊔ Theorem 2. P ∼ o Q if and only if P ≈sb Q.

Proof. The proof proceeds as follows:

-From ≈sb to ∼ o . Suppose that P, true ≈sb Q, true and take a finite input b ∈ Con 0 . Let -From ∼ o to ≈sb . Suppose that P ∼ o Q. We first show that for all b ∈ Con 0 , P, b and Q, b satisfy the same weak barbs. Let

P, b -→ P 0 , d 0 -→ P 1 , d 1 -→ . . . -→ P n , d n -→ . . . Q, b -→ Q 0 , e 0 -→ Q 1 , e 1 -→ . . . -→ Q n , e n -→ . . .
P, b -→ P 0 , d 0 -→ P 1 , d 1 -→ . . . -→ P n , d n -→ . . . Q, b -→ Q 0 , e 0 -→ Q 1 , e 1 -→ . . . -→ Q n ,
R = {(γ 1 , γ 2 ) | ∃b s.t. P, b -→ * γ 1 , Q, b -→ * γ 2 }
is a weak saturated barbed bisimulation (Def. 7). Take (γ 1 , γ 2 ) ∈ R.

If γ 1 ⇓ c then P, b ⇓ c and, by the above observation,

Q, b ⇓ c . Since ccp is confluent, also γ 2 ⇓ c . The fact that R is closed under -→ * is evident from the definition of R. While for proving that R is upward-closed take γ 1 = P ′ , d ′ and γ 2 = Q ′ , e ′ . It is easy to see that for all a ∈ Con 0 , P, b ⊔ a -→ * P ′ , d ′ ⊔ a and Q, b ⊔ a -→ * Q ′ , e ′ ⊔ a . Thus, by definition of R, ( P ′ , d ′ ⊔ a , Q ′ , e ′ ⊔ a ) ∈ R. ⊓ ⊔

Labeled Semantics

Although ∼sb is fully abstract, it is at some extent unsatisfactory because of the upwardclosure (namely, the quantification over all possible a ∈ Con 0 in condition (iii)) of Def. 6. We shall deal with this by refining the notion of transition by adding to it a label that carries additional information about the constraints that cause the reduction.

Labelled Transitions. Intuitively, we will use transitions of the form

P, d α -→ P ′ , d ′
where label α represents a minimal information (from the environment) that needs to be added to the store d to evolve from P, d into P ′ , d ′ , i.e., P, d ⊔ α -→ P ′ , d ′ . From a more abstract perspective, our labeled semantic accords with the proposal of [START_REF] Sewell | From rewrite to bisimulation congruences[END_REF][START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF] of looking at "labels as the minimal contexts allowing a reduction". In our setting we take as contexts only the constraints that can be added to the store.

The Rules. The labelled transition -→ ⊆ Conf × Con 0 × Conf is defined by the rules in Table 3. We shall only explain rules LR2 and LR4 as the other rules are easily seen to realize the above intuition and follow closely the corresponding ones in Table 1.

The rule LR2 says that ask (c) → P, d can evolve to P, d⊔α if the environment provides a minimal constraint α that added to the store d entails c, i.e., α ∈ min{a

∈ LR1 tell(c), d true -→ stop, d ⊔ c LR2 α ∈ min{a ∈ Con0 | c ⊑ d ⊔ a } ask (c) → P, d α -→ P, d ⊔ α LR3 P, d α -→ P ′ , d ′ P Q, d α -→ P ′ Q, d ′ LR4 P, e ⊔ d[z/x] α -→ P ′ , α ⊔ e ′ ⊔ d[z/x] ∃ e x P, d α[x/z] -→ ∃ e ′ x P ′ , α[x/z] ⊔ (∃xe ′ ) ⊔ d with x ∈ fv (α), z ∈ fv (P ) ∪ fv (e ⊔ d) LR5 P [z/x], d α -→ γ ′ p(z), d α -→ γ ′
where p(x) def = P is a process definition in D Table 2. Labelled Transitions. (The symmetric Rule for LR3 is omitted)

Con 0 | c ⊑ d ⊔ a }.
Note the assuming (Con, ⊑) to be well-founded (Sec. 1.1) is necessary to guarantee that α exists whenever {a ∈ Con 0 | c ⊑ d ⊔ a } is not empty.

To give an intuition about LR4, it may be convenient to first explain why a naive adaptation of the analogous reduction rule R4 in Table 1 would not work. One may be tempted to define the rule for the local case, by analogy to the labelled local rules in other process calculi (e.g., the π-calculus) and R4, as follows:

(*) P, e ⊔ ∃ x d α -→ Q, e ′ ⊔ ∃ x d ∃ e x P, d α -→ ∃ e ′ x Q, d ⊔ ∃ x e ′
where x ∈ fv(α) This rule however is not "complete" (in the sense of Lemma 5 above) as it does not derive all the transitions we wish to have. Note that α = x > 1 is a minimal constraint that added to d enables a reduction from P . In Ex. 3 we obtained the transition:

P, d ⊔ α -→ ∃ x<1 x Q, d ⊔ α ⊔ ∃ x (x < 1)
Thus, we would like to have a transition from P, d labelled with α. But such a transition cannot be derived with Rule (*) above since x ∈ fv(α).

⊓ ⊔ Now, besides the side condition, another related problem with Rule (*) arises from the existential quantification ∃ x d in the antecedent transition P, e ⊔ ∃ x d α -→ Q, e ′ ⊔ ∃ x d . This quantification hides the effect of d on x and thus is not possible to identify the x in α with the x in d. The information from the environment α needs to be added to the global store d, hence the occurrences of x in both d and α must be identified. Notice that dropping the existential quantification of x in d in the antecedent transition does identify the occurrences of x in d with those in α but also with those in the local store e thus possibly generating variable clashes.

The rule LR4 in Table 2 solves the above-mentioned issues by using in the antecedent derivation a fresh variable z that acts as a substitute for the free occurrences of x in d and α. (Recall that c[z/x] represents c with x replaced with z). This way we identify with z the free occurrences of x in d and α and avoid clashes with those in e. E.g., for the process defined in the Ex.6, using LR4 (and LR2) one can derive

ask (y > 1) → Q, x < 1 ⊔ y > z z>1 -→ Q, x < 1 ⊔ y > z ⊔ z > 1 ∃ x<1 x (ask (y > 1) → Q), y > x x>1 -→ ∃ x<1 x Q, ∃ x (x < 1) ⊔ y > x ⊔ x > 1
The labeled semantics is sound and complete w.r.t. the unlabeled one. Soundness states that P, d α -→ P ′ , d ′ corresponds to our intuition that if α is added to d, P can reach P ′ , d ′ . Completeness states that if we add a to (the store in) P, d and reduce to P ′ , d ′ , it exists a minimal information α ⊑ a such that P, d

Strong and Weak Bisimilarity

Having defined our labelled transitions for ccp, we now proceed to define an equivalence that characterizes ∼sb without the upward closure condition.

When defining bisimilarity over a labeled transition system, barbs are not usually needed because they can be somehow inferred by the labels of the transitions. For example in CCS, P ↓ a iff P a -→. The case off ccp is different: barbs cannot be removed from the definition of bisimilarity because they cannot be inferred by the transitions. In order to remove barbs from ccp, we could have inserted labels showing the store of processes (as in [START_REF] Saraswat | Concurrent constraint programming[END_REF]) but this would have betrayed the philosophy of "labels as minimal contexts". Then, we have to define bisimilarity as follows.

Definition 8. (Syntactic bisimilarity). A syntactic bisimulation is a symmetric relation

R on configurations such that whenever (γ 1 , γ 2 ) ∈ R:

(i) if γ 1 ↓ c then γ 2 ↓ c , (ii) if γ 1 α -→ γ ′ 1 then ∃γ ′ 2 such that γ 2 α -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are syntactically bisimilar, written γ 1 ∼ S γ 2 , if there exists a syntactic bisimulation R such that (γ 1 , γ 2 ) ∈ R. We called the above bisimilarity "syntactic", because it does not take into account the "real meaning" of the labels. This equivalence coincides with the one in [START_REF] Saraswat | Concurrent constraint programming[END_REF] (apart from the fact that in the latter, barbs are implicitly observed by the transitions) and, from a more general point of view can be seen as an instance of bisimilarity in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF]. In [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF], it is argued that the equivalence in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF] is often over-discriminating. This is also the case of ccp, as illustrated by the following example.

Example 7. Let P = ask (x < 10) → tell(y = 0) and Q = ask (x < 5) → tell(y = 0). The configurations γ 1 = P Q, true and γ 2 = P P, true are not equivalent according to ∼ S . Indeed

γ 1 x<10 -→ γ ′ 1 x<5 -→ γ ′′ 1 , while γ 2 after performing γ 2 x<10 -→ γ ′ 2 can only perform γ ′ 2 true -→ γ ′′ 2 . However γ 1 ∼sb γ 2 . ⊓ ⊔
To obtain coarser equivalence (coinciding with ∼sb ), we define the following.

Definition 9. (Strong bisimilarity).

A strong bisimulation is a symmetric relation R on configurations such that whenever (γ 1 , γ 2 ) ∈ R with γ 1 = P, d and γ 2 = Q, e :

(i) if γ 1 ↓ c then γ 2 ↓ c , (ii) if γ 1 α -→ γ ′ 1 then ∃γ ′ 2 s.t. Q, e ⊔ α -→ γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are strongly bisimilar, written γ 1 ∼ γ 2 , if there exists a strong bisimulation R such that (γ 1 , γ 2 ) ∈ R.

To give some intuition about the above definition, let us recall that in P, d α -→ γ ′ the label α represents minimal information from the environment that needs to be added to the store d to evolve from P, d into γ ′ . We do not require the transitions from Q, e to match α. Instead (ii) requires something weaker: If α is added to the store e, it should be possible to reduce into some γ ′′ that it is in bisimulation with γ ′ . This condition is weaker because α may not be a minimal information allowing a transition from Q, e into a γ ′′ in the bisimulation, as shown in the previous example.

Definition 10. (Weak bisimilarity). A weak bisimulation is a symmetric relation R on configurations such that whenever

(γ 1 , γ 2 ) ∈ R with γ 1 = P, d and γ 2 = Q, e : (i) if γ 1 ↓ c then γ 2 ⇓ c , (ii) if γ 1 α -→ γ ′ 1 then ∃γ ′ 2 s.t. Q, e ⊔ α -→ * γ ′ 2 and (γ ′ 1 , γ ′ 2 ) ∈ R.
We say that γ 1 and γ 2 are weakly bisimilar, written γ 1 ≈ γ 2 , if there exists a weak bisimulation R such that (γ 1 , γ 2 ) ∈ R.

R = {(γ 2 , γ 1 ), (γ 2 , stop, true ), ( tell(d), c , stop, c ), ( stop, c , stop, c )} ⊓ ⊔
The following theorem states that strong and weak bisimilarity coincide, resp., with ∼sb and ≈sb . Hence γ 1 and γ 2 in the above example are also in ≈sb (and, by Thm 2, also in ∼ o ). It is worth noticing that any saturated barbed bisimulation (Def. 7) relating γ 1 and γ 2 is infinite in dimension, since it has to relate tell(true), a and ask(c) → tell(d), a for all constraints a ∈ Con 0 . Instead, the relation R above is finite and it represents (by virtue of the following theorem) a proof also for γ 1 ≈sb γ 2 . Theorem 3. ∼sb = ∼ and ≈sb = ≈. This is proved in Appendixes A.3 and A.4.

Conclusions, Related and Future Work

In this paper we introduced labeled semantics and bisimilarity for ccp. Our equivalence characterizes the observational semantics introduced in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] based on limits of infinite computations, by means of a co-inductive definition. It follows from [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] that our bisimilarity coincides with the equivalence induced by the standard closure operators semantics of ccp. Therefore, our weak bisimulation approach represents a novel sound and complete proof technique for observational equivalence in ccp.

Our work is also interesting for the research programme on "labels derivation". Our labeled semantics can be regarded as an instance of the one introduced at an abstract level in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF]. Syntactical bisimulation (Def. 8) as an instance of the one in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF], while strong and weak bisimulations (Def. 9 and Def. 10) as instances of those in [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]. Furthermore, syntactical bisimulation intuitively coincides with the one in [START_REF] Saraswat | Concurrent constraint programming[END_REF], while saturated barbed bisimulation (Def. 6) with the one in [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF]. Recall that syntactical bisimilarity is too fine grained, while saturated barbed bisimulation requires the relation to be upward closed (and thus, infinite in dimension). Our weak bisimulation instead is fully abstract and avoid the upward closure. Summarizing, the framework in [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF] provides us an abstract approach for deriving a novel interesting notion of bisimulation.

We chose not to employ the categorical machinery of [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF], for two raisons. First, the use of category theory would have restricted the audience of the paper. Second, the techniques in [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF] would have derived a transition system not defined in a SOS style.

It is worth noticing that the restriction to the summation-free fragment is only needed for proving the coincidence with [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. The theorem in Section 2.1 still holds in the presence of summation. Analogously, we could extend all the definitions to infinite constraints without invalidating these theorems.

Some recent works [START_REF] Buscemi | Open bisimulation for the concurrent constraint picalculus[END_REF][START_REF] Johansson | A fully abstract symbolic semantics for psi-calculi[END_REF][START_REF] Johansson | Weak equivalences in psi-calculi[END_REF] have defined bisimilarity for novel languages featuring the interaction paradigms of both ccp and the π-calculus. In these works, bisimilarity is defined starting from transition systems whose labels represent communications in the style of the π-calculus. Instead we employ barbs on a purely unlabeled semantics. Preliminary attempts have shown that defining a correspondence with our semantics is not trivial. We left this for an extended version of the paper.

As shown e.g. in [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF] there are strong connections between ccp processes and logic formulae. As future work we would like to investigate whether our present results can be adapted to provide a novel characterization of logic equivalence in terms of bisimilarity. Preliminary results show that at least the propositional fragment, without negation, can be characterized in terms of bisimilarity.

A.3 Proof of the strong case

In Section 2.1 we introduced ∼sb and its weak variant ≈sb . By relying on labeled transitions, in Section 2 we introduced ∼ and ≈. This technical Appendix is devoted to show that ∼sb = ∼ and ≈sb = ≈.

For technical reasons we shall use an equivalent formulation of Rule R4.

= ∃ e x Q, P ′ = ∃ e ′ x Q ′ , α = α ′ [x/z] and d ′ = d ⊔ (∃ x e ′ ) ⊔ α ′ [x/z] with Q, e ⊔ d[z/x] α ′ -→ Q ′ , e ′ ⊔ d[z/x] ⊔ α ′ by a shorter inference. By appeal to induction then Q, e ⊔ d[z/x] ⊔ α ′ -→ Q ′ , e ′ ⊔ d[z/x] ⊔ α ′ . Note that α ′ = (α ′ [x/z])[z/x] = α[z/x]. Thus, the previous transition is equivalent to Q, e ⊔ (d ⊔ α)[z/x] -→ Q ′ , e ′ ⊔ (d ⊔ α)[z/x] . Using this reduction, the transition ∃ e x Q, d ⊔ α -→ ∃ e ′ x Q ′ , d ⊔ (∃ x e ′ ) ⊔
′ = d ⊔ a = d ⊔ α ⊔ b = d ′′ ⊔ b. -Using the rule R4'. Then P = ∃ e x Q, P ′ = ∃ e ′ x Q ′ , and d ′ = d⊔a⊔∃ x e ′ with Q, e⊔ (d⊔a)[z/x] -→ Q ′ , e ′ ⊔(d⊔a)[z/x] where z ∈ fv (Q)∪fv (e)∪fv (d)∪fv (a), by a shorter inference. This transition is equivalent to Q, (e ⊔ d[z/x]) ⊔ a[z/x] -→ Q ′ , (e ′ ⊔ d[z/x]) ⊔ a[z/x]
. By induction hypothesis, we have that there exist α and b such that

Q, e ⊔ d[z/x] α -→ Q ′ , d ′′ 1 with a[z/x] = α ⊔ b and e ′ ⊔ d[z/x] ⊔ a[z/x] = d ′′ 1 ⊔ b.

Note that the active process generating this transition could be either an ask or a tell. If it is generated by an ask then

d ′′ 1 = d[z/x] ⊔ e ⊔ α.
∃ e x Q, d α[x/z] -→ ∃ e ′ x Q ′ , d ⊔ ∃ x e ′ ⊔ α[x/z] . From a[z/x] = α ⊔ b, we have that (a[z/x])[x/z] = (α ⊔ b)[x/z] that is a = α[x/z] ⊔ b[x/z]. Now, take d ′′ = d ⊔ ∃ x e ′ ⊔ α[x/z]. We have that d ′′ ⊔ b[x/z] = d ⊔ ∃ x e ′ ⊔ α[x/z] ⊔ b[x/z] that, by the previous equivalence is equal to d ⊔ ∃ x e ′ ⊔ a, that is d ′ . ⊓ ⊔
Note that Lemma 1 is needed for the above proof in the case of rule R2. This actually the reason why in Sec. 1.1 we have assumed (Con, ⊑) to be well-founded.

( P ′ , d ′′ ⊔ b ′ , Q ′ , e ′′ ⊔ b ′ ) ∈ R and, by (2), P ′ , d ′′ ⊔ b ′ = P ′ , d ′ . ⊓ ⊔
We have all the results to prove that ∼sb = ∼. We split the two directions of the proof in two lemmas.

Lemma 7. ∼ ⊆ ∼sb Proof. Let R = {( P, d , Q, e ) s.t P, d ∼ Q, e }.
We show that R is a saturated barbed bisimulation. We take ( P, d , Q, e ) ∈ R and we prove that they satisfy the three conditions of Definition 6. In order to prove that ≈ = ≈sb , we essentially use the same proof-scheme of the strong case ( ∼ = ∼sb ). The main difference concerns two technical lemmata (namely Lemma 9 and Lemma 11) stating that weak barbs are preserved by the addition of constraints to the store (this was trivial for the strong case). We have now all the ingredients to prove that ≈ = ≈sb .

  ξ 1 and ξ 2 are fair, then Result(ξ 1 ) = Result(ξ 2 ). This allows us to set Result(γ) def = Result(ξ) for any fair computation ξ of γ. Definition 4. (Observational equivalence) Let O : Proc → Con 0 → Con be given by O(P )(d) = Result( P, d ). We say that P and Q are observational equivalent, written P

Example 5 .

 5 [-] s.t., replacing it with a process P yields a process term C[P ]. E.g., C = tell(c) [-] and C[tell(d)] = tell(c) tell(d). Let us consider the context C = tell(a) [-] and the processes P = ask (b) → tell(d) and Q = ask (c) → tell(d) with a, b, c, d = true, b ⊑ a and c ⊑ a. We have P, true ∼b Q, true because both configurations cannot move and they only satisfy the barb true. But C[P ], true ∼b C[Q], true , because the former can perform three transitions (in sequence), while the latter only one.

Definition 7 .

 7 (Weak saturated barbed bisimilarity). Weak saturated barbed bisimilarity ( ≈sb ) is obtained from Def. 6 by replacing -→ with -→ * and ↓ c with ⇓ c .

  and e 0 ⊑ e 1 ⊑ • • • ⊑ e n ⊑ . . . be two chains.[START_REF] Abramsky | Domain theory[END_REF] If they are cofinal, then they have the same limit, i.e., d i = e i . (2) If the elements of the chains are finite and d i = e i , then the two chains are cofinal.

Lemma 3 .

 3 Let P 0 , d 0 -→ P 1 , d 1 -→ . . . -→ P n , d n -→ .. . be a (possibly infinite) fair computation. If P 0 , d 0 ⇓ c then there exist a store d i (in the above computation) such that c ⊑ d i .

  be two fair computations. Since ≈sb is upward closed, P, b ≈sb Q, b and thus, for all d i , Q, b ⇓ di . By Lemma 3, it follows that there exists an e j (in the above computation) such that d i ⊑ e j . Analogously, for all e i there exists a d j such that e i ⊑ d j . Then the two chains are cofinal and by Lemma 2.1, it holds that d i = e i , that means O(P )(b) = O(Q)(b).

Example 6 .

 6 Let P as in Ex. 3, i.e., P = ∃ x<1 x (ask (y > 1) → Q) and d = y > x.

  α -→ P ′ , d ′′ with d ′′ ⊑ d ′ . The following lemmata are proved in Appendix A.3. Lemma 4. (Soundness). If P, d α -→ P ′ , d ′ then P, d ⊔ α -→ P ′ , d ′ . Lemma 5. (Completeness). If P, d⊔a -→ P ′ , d ′ then ∃α, b s.t. P, d α -→ P ′ , d ′′ and α ⊔ b = a, d ′′ ⊔ b = d ′ . Corollary 1. P, d true -→ P ′ , d ′ if and only if P, d -→ P ′ , d ′ .

Example 8 .

 8 We can show that tell(true) ≈ ask(c) → tell(d) when d ⊑ c. Intuitively, this corresponds to the fact that the implication c ⇒ d is equivalent to true when c entails d. Let us take γ 1 = tell(true), true and γ 2 = ask(c) → tell(d), true . Their labeled transition systems are the following: γ 1 true -→ stop, true and γ 2 c -→ tell(d), c true -→ stop, c . It is now easy to see that the symmetric closure of the relation R given below is a weak bisimulation.

  R4' P, e ⊔ d[z/x] -→ P ′ , e ′ ⊔ d[z/x] ∃ e x P, d -→ ∃ e ′ x P ′ , d ⊔ ∃ x e ′ with z ∈ fv (P ) ∪ fv (e) ∪ fv (d) Lemma 4. (Soundness). If P, d α -→ P ′ , d ′ then P, d ⊔ α -→ P ′ , d ′ . Proof. By induction on (the depth) of the inference of P, d α -→ P ′ , d ′ . Here we confine ourselves to considering two cases, the others are similar or easier to verify. -Using LR2 then P = ask (c) → P ′ , α ∈ min{a | c ⊑ d ⊔ a} and d ′ = d ⊔ α. Now the transition P, d ⊔ α -→ P ′ , d ⊔ α = P ′ , d ′ follows from the fact that c ⊑ d ⊔ α and by applying Rule R2. -Using LR4 then P

Lemma 5 .

 5 α follows from rule R4'. Hence P, d ⊔ α -→ P ′ , d ′ . ⊓ ⊔ (Completeness). If P, d⊔a -→ P ′ , d ′ then ∃α, b s.t. P, d α -→ P ′ , d ′′ and α ⊔ b = a, d ′′ ⊔ b = d ′ . Proof. The proof proceeds by induction on (the depth) of the inference of P, d⊔a -→ P ′ , d ′ . Here we show only two cases, the rest are similar or easier to verify. -Using the rule R2. Then P = ask (c) → P ′ , d ′ = d ⊔ a and c ⊑ d ⊔ a. Note that a ∈ {a ′ ∈ Con 0 |c ⊑ d ⊔ a ′ } and then, by Lemma 1, there exists α ∈ min{a ′ ∈ Con 0 |c ⊑ d ⊔ a ′ } such that α ⊑ a. By rule LR2, P, d α -→ P ′ , d ⊔ α . Let d ′′ = d ⊔ α and take b = a. We have that a = α ⊔ b and that d

Lemma 6 .

 6 If P, d ∼ Q, e , then ∀a ∈ Con 0 , P, d ⊔ a ∼ Q, e ⊔ a . Proof. Let R = {( P, d ⊔ a , Q, e ⊔ a ) s.t. P, d ∼ Q, e }. We show that R is a strong bisimulation. We take ( P, d ⊔ a , Q, e ⊔ a ) ∈ R and we prove that they satisfy conditions (i) and (ii) of Definition 9. (i) By hypothesis P, d ∼ Q, e . Since P, d ↓ d then Q, e ↓ d , that is, d ⊑ e. For the same reason, d ⊑ e and thus d = e. So, trivially, P, d ⊔ a and Q, e ⊔ a satisfy the same barbs. (ii) Suppose that P, d ⊔ a α -→ P ′ , d ′ . We need to prove that there exist Q ′ and e ′ such that Q, e ⊔ a ⊔ α -→ Q ′ , e ′ and ( P ′ , d ′ , Q ′ , e ′ ) ∈ R. By Lemma 4, we have that P, d ⊔ a ⊔ α -→ P ′ , d ′ . From this, we can obtain a labelled transition of P, d by using Lemma 5: P, d α ′ -→ P ′ , d ′′ and there exists b ′ such that (1) α ′ ⊔ b ′ = a ⊔ α and (2) d ′′ ⊔ b ′ = d ′ . From the labelled transition of P, d and the hypothesis P, d ∼ Q, e , we have that Q, e ⊔ α ′ -→ Q ′ , e ′′ (matching the transition) with P ′ , d ′′ ∼ Q, e ′′ (3). Note that by (1) Q, e ⊔ a ⊔ α = Q, e ⊔ α ′ ⊔ b ′ and that Q, e ⊔ α ′ ⊔ b ′ -→ Q, e ′′ ⊔ b ′ , by monotonicity of the store. Finally, by the definition of R and (3) we can conclude that

  (i) Suppose P, d ↓ c . Since P, d ∼ Q, e then Q, e ↓ c . (ii) Suppose that P, d -→ P ′ , d ′ . By Corollary 1 P, d true-→ P ′ , d ′ . Since P, d ∼ Q, e then Q, e ⊔ true -→ Q ′ , e ′ with P ′ , d ′ ∼ Q ′ , e ′ . Since e = e ⊔ true we have Q, e -→ Q ′ , e ′ and ( P ′ , d ′ , Q ′ , e ′ ) ∈ R.(iii) By P, d ∼ Q, e and Lemma 6, we have that ∀a ∈ Con 0 , (P, d ⊔ c ′ , Q, e ⊔ c ′ ) ∈ R. ⊓ ⊔ Lemma 8. ∼sb ⊆ ∼ Proof. Let R = {( P, d , Q, e ) s.t. P, d ∼sb Q, e }.We show that R is a strong bisimulation. We take ( P, d , Q, e ) ∈ R and we prove that they satisfy the two conditions of Definition 9. (i) Suppose P, d ↓ c . Since P, d ∼sb Q, e then Q, e ↓ c . (ii) Suppose that P, d α -→ P ′ , d ′ . Then by Lemma 4 P, d ⊔ α -→ P ′ , d ′ . Since P, d ∼sb Q, e then Q, e ⊔ α -→ Q ′ , e ′ with P ′ , d ′ ∼sb Q ′ , e ′ . Then ( P ′ , d ′ , Q ′ , e ′ ) ∈ R. ⊓ ⊔ Theorem 4 (Theorem 3 in the Strong Case). ∼sb = ∼ A.4 Proof of the weak case

Lemma 9 .-→ P 1 , d ′ 1 and d ′ 1 ⊔

 9111 Given P, d and Q, e such that P, d ≈ Q, e , if P, d ⊔ a ↓ c then Q, e ⊔ a ⇓ c . Proof. If P, d⊔a ↓ c , then c ⊑ d⊔a. Since P, d ≈ Q, e , then there exists a Q ′ , e ′ such that Q, e -→ * Q ′ , e ′ and d ⊑ e ′ . Moreover Q, e ⊔ a -→ * Q ′ , e ′ ⊔ a , because all reductions are preserved by the addition of constraints. Finally c ⊑ d ⊔ a ⊑ e ′ ⊔ a, that means Q ′ , e ′ ⊔ a ↓ c , i.e., Q, e ⊔ a ⇓ c .With the above lemma, we can use the same technique of Lemma 6 to prove that ≈ is a congruence.Lemma 10. If P, d ≈ Q, e then ∀a ∈ Con 0 , P, d ⊔ a ≈ Q, e ⊔ a .Proof. We take the relationR = {( P, d ⊔ c ′ , Q, e ⊔ c ′ ) s.t. P, d ≈ Q, e } and we prove that it is a weak bisimulation. (i) Suppose P, d ⊔ a ↓ c . Since P, d ≈ Q, e , by Lemma 9, then Q, e ⊔ a ⇓ c . (ii) Suppose P, d ⊔ a α -→ P ′ , d ′ . By Lemma 4 P, d ⊔ a ⊔ α -→ P ′ , d ′ . By Lemma 5 P, d β -→ P ′ , d ′′ and exists b such that β ⊔ b = a ⊔ α and d ′′ ⊔ b = d ′ . Since P, d ≈ Q, e , then Q, e ⊔ β -→ * Q ′ , e ′′ with P ′ , d ′′ ≈ Q ′ , e ′′ .Note that all reductions are preserved when adding constraints to the store, therefore fromQ, e ⊔ β -→ * Q ′ , e ′′ we can derive that Q, e ⊔ β ⊔ b -→ * Q ′ , e ′′ ⊔b . This means that Q, e⊔a⊔α -→ * Q ′ , e ′′ ⊔b . Now we have P ′ , d ′ = P ′ , d ′′ ⊔ b and ( P ′ , d ′′ ⊔ b , Q ′ , e ′′ ⊔ b ) ∈ R, because P ′ , d ′′ ≈ Q ′ , e ′′ .The following lemma extends Lemma 9 to the case of weak barbs. Lemma 11. Given P, d and Q, e such that P, d ≈ Q, e , if P, d ⊔ a ⇓ c then Q, e ⊔ a ⇓ c . Proof. If P, d ⊔ a ⇓ c , then there are two possibilities: (i) P, d ⊔ a ↓ c . The result follows by Lemma 9. (ii) P, d ⊔ a ↓ c and P, d ⊔ a -→ P 1 , d 1 -→ * P n , d n ↓ c . From P, d ⊔ a -→ P 1 , d 1 and by Lemma 5 we have a = β ⊔ b such that P, dβ b = d 1 . Since P, d ≈ Q, e , then Q, e ⊔ β -→ * Q 1 , e ′ 1 with P 1 , d ′ 1 ≈ Q 1 , e ′ 1 . By Lemma 10, P 1 , d 1 = P 1 , d ′ 1 ⊔ b ≈ Q 1 , e ′ 1 ⊔ b and thus Q 1 , e ′ 1 ⊔ b -→ * Q n , e n ↓ c. By putting all our pieces together, we have Q, e⊔a = Q, e⊔β ⊔b -→ * Q 1 , e ′ 1 ⊔b -→ * Q n , e n ↓ c , i.e., Q, e⊔a ⇓ c .

Lemma 12 .

 12 If P, d ≈ Q, e , then P, d ≈sb Q, e . Proof. We take the relation S = {( P, d , Q, e ) | P, d ≈ Q, e } and we prove that S is a weak saturated barbed bisimulation (Definition 7). (i) Suppose P, d ⇓ c . Since P, d ≈ Q, e then, by Lemma 11, Q, e ⇓ c . (ii) Suppose P, d -→ * P ′ , d ′ . By definition of -→ * , there exist P 1 , d 1 , P 2 , d 2 , . . . , P n , d n such thatP, d -→ P 1 , d 1 -→ P 2 , d 2 -→ . . . -→ P n , d n -→ P ′ , d ′ n , d n true -→ P ′ , d ′ . Now, since P, d ≈ Q, e , then Q, e = Q, e ⊔ true -→ * Q 1 , e 1 and P 1 , d 1 ≈ Q 1 , e 1 .By iterating this reasoning one have thatQ, e -→ * Q 1 , e 1 -→ * Q 2 , e 2 -→ * . . . -→ * Q n , e n -→ * Q ′ , e ′ with P ′ , d ′ ≈ Q ′ , e ′ . Summarizing Q, e -→ * Q ′ ,e ′ and ( P ′ , d ′ , Q ′ , e ′ ) ∈ S. (iii) ∀a ∈ Con 0 ( P, d ⊔ a , Q, e ⊔ a ) ∈ S, by Lemma 10. Lemma 13. If P, d ≈sb Q, e then P, d ≈ Q, e . Proof. We take the relation R = {( Q, e , Q, e ) s.t. Q, e ≈sb Q, e } and we prove that it is a weak bisimulation (Definiton 10). (i) Suppose P, d ↓ c . Then P, d ⇓ c . Since P, d ≈sb Q, e , then Q, e ⇓ c . (ii) Suppose that P, d α -→ P ′ , d ′ . By Lemma 4 P, d ⊔ α -→ P ′ , d ′ . By Definition of -→ * , we can say that P, d ⊔ α -→ * P ′ , d ′ . Since P, d ≈sb Q, e we have Q, e ⊔ α -→ * Q ′ , e ′ with P ′ , d ′ ≈sb Q ′ , e ′ . Theorem 5 (Theorem 3 in the Weak Case). ≈sb = ≈

  e n -→ . . . be two (possibly infinite) fair computations. Since P ∼ o Q, then d i = e i . Since all the stores of computations are finite constraints, then by Lemma 2.2, it holds that for all d i there exists an e j such that d i ⊑ e j . Now suppose that P, b ⇓ c . By Lemma 3, it holds that there exists a d i (in the above computation) such that c⊑ d i . Thus c ⊑ d i ⊑ e j that means Q, b ⇓ c .With this observation it is easy to prove that

  If it is generated by a tell, then α = true and d ′′ = d[z/x] ⊔ e ′ ⊔ α. Thus in both cases it is safe to assume that d ′′ 1 = d[z/x] ⊔ e ′ ⊔ α. Now, note that x / ∈ fv (a[z/x]) = fv (α ⊔ b), and thus x / ∈ fv (α) ∪ fv (b). By rule LR4, we have that

As usual, -→ * denotes the reflexive and transitive closure of -→.

R4P, e ⊔ ∃ x d -→ P ′ , e ′ ⊔ ∃ x d ∃ e x P, d -→ ∃ e ′ x P ′ , d ⊔ ∃ x e ′ Intuitively, ∃ ex P behaves like P , except that the variable x possibly present in P must be considered local, and that the information present in e has to be taken into account. It is convenient to distinguish between the external and the internal point of view. From the internal point of view, the variable x possibly occurring in the global store d is hidden.This corresponds to the usual scoping rules: the x in d is global, hence "covered" by the local x. Therefore, P has no access to the information on x in d, and this is achieved by filtering d with ∃ x . Furthermore, P can use the information (which may concern also the local x) that has been produced locally and accumulated in e. In conclusion, if the visible store at the external level is d 2 , then the store that is visible internally by P is e ⊔ ∃ x d. Now, if P is able to make a step, thus reducing to P ′ and transforming the local store into e ′ , what we see from the external point of view is that the process is transformed into ∃ e ′x P ′ , and that the information ∃ x e present in the global store is transformed into ∃ x e ′ .[START_REF] Amadio | On bisimulations for the asynchronous picalculus[END_REF] Operationally ∃ ex P can only derive from a ccp process of the form ∃ x P ′′ , which has produced the local information e while evolving into ∃ ex P . This local information is externally seen as ∃xe, that is, ∃xe ⊑ d

A Appendix

A.1 Cylindric Constraint System Definition 11. A cylindric constraint system over a set of variables Var is a constraint system whose support set Con ⊇ D Var is closed under the cylindric operators ∃ Var and quotiented by Axioms C1 -C4, and whose ordering ⊑ satisfies Axioms C5 -C7 :

where c, c i , d indicate finite constraints, and

The axioms of cylindric constraint systems given above have been proposed in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] following the work of cylindric algebras. They give ∃ x the flavour of an existential quantifier, as the notation suggest. The constraint d xy can be viewed as the equality x = y.

A.2 Description of the Local Rule

Here we shall describe the reduction rule for local processes give in Section 1.3, Table 1. Rule R4 is given as follows:


Véronique Letort
email: letort@mas.ecp.fr

Patrick Heuret

Paul-Camilo Zalamea

Eric Nicolini

Philippe De Reffye

Analysis of Cecropia sciadophylla Morphogenesis Based on a Sink-Source Dynamic Model

Although there is an increasing number of models simulating the functional and structural development of trees at organ scale, few of them can be fully calibrated, evaluated and validated. A major obstacle resides in the intrinsic complexity of trees due to their high stature, large number of organs and long life span that limits the possibilities of experimental work and the access to measurement data. This is why 'model plants' such as the neotropical genus Cecropia are of great interest. This genus has a simple architecture and some qualities that allow collecting exhaustive datasets at the organ scale. In this paper, we evaluate the GreenLab model on data recorded on 11 individuals measured in 2007 in French Guiana. The branching and flowering patterns are analyzed using an index of trophic competition.

Introduction

Trees are characterized by their high stature, by the complexity of their structure and by their long lifespan. These properties drastically increase the experimental work required for analysing trees as a whole. This intrinsic difficulty for collecting adequate data is a major obstacle for model development, parameterization and validation. This is particularly true when ones aims to considerer the growth processes at the organ scale and to account for interactions between plant functioning and structure [START_REF] Sievänen | Components of a functionalstructural tree model[END_REF], [START_REF] Prusinkiewicz | Modelling plant growth and development[END_REF].

In that context, it is of great interest to consider 'model plants' to build and validate tree growth models. The neotropical genus Cecropia Loefl. includes 61 species, distributed from southern Mexico to northern Argentina, with some species occurring in the Antilles. It is the most important genus of pioneer trees in the neotropics; it grows rapidly and ably colonizes gaps [3]. Species of this genus present all the required characteristics for a 'model plant'. It has a continuous growth, immediate branching and flowering, a very simple architecture following the architectural model of Rauh with a pronounced candelabrum-like branching system [START_REF] Hallé | Tropical trees and forests, An architectural analysis[END_REF] and associated to a low complexity for a relatively high lifespan (i.e., some decades). For example, an eleven-yearold measured individual of C. sciadophylla was constituted by approximately 1700 nodes and 400 leaves still alive that is relatively low compared to the majority of trees (see Figure 1). Furthermore, for Cecropia species, the rate of emission of new nodes is remarkably stable among the axes of a tree but also among the trees of a population [START_REF] Heuret | Synchronization of growth, branching and flowering processes in the south american tropical tree Cecropia obtusa (Cecropiaceae)[END_REF], [START_REF] Zalamea | Growth pattern and age determination for Cecropia sciadophylla (Urticaceae)[END_REF]; for example in Cecropia sciadophylla each axis increases by 25 phytomers per year. As the scar of leaves are identifiable during the whole tree life, it gives a temporal reference to retrospectively assess the tree age [START_REF] Zalamea | Growth pattern and age determination for Cecropia sciadophylla (Urticaceae)[END_REF]. Moreover, these species exhibit strong periodic patterns for branching and flowering as well as for the variations of internode length. The origins of these periodic patterns is questionable: among others, can we involve climatic fluctuation or/and dynamic trophic competition during the plant development?

Such question could be investigated using a model that simulates biomass production and allocation in relation with the plant structure, such as for instance the GreenLab model [START_REF] Cournède | Structural factorization of plants to compute their functional and architectural growth[END_REF]. Mathieu et al [START_REF] Mathieu | Rhythms and alternating patterns in plants as emergent properties of a model of interaction between development and functioning[END_REF] have shown that cyclic flowering or branching patterns can be generated as emergent properties in the model. These cyclic patterns are driven by the sourcesink ratio that is calculated by GreenLab and that represents an index of internal trophic competition. A first attempt of parametric identification of the model on adult trees was performed by [START_REF] Letort | Parameter identification of a functionalstructural tree growth model and application to beech trees (Fagus sylvatica)[END_REF] on two beech trees but, while each metamer dimensions were measured on the trunk, on the branches only compartment data were collected. In contrast, a major advantage of Cecropia is that all phytomers of the trees can be exhaustively measured. Therefore, studying this genus offers for the first time (to our knowledge) the opportunity to evaluate the performances of a functionalstructural model using a complete dataset at the organ level.

In this study, we focus on C. sciadophylla that recently was the object of a detailed morphological and architectural study [START_REF] Zalamea | Growth pattern and age determination for Cecropia sciadophylla (Urticaceae)[END_REF]. Its habitat covers the Amazonian basin, the Llanos region in Colombia and Venezuela, and the Guiana shield.

With the objective to simulate the growth of Cecropia sciadophylla at an organ scale and to reproduce the biomass production and allocation at metamer level, the aims of this work are (i) to determine morphological allometries to simplify future measurements, (ii) to evaluate the ability of the GreenLab model to trace back the dynamics of internal trophic competition within the plants and to reproduce their observed varibility, and (iii) to assess whether the index of trophic comptetition can be linked to the appareance of the first tier of branches and inflorescences.

Material and Methods

Study site

Plant material and measurements

In September 2007, 11 individuals were felled and measured, ten at Saint-Elie road and one at Counami Road. All the trees from Saint-Elie population were sterile and only one had branches. The tree from Counami road was pistillate and had branches. For all trees, trunk diameter at breast height (1.30 m) and tree height were measured on the fallen tree (Table 1).

Trees were described node by node as a collection of phytomers following the protocol defined in [START_REF] Heuret | Synchronization of growth, branching and flowering processes in the south american tropical tree Cecropia obtusa (Cecropiaceae)[END_REF]. Tree topology, i.e. the relative position of the different botanical units described (nodes and axes), was recorded following the MTG formalism [START_REF] Godin | A multiscale model of plant topological structures[END_REF] and analysed using the VPlant package, the successor of AMAPmod [START_REF] Godin | Exploring plant topological structure with the amapmod software: an outline[END_REF] now integrated in the OpenAlea platform [START_REF] Pradal | PlantGL : A python-based geometric library for 3d plant modelling at different scales[END_REF]. The age determination of trees and annual growth delimitation were performed following the protocol proposed by [START_REF] Zalamea | Growth pattern and age determination for Cecropia sciadophylla (Urticaceae)[END_REF].

Each phytomer was indexed according to its ontogenetical age as defined by [START_REF] Barthélémy | Plant architecture: a dynamic, multilevel and comprehensive approach to plant form, structure and ontogeny[END_REF] and the following information was recorded: the length of the underlying internode, the diameter in the middle of the internode, and the presence of developed branches, inflorescences and/or leaves at each internode. Each leaf was cut and its petiole was separated from the blade. The blade was weighed and pressed between two plates of Plexiglas and then photographed using a digital camera with a focal length of 50 mm. Blade areas were estimated by analysing the photographies with the ImageJ freeware (http://rsbweb.nih.gov/ij/). The length, the diameter in the middle and the fresh weight of the petioles were recorded. The fresh weight of inflorescence or infructescence were recorded. The plant axes were then cut node by node, 1 cm above the top of the stipule scar. The length of the cut segment (not exactly equal to the internode as there is a 1 cm shift) was recorded as well as its fresh weight and two orthogonal diameters of the pith. Node segments, leaves, and petioles were dried at 103 o C during 72 h and the dry mass was measured. For young individuals (number of phytomers less than around 55), the root system was extracted, washed, dried and weighed.

Model and procedure for its parametric identification

The GreenLab model was used with some adaptations to perform the analysis of source-sink dynamics during Cecropia growth. GreenLab is a functional-structural model based on carbon source-sink relationships within individual plants that are represented as sets of topologically connected phytomers [START_REF] Cournède | Structural factorization of plants to compute their functional and architectural growth[END_REF], [START_REF] Guo | Parameter optimization and field validation of the functional-structural model GreenLab for maize[END_REF], [START_REF] Mathieu | A dynamic model of plant growth with interactions between development and functional mechanisms to study plant structural plasticity related to trophic competition[END_REF]. The model time step corresponds to the time lag between the emission of two successive phytomers, called growth cycle (GC). For Cecropia, all axes are assumed to have the same functioning and set of parameters. Two phases can be distinguished in axis development: a growth establishment phase (as defined in [START_REF] Barthélémy | Plant architecture: a dynamic, multilevel and comprehensive approach to plant form, structure and ontogeny[END_REF]) during which the allometric and sink relationships within organs vary, and a stable phase.

Biomass production.

The initial biomass input in the system, Q(0), corresponds to the dry mass of the first phytomer. It was estimated from data on dry mass of the last phytomers produced by the plants. Biomass production at GC t, Q p (t), is computed according to the available blade surface S(t) as follows:

Q p (t) = E R • S(t) (1)
where 1/R is a factor of biomass conversion efficiency and E is a factor representing the local environmental conditions: it can be considered as a site-specific factor that regulates the potential biomass production (independent of time). Contrary to the precedent versions of the GreenLab model (e.g. [START_REF] Guo | Parameter optimization and field validation of the functional-structural model GreenLab for maize[END_REF]), no exponential term appears which would drive a saturation of biomass production due to self-shadowing and competition with neighbour trees. Indeed, for Cecropia, leaves are spatially organized at tips of axes so that selfshadowing is low; there is few overlapping. A similar observation of low self-shading was reported in [START_REF] Kitajima | Decline of photosynthetic capacity with leaf age and position in two tropical pioneer species[END_REF] for Cecropia longipes.

Biomass allocation to the main growth compartments.

The biomass produced is first allocated based on a model of sink competition at compartment level: roots, rings, new organs, and expansion of existing organs. As no sufficient information was available on the dynamics of the root compartment, we assumed that a constant proportion of biomass is allocated to root growth. The resting aerial biomass, Q(t) is partitioned to the aerial compartments proportionnally to their respective demands, the sum of which defines the total demand of the plant at GC t, D(t).

The demand of new organs compartment D b (t) is the sum of the active meristem sinks of the plant. The demand d b (k) of a meristem (hereafter called bud) of rank k varies linearly with k to account for the ontogenetical variations during the establisment phase:

d b (k) = P b • min(1, k • V b ) (2)
where P b is the value of bud sink once the stable phase is reached. The slope of the variation, V b , is a parameter of the model. The demand includes only the sinks of buds that will produce phytomers: resting or aborted lateral buds are not taken into account.

The demand of the expansion compartment D e (t) is defined as the sum of sinks of active organs within the plant. Demand of an organ for its expansion is defined as in [START_REF] Christophe | Model-based analysis of the dynamics of trophic competition during Arabidopsis thaliana development[END_REF] by a beta law density function normalized by its maximum value and multiplied by the organ sink value.

The demand of the ring compartment D r (t) is assumed to depend on the total active blade surface S(t), in reference to the widely used pipe model theory [START_REF] Shinozaki | A quantitative analysis of plant form -the pipe model theory i. basic analysis[END_REF]. As biomass allocated to ring increment is also known to depend on the environmental conditions and on the vigour state of the tree, a dependance to the supply to demand ratio (Q/D(t)) is also taken into account as follows:

D r (t) = P r • S(t) • Q D (t) (3)
P r is a parameter representing the sink strenght of the ring compartment. Note that due to the presence of this term, the total aerial plant demand D(t) must be calculated as the solution of an order 2 polynomial equation. Then biomass is allocated to each compartment:

Q c (t) = D c (t)•Q/D(t)
, where c ∈ b, e, r stands for buds, expansion and rings respectively.

Biomass partitioning within compartments.

The biomass allocated to the bud compartment, Q b , is shared between all new phytomers for their primary growth proportionally to their demand d b (k) as defined above. Within each phytomer, a submodel of sink competition is run to compute the biomass allocated to each organ, as defined in [START_REF] Mathieu | A dynamic model of plant growth with interactions between development and functional mechanisms to study plant structural plasticity related to trophic competition[END_REF], according to their respective sinks P o .

Biomass for expansion Q e (t) is partitioned between all expanding organs according to their age and to the shape of their sink variation, as classically done (e.g. [START_REF] Christophe | Model-based analysis of the dynamics of trophic competition during Arabidopsis thaliana development[END_REF]).

The biomass of the ring compartment, Q r , is spread along the tree axes to add a new layer to every internode. The ring growth of each phytomer depends on their length and on the functinal blade surface above them in the tree architecture:

q r k (b o , t) = Q r • l k (b o , t) • S a k (b o , t)/d r (t) (4)
where l k (b o , t) is the length of the phytomer considered, indexed by its rank k, its branching order b o and the current GC t. S a k (b o , t) is the active blade surface located above it. d r (t) is the secondary demand for ring partitioning from the ring pool of biomass. It is calculated as:

d r (t) = t k=1 max bo bo=1 l k (b o , t) • S a k (b o , t) (5)
where max b o is the maximal branching order.

2.3.4. Variable allometries. As the pith is hollow, internodes of Cecropia have shapes of hollow cylinders. To simplify the computation of geometrical shapes and to reduce the number of parameters, we considered that the organ shape is equivalent to the full cylinder that has the same volume as the hollow one. This volume v(k, t, b o ) is computed from the amount of dry mass allocated to the internode. The dry mass to volume ratio depends on the distance of the phytomer to the apex: an allometric relationship was establised from observed data (see section 3). The internode length l is deduced from its volume v by the classical allometry:

l(k, t, b o ) = Be k • (v(k, t, b o )) 1 + β k 2 (6)
Be k and β k vary with phytomer rank k during the establishment phase and then stabilize. Blade area is computed from blade dry mass using the specific blade mass (SBM) factor, which is the ratio of blade dry mass (g) to blade fresh area (cm 2 ). As SBM values may change with plant age [START_REF] Kitajima | Decline of photosynthetic capacity with leaf age and position in two tropical pioneer species[END_REF] or when the light environment of the plant changes (e.g. at emergence from the surrouding vegetation), it was chosen to link SBM to the ratio of biomass supply to demand (Q/D) that should be a good indicator of the plant current state. To account for the stabilization of SBM, a maximal value (SBM max ) was estimated from the data for each individual. Thus the SBM value of individual i at time t was calculated as follows:

SBM (i, t) = min{SBM max (i), SBM min + V S • Q D (i, t)} (7)
where SBM min is the minimal value of SBM observed for our youngest individuals and V S is a parameter of the model.

Target data and parameter estimation.

For each tree, the target data consisted in a topological description (phytomers and axes positions) and for each phytomer in its internode dry mass, internode (fresh) length, internode (fresh) diameter, blade dry mass, blade (fresh) area, petiole dry mass and infructescence dry mass. Specific allometries were estimated from the data to link organ dry mass to their fresh dimensions (e.g. SBM was computed from the ratios of blade dry weight to blade area).

As our goal in this study was to reproduce the growth of several individuals in order to extract the variations of their source-sink ratio over time, the topology was set directly as read in target files. Although the individuals were growing in different environments and despite the variability observed among their characteristics, we tested whether they could be considered as several realizations of the same theoretical individual. Therefore, 11 individuals were fitted in parallel, simulating their growth using a single set of parameters (multi-fitting [START_REF] Guo | Parameter optimization and field validation of the functional-structural model GreenLab for maize[END_REF]), except for three parameters that were considered as individual-specific: a local environmental factor, maximal blade thickness and leaf lifespan. The parameter estimation was performed using the generalized non linear least squares implemented in the Digiplante software [START_REF] Cournède | Structural factorization of plants to compute their functional and architectural growth[END_REF].

Results

Data analysis and parameter inputs

The period between the emission of two successive phytomers is approximatively two weeks. The age of the measured individuals was determined using (i) the periodic variations of internode lengths and pith diameters and (ii) the positions of branches and inflorescences (Figure 2). Results are presented in table 1 along with other main characteristics classically used to describe trees (e.g. diameter at breast height, height, aerial biomass). It illustrates the high variability of the individuals measured: for instance, the fresh mass of tree 9 was similar to that of tree 8, although the latter was 5 years older than the former. Tree 8 was older than tree 10 but it had only one branch while tree 10 had two branches of second order and one branch of third order. Besides, only tree 10 had infructescences.

A good linear correlation was found between blade area and blade dry mass (a = 56.3m + 186.6, R 2 =0.91, n=523) and petiole fresh diameter (a = 35.3d -14.1, R 2 =0.92, n=523). The specific blade mass estimated for each tree as the mean ratio of blade dry mass to blade area can be found in Table 2. Root dry mass was measured for the eight youngest individuals. The ratio between root mass and total mass was found equal to 0.19 in average (SD 0.059).

An assumption in the model is that all axes of Cecropia share the same parameter values. For the two branched trees (8 and 10), organ weights were similar regardless of the branching order (see figure 3). At the axis emergence, there is a phase of growth establishment during which the phytomer characteristics vary. Younger branches have phytomers with lower mass (five times lower in average) and within phytomers, the partitioning of biomass favors more the internodes than in older branches (Figure 3). The ratio between petiole dry mass and blade dry mass was found relatively stable with a mean value of 0.27 (SD=0.089, n=587). In contrast, the proportion of internode mass within a phytomer decreases with phytomer mass and hence the internode sink was linked by an allometric relatioship to the phytomer meristem dry mass: P i = 0.466 * (q b ) 0.27 , R 2 = 0.21, n = 563 (data not shnown). The ratio between internode dry mass and its volume was found relatively constant except for the young phytomers. This can be due to the fact that maturating internodes have a different wood density value. In the simulation, this ratio was set dependent on the phytomer distance to apex, d, as follows: m/v(d) = 0.24•d 0.12 , R 2 = 0.15. The allometric coefficient β defining internode dimensions (length and section area) was set to 0.9, since the internodal length is highly variable. The coefficient β was varied during the establishment phase following a beta-shape function fitted with the model.

3.1.1. Fitting results. The 11 measured individuals were fitted in parallel with data of their organ dimensions and mass, representing a total of more than 4600 data points. Table 2 gathers the parameter values estimated from the data or fitted through the model by global optimization (18 fitted parameters). For each plant, a value of site-specific local environment is fitted. As the parameter of resistivity to biomass production, R, is also fitted, the two parameters E and R are not identifiable together. A reference value has to be chosen for at least one tree, otherwise there would be an inifinite number of possible solutions. The reference value is arbitrarily set to 10, for tree 10. Values of the environmental factor for the remaining trees are estimated relatively to this reference tree and the results are consistent with qualitative observations of the tree local environments. The adjusted coefficients of determination (R 2 ) are 0.65, 0.18, 0.54, 0.75, 0.75, 0.75, 0.56 for internode mass, length, diameter, blade area, mass and petiole mass respectively. The coefficient of determination for compartment data are all above 0.98. Figure 4 shows some of the graph outputs: simulated and observed internode and blade mass along the trunk according to phytomer rank (a-c); variations of simulated internode and blade biomass of the whole plants from emergence to the date of our destructive measurement (observed values represented as dots) (b-d). Figure 5 shows the evolution of the ratio of biomass supply to demand over time for the 11 fitted trees. Branch appearance induces a decrease in this ratio as it increases the demand. This effect is not pronounced for two main reasons: (i) the phytomer bud sink is small at branch emergence and (ii) branch emergence also increases the plant photosynthetical sources. In contrast, the appearance of fruits has a strong impact on the sourcesink ratio but this influence is limited to the duration of fruit expansion. One of our objectives was to investigate the existence of a relationship between the state of trophic competition within the plant (represented by the source-sink ratio) and the rhythms of branching and flowering. In that context, our results showed that the source-sink ratio might be a driving variable of branch and fruit emergence but has to be coupled with other factors as tree 9 has no branches although it exhibits the highest values of sink-source ratio (see Figure 5).

Discussion and Conclusion

For the first time, it was possible to analyse tree growth with the GreenLab model using a complete set of data. A first interesting result was the strong linear correlation found between fresh petiole diameter and blade area, which may considerably simplify the future experimental work. This study aimed to simulate all individuals with a single set of parameters and to reproduce the observed biomass varibility by using a single factor of environmental control. It allows to verify that the model structure is robust enough to simulate the growth of individuals at different ages and grown in different conditions. Indeed, when biomass data are considered, destructive measurements are required: data are collected on the tree at a fixed date and there is no data about their past growth, although the data collected result from the integration of long-term processes. This highlights the importance of multi-fitting (i.e. simultaneous fitting on several individuals at different growth stages) to evaluate the model, as well as for crops [START_REF] Guo | Parameter optimization and field validation of the functional-structural model GreenLab for maize[END_REF].

Although the core of GreenLab principles have been conserved, some equations of the model have been slightly modified to take into account the specificities of Cecropia, that mixes characteristics of both herbs and trees. In particular, it has been observed that when a new axis is emitted (including the main stem), there is a phase of growth establishment during which internode allometries vary (longer and thinner internodes) while the partitioning of biomass within the phytomer changes (more biomass is allocated to internode) and while pith diameter increases linearly (Figure 2). Here, the slope is presumably related to environmental conditions: a quick increase was observed for individuals growing in favorable environment. Most of these characteristics might be related to the meristem size whose diameter is smaller at branch emergence.

The fitting results highlighted some weak points of the model. As sinks are relative in GreenLab, the increase of organs with high demand, such as fruits, mechanistically induces a decrease of the size of the other organs. This effect is not observed on the measured individuals, even on the phytomers bearing fruits; it implies that other modelling choices should be considered for biomass allocation. For instance, Dingkuhn et al. discuss the possiblity that plant growth would be driven by sink regulation rather than by sources as classically done in allocation models [START_REF] Dingkuhn | Is plant growth driven by sink regulation ? implications for crop models, phenotyping approaches and ideotypes[END_REF]. Biomass allocation to the roots was coarsely simulated by allocating a constant proportion of the biomass production at each GC. This hypothesis is reasonable with regard to the data on young inidividuals but further investigation would be needed on older trees to get a more accurate model of root growth dynamics, in particular to take into account the growth of stilt-roots, that might be related to mechanical stability of the tree. The duration of leaf activity was set as a model input and estimated from observations. However, a more mechanistic modelling would be needed. It could be based on the theory of cost-benefit [START_REF] Navas | Leaf life span, dynamics and construction cost of species from mediterranean old-fields differing in successional status[END_REF].

Previous studies on Cecropia have shown that internodal length have sinusoidal variations that could be related to the seasonal variations of rainfall [START_REF] Heuret | Synchronization of growth, branching and flowering processes in the south american tropical tree Cecropia obtusa (Cecropiaceae)[END_REF], [START_REF] Zalamea | Growth pattern and age determination for Cecropia sciadophylla (Urticaceae)[END_REF]. This pattern was also observed in our study but, to simplify our exploratory analysis, only a constant environment factor was considered for each tree. Further works must take into account these seasonal variations. It requires defining methods to detect accurately the number of phytomers emitted each year as the growth rates can slightly fluctuate. Despite these limitations, the fitting procedure gives an insight in the plant internal trophic competition. The appearance of infructescences and branches induces a decrease in the supply to demand ratio. At emergence, new branches are more sinks than sources. This could be a first reason to explain the observed periodic branching patterns, although trophic competition is certainly not the only influent factor (for instance, tree 9 had a high sink-source ratio but had no branches). Further studies on individuals with more branches should help unraveling the effects of genetic control, seasonal environmental variations and internal trophic competition.

Figure 1 .

 1 Figure 1. (a) Habit of Cecropia sciadophylla ; this individual is 11 year old with a height of 19.5 m, a DBH of 12.5 cm and composed of 21 axes with a total of 1780 nodes and 381 leaves ; (b) detail of a compound leaf ; (c) detail of an axis at the point of insertion of lateral shoots ; (d) detail of a female inflorescence and (e) transversal cuts for each node of the terminal part of an axis.

Figure 2 .

 2 Figure 2. Age determination. Internodes length (bold black line) and pith diameter (line) of phytomers along the main stem of tree 10 and localization of branches (open triangles) and inflorescences (open circles).

Figure 3 .

 3 Figure 3. Internode and blade fresh mass on tips of branches for trees 8 and 10. A1: trunk, A2: branch order 2, A3: branch order 3.

Figure 4 .Figure 5 .

 45 Figure 4. Fitting results for the 11 individuals: internode(a) and blade (b) phytomer mass vs. rank along the main stem, internode (b) and blade (d) accumulated mass vs. time

  Two populations of Cecropia sciadophylla Mart. were studied in French Guiana. The first one was located at Saint-Elie road (5 o 17' N, 53 o 04 W). The second one was located at ca. 20 km from Saint Elie road, on Counami road (05 o 24 N, 53 o 11 W). Climate in French Guiana is seasonal with a 3-months dry season from mid-August to mid-November and a rainy season during the other 9 months. Additionally, a short dry season may occur in February and March. Mean annual rainfall is ≈3000 mm/yr.

Table 1 .

 1 Characteristics of measured individuals.

	ID Age Nphyt. Loc.	H(m)	DBH(cm) AerMass(g)
	1	2	55	E	3.61	3.9	5481
	2	2	55	E	2.97	2.3	1092
	3	2	45	E	2.2	1.2	341
	4	1	18	E	0.35	-	38
	5	1	29	E	0.08	-	2
	6	2	33	E	0.71	-	70
	7	2	37	E	0.77	-	125
	8	8	248	E	9.87	9.3	40 720
	9	3	74	E	7.72	9.5	40 605
	10	8	391	C	12.64	13.4	71 741
	11	2	52	E	1.49	1.6	486
			ID: identifier index, Age: ontogenetical age (years),
			Nphyt.: total number of phytomers,
		Loc. : location (E:Saint-Elie, C: Counami), H: height (m),
	DBH: diameter at breast height (cm), AerMass: total aerial fresh mass (g).

Table 2 .

 2 Estimated parameters diretcly from data or by using global model calibration (marked with asterisk).

		Tree-specific parameters (Tree 1 to 11)
	SBMmax	Specific blade mass, g.cm -2
		0.012; 0.0091; 0.0086; 0.0075; 0.0080;
		0.0079; 0.0089; 0.017; 0.015; 0.017; 0.012
	T f	Maximal number of active leaves
		21; 10; 7; 7; 6 ; 6; 7; 21; 22; 16; 15
	E i	Environment factor *
		6.77; 7.12; 7.15; 6.02; 3.17;
		6.43; 6.52; 7.39; 13.47; 10 (reference); 6.09
		Parameters common to all trees
	Q 0	Initial biomass	1.5g
	xr	Biomass proportion to roots	19%
	R	Inverse of conversion efficiency *	1322
	P a	Blade sink (ref)	1
	P p	Petiole sink	0.27
	P f	Fruit sink	13.49
	Exp f	Fruit expansion duration	Te = 6
		Fruit expansion parameters	a = 4, b = 1.5
	P i (k, t)	Internode sink:	x = 0.46
	P b	x • (q b k (t)) y Bud sink, maximal value *	y = 0.32 69.8
	V b	Bud sink, slope * with rank k	0.015
	P r	Ring sink *	14.91
	SBM min	SBM variation, minimum	0.00749g.cm -2
	V S	SBM variation, slope * with Q/D	0.0074cm -2
	Be	Internode allometry factor *	ini=1313, end=3.87
	β	Internode allometry exponent	0.9
	m/v(d)	In. dry mass to volume ratio:	x = 0.238
		x • (d) y , d: distance to apex	y = 0.12165

Acknowledgment

The authors thank the students who helped us for the measurements during the training programm FTH organized by AgroParisTech, Kourou (UMR Ecofog): V. Bellassin, S. Braun, O. Djiwa, V. Le Tellier (FTH2007), L. Menard, A. Jaecque, K. Amine, J. Kaushalendra (FTH2008). We also thank B. Leudet, J. Beauchêne and F. Boyer for their help on the field, P.-H. Cournède for the use of the Digiplante software (Ecole Centrale Paris, EPI Digiplante) and C. Sarmiento for her valuable comments on our manuscript.