Damien Pous

Weak Bisimulation up to Elaboration

We study the use of the elaboration preorder (due to Arun-Kumar and Natarajan) in the framework of up-to techniques for weak bisimulation. We show that elaboration yields a correct technique that encompasses the commonly used up to expansion technique. We also define a theory of up-to techniques for elaboration that in particular validates an elaboration up to elaboration technique, while it is known that weak bisimulation up to weak bisimilarity is unsound. In this sense, the resulting setting improves over previous works in terms of modularity. Our results are obtained using nontrivial proofs that exploit termination arguments. In particular, we need the termination of internal computations for the up-to techniques to be correct. We show how this condition can be relaxed to some extent in order to handle processes exhibiting infinite internal behaviour.

Introduction

Weak bisimilarity (≈) is a commonly used behavioural equivalence for the analysis of concurrent systems. Weak here means distinguishing between visible actions of a system, that express interactions with its environment, and τ transitions, that are treated as internal moves, and hence unobservable. To prove a weak bisimilarity result, one usually exhibits a relation R between states of the systems being compared, and shows that R is a weak bisimulation relation (we shall often simply use 'bisimilarity' and 'bisimulation' in the sequel, and refer explicitly to the strong version of these relations when necessary).

The crux of a bisimulation proof is often the study of silent transitions, as this part of the proof expresses the fact that internal calculations do not introduce unexpected behaviours. Typically, this is where it is shown that an optimisation is valid, that an encoding is fully abstract, or that some invariant about a data structure is preserved. Because one has to take into account all possible silent transitions, this makes bisimulation relations grow a lot, although, intuitively, many of the τ transitions being examined are irrelevant from the point of view of the overall behaviour of the system.

Several up-to techniques have been proposed to alleviate the task of bisimulation proofs. The idea of up-to techniques is to manipulate functions from relations to relations, that compute a form of closure. These functions are used in the bisimulation game as shown on the diagram on the left below:

P α R Q α P F(R) Q U : R → R ∪ ≈ W : R → ≈ R ≈ X : R → R ≈ E : R → R ≈
When the symmetric candidate relation R contains a pair P, Q , and P does a transition to P along an action α, Q has to perform the same action, modulo some internal computation (τ transitions), to yield a process Q . The point is that the resulting pair P , Q has to belong to F(R) instead of R (bisimulation is obtained by taking the identity function for F).

For example, if we take for F the function U above, we can use known facts about ≈ when examining the transitions of processes related by R. More interestingly, function W allows one to apply known bisimilarity laws to transform P and Q in order to obtain a pair belonging to R. Unfortunately, the technique given by W is unsound, as shown by the following standard counterexample (written in CCS): consider a process P which is not bisimilar to 0, and define R { τ.P, 0 }. Since τ.P ≈ P , we can use W to repeatedly undo the silent transition τ.P τ → P , so that in the game of weak bisimulation up to weak bisimilarity, we never explore the actual behaviour of P . To address this difficulty, [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF] introduces expansion ( ), a behavioural preorder included in weak bisimilarity, that leads to the up-to technique given by function X defined above. Unlike W, X yields a correct proof technique, because expansion expresses a kind of efficiency constraint: intuitively, if P Q, then Q is 'faster' than P , in the sense that P and Q exhibit the same behaviour, but Q has to require less silent transitions to do so (we define formally below). Since P τ.P does not hold, X rules out the above counterexample.

However, as experience shows [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF][START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], there are cases where reasoning up to expansion does not suffice, because the silent moves one would like to factor out in a bisimulation proof are not contained in expansion. Typically, this occurs when the 'faster process' has to spend some time at certain points to do some internal bookkeeping, for instance to update a data structure. To go beyond expansion, we have proposed in [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] a general and, at least to some extent, modular theory of up-to techniques for weak bisimulation. [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] introduces a notion of controlled relation, which guarantees that a given relation can be used in place of expansion. Several sufficient conditions for a relation to be controlled are given, among which, most notably, a criterion based on a termination property that prevents the existence of what we call 'infinite ladders' like depicted on the diagram above (which shows an infinite τ →≈ ladder). Nevertheless, the resulting setting lacks flexibility, essentially because the property of being a controlled relation is not stable by union. This prevents the incremental construction of bisimulation proofs, and thus represents a drawback in terms of modularity: in this setting, extending a proof requires an involved knowledge of the up-to techniques at work, in order to check that relations remain controlled along the extension (we discuss this at the end of Sect. 3).

In this paper, we focus on the elaboration preorder, which has been introduced in [START_REF] Arun-Kumar | Conformance: A Precongruence Close to Bisimilarity[END_REF]. Elaboration, written , is somehow the dual of expansion: informally, P Q means that P performs at least as many silent transitions as Q, while exhibiting the same behaviour. Elaboration strictly contains expansion, and is in some sense very close to ≈. The focus in [START_REF] Arun-Kumar | Conformance: A Precongruence Close to Bisimilarity[END_REF] is on congruence properties of in the setting of CCS, and on the axiomatisation of this relation.

The first result we establish is that yields a correct up-to technique for bisimulation when the system is terminating, that is, when it does not exhibit infinite sequences of silent transitions. Rather remarkably, this result cannot be derived by a simple diagram chasing (as is the case for the up to expansion technique). The proof relies instead on the approach of [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], the termination hypothesis being used to derive the absence of infinite 'ladders'.

Our second contribution is to show that supports the development of a modular theory of up-to techniques, along the lines of the treatment of up-to techniques for strong bisimulation presented in [START_REF] Sangiorgi | On the Bisimulation Proof Method[END_REF]. This represents a significant step forward w.r.t. [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] in terms of modularity, notably because the up to transitivity proof technique, given by T : R → R * , is shown to be correct for elaboration (under the previous termination hypothesis). We devote particular attention to this important result: when applicable to reason about a coinductively defined relation , T provides the powerful techniques given by R → (R ∪ ) , or the more restrictive (but more commonly used) R → R . As we show in the paper, an application of the resulting framework is the study of an up to polyadic contexts proof technique (a polyadic context is a context with possibly many holes in it). Establishing directly the correctness of this technique can be really tedious, while correctness of T allows one to derive a modular proof that boils down to correctness in the -simpler -monadic case.

Although it can be argued that the termination of silent transitions is realistic in many systems (typically, when silent moves are used to update the internal representation of a data structure), some programming techniques may be the source of deliberate infinite internal behaviours, such as busy waiting loops. In order to be able to handle some of these situations, we move to a setting where silent transitions are decomposed into two kinds of internal moves, respectively called the progressive and non-progressive silent transitions (as in [START_REF] Groote | Algebraic Process Verification[END_REF]). Only progressive silent transitions are supposed to be terminating. We show that under this relaxed hypothesis, the previous results can be adapted, by validating an 'up to progressive elaboration' technique for bisimulation, and showing the correctness of progressive elaboration up to transitivity. While being similar to the proofs of the results above, establishing the properties for non-terminating systems involves rather intricate usages of well-founded induction. Beyond this technical aspect, we believe that the general proof pattern adopted in this paper exposes an interesting application of rewriting techniques to concurrency.

Outline of the paper. In Sect. 1, we introduce our notations and briefly recall the results of [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] that will be used in the sequel. In Sect. 2 we define the elaboration preorder, and establish correctness of the up to elaboration proof technique when silent transitions of the system are terminating. We develop in Sect. 3 a theory of up-to techniques for elaboration, and draw a comparison with existing techniques. We extend these results to non-terminating systems in Sect. 4, and give final remarks in Sect. 5.

Preliminaries

Labelled Transition Systems, Definitions

We consider labelled transition systems (LTS) P, L, → , with domain P, labels or actions in L and transition relation → ⊆ P × L × P. The elements of P are called processes and are denoted by P, Q. Except in Sect. 4, L will always implicitly contain a distinguished silent action, noted τ . We let α, β (resp. a, b) range over actions, in L (resp. visible actions, in L\{τ }). Some examples will be given using the syntax of CCS, which we suppose known to the reader.

We let R, S, B range over binary relations (simply called relations in the sequel) between processes. We denote respectively by R + , R = , R the transitive, reflexive, transitive and reflexive closures of a relation R. P RQ means P, Q ∈ R. The composition of two relations R and S, written RS, is defined by RS { P, Q /P RT and T SQ for some process T }. We also define the inverse of a relation: R -1 { P, Q /QRP }. I is the identity relation, defined by I { P, P /P ∈ P}. We say that R contains S (alternatively, that S is contained in R), written S ⊆ R, if P SQ implies P RQ. Given an action α, the set of transitions along α induces a relation denoted by

α →: α → { P, Q / P, α, Q ∈ →}.
Its inverse is written using a reversed arrow:

a ← = ( a →) -1
, and similarly for other forms of arrows, defined below. Finally, we call function a mapping from relations to relations.

Definition 1.1 (Termination).

A relation R terminates if there is no infinite sequence (P i ) i∈N such that ∀i, P i RP i+1 .

Such terminating relations are also called Noetherian in the literature. They lead to the powerful technique of proof by well-founded induction on which we heavily rely in the sequel. We will also make use of lexicographic inductions, that is, inductions based on lexicographic orders. In our case, such orders will always consist of the product of a terminating relation R with the standard ordering of natural numbers: P, n Q, m iff P RQ or (P = Q and n > m). The definitions of behavioural equivalences and preorders will make use of the following weak transition relations.

Definition 1.2 (Weak transitions). α → τ → = if α = τ a → if α = a ∈ L\{τ } α ⇒ τ → α → τ → α ⇒ τ → α → τ →
We can remark the following properties:

τ ⇒ = τ → , τ ⇒ = τ → + , a ⇒ = a ⇒ (note in particular the difference between τ ⇒ and τ ⇒).

Definition 1.3 (Evolution of relations).

Let α be an action and R, S two relations. We say that R α-evolves to S if whenever P RQ, P α → P implies Q α ⇒ Q and P SQ for some Q . Given two relations R and S, we say that:

-R evolves to S if R α-evolves to S for all α ∈ L, -R evolves silently to S if R τ -evolves to S, -R evolves visibly to S if R a-evolves to S for all a ∈ L\{τ }. Definition 1.4 (Bisimulation, Bisimilarity). Let R be a relation. R is a bisimulation if it is symmetric and evolves to itself. Bisimilarity, denoted by ≈, is defined as the union of all bisimulations.

Existing Up-to Techniques for Bisimulation

The following lemma will be useful in the sequel. It states correctness of reasoning up to transitivity on visible actions. Lemma 1.5. Let R be a relation. If R evolves silently to itself, and visibly to R , then R evolves to itself.

Proof. By two successive inductions, we show that for any n, R n evolves silently to itself, and R n evolves visibly to R (R n is the composition of R with itself, n times). Some important up-to techniques for bisimulation are given by the two following results which are simple reformulations of [7, Theorems 2.6 and 3.6].

Theorem 1.6. Let R be a symmetric relation. If R evolves silently to R ≈ and visibly to R , then R is contained in bisimilarity.

Theorem 1.7. Let B be a relation contained in bisimilarity, evolving to B , and such that B + τ ⇒ terminates. If R is a symmetric relation that evolves silently to B R ≈ and visibly to R , then R is contained in bisimilarity.

In both cases, visible and silent transitions are treated differently, and up to transitivity is allowed on visible actions only. The difference between these two results is in the up-to technique that is allowed after a silent action: in the first case, one uses the compression preorder, written ( will be defined in Sect. 2.1). This result is essentially already present in [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], without the transitivity on visible actions. In the second case, the up-to technique is given by a relation B, which has to satisfy a termination property. In [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], the actual requirement for B is to be a controlled relation [7, Definition 3.1], and it is shown that the conditions in the above theorem are sufficient for B to be controlled.

The compression, used in Theorem 1.6, is not as involved as the sufficient condition expressed by Theorem 1.7. On the other hand, as will be discussed in Sect. 3, the technique given by the former theorem is more amenable to the incremental development of proofs than the setting of the latter.

Elaboration

Definition and Basic Properties

We now define elaboration, that has been introduced in the setting of CCS in [START_REF] Arun-Kumar | Conformance: A Precongruence Close to Bisimilarity[END_REF].

Definition 2.1 (Elaboration relation, Elaboration).

A relation R is an elaboration relation (in short, an elaboration) if whenever P RQ:

(i) if P α → P , then Q α ⇒ Q with P RQ , (ii) if Q α → Q , then P α ⇒ P with P RQ .
Elaboration, denoted by , is the union of all elaboration relations.

Note that [START_REF] Arun-Kumar | Conformance: A Precongruence Close to Bisimilarity[END_REF] uses a reversed version of the symbol for elaboration -we adopted this choice to follow the convention in other papers about up-to techniques and behavioural preorders, notably [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF].

The intuition behind elaboration is that if P Q, then P is able to always be at least as slow as Q, as expressed by clause (ii). In relation to this, we may remark that divergences blur the difference between elaboration and bisimilarity: if P ≈ Q, then P |!τ Q. This observation suggests that elaboration is a coarse relation, rather close to ≈ (see also Prop. 2.3 below). Moreover, if we consider the bisimilarity defined by using clause (ii) on both sides, we obtain progressing bisimulation [START_REF] Montanari | Dynamic Congruence vs. Progressing Bisimulation for CCS[END_REF]. On CCS agents, the latter equivalence (which is contained in ) coincides with the greatest weak bisimulation that is a congruence.

To draw a comparison between and other behavioural preorders, we recall the definition of expansion [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] (called efficiency preorder in [START_REF] Arun-Kumar | An Efficiency Preorder for Processes[END_REF]). A slightly coarser definition of expansion appears in [START_REF] Fournet | The Join-Calculus: a Calculus for Distributed Mobile Programming[END_REF][START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], here we call it compression in order to avoid confusions. The difference has consequences as far as up-to techniques are concerned, as will be explained in Sect. 3.

Definition 2.2 (Expansion, Compression).

Expansion, denoted by , is the largest relation such that whenever P Q,

-if P α → P , then Q α → Q with P Q , -if Q α → Q , then P α ⇒ P with P Q .
Compression, denoted by , is the largest relation such that whenever P Q,

-if P α → P , then Q α → Q with P Q , -if Q α → Q , then P α ⇒ P with P Q .
In contrast with , P Q intuitively captures the fact that Q is able to be always faster than P (and similarly for P Q). As shown by the examples above, elaboration and compression are not comparable in general. These examples can be used to make the same observation with almost weak bisimulation [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF] or relaxed expansion [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] instead of compression.

Bisimulation up to Elaboration

In order for elaboration to yield a correct up-to technique, we need a termination hypothesis, for which we introduce the following terminology.

Definition 2.4 (α-terminating LTS). Let S = P, L, → be an LTS, and α ∈ L a label of S. We say that S is α-terminating if α ⇒ terminates.

Lemma 2.5. Let α be an action and R a relation such that

R α ⇒ ⊆ α ⇒ R. If α ⇒ terminates, then so does R α ⇒. Proof. First we prove ϕ : ∀n, R n α ⇒ ⊆ α ⇒ R n . Then, suppose that R α ⇒ does not terminate: there exists an infinite sequence (Q i ) i≥0 such that Q i R α ⇒ Q i+1 .
Using ϕ, we can define by induction an infinite sequence (P i ) i≥0 such that P i α ⇒ P i+1 and P i R i Q i . This sequence is contradictory with the termination of α ⇒. We make some comments about this result and its proof.

We have

τ ⇒ = τ → +
, so that the τ -termination is actually the termination of τ → (a property called convergence in [START_REF] Groote | Algebraic Process Verification[END_REF]). Without this hypothesis, up to elaboration fails to be correct: in CCS, we have !τ |a !τ |τ.a, and hence the (symmetric) relation R = { !τ |τ.a, 0 ; 0, !τ |τ.a } evolves to R, but R ⊆ ≈. We show in Sect. 4 how to relax the τ -termination requirement in some cases.

Theorem 2.6 is an application of the results proved in [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] -summed up in Theorem 1.7 -that exploit the termination of ladders (that is, sequences of processes related by B + τ ⇒). Remarkably, we are able to require here a termination property that does no longer involve the relation of interest ( ). This is achieved by using the right-to-left part of the elaboration game: as shown in the proof of Lemma 2.5, and depicted on the left diagram below, we use this part of the elaboration game in order to transform any infinite ladder into an infinite sequence of τ -transitions, that would contradict the τ -termination hypothesis. By contrast, when considering ≈ instead of , the same argument does not hold, as shown on the right diagram, which recasts the counterexample seen in the introduction: in a bisimulation game, the left hand side process is allowed not to move and hence an infinite ladder may yield a finite sequence of τ -moves. We can moreover remark that Lemma 2.5 actually entails that can be used in the general setting proposed in [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] (it is a controlled relation -cf. [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF]). In particular, in systems where is a precongruence, up to elaboration can be combined with the 'up to context' technique, yielding a powerful tool for bisimulation proofs.

Up-to Techniques for Elaboration

We now present some techniques that can be used to establish elaboration results, which in turn can be used for bisimulation proofs, by Theorem 2.6. We develop a theory of up-to techniques for elaboration along the lines of the study of up-to techniques for strong bisimulation in [START_REF] Sangiorgi | On the Bisimulation Proof Method[END_REF]. Definition 3.1 (Progression). Let R, S be two relations. We say that R progresses to S, denoted by R S, if whenever P RQ,

-if P α → P , then Q α ⇒ Q with P SQ , -if Q α → Q , then P α ⇒ P with P SQ .
This notion of progression is the counterpart of evolution (Definition 1.3) where an 'elaboration game' replaces the 'simulation game'. In particular, R is an elaboration iff R progresses to itself.

First we show that like strong bisimilarity, elaboration validates the powerful up to transitivity technique. As a corollary, elaboration up to elaboration is a correct technique: this means in particular that the elaboration preorder does not suffer from the irregularities of weak bisimilarity. Theorem 3.2 (Elaboration up to transitivity). In a τ -terminating LTS, if R is a relation that progresses to R , then R is contained in elaboration.

Proof. We show that R is an elaboration relation. For α ∈ L, let ϕ α (P, n) denote the predicate: "for any

Q such that P R n α ⇒ Q , P α ⇒ R Q ". We prove R τ ⇒ ⊆ τ ⇒ R (1)
by a lexicographic induction based on the termination of τ ⇒, with the predicate ϕ τ . The argument for the non-trivial case is sketched on the left diagram below:

P τ R n (ϕτ (P,n)) Q 1 τ R (H) Q τ P 1 τ R Q 1 (ϕτ (P1, )) R τ P R Q P τ R n+1 (1)
Q τ P 1 a R (ϕa(P1, )) a τ R (1) τ P R Q P a R n (ϕa(P,n)) a R (H) Q a τ R (1)
R τ P R Q Then we prove R a ⇒ ⊆ a ⇒ R (2)
by a second lexicographic induction with the predicate ϕ a . The two diagrams on the right above give the interesting cases. Finally, by applying Lemma 2.5 to R and (1), we obtain the termination of

R τ ⇒, that leads to α ← R ⊆ R α ⇐ using [7, Theorem 3.12].
We now introduce a class of functions corresponding to correct up-to techniques, that enjoys nice compositional properties.

Definition 3.3 (Safe function). A function

F is safe if for any relations R and S, if R ⊆ S R S then F(R) ⊆ F(S) F(R) F(S)
This definition corresponds to [9, Definition 2.5]. The main difference is that we consider progressions to the reflexive transitive closures of relations. As shown in the following theorem, using Theorem 3.2, this makes it possible to use safe functions 'up to transitivity'.

Theorem 3.4 (Correctness of safe functions). Let F be a safe function. In a τ -terminating LTS, if a relation R progresses to F(R) , then it is contained in elaboration.

Proof. Let R 0 = R, R n+1 = R n ∪ F(R n ), R ω = n R n .
We show by induction ∀n, R n R n+1 . Hence R ω R ω , and finally R ω ⊆ using Theorem 3.2.

The main point of safe functions is that they can be combined in a modular way: given two safe functions F and G, their union F ∪ G : R → F(R) ∪ G(R) and their functional composition F • G : R → F(G(R)) are safe. Hence, we can define correct up-to techniques incrementally (see for example the proof of Corollary 3.7). By contrast with [START_REF] Sangiorgi | On the Bisimulation Proof Method[END_REF], composing functions using the chaining operator F G : R → F(R)G(R) does not preserve safety, essentially for the same reasons as in the weak bisimilarity case [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] (in particular, τ -termination does not help). However, chaining can be 'emulated' since we are allowed to use safe functions up to transitivity: instead of F G, we can work with (F ∪ G) , which we believe provides enough flexibility for actual elaboration proofs.

Elaboration up to context. We further enrich the set of up-to techniques for elaboration with an up to context technique. We call context a mapping from processes to processes (like in [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], we adopt an approach that allows us to abstract over the details of the underlying syntax). We denote by C[P ] the application of a context C to a process P . In the following technical definition, both → and ⇒ are synonyms for the identity relation I (we suppose / ∈ L).

Q δ ⇒ Q , C[Q] α ⇒ C [Q ].
This is the direct adaptation to the weak case of the notion of faithfulness found in [START_REF] Sangiorgi | On the Bisimulation Proof Method[END_REF]. In CCS non-degenerate contexts [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF] are faithful; in the π-calculus, noninput guarded contexts are faithful. The following proposition shows that these families of contexts yield correct up-to techniques for elaboration. The proof is very similar to the proof of the corresponding result in [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

Proposition 3.6 (Safety of faithful families of contexts). Let C be a faithful family of contexts; the following closure up to C function is safe:

C : R → { C[P ], C[Q] / C ∈ C and P RQ} .
The following corollary sums up all previous results, yielding a powerful upto technique for elaboration. It appears that the theory of up-to techniques for elaboration is as smooth as that for strong bisimilarity. Also notice that while we considered only monadic contexts in Prop. On Modularity Properties of Up-to Techniques. Introducing the up to elaboration proof technique enriches the existing landscape of up-to techniques for bisimulation. We have seen that this behavioural preorder enjoys nice properties, allowing one to develop elaboration proofs in an incremental and modular fashion. We now study other up-to techniques from this point of view.

On the use of compression. As shown in [START_REF] Fournet | The Join-Calculus: a Calculus for Distributed Mobile Programming[END_REF][START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], compression also yields a correct up-to technique. By Proposition 2.3 above, elaboration and compression are not comparable. The following example in CCS shows that they are neither compatible, in the sense that they cannot be used in the same bisimulation proof. Let P = τ.τ.a and Q = τ.(τ.τ |a); we have

P τ → τ.a Q τ → τ.τ |a P so that the symmetric relation R = { P, 0 ; Q, 0 ; 0, P ; 0, Q } evolves to ( ∪ )R, but obviously R ⊆ ≈.
Another observation we can make about compression is that unlike elaboration, compression result cannot be proved up to transitivity, even when the LTS is τ -terminating. Indeed, the relation { 0, τ.a ; τ.a, a ; 0, 0 ; a, a } over finite CCS processes is a 'compression up to transitivity', but it is clearly not contained in bisimilarity, and thus neither in compression.

Incrementality in the setting of [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF]. Stability by union for up-to techniques provides a form of modularity, since it allows one to extend an existing proof by simply adding new behavioural laws. This property is immediate for coinductively defined relations such as , or . On the contrary, the setting of [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] lacks this facility: in order to extend a bisimulation proof up to B * 1 using a relation B 2 (B 1 and B 2 are supposed to satisfy the hypotheses of Theorem 1.7), one needs to prove the termination of (B 1 ∪ B 2 ) + τ ⇒, which involves some knowledge about B 1 . To illustrate the difficulties, consider the following example in CCS: These relations satisfy the required property: for i ∈ {1, 2}, B i evolves to B i and

B + i τ ⇒ terminates. But (B 1 ∪ B 2 )
+ contains the pair a, τ.a , and hence B 1 ∪ B 2 does not qualify to apply Theorem 1.7. We return to this question in Sect. 5.

If, on the contrary, the system we would like to reason about does contain divergences, a first approach could be to 'tag' non-terminating silent moves and treat these as visible. However, such visible transitions must be mapped to some visible actions on the other side of the elaboration game, in order to play these in one-to-one correspondence. This of course might be too demanding in some cases, typically when divergences arise because implementing a given behaviour introduces some loops (that are not present in the original specification). In order to address such situations, we adopt an approach from [START_REF] Groote | Algebraic Process Verification[END_REF], which consists in isolating a subset of the τ transitions that are terminating, while still treating all τ moves as silent.

In the following we consider a LTS where silent moves are split into two special actions: {τ > , τ = } ⊆ L. Transitions

⇒ = τ → a ⇒ = a ⇒ = τ → a → τ → τ> ⇒ = τ → τ> → τ →
In this setting the notions of bisimulation and bisimilarity ignore the distinction between the two kinds of silent transitions (in particular, these relations do not coincide with what we would obtain by treating τ = as visible actions). The definition of elaboration is adapted so as to control progressive transitions only: Definition 4.1 (τ > -Elaboration). τ > -Elaboration, denoted by > , is the largest relation such that whenever P > Q,

(i) if P α → P then Q α ⇒ Q with P > Q , for any α ∈ L, (ii) if Q α → Q then P α ⇒ P with P > Q , for any α = τ > , (iii) if Q τ> → Q then P τ> ⇒ P with P > Q .
τ > -expansion is the 'progressive elaboration' we alluded to in the introduction. Clause (i) corresponds to bisimulation, while when playing from right to left, we ensure that progressive silent transitions are 'preserved' (iii). We can easily check that > is a preorder, and that we have ∼ ⊂ > ⊂ ≈.

This adaptation leads to the following theorem, where the termination hypothesis concerns progressive silent transitions. As expected, up to transitivity is allowed on visible transitions (i), and up to τ > -elaboration is supported only on progressive silent transitions (ii). Clause (iii) for non-progressive transitions does not allow up-to reasoning on the left of R. We show in [START_REF] Pous | Weak Bisimulation up to Elaboration[END_REF] how to relax this condition by using an adapted version of expansion. We omit this development here for the sake of simplicity. Theorem 4.2 (Bisimulation up to τ > -Elaboration). Let R be a symmetric relation. If the following conditions hold whenever P RQ:

(i) if P a → P then Q a ⇒ Q with P R Q , (ii) if P τ> → P then Q τ ⇒ Q with P > R ≈ Q , and (iii) if P τ= → P then Q τ ⇒ Q with P R ≈ Q ,
and the LTS is τ > -terminating then R is contained in bisimilarity.

Proof. We first prove the termination of > τ> ⇒ using Lemma 2.5. Then we show that the symmetric relation (R ∪ ≈) is a bisimulation. Let S = > R ≈; we remark that (R ∪ ≈) = ≈ S , so that it is sufficient to show that S evolves to itself. This is established by proving successively the following inclusions:

(1)

τ= ← R ⊆ R ≈ τ ⇐ (2) τ ⇐ S ⊆ S τ ⇐ (3) a ← S ⊆ S a ⇐
We obtain (1) from (iii) and a simple induction over the sequence τ= → . We prove (2) by well-founded induction using the termination of > τ> ⇒ and the predicate ϕ(P ): "for any P , Q such that P τ ⇒ P and P SQ, we have P S τ ⇐ Q". This leads to the diagrams below, where we reason by cases according to whether there is a progressive silent transition between P 0 and P 0 or not. In the former case, P > τ ⇒ P 1 so that ϕ(P 1 ) holds. Otherwise, we just use [START_REF] Arun-Kumar | An Efficiency Preorder for Processes[END_REF].

P τ > P 0 τ= R (1) τ ≈ Q τ τ> R ≈ (ii) τ P 1 τ (ϕ(P1)) S ≈ τ P > P 0 S Q P τ > P 0 τ= R (1) τ ≈ Q τ P > P 0 R ≈ ≈ Q
Then we prove (3) by well-founded induction using the termination of > τ> ⇒ and the predicate ψ(P ): "for any P , Q such that P a → P and P SQ, we have P S a ⇐ Q". As depicted in the following diagrams, if there is a progressive silent transition transition between P 0 and P 1 , we use the induction hypothesis, otherwise, (1) is sufficient to close the diagram.

P a > P 0 τ> R (2) τ ≈ Q a P 1 a S (ψ(P1)) a τ S (2) τ P > S ≈ Q P a > P 0 τ= R (1) τ ≈ Q a a R ≈ (i) a τ R ≈ (2) τ P > S ≈ Q
Finally, we apply Lemma 1.5 with (2) and (3) so that S evolves to itself.

We now show that τ > -elaboration validates the powerful up to transitivity proof technique on visible and progressive silent actions.

(i) if P α → P then Q α ⇒ Q with P R Q , for any α = τ = , (ii) if P τ= → P then Q τ ⇒ Q with P RQ , (iii) if Q α → Q then P α ⇒ P with P R Q , for any α = τ = , and (iv) if Q τ= → Q then P τ ⇒ P with P RQ ,
and the LTS is τ > -terminating then R is contained in τ > -elaboration.

Proof. We show that R is a τ > -elaboration relation by successively establishing the following properties.

R τ= → ⊆ τ ⇒ R (1)
R τ= → ⊆ τ ⇒ R (2)
R τ> ⇒ ⊆ τ> ⇒ R (3) R a ⇒ ⊆ a ⇒ R (4) R τ> ⇒ terminates (5) τ= ← R ⊆ R τ ⇐ (6) τ ⇐ R ⊆ R τ ⇐ (7) a ⇐ R ⊆ R a ⇐ (8)
A simple induction and (iv) yields (1), we prove ( 2) and (3) simultaneously by a lexicographic induction, using the termination of τ ⇒ and ϕ(P, n): "for any Q, Q

such that P R n Q, if Q τ= → Q then P τ ⇒ R Q , and if Q τ> ⇒ Q then P τ> ⇒ R Q ".
The non-trivial cases are respectively depicted on the two diagrams below.

P τ R n (ϕ(P,n)) S τ R (1)
Q τ= P R S R Q P τ> R n (ϕ(P,n)) τ R (1)
R τ P R Q
We obtain (5) by applying Lemma 2.5 to R and (3). A simple induction and (ii) give [START_REF] Montanari | Dynamic Congruence vs. Progressing Bisimulation for CCS[END_REF]. We show [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] with a lexicographic induction using the termination of The proof of (8) follows the lines of (7).

Concluding Remarks

We have proposed the new up to elaboration proof technique for bisimulation as an alternative to existing approaches. The proofs in this paper demonstrate how nontrivial termination arguments can be used to validate sophisticated proof techniques for bisimulation.

We have argued that up to elaboration offers advantages with respect to existing up-to techniques, in terms of expressiveness, flexibility or modularity. Our hope is that this technique can help addressing more complex weak bisimulation proofs. That it could be the case is suggested by the mathematical elegance of the framework we obtain, which opens the way for modular and incremental construction of proofs. This should nevertheless be confirmed by actual experiments in the study of systems involving manipulation of large bisimulation relations.

Several results in this paper suggest directions for future investigations. To enhance further our framework, it would be interesting to study how to integrate different kinds of methods in order to guarantee τ -termination, which is necessary for the results in Sect. 2. A possible approach would be to provide a measure together with the LTS, or to adopt syntactical criteria when the LTS is given by a calculus (a process algebra). Another interesting idea in this direction is given by type systems for termination. In Sect. 4, we proposed a way to handle the case of non terminating systems. We can however think of other approaches; in particular, we would like to study LTS where non-termination of τ → comes from cycles only, or where any state has a finite number of derivatives.

Finally, we would like to have a better understanding of the main problem of the setting of [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] (to which this paper proposes an alternative solution), namely the fact that controlled relations are not stable by union. An interesting direction would be to look for connections with the question of termination of the union of terminating rewrite systems, that has been widely studied in rewriting theory.

Proposition 2 . 3 .

 23 In any LTS, we have ∼ ⊂ ⊂ ⊂ ≈ and ⊂ ⊂ ≈.Moreover, in CCS, a|τ τ.a and a a|τ .

Theorem 2 . 6 (⇒

 26 Bisimilarity up to Elaboration). In a τ -terminating LTS, any symmetric relation R that evolves silently to R ≈ and visibly to R is contained in bisimilarity.Proof. We show easily τ terminates by Lemma 2.5. Then we check that and R satisfy the hypotheses of Theorem 1.7.

Definition 3 . 5 (

 35 Faithfulness). Let C be a family of contexts. We say that C is faithful if for all C ∈ C, whenever C[P ] α → R, there are C ∈ C, P ∈ P and δ ∈ L ∪ { } such that R = C [P ] and P δ → P , and for any Q, Q such that

3 . 6 ,→

 36 Theorem 3.4 allows us to use C transitively, thus validating the up to polyadic contexts technique. Corollary 3.7 (Elaboration up to context and transitivity). Let C be a faithful family of contexts and R a relation. If τ → terminates and R progresses to ( C(R) ∪ ) , then R is contained in elaboration.Proof. The functions R → and C are safe, hence so is R → C(R) ∪ .Up to deterministic transitions. Let us finally mention a corollary of Theorem 3.2, that extends a technique which has been introduced in[START_REF] Fournet | The Join-Calculus: a Calculus for Distributed Mobile Programming[END_REF] Chap. 4] in the setting of barbed bisimilarity. Together with Theorem 2.6, this result gives the possibility, when τ → is terminating and deterministic, to normalise processes w.r.t. τ → along a bisimulation proof. Notice that[START_REF] Fournet | The Join-Calculus: a Calculus for Distributed Mobile Programming[END_REF] does not suppose τ -termination, but requires the stronger commutation hypothesis α satisfies the requirements of Theorem 3.2, and hence is an elaboration up to transitivity.

B 1 =

 1 {(a + a, τ.τ.a), (τ.τ.a, τ.a)} B 2 = {(a, a + a)} a B2 / / a + a B1 / / τ.τ.a

→

  will respectively be called progressive and non-progressive silent transitions. Silent transitions, written τ Coherently, a, b will range over L \ {τ > , τ = }. We recall our notations for weak transitions (Definition 1.2) below.

  τ

Theorem 4 .

 4 3 (τ > -Elaboration up to Transitivity). Let R be a relation. If the following conditions hold whenever P RQ:

  We prove[START_REF] Groote | Algebraic Process Verification[END_REF] with another lexicographic induction, with the predicate ψ(P, n): "for anyQ if P R n a ⇒ Q then P a ⇒ R Q ".Depending on the existence of a progressive silent transition before the visible action of the transition Q a ⇒ Q , we close the diagrams as depicted below.

R⇒⇒

  τ> and the predicate Φ(P, n): "if P R n Q and P α

The Case of Non-Terminating SystemsWe now show how the results from the two previous sections can be adapted to cases where the τ -termination assumption is not satisfied. Before moving to the formal definitions, we make a few remarks on the τ -termination requirement. It should be noticed that for the up to elaboration technique to be applicable, the whole LTS does not necessarily need to be τ -terminating. What we need is rather a transition closed subset of (pairs of) processes for which this condition holds. For instance, we might want to represent a system in CCS, a calculus where divergences are of course expressible, but the processes used for the modelling do not exhibit τ -divergences.

Acknowledgements. We are very thankful to Daniel Hirschkoff for his numerous comments and suggestions, and his great help during the redaction process. We would also like to thank an anonymous referee for pointing out an incorrect proof.

This work has been supported by the french initiatives "ACI GEOCAL" and "ANR ARASSIA, projet ModyFiable"


David Colliaux

Pierre Bessière

Jacques Droulez

Cell signaling as a probabilistic computer

Living organisms survive and multiply even though they have uncertain and incomplete information about their environment and imperfect models to predict the consequences of their actions. Bayesian models have been proposed to face this challenge. Indeed, Bayesian inference is a way to do optimal reasoning when only uncertain and incomplete information is available. Various perceptive, sensory-motor, and cognitive functions have been successfully modeled this way. However, the biological mechanisms allowing animals and humans to represent and to compute probability distributions are not known. It has been proposed that neurons and assemblies of neurons could be the appropriate scale to search for clues to probabilistic reasoning. In contrast, in this paper, we propose that interacting populations of macromolecules and diffusible messengers can perform probabilistic computation. This suggests that probabilistic reasoning, based on cellular signaling pathways, is a fundamental skill of living organisms available to the simplest unicellular organisms as well as the most complex brains.

Introduction

The information available to living organisms about their environment is uncertain, not only because biological sensors are imperfect, but more importantly because sensors inevitably provide an incomplete, partial description of the environment. Moreover, timing is a crucial constraint for biological systems. During a fight-or-flight dilemma, animals must quickly decide to fight or flee, and they can never be sure of the good or bad consequences of their decision. Incompleteness is therefore a key notion for an autonomous agent facing the complexity of the world. There is now growing evidence that probabilistic reasoning is a rigorous and efficient way to represent partial or incomplete knowledge and to answer optimally questions that have no uniquely defined solution [START_REF] Jaynes | Probability Theory: the Logic of Science[END_REF].

Perception is a well-known example of ill-posed problems, because an indefinite number of object characteristics can theoretically give rise to the same set of sensory data. For instance, an indefinite number of objects with various shapes, sizes and movements can induce exactly the same retinal projection. A number of studies have shown that Bayesian models can accurately account for various aspects of perception [START_REF] Knill | Perception as bayesian inference[END_REF][START_REF] Weiss | Motion illusions as optimal percepts[END_REF][START_REF] Rao | Probabilistic models of the brain: perception and neural function[END_REF][START_REF] Mamassian | Bayesian modelling of visual perception[END_REF][START_REF] Ernst | Humans integrate visual and haptic information in a statistically optimal fashion[END_REF][START_REF] Laurens | Bayesian processing of vestibular information[END_REF] and sensory-motor integration [START_REF] Körding | Bayesian integration in sensorimotor learning[END_REF][START_REF] Körding | Bayesian decision theory in sensorimotor control[END_REF][START_REF] Colas | A unified probabilistic model of the perception of three-dimensional structure from optic flow[END_REF][START_REF] Todorov | General duality between optimal control and estimation[END_REF].

Non-probabilistic models assume that the brain computes internal estimates of relevant state variables such as motion, object distance, and color. Each variable is supposed to have a unique estimate, on which no evaluation of uncertainty is performed. In contrast, Bayesian models assume that the brain evaluates the probability corresponding to each possible value of the relevant variables. Probability computation results from straightforward application of the Bayes (i.e., multiplicative) and marginalization (i.e., additive) rules, which can been seen as a generalization of logical inference to probability distributions [START_REF] Bessière | Probabilistic Reasoning and Decision Making in Sensory-Motor Systems[END_REF][START_REF] Bessière | Bayesian Programming[END_REF]. Following Pearl [START_REF] Pearl | Probabilistic reasoning in Intelligent Systems: Networks of Plausible Inference[END_REF] and Jaynes [START_REF] Jaynes | Probability Theory: the Logic of Science[END_REF], we define probabilistic reasoning as the ability to perform inference within a probabilistic knowledge base. In the following, we will call a subjective Bayesian model the specification of the variables of interest, their conditional dependencies, the parametric forms, and the way probability distributions can be inferred. logical systems, can effectively perform probabilistic computation. The problem is to show possible correspondences between subjective Bayesian models and descriptive models of biological systems and signal processing.

Most existing studies proposed assemblies of neuronal cells or single neurons as the appropriate level of analysis to explain how a brain could perform probabilistic inference. Several authors have proposed that the firing rate of a group of cells within a given temporal window [START_REF] Zemel | Probabilistic interpolation of population code[END_REF][START_REF] Deneve | Reading population codes: a neural implementation of ideal observers[END_REF][START_REF] Gold | Banburismus and the brain: decoding the relationship between sensory stimuli, decisions, and reward[END_REF]? ? ] could represent probability distributions over state variables. The mean firing rate might be well approximated by a graded value, to which a subjective probabilistic meaning can be attributed: for instance, the probability that a given proposal over a state variable is true, or its loglikelihood ratio. Other approaches are based on the Poisson-like variability of spike trains [START_REF] Ma | Spiking networks for bayesian inference and choice[END_REF] or kernel convolution for encoding/decoding spike trains [START_REF] Deneve | Bayesian spiking neurons i: Inference[END_REF].

In contrast, we consider the molecular scale as an adequate framework to solve this matching problem between subjective Bayesian models and descriptive biological ones.

A common distinction is made between two classes of biochemical components that interact with one another. Simple molecules, called messengers, are available in large amount and/or diffusing rapidly across cellular compartments. Allosteric macromolecules, much more complex, have limited mobility and participate in the signaling pathway through changes in the spatial arrangement of their atoms. The messengers can bind to the allosteric macromolecules inducing their conformation changes. These conformation changes can, when in active states, modify the concentrations of the messengers either producing new ones or degrading existing ones. Enzymes are examples of macromolecules where these global changes in conformation are exposing parts of the molecules where reactants may bind to facilitate reactions producing or degrading messengers. Ionic channels belong to another class of macromolecules where the messengers' concentrations is controlled through opening or closing of the channel, letting ions flow across the membrane. Populations of macromolecules in their various conformational states and diffusible messenger concentrations are assumed to be the substrates used at sub-cellular level to represent and to compute probability distributions. Our proposal is that the biochemical processes involved in cell signaling can perform the elementary computations needed for subjective probabilistic reasoning, and that this biochemical computation is used extensively by the brain as an elementary component: a Bayesian "nano-gate." Specifically, we propose that macromolecular assemblies (receptors, ionic channels, and allosteric enzymes) coupled through several diffusible messengers (G-proteins, cytoplasmic calcium, cyclic nucleotides and other second messengers, membrane potentials, and neurotransmitters) are the biochemical substrates for subjective probability evaluation and updating. On the one hand, messenger concentrations play the role of parameters encoding probability distributions, on the other hand, allosteric conformational changes compute the probabilistic inferences. Diffusible messenger concentrations, including electric charge density, control the probability of conformational changes, which are in turn responsible for inflow and outflow rates of messengers and are then controlling their kinetics.

We started exploring these ideas in [START_REF] Houillon | The probabilistic cell: Implementation of a probabilistic inference by the biochemical mechanisms of phototransduction[END_REF], where the kinetics of a rhodopsin channel were shown to converge to a posterior distribution of states in a hidden Markov model, the hidden state representing the presence or absence of light. A similar kinetic scheme derived from Bayesian formulation of receptor activations was compared with other common signaling schemes in [START_REF] Kobayashi | Implementation of dynamic bayesian decision making by intracellular kinetics[END_REF] to emphasize its optimality. Rather than considering a binary (ON or OFF) hidden state, multiple activated states were considered in [START_REF] Siggia | Decisions on the fly in cellular sensory systems[END_REF] (like self and nonself in the immune system) and they discussed how Koshland-Goldbeter could solve this decision problem. Napp and Adams proposed in a recent paper [START_REF] Napp | Message passing inference with chemical reaction networks[END_REF] a procedure to compile a probabilistic graphical model into a chemical reaction network.

In section 2 we present biochemical cascades, we exhibit elementary building blocks for which the concentration of the secondary messenger (output) is either the product, the sum or the ratio of the concentrations of the 2 primary messengers (inputs), we show that these building blocks can be combined into cascade and we demonstrate that these cascades are abel to compute any Rational Function with Non-negative Coefficients (RFNC).

In section 3 we demonstrate that to solve any Bayesian inference problem it is necessary and sufficient to compute an RFNC. Consequently, we show that for any Bayesian inference problem it exists a theoretical biochemical cascade that solves it.

In section 4 we give a simple example of theoretical biochemical cascade to implement a phototaxis behavior for a unicellular organism.

Finally, in section 5 we discuss the different hypothesis and simplifications made in the paper and we propose different directions to extend this work.

Biochemical cascades

The biochemical processes in a cell form very complex networks of reactions that insures the survival of the cell for unicellular organisms or participate to the survival of the multi-cellular organism they belong to. These reactions are organized into pathways either metabolic that provide homeostasis (for instance, energy regulation) or sensorymotor that elaborate appropriate responses to given stimuli (for instance, phototaxis and chemotaxis behaviors or transduction of light in the retina). Some common messengers encountered in biochemical pathways include charged elements (electrons, calcium ions), cyclic AMP, phosphate or methyl groups. Two examples of biochemical cascades are presented (i) the detection of high nutrient areas during bacterial chemotaxis (Figure 1) and (ii) the conversion of light impinging the retina into biochemical signals (Figure 2).

The biochemical components participating in these pathways are subject to various dynamics and there are two common ways for allosteric macromolecules and messengers to interact:

1. Ligand (messenger) binding to macromolecules and activation. 2. Enzymatic action of messengers on the production and degradation of messengers.

The aim of this section is to study the dynamics of biochemical cascades in an abstract manner. This will provide us with a general description of the computations which it can implement.

Figure 1: Bacterial chemotaxis: Bacteria are unicellular organism often able of chemotaxis either moving toward attractant chemical components or away from repellent ones. The detection of these components by specific receptors initiate a cascade of biochemical reactions which in fine change the movement of flagella and the motion of the bacteria. In this example [START_REF] Sourjik | Receptor clustering and signal processing in e. coli chemotaxis[END_REF] attractant or repellent ligands binding to the specific receptors favors auto-phosphorylation of the histidine kinase (A -macromolecules) and the production of phosphoryl groups (messengers) which are then transferred to regulator (Y -macromolecules) which in turn modulate the flagellar motor activity. The allosteric macromolecule Y is itself controlled by the phosphatase activity of Z. Other allosteric macromolecules (R and W) modulate the receptor sensitivities through methyl messengers (CH3), while negative feedback is provided by a third macromolecule (B) through phorphoryl group messengers (P). Apart from specific receptors and flagella motors, six allosteric macromolecules (A, B, R, W, Y, Z) and 2 messengers (CH3 and P) are involved in bacterial chemotaxis.

Figure 2: Retina photo-transduction: When photons hit the retina, it changes the conformation of retinal which turns the rhodopsine in an active state, releasing the active G-protein (an example of macromolecule acting as a messenger). The G-protein activates the next macromolecule in the cascade; the phosphodiesterase (PDE) which in turn degrades the messenger cyclic GMP (cGMP) which is produced by the enzyme guanyl cyclase (GC). cGMP is the main messenger acting on the ionic channel. The light-induced decrease of cGMP concentration increases the probability for the channel to be closed. Adapted from [START_REF] Houillon | The probabilistic cell: Implementation of a probabilistic inference by the biochemical mechanisms of phototransduction[END_REF].

Allosteric macromolecules and messengers

In this section we will demonstrate that the interaction between messengers and allosteric macromolecules result in concentration of active macromolecules or in secondary messengers that are Rational Function with Non-negative Coefficients (RFNC) of the concentration of the primary messengers.

Formally, a RFNC is defined as follow: RFNC: Given a vector x = (x 1 , x 2 , • • • , x N ) of N entries, h(x) is an RFNC of x if one of the following conditions is satisfied:

1. h(x) is a non-negative constant; 2. h(x) = x n ; 3. h(x) = h 1 (x)h 2 (x) where h 1 (x) and h 2 (x) are RFNC of x; 4. h(x) = h 1 (x) + h 2 (x) where h 1 (x) and h 2 (x) are RFNC of x; 5. h(x) = h 1 (x)/h 2 (x)
where h 1 (x) and h 2 (x) are RFNC of x.

Ligand binding to macromolecules and activation

The first reaction network motif describes the binding of messengers to a receptor, with deactivating messengers S d favoring its transitions to inactive states M and activating messengers S a favoring activations to states M * according to the reaction:

M S a S d M * (1)
The full reaction mechanism is illustrated in the transition diagram of Figure 3 for a receptor having two binding sites and four active states.

In this general form, the model implies that the various events (binding of messengers, activation) occur in a random order [START_REF] Liebermeister | Bringing metabolic networks to life: convenience rate law and thermodynamic constraints[END_REF]. The probability of the macromolecule to change its conformation state towards an activate state is modulated by one or several messengers. The transition among states is often reduced to a Markov network dynamics [START_REF] Monod | On the nature of allosteric transitions: A plausible model[END_REF][START_REF] Changeux | Allosteric mechanisms of signal transduction[END_REF], the activity of a macromolecule depends on its tridimensional tertiary or quaternary structure, which can be in a discrete number of states, typically two, named "tensed" and "relaxed" in the original formulation of the model. The transition probability between these allosteric conformations depends on the status (free or not) of the receptor sites, and the affinity for specific messengers depends on the allosteric conformation. An example is given here, for a macromolecule with 8 states and 2 binding sites for primary messenger (represented as green circles and orange triangles). Four of these states are considered as "active": able to change the concentration of a secondary messenger (marked by a yellow star denoting their relaxed conformation). The dynamic of the configuration changes may be specified by the 24 propensities of the possible changes (corresponding to the 24 arrows). At equilibrium, the probability to be in any of the 8 configuration can be obtained as a RFNC of the concentrations of the primary messengers (see text for demonstration). The non-negative coefficient of the RFNC are the propensities. The probability to be active, as the sum of the probabilities of the four active states, is itself an RFNC of the concentrations of the messengers. and the binding rates are supposed to be proportional to the messengers' concentrations. For macromolecules with total concentration M t spread among n states, M = {M k } k∈{0,n} , each with concentration M k evolves according to the law of mass action for unimolecular reaction under the constrain M t = n k=0 M k which leads to k differential equations:

τ k dM k dt = -M k + R k M (2)
where R k gathers the rescaled reaction rates for transitions towards state k and the time constant τ k gathers the ones for its degradation, R ki is the propensity of the reaction from state i to k. Moreover, due to conservation law, we have l R lm = 1 so that all of the molecules departing from a state m are spread among other states.

The stationary concentrations are in the eigenvector of (I -R), with the matrix R lines composed of R k , for eigenvalue 1 which for this matrix is:

M k = det (I -R) {k} n j=1 det (I -R) { j} (3)
where the super index {k} on a matrix, M {k} , denotes the matrice M from which column and row of index k have been removed.

The concentration for each macromolecule state, in particular for the active ones, is thus a Rational Function with Non-negative Coefficient (RFNC as defines in the box RFNC) of the input concentrations of the messengers (see [START_REF] Droulez | Toward Biochemical Probabilistic Computation[END_REF] for a detailed demonstration). The coefficients are the propensities of each of the reaction corresponding to the different possible change of configuration of the macromolecule.

Enzymatic action of macromolecules on the production and degradation of messengers

The second reaction network motif describes how two antagonist macromolecules regulate the production of a secondary messenger. M * p is the equilibrium concentration of active allosteric macromolecules producing the secondary messenger S , when M * r is the analogous for the macromolecules reducing S (see Figure 4). It is a very common motif in both signaling and metabolic pathways:

Ø M * p M * r S (4)
∅ S This motif (often call "enzymatic futile cycle") following the Koshland-Goldbeter kinetics has been shown to act as a signal amplifier [START_REF] Goldbeter | An amplified sensitivity arising from covalent modification in biological systems[END_REF] or insulator depending on the relative time scales of complex formation and messenger production [START_REF] Vecchio | A Control Theoretic Framework for the Analysis and Design of Biological Networks[END_REF]. We assume in our model that the catalysis is a first process in the law of mass action so that the rates of production and degradation of messengers is proportional to the corresponding enzymes concentrations.

Macromolecules with concentrations in active states M * d , M * r are acting with first order kinetics:

dS dt = K p M * p -K r M * r S (5)
so that at steady state: S = r . Note that it is assumed that precursors messengers to be in large amount so that it is not limiting the production of messengers. As M * p and M * r are both RFNC of the concentrations of the primary messengers, S is also an RFNC of these concentrations.

Artificial biochemical cascades

In this section, we will demonstrate that for any RFNC it exists an artificial biochemical cascade to compute this RFNC. We will first propose an elementary module made of the 2 motifs just presented for which the concentration of the secondary messenger (output of the module) is an RFNC of the concentrations of the 2 primary messengers (inputs of the module). We will then show, that by adequate choice of the propensities, we may obtained the output concentration to be either the product, the sum or the ratio of the inputs concentrations. In a third step, we will demonstrate that it is possible for any RFNC to combine these elementary operator modules into cascade to obtain the desired computation. The obtained biochemical cascade is "artificial" because we do not pretend that the chosen propensities for the operators have any kind of biological plausibilities and also because the way the cascade is build is only a proof of existence and in no way an arrangement pretending to any optimality criteria or biological plausibility.

Elementary module

As an elementary module, we propose to consider two populations of primary messengers x and y, a population of secondary messengers S and two populations of macromolecules with state vectors M p , M r (see Figure 5). The two types of messengers both bind and modulate the activations of enzymes. The concentrations in active states are thus M * p = RFNC p (x, y) and M * r = RFNC r (x, y) and the output messenger concentration is itself an RFNC of the concentrations of the primary messengers:

S = k p * M * p k r * M * r = k p * RFNC p (x, y) k r * RFNC r (x, y) (6)
2.2.2. Product, sum and division modules For an elementary building block as just described we have 50 parameters available to design the RFNC: S = RFNC (x, y). These 50 parameters are the 24 propensities of the macromolecule producing S , the 24 propensities of the macromolecule reducing S , k p and k r . For a theoretical biochemical cascade, we can chose these parameters as we wish 1 .

In this section we will show how to choose these coefficients in order to obtain 3 elementary building blocks for which the concentrations of secondary messengers are respectively the product, the sum and the ratio of the concentrations of primary messengers.

Product:. The product may be obtain by the propensities choice shown in Table 1. Only 4 states among the 8 possibles are necessary for both the producing macromolecules and the reducing ones. For the chosen propensities, using Equation 3, we get:

RFNC r (x, y) = 1 2 (1 + x + xy) (7)
and :

RFNC p (x, y) = xy 2 (1 + x + xy) (8)
and finally, choosing k r = k p = 1, we obtain:

S = x × y (9)
Transition matrix for reduction In Figure 6 we present a simulation of the behavior of such an elementary product building block. Sum:. For the sum, a possible choice for the propensities is given in Table 2. Note that we use 5 states for the producing macromolecules. Choosing k p = 1 and k r = 2, we get:

* 1 0 1 2x * 1 0 y * 0 1 0 0 * RFNC r (x, y) = 1 2(1+x+xy) ∅ S Production matrix * 1 0 0 x * 2 0 0 y * 1 0 0 1 * RFNC p (x, y) = xy 2(1+x+xy)
S = x + y (10)
Reduction matrix Ratio:. For the ratio, a possible choice for the propensities is given in Table 3. Choosing k p = k r = 1, we get:

* 1 1 1 4x * 0 0 4y 0 * 0 1 0 0 * RFNC r (x, y) = 1 2(1+2(x+y)) ∅ S Production matrix * 1 1 0 0 x * 0 1 0 y 0 * 0 1 0 1 0 * 0 0 0 1 0 * RFNC p (x, y) = x+y 1+2(x+y)
S = x/y (11)
Reduction matrix

* 1 1 0 x * 0 1 0.5y 0 * 0 0 1 0 * RFNC r (x, y) = 0,5x 1+x+y
∅ S Production matrix * 1 1 0 0.5x * 0 0 y 0 * 1 0 0 1 * RFNC p (x, y) = 0,5y 1+x+y
Table 3: Propensities for ratio. Only the non-null propensities are represented.

Any RFNC can be computed by an artificial biochemical cascade

Given any RFNC of the concentration of some input messengers, it is always possible, by definition of an RFNC, to considered it as an arborescent cascade of application of the 3 basic operators: product, sum and division.

As we just demonstrated that these basic operators may be implemented by the proposed elementary modules, it is always possible to build the arborescent artificial biochemical cascade that exactly correspond to the required computation.

Due to the ability of the enzymatic futile cycle (motif 2) to act as an insulator, the concentrations in messengers at a given depth in the tree only depends on messengers' concentrations at the depth below. However, all the intermediary messengers encoding different quantities used in some branch or at some depth of this tree should be different from one another in order to insure that there is no possible confusion.

Subjective probabilistic inferences

Subjective probabilistic models (often called Bayesian models) include variables describing states of the world highly relevant for the organism, such as the presence of food or predators. The values taken by these variables cannot be known with certainty by the organism. However, according to the Bayesian approach, the organism can evaluate the probability distribution over these variables on the basis of specific observations, such as the detection of light or the detection of an odorant molecule. Furthermore, they can infer the probability for their actions according to the probabilities of these state variables and in fine decide what to do.

More formally, subjective probabilistic model and inference may be algebraically defined as follow (see [START_REF] Bessière | Bayesian Programming[END_REF] for thorough definitions and discussions and review of numerous examples):

Subjective probabilistic model: a A subjective probabilistic model is defined by a set X = {X 1 , X 2 , . . . , X N } of relevant variables and by a decomposition which states the joint distribution as a product of simpler ones assuming some conditional independencies between variables:

P (X 1 , X 2 , • • • , X N ) = M m=0 [P (L m |R m )] (12)
where L m and R m are subsets of X verifying the following conditions which simply impose that each variable is appearing once and only once left of the conditional sign in the decomposition:

1. Sets L m are a partition of set X:

∪ M m=0 [L m ] = X and ∀i, j ≤ M, i j, L i ∩ L j = ∅ 2.
Any variable appearing left of the conditional sign previously appeared right:

R 0 = ∅ and R m ⊆ ∪ m-1 i=0 [L i ]
a This definition is, in algebraic terms, equivalent to the definition of probabilistic factor graphs ([? ]) and consequently a generalization of Bayesian nets ( [START_REF] Pearl | Probabilistic reasoning in Intelligent Systems: Networks of Plausible Inference[END_REF]).

Subjective probabilistic inference: Let us consider a partition of the set X of relevant variables in 3 subsets: S the set of searched variables, K the set of known variables and F the set of free variables. A subjective probabilistic inference is defined as the computation of the probability of

P(S |[K = k])
To compute the probability distribution on the searched variables S knowing the known variables K we must marginalize out the variables F, the variables which are neither in the search variables S nor in the known variables,and normalize the result:

P ([S = s] | [K = k]) = F [P ([S = s] , [K = k] , F)] S F [P (S , [K = k] , F)] (13)
This is the general formula for Bayesian inference. The involved computation is very simple as it supposes only to compute sums and quotients of probabilities. However, the exact computations is most of the time intractable as the number of operations grows exponentially with the number of elementary variables in F and S . The joint probability distribution may be replaced by the decomposition defined in the model:

P ([S = s] | [K = k]) = F M m=0 [P (L m |R m )] [S =s][K=k] S F M m=0 [P (L m |R m )] [K=k] (14)
where we see that, now, the necessary computations suppose only product, sums and quotients of probabilities. The decomposition is a great help as the joint distribution is broken in smaller pieces of lower dimensionality. Rearranging the order in which the sums and products are done allows, most of the time, for drastic simplifications in the number of necessary computations (see [START_REF] Bessière | Bayesian Programming[END_REF], Chapter 14). After these simplification and given the chosen order,

P ([S = s] | [K = k]
) can be computed by an arborescent structure (a calculus tree) of products, sums and ratios of positive quantities: an RFNC. Finally, for any subjective probabilistic inference, it exists numerous calculus tree that can be mapped to an artificial biochemical cascade.

A simple example of biochemical cascade for phototaxis

Many unicellular algae, like Chlamydomonas reihnardtii, are able to do photosynthesis to produce the energy they need. Consequently, many of them are also able to detect and measure the quantity and eventually the rough direction of light in order to do phototaxic or photophobic movements to get the adequate illumination (see Figure 7).

As an example of what was described before we propose in this section a very simple instance of a phototaxis model and its possible implementation as a theoretical biochemical cascade made of 4 elementary building blocks. Let's consider a model made of 3 binary variables:

1. L 1 a binary variable taking the value 1 if there is light in direction 1 2. L 2 a binary variable taking the value 1 if there is light in direction 2 3. G a binary variable taking the value 1 when the alga have to swim straight and 0 when it should change direction.

The considered decomposition of the joint probability distribution on these 3 variables is:

P (L 1 , L 2 , G) = P (L 1 ) P (L 2 ) P (G|L 1 , L 2 ) ( 15
)
where P (G|L 1 , L 2 ) is defined as follow:

L 1 L 2 P ([G = 1] |L 1 , L 2 ) 0 0 0 0 1 0 1 0 0 1 1 1
which specifies that the algae should go straight (G = 1) only when both light measurements are positive (L 1 = 1, L 2 = 1).

The phototaxis behavior, has to decide of going straight or not (P (G)) according to probabilistic evaluations of the enlightenment (P (L 1 ) , P (L 2 )), which is obtained by:

P (G) = L 1 ,L 2 [P (L 1 ) P (L 2 ) P (G|L 1 , L 2 )] ( 16
)
This formula can be restated using the odds of the 3 variables defined by O (X) = P([X=1]) P([X=0]) :

O (G) = P([G=1]|00)+P([G=1]|01)O(L 2 )+P([G=1]|10)O(L 1 )+P([G=1]|11)O(L 1 )O(L 2 ) P([G=0]|00)+P([G=0]|01)O(L 2 )+P([G=0]|10)O(L 1 )+P([G=0]|11)O(L 1 )O(L 2 ) (17)
Replacing the terms P (G|L 1 , L 2 ) by their values, we finally obtain:

O (G) = O (L 1 ) O (L 2 ) 1 + O (L 2 ) + O (L 1 ) (18)
Using the 3 building blocks described in Section 2.2.2, it is very easy to build the theoretical biochemical cascade that implement the calculus corresponding to Equation 18(see Figure 8).

(G) = O(L 1 )O(L 2 )
1+O(L 2 )+O(L 1 ) .

Discussion

We proposed to look at an aspect of cell signaling and biochemistry from a new viewpoint, assuming that these processes may be seen as performing probabilistic inference.

This proposition is supported by the demonstration that any subjective probabilistic inference may be computed by an RFNC which in turned may be mapped to artificial biochemical cascade.

The main necessary hypotheses may be summarized as follows.

Assuming these four hypotheses, we have demonstrated that descriptive models of biochemical systems might be seen as performing probabilistic inference of some subjective models. Although the validity of these four hypotheses remains to be discussed, the propositions made in this paper open new perspectives for future directions of study, for instance: can we propose subjective interpretations of descriptive models of other types of biochemical interactions? At the same time and space scale? At different time and space scales?

Validity of the hypotheses?

A critical issue for designing descriptive model is to specify the space and time range in which processes are analyzed.

In the spatial domain, molecular assemblies of nanometer size govern the behavior of organisms that are several meters long. In this paper, we have restrained our analysis to small compartments of a single cell, typically a portion of a dendrite or axon. The order of magnitude of the size of such a compartment is 1µm 3 = 10 -18 m 3 .

Biological events range from about 10 -12 s [START_REF] Knapp | Allosteric action in real time: Time-resolved crystallographic studies of a cooperative dimeric hemoglobin[END_REF][START_REF] Elbert | A milestoning study of the kinetics of an allosteric transition: Atomically detailed simulations of deoxy scapharca hemoglobin[END_REF] for the fastest observed conformational changes to millions of years for gene evolution. We have restrained our analysis to time windows of 1ms to 1s, which is long enough to insure homogeneous concentrations of messengers in the considered compartments.

Our description of biochemical system is still too schematic for several reasons.

• The distinction between macromolecules and diffusible messengers is not sharp. Macromolecules also diffuse within membranes [START_REF] Triller | Surface tracking of receptors between synaptic and extrasynaptic membranes: and yet they surface tracking of receptors between synaptic and extrasynaptic membranes: and yet they do move[END_REF] and their spatial distribution, for instance, between cytoplasmic and nuclear compartments, is also controlled by specific biochemical mechanisms [START_REF] Stipanovich | A phosphatase cascade by which rewarding stimuli control nucleosomal response[END_REF]. However, at the space and time scale we are considering, this mobility of macromolecules may be neglected as a first approximation.

• A number of macromolecules directly act on other macromolecules without intermediate messengers. A clear example in cell signaling is given by the interplay of kinases and phosphatases. This was also discarded from our study for the moment.

• Detailed models of biochemical processes should also take into account the particular geometry of the cell. This includes (3D) phenomena arising in homogeneous volumes (such as the concentration of diffusible messengers), (2D) phenomena arising on a membrane area (such as the distribution of channels), and (1D) phenomena arising mainly along a symmetry axis (such as the propagation of potential along dendrite or axon branches). At present, we have only considered homogeneous concentrations of messengers and fixed distributions of channels, and we have neglected the effect of membrane potentials.

• We have only considered biochemical systems at equilibrium. Clearly, the temporal evolution of concentrations and macromolecular configurations must be further developed, in particular to account for slow reaction and diffusion processes, and for the various roles of biochemical feedback pathways. These dynamic processes could be related to time-evolving probabilistic reasoning, for instance hidden Markov models and Bayesian filters. However, the wide diversity of time scales encountered in biological systems contrasts with the somewhat schematic and oversimplified view of time representation in the usual subjective models. In future work, promising ideas could be the development of a more complex temporal hierarchy, and a subtler view of the respective roles of memory and temporal reasoning in subjective models.

Subjective interpretation of other biochemical interactions?

Obviously, the above detailed hypotheses are too restrictive. Furthermore, in this work, we have only considered a few possible biochemical interactions among the huge variety of possible ones. An important task in the near future will be to relax these hypotheses and look for subjective models that could be associated with other kinds of biochemical interactions. Some instances of such perspectives are discussed in the sequel to this section.

At the same time and space scale

Macromolecules with more allosteric states:. The allosteric theory [START_REF] Monod | On the nature of allosteric transitions: A plausible model[END_REF], initially developed to account for regulatory enzyme kinetics, postulated that proteins undergo fast, reversible transitions between a discrete number of conformational states. Transitions occur spontaneously, but some are favored by fixation of ligand to specific receptor sites. This model has been successfully applied to a large number of fundamental macromolecular assemblies, such as hemoglobin, ionic channels, and nuclear or membrane receptors (see [START_REF] Changeux | Allosteric mechanisms of signal transduction[END_REF] for a review).

The number of conformational states and the variety of controlled mechanisms for conformational changes can be relatively high. As an example, DARPP-32, a key macromolecule in the integration of dopamine and glutamate inputs to the striatal GABAergic neurons, exhibits four phosphorylation sites, thus 16 conformational states, and each phosphorylation is controlled by a different chemical messenger pathway [START_REF] Fernandez | DARPP-32 is a robust integrator of dopamine and glutamate signals[END_REF]. Inactivation of rhodopsin in vertebrate photoreceptors involves up to 12 phosphorylation sites, which are all controlled by the intracellular calcium concentration. In [START_REF] Houillon | The probabilistic cell: Implementation of a probabilistic inference by the biochemical mechanisms of phototransduction[END_REF] we described a first application of our approach to the vertebrate photo-transduction biochemical cascade. Augmenting the number of conformational states opens very exciting perspectives on the complexity of the computation that a single population of macromolecules could perform, but the corresponding subjective models are still to be proposed.

Macromolecules with several receptor sites for the same messenger:. Macromolecules with several receptor sites for the same messenger are very frequent in biochemistry. A number of allosteric macromolecules, including ionic channels, are composed of several subunits, and some of them are identical. The presence of a receptor site for a specific messenger on each subunit makes the whole macromolecule controlled by the second, third, or fourth power of the concentration. As a consequence, the catalytic activity is a highly nonlinear function of the messenger concentration, and may exhibit very sharp sensitivity.

In terms of subjective models, this means that similar observations, converted into likelihood ratios, are performed several times to infer the posterior distribution. This might be a simple and elegant way to enrich the computational complexity performed by macromolecules without requiring high dynamic ranges of messenger concentration. In the present work, we have assumed a simple proportional relationship between likelihood ratios and messenger concentrations. The presence of multiple receptor sites for the same messenger, and more generally the multimeric structure of some macromolecules can be interpreted as a nonlinear coding of the likelihood ratio, which could be better adapted to the biological constraints. For instance, a tenfold increase in messenger concentration could correspond to a likelihood ratio multiplied by 10 4 for a tetrameric receptor.

Allosteric changes governed by other events instead of chemical messengers:. Allosteric changes may be caused by other types of events besides chemical messengers such as electrical or mechanical ones. These events are not considered in the present model and should be studied in future.

Single-channel voltage clamp recordings [START_REF] Neher | Single-channel currents recorded from membrane of denervated frog muscle fibres[END_REF][START_REF] Sakmann | Single-Channel Recording[END_REF] have revealed several important characteristics of channels: (i) currents through isolated channels, and thus channel conductance, alternate between discrete values; (ii) transitions between current/conductance values are random brisk events; (iii) the transition probabilities can be modulated by pharmacological and biological agents (neurotransmitters, second messengers), ions (calcium), or membrane potentials. In agreement with the allosteric theory, the current descriptive model of ion channels [START_REF] Colquhoun | On the stochastic properties of single ion channels[END_REF][START_REF] Laüger | Conformational transitions of ionic channels[END_REF][START_REF] Chung | Coupled markov chain model: characterization of membrane channel currents with multiple conductance sublevels as partially coupled elementary pores[END_REF] is that of a finite state Markov model, similar to the one we used in this paper. Some transitions depend on the presence of a specific messenger in the vicinity of receptor sites, either in the extracellular domain (ionotropic receptor-channels) or in the intracellular domain, where receptor sites are specific to second messengers or calcium transporters. In voltage-dependent channels, transition probabilities are controlled by the membrane potential.

Local cascades and feedbacks:. Metabotropic receptors are transmembrane macromolecular assemblies with a receptor site in the extracellular domain and an activatable site in the intracellular domain. Chemical binding of the neurotransmitter with the extracellular receptor site induces allosteric conformational change of the macromolecule, which activates the intracellular site (an activatable enzyme site such as protein kinase, protein phosphatase, or Gprotein release). More generally, macromolecules can be activated by various events like mechanical strength, photoisomerization, pheromones, or odor detection. The intracellular activity results in the release of a primary messenger (e.g., the G α subunit in the G-protein-dependent signaling), which triggers the production or elimination of a diffusible second messenger (cyclic nucleotides, inositol triphosphate, \dots), which in turn acts on ionic channels.

In the complex molecular chain from the primary receptor to the set of ionic channels, several allosteric macromolecules intervene. Most of them have receptor sites for calcium, or are calcium transporters like calmodulin, thus allowing feedback regulation. As discussed above, the role of feedback should be understood in terms of the dynamics of the systems, including long-term adaptation.

At different time and space scales

Different dynamics to store information:. In the core of our model, we postulate that the existence of well-separated fast rates (10 4 to 10 5 s -1 ) and relatively slow rates (10 to 10 3 s -1 ) of biochemical reactions is fundamental. It allows the Markov processes of molecular collision and configuration changes generated by thermal agitation to converge to quasi stationary states that approximate probabilistic inference of subjective models. We have not yet considered the very slow dynamics of some allosteric changes (like desensitization) or the diffusion of large molecules in membranes, among many other slow biochemical events. These mechanisms can clearly be used for accumulating and storing information over long periods, which is a key computational capacity for adaptation and learning.

The role of membrane potential at cell scale:. The overall effect of all ionic fluxes can be summed up in the membrane potential kinetics. Though it is rather unusual to include membrane potentials in the set of messengers, it seems appropriate because the kinetic equations of membrane potential are similar to those for chemical messenger concentrations. Moreover, the membrane potential controls macromolecule conformational transition in a similar way, although constrained to a particular, but important, class of macromolecules, namely the voltage-gated channels [START_REF] Bezanilla | The voltage sensor in voltage-dependent ion channels[END_REF]. In turn, ionic channels change the membrane potential similarly to the way that activatable enzymes control chemical messenger concentration. Membrane potentials propagate much faster than messengers diffuse and can transmit the result of a given local computation to the whole cell. Consequently, including membrane potentials into our proposed framework would extend the space scale from a compartment to the whole cell.

Unicellular organisms:. At this molecular description level, our proposal applies not only to brain-controlled complex organisms and not only to small neuron networks, but also to unicellular organisms. Simple organisms like Paramecium or Euglena gracilis have limited numbers of sensors, and a greatly reduced repertoire of actions, but they must nevertheless adapt their behavior to an even more unpredictable environment. The efficiency of probabilistic reasoning with an incomplete model of the world applies equally to these simple organisms. Furthermore, the biochemical mechanisms that we propose for implementing probabilistic computation are already effective in controlling the behavior of eukaryotes. Among many other examples, it has been shown [START_REF] Iseki | A blue-light-activated adenylyl cyclase mediates photoavoidance in euglena gracilis[END_REF] that the photo-avoidance behavior of the micro-algae (E. gracilis) is mediated by concentration changes of cyclic adenosine monophosphate, a second messenger known to be involved in olfaction and many neuronal signaling pathways of multicellular animals.

Information transmission in multicellular organisms:. Excitable cells, particularly neurons, differentiate from other cells in complex multicellular organisms, from cnidarians to all bilaterians. These excitable cells provide a distant and discrete mode of messenger flux control: both chemical or ionic diffusion and passive electrical propagation become very ineffective at long distances. Note, however, that slow, but distant, signal propagation through active biochemical processes without action potentials has been recently discovered [START_REF] Fasano | Neuronal conduction of excitation without action potentials based on ceramide production[END_REF]. On the contrary, active regeneration of action potential thanks to voltage-gated channels allows the message to be transmitted unchanged at high speed along axonal branches up to the presynaptic terminals, where it is converted into chemical signals. Distant interactions between macromolecular assemblies by action potential propagation allow multicellular organisms to reach sizes and speeds far greater than the limit imposed by passive diffusion process. This constitutes an obvious gain for long-distance communication. However as opposed to membrane potential and messengers' concentrations which are graded and local signals, the action potentials are all-or-none signals. Therefore long distance communication is achieved at the cost of signal impoverishment. According to our view, fast-spike propagation must be completed by local and graded signal processing involving complex biochemical interactions that constitute a fundamental mechanism for probability computation.

Acknowledgment

This work is part of the European FP7 project BAMBI (Bottom-up Approaches to Machines dedicated to Bayesian Inferences), project number 618024. The authors warmly thank Emmanuel Mazer, Julie Grollier, and Damien Quer-

Figure 3 :

 3 Figure 3: According to the Monod-Wyman-Changeux (MWC) model[START_REF] Monod | On the nature of allosteric transitions: A plausible model[END_REF][START_REF] Changeux | Allosteric mechanisms of signal transduction[END_REF], the activity of a macromolecule depends on its tridimensional tertiary or quaternary structure, which can be in a discrete number of states, typically two, named "tensed" and "relaxed" in the original formulation of the model. The transition probability between these allosteric conformations depends on the status (free or not) of the receptor sites, and the affinity for specific messengers depends on the allosteric conformation. An example is given here, for a macromolecule with 8 states and 2 binding sites for primary messenger (represented as green circles and orange triangles). Four of these states are considered as "active": able to change the concentration of a secondary messenger (marked by a yellow star denoting their relaxed conformation). The dynamic of the configuration changes may be specified by the 24 propensities of the possible changes (corresponding to the 24 arrows). At equilibrium, the probability to be in any of the 8 configuration can be obtained as a RFNC of the concentrations of the primary messengers (see text for demonstration). The non-negative coefficient of the RFNC are the propensities. The probability to be active, as the sum of the probabilities of the four active states, is itself an RFNC of the concentrations of the messengers.

Figure 4 :

 4 Figure 4: Two antagonist allosteric macromolecules producing and reducing a secondary messenger S . The purple macromolecule (top), when active, reduces the secondary messenger S . The orange macromolecule (bottom), when active, produces S .

  * r . Alternatively, we can consider the stochastic Poisson kinetics for this reaction which result in a Poisson distribution of mean k p M * p k r M *

Figure 5 :

 5 Figure5: Two populations of antagonist macromolecules combined to form an elementary module to regulate the production of a secondary messenger S . The 2 populations change their configuration influenced by the 2 same species of primary messengers (x in yellow and y in green). The 2 populations when active influence the production or degradation of a secondary messenger S (in purple).

Figure 6 :

 6 Figure6: Result of the simulations where macromolecule transitions are updated using stochastic simulation and S production is computed using Euler integration. The surface shows the product of ligand concentrations x × y and the wireframe shows the scaled simulated concentration in S .

Figure 7 :

 7 Figure7: Chlamydomonas has an "eye spot" (the red dot on the figure) sensible to illumination and 2 flagella to swim toward or away from light. It swims following an helicoidal trajectory. Consequently, the eye spot scans different directions during a rotation of an alga. According to the successive light measurements coming from the eye spots, the algae either swim straight (synchronized motion of flagella) or makes random changes of direction (desynchronized motion of the flagella). This behavior, even very simple, appears to be very efficient to drive the algae toward the adequately illuminated places where their production of photosynthetic energy is optimal.

  The stationary concentrations of the messengers encode for the initial odds (O (L 1 ) and O (L 2 )), the intermediary results (O (L 1 ) O (L 2 ), O (L 1 ) + O (L 2 ) and 1 + O (L 1 ) + O (L 2 )) and the final result (O (G)).

Figure 8 :

 8 Figure 8: A 4 building blocks cascade to solve a phototaxis problem. The cascade takes as inputs 2 messengers with concentrations O (L1) (green) and O(L 2 ) (orange). The top building block produces a secondary messenger S 1 (yellow) with stationary concentration O (L 1 ) O (L 2 ). The bottom left building block produces a secondary messenger S 2 (blue) with stationary concentration O (L 1 ) + O (L 2 ). The bottom middle building block produces a secondary messenger S 3 (red) with concentration 1 + O (L 1 ) + O (L 2 ). Finally, the right building block is activated by messengers S 1 and S 3 and produce as output the messenger G (purple) with concentration O (G) = O(L 1 )O(L 2 )1+O(L 2 )+O(L 1 ) .

Table 1 :

 1 Propensities for product. Only the non-null propensities are represented.

Table 2 :

 2 Propensities for sum. Only the non-null propensities are represented.

Of course, biochemistry imposes for real biochemical cascades numerous constraints on the value of these parameters that we do not consider here.

Acknowledging the efficiency of probabilistic reasoning in accounting for a large variety of perceptive reports or motor behaviors, one of the main scientific challenges is to explicitly demonstrate that the brain, and more generally bio-1. We consider a small volume (order of magnitude: 1µm 3 ) of cell cytoplasm in which thermal diffusion ensures homogeneous concentrations of messengers at the considered time scale (in the range 1ms to 1s). 2. We consider one or several populations of allosteric macromolecules with a fixed concentration but variable conformations. 3. We consider one or several messengers with a single conformation but varying concentrations. 4. We consider the conformational changes of the macromolecules, which control the concentrations of the messengers and reciprocally, the concentrations of the messengers, which control the conformational changes of the macromolecules.