Vincent Danos

Jérôme Feret

Walter Fontana

Jean Krivine

Interpretation of Cellular Signalling Networks

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

Introduction

Biological signalling pathways are large, natural, quantitative concurrent systems in charge of sending and receiving extra-cellular signals and triggering appropriate responses in the cell -eg differentiation, migration, or growth. They involve multiple proteins, from membrane bound receptors to adapters and relays to transcription factors. As thorough a description as possible of these pathways is key to their understanding and control. Such a task is difficult for a variety of reasons, one being of a purely representational nature. Those networks are highly combinatorial, meaning that their agents can assemble and be modified in a huge number of ways -about   unique complexes for the EGF receptor pathway model we consider later. Usual representations based on reactions between structureless entities must inevitably sample down this combinatorial Abstraction Project (INRIA, CNRS, and École Normale Supérieure) complexity, and obtain models which stand in no clear relation to biological facts and are hard to keep abreast of new developments. Regev et al. have proposed using π-calculus [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF] to avoid the combinatorial explosion besetting differential equations [START_REF] Priami | Application of a stochastic name-passing calculus to representation and simulation of molecular processes[END_REF][START_REF] Regev | Cells as computation[END_REF]. Other process-based languages have been proposed [START_REF] Regev | BioAmbients: an abstraction for biological compartments[END_REF][START_REF] Cardelli | Brane calculi[END_REF][START_REF] Priami | Beta binders for biological interactions[END_REF][START_REF] Danos | Formal molecular biology done in CCS[END_REF]. The rule-based languages κ [START_REF] Danos | Rule-based modelling of cellular signalling[END_REF][START_REF] Danos | Scalable modelling of biological pathways[END_REF][START_REF] Danos | Formal molecular biology[END_REF][START_REF] Danos | Core formal molecular biology[END_REF] and BNG [START_REF] Blinov | Graph theory for rule-based modeling of biochemical networks[END_REF][START_REF] Hlavacek | Rules for Modeling Signal-Transduction Systems[END_REF] bring additional ease in the building and modification of models [START_REF] Danos | Agile modelling of cellular signalling[END_REF].

The object of this paper is to explain and illustrate on a sizable example a method to explore the set of complexes that can be generated by a κ rule set, aka the system's reachable complexes. Although κ models can be run with no prior enumeration of reachable complexes [START_REF] Danos | Scalable modelling of biological pathways[END_REF], a convenient method for describing those can be used to: -detect dead rules (which is useful when developing large models) -coarsen rules (ie get rid of superfluous conditions while preserving the underlying qualitative transition system) -refine rules (eg for kinetic reasons) -determine whether a rule may activate another (which brings down the cost of stochastic simulations [START_REF] Danos | Scalable modelling of biological pathways[END_REF]) -generate the underlying ground system (or a truncated version thereof if too large), and equip it with a differential equation semantics for the purpose of fast calibration of a model on available data (not implemented yet).

The very combinatorial nature of signalling systems manifests itself in that computing reachables by transitive closure is unfeasible for any but the simplest networks. Our method works around this problem by defining a finite interpretation of rule sets. This finitisation is based on an approximation of complexes as sets of radius 1 neighbourhoods, which we call views, and a pair of adjoint maps to break down complexes into views, and recombine views into complexes. Thus one can generate efficiently a superset of the reachable views, and decide whether the corresponding set of complexes is infinite by detecting repeatable patterns (section 3). This begs the question when the reachable views recombine to form exactly the reachable complexes, not just a super-set. This happens when the set of reachables is closed under swap, an operation whereby pairs of edges of the same type can permute their ends (section 4). We call such sets local, and by extension say a model is local if its set of reachables is. The definition of locality for a model is not syntactical, since it is a condition on the set of associated reachables, but one can guarantee locality by placing syntactical restrictions on the model's rule set (section 5). Our EGF receptor network example satisfies that syntactical condition -up to some reachables-preserving transformations-and is local despite its apparent complexity (section 6). This touches on an interesting and more speculative question. Situations can be expressed in κ which have little to do with biological signalling (eg it is straightforward to represent Turing machines). One would like to think, as the EGF example model indicates, that we have delineated a fragment of κ -that of local rule sets-where natural signalling pathways predominantly fall. What that may mean biologically is briefly discussed in the conclusion together with leads for future work.

κ

We first briefly present a simplified core κ using a process-like notation which facilitates the reachability analysis of the next section. This is in contrast with the equivalent graph-theoretical presentation chosen in Ref. [START_REF] Danos | Scalable modelling of biological pathways[END_REF] for the definition of the quantitative (stochastic) semantics.

We suppose given a finite set of agent names A, representing different kinds of proteins; a finite set of sites S, corresponding to protein domains and modifiable residues; a finite set of values V, representing the modified states. The syntax of agents and expressions is given in Fig. 1.

An interface is a sequence of sites with internal and binding states; specifically one writes x λ ι for a site x with internal state ι, and binding state λ. If the binding state is , the site is free; otherwise it is bound. On the other hand, if the internal state is , this means the internal state is left unspecified. In the concrete notation both s are omitted.

An agent is given by a name in A and an interface. A well-formed expression is a sequence of agents such that: -a site name can occur only once in an interface, -a binding state occurs exactly twice if it does at all. We suppose hereafter all expressions to be well-formed.

Sites sharing a same binding state are said to be bound. The structural equivalence ≡ defined as the smallest binary equivalence between expressions that satisfies the rules given in Fig. 2 stipulates that: neither the order of sites in interfaces, nor the order of agents in expressions matters, and that bindings states can be injectively renamed.

Equivalence classes of ≡ are called solutions and one writes [E] for the class of expression E. One says a solution [E] is reducible whenever E ≡ E , E for some non empty expressions E , E . A complex is an irreducible solution.

Complexes and solutions can equivalently be presented graphically. Fig. 3 shows an example for the following expression: Fig. 3. A complex from the EGF receptor pathway: sites correspond to protein domains SH2, SH3, . . . and modifiable amino-acid residues Y317, Y1048, . . . edges correspond to bindings, solid black stands for phosphorylated tyrosine residues. The left hand side E l describes the agents taking part in the event and various conditions on their internal and binding states for the event to actually happen. The right hand side E r describes the rule's effect which is either: -a binding (unbinding): E r (E l ) is obtained by binding two free sites in E l (E r ), -or a modification: E r is obtained by modifying some internal state in E l .

EGF(r 1 ), EGF(r 2 ), EGFR(l 1 , r 3 , Y1048 4 p , Y1148 p ), EGFR(l 2 , r 3 , Y1048 u , Y1148 5 p ), GRB2(SH2 4 , SH3 6 ), SOS(a 6 ), SHC(PTB 5 , Y317 7 p ), GRB2(SH2 7 , SH3) A rule is a pair of expressions E l , E r .
n λ ι |= n λ ι n λ ι [n λr ιr ] = n λr ιr n λ ι |= n λ n λ ι [n λr ] = n λr ι σ |= ∅ σ[∅] = σ s |= s l σ |= σ l s, σ |= s l , σ l s, σ[sr , σr ] = s[sr ], σ[σr ] σ |= σ l N (σ) |= N (σ l ) N (σ)[N (σr )] = N (σ[σr ]) E |= ∅ E[∅] = E a |= a l E |= E l a, E |= a l , E l (a, E)[ar , Er ] = a[ar ], E[Er ]
Note that bindings and unbindings are symmetric, while modifications are self-symmetric.

In order to apply a rule E l , E r to a solution [E], one uses structural equivalence (Fig. 2) to bring the participating agents at the beginning of the expression, with their sites in the same order as in E l , and renames bindings to obtain an equivalent expression E that matches E l (Fig. 4, left). One then replaces E with E [E r ] (Fig. 4,right).

This yields a transition system between solutions defined as

[E] → E l ,Er [E[E r ]] whenever E |= E l .
Note that sites not occurring in E l are not constrained in any way, and that matching only uses structural equivalence on E, not E l .

Our implementation also allows rules for agent creation and deletion. The methods and results presented here can be readily extended to this richer setting. Here is an example of a modification, and a binding (see also Fig. 5):

EGF(r 1 ), EGFR(l 1 , r 2 , Y1148 u ), EGFR(r 2 , l 3 ), EGF(r 3 ) → EGF(r 1 ), EGFR(l 1 , r 2 , Y1148 p ), EGFR(r 2 , l 3 ), EGF(r 3 ) EGF(r 1 ), EGFR(l 1 , r), EGFR(r, l 2 ), EGF(r 2 ) → EGF(r 1 ), EGFR(l 1 , r 3 ), EGFR(r 3 , l 2 ), EGF(r 2 )
3 Reachability

Let Σ denotes the set of all solutions, and Γ be the set of all complexes. Given R a set of rules and S 0 an initial solution, the set of reachable solutions is given as the least fixpoint in ℘(Σ) greater than S 0 , written lfp S0 post, of the map post(X)

:= X ∪ {S | ∃S ∈ X, ∃r ∈ R, S → r S }. Write [F ] ∈ [E] if there is an expression E such that E ≡ F, E . Define the maps α c : ℘(Σ) → ℘(Γ ), γ c : ℘(Γ ) → ℘(Σ) as: α c (X) := {c ∈ Γ | ∃S ∈ X : c ∈ S} γ c (Y ) := {S ∈ Σ | c ∈ S ⇒ c ∈ Y }
The pair α c , γ c form a Galois connection and the set Γ * of reachable complexes is α c (lfp S0 post). The most precise counterpart to post, post c := α c post γ c can be written

post c (X) = X ∪ {c ∈ Γ | ∃[c 1 ], . . . , [c m ] ∈ X ∃r ∈ R ∃S ∈ Σ : [c 1 , . . . , c m ] → r S ∧ c ∈ S}. Clearly Γ * ⊆ lfp αc(S0) post c .
This abstraction is not always exact since it does not take into account the number of occurences of a complex in a solution. In practice rules are rarely asking for many occurrences of a same agent or complex, and it is safe to consider that each kind of agent occurs an unbounded number of time in S 0 .

One thing that does matter in the application is that Γ * may be large (even infinite in case of polymerisation) and this is why we set up now a finite approximation of this set. The idea is to only retain from a solution the information which is local to the agents and which we call agents views (as in Ref. [START_REF] Feret | Dependency analysis of mobile systems[END_REF]). Specifically, we replace each binding state in an expression with its associated typed link, ie the site and agent names of the opposite end of the link, and call β the obtained transformation. An example is:

β(EGF(r 1 ), EGFR(l 1 , r 2 ), EGFR(r 2 , l 3 ), EGF(r 3 )) = EGF(r l.EGFR ), EGFR(l r.EGF , r r.EGFR ), EGFR(l r.EGF , r r.EGFR ), EGF(r l.EGFR )
The syntax of views is given in Fig. 6, and the structural congruence which allows to reorder sites in a view is given in Fig. 7.

Operations on solutions transfer naturally to sequences of views. In particular one can define an abstract transition step between sequences of views (Fig. 8) that tests some conditions over the view relation |= , and either changes the internal state of a site, or adds/removes the appropriate typed links in the binding state of two modified views. Fig. 9 shows the graphical representation (repetitions are omitted) of the phosphorylation and dimerisation abstract rules (Fig. 5).

Thus one may now define the abstraction that collects the set of views that can be built during a computation sequence.

Define ∆ to be the set of views and the map α :

℘(Γ ) → ℘(∆) as α(X) := {[v i ] | ∃[c] ∈ X, β(c) = v 1 , . . . , v n }.
By construction α is a ∪-complete morphism of complete lattices, and has therefore an adjoint concretization γ : ℘(Γ ), defined as γ(Z) = ∪{X ∈ ℘(Γ ) | α(X) ⊆ Z}, which maps a set of views to the set of complexes that can be built from these, and verifies α(X) ⊆ Z iff X ⊆ γ(Z). It is easy to see that α, γ are monotonic, αγ is a lower closure operator (anti-extensive, monotonic, and idempotent), and γα an upper closure operator (extensive, monotonic, and idempotent) [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF].

℘(∆) → n λ ι |= n λ ι n λ ι [n λr ιr ] = n λ r ιr n λ ι |= n λ n λ ι [n λr ] = n λr ι σ |= ∅ σ[∅] = σ s |= s l σ |= σ l s, σ |= s l , σ l s, σ[sr , σr ] = s[sr ] , σ[σr ] σ |= σ l N (σ) |= N (σ l ) N (σ)[N (σr )] = N (σ[σr ] ) r = E l → Er β(E l ) = v 1 l , . . . , v n l β(Er ) = v 1 r , . . . , v n r v i |= v i l [v 1 ], . . . , [v n ] → r [v 1 [v 1 r ] ], . . . [v n [v n r ] ]
Let us consider a couple of examples of upper and lower closure:

γα({[A(a 1 , b 1 )]}) = {[A(a n , b 1 ), . . . , A(a n-1 , b n )]; n ∈ N} αγ({[A(a b.A , b a.A )], [B(a b.A , b a.A )]}) = {[A(a b.A , b a.A )]}
In the first example the upper operator constructs rings of all lengths; in the second one the typed link B(b a.A ) has no corresponding dual typed link A(a b.B ) in the view set, so its view cannot be combined with an other one. 6Define

post v (Z) := Z ∪ {u i ∈ ∆ | ∃v 1 , . . . , v n ∈ Z ∃r ∈ R : v 1 , . . . , v n → r u 1 , . . . , u n }.
This map is a ∪-complete endomorphism and it satisfies post c γ ≤ γ post v for the pointwise ordering. As a consequence, lfp α(Γ0) post v the least fixpoint of post v containing α(Γ 0 ) exists and we can state the soundness of our abstraction as follows: lfp Γ0 post c ⊆ γ(lfp α(Γ0) post v ). Thus the views generated by the abstract system reconstruct, via γ, a superset of the generated complexes. Note that while lfp α(Γ0) post v is certainly finite, its image under γ may not be.

One may wonder how efficient that finite computation is, and how precise. Regarding efficiency, we use decision diagrams [START_REF] Lee | Representation of switching circuits by binary-decision programs[END_REF] to manipulate view sets. To avoid an exponential blow up (the number of views of an agent is exponential in its number of sites), we use 'packing' techniques [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], splitting the interface of agents into smaller subinterfaces, and then considering only relations between states of sites belonging to a common subset. Our syntactic analysis ensures that the result is unchanged. The next section answers accuracy concerns.

Local sets

Say X ⊆ Γ is local if X ∈ Im(γ), or equivalently γα(X) = X. We prove first that for such local sets, the finite interpretation is exact.

Theorem 1. Consider Inv ∈ ℘(Γ ), a set of complexes such that: Γ 0 ⊆ Inv, post c (Inv) ⊆ Inv, and Inv = γα(Inv), then γ(lfp α(Γ0) post v ) ⊆ Inv.

The map post v is not the most precise counterpart of post c , because the relation |= does not require views to be embeddable in complexes. However we shall see below that post v α = αpost c γα which means that post v is the most precise counterpart of post c when applied to abstract elements that are closed with respect to αγ. Assuming this for the moment we can prove Th. 1.

Proof. We first prove post n v α(Γ 0 ) ∈ α(℘(Γ )) and post n v α(Γ 0 ) ⊆ α(Inv): -α(Γ 0 ) ∈ α(℘(Γ )), and Γ 0 ⊆ Inv, so α(Γ 0 ) ⊆ α(Inv); -If Z ∈ α(℘(Γ )) and Z ⊆ α(Inv), then Z = αγ(Z), so post v (Z) = post v αγ(Z), and since

post v α = αpost c γα, post v (Z) = αpost c γ(Z) ⊆ αpost c γα(Inv) = αpost c (Inv) ⊆ α(Inv). Because ℘(∆) is finite, lfp α(Γ0) post v = post n v α(Γ 0 ) for some n, so lfp α(Γ0) post v ⊆ α(Inv), hence γ(lfp α(Γ0) post v ) ⊆ γα(Inv) = Inv.
By setting Inv = lfp Γ0 post c , one gets the immediate corollary:

Corollary 1. If lfp Γ0 post c ∈ γ(℘(Γ )), then lfp Γ0 post c = γ(lfp α(Γ0) post v ).
In words, if lfp Γ0 post c is local, the finite interpretation is exact. Likewise, taking Inv to be the local closure of lfp Γ0 post c , one obtains the slightly more general result that γ(lfp α(Γ0) post v ) is the smallest local set containing lfp Γ0 post c , supposing that closure is itself closed under post c (it does not have to be).

We proceed now to the characterisation of local sets.

We call a swap any of the three transformations over solutions given Fig. 10. Note that swapped links have to be of the same A, a, B, b type. Theorem 2. X ∈ is local iff the set of solutions over X is closed under swaps.

Clearly views are invariant under swaps, which gives the left to right implication. To prove the other implication we introduce an 'assembly grammar' to describe γ(Z) for Z ⊆ ∆. This grammar also allows the enumeration (and the counting) of the elements of γ(Z). It will also help in proving that post v α = αpost c γα by taking Z ∈ Im(α).

The assembly grammar ⇒ Z where E, E stand for hybrid expressions (ie expressions mixing ordinary binding states and typed links), σ, σ for hybrid interfaces, and x is a fresh binding, is given as:

-E ⇒ Z E if E ≡ E -⇒ Z v for v ∈ Z -A(a b.B ι , σ), E ⇒ Z A(a x ι , σ), B(b x ι , σ ), E for B(b a.A , σ ) ∈ Z -A(a b.B ι , σ), B(b a.A ι , σ ), E ⇒ Z A(a x ι , σ), B(b x ι , σ ), E -A(a b.A ι , b a.A ι , σ), E ⇒ Z A(a x ι , b x ι , σ
), E The third clause states that a typed link in a view can be connected to any view taken from Z showing the dual typed link. Similarly, the last two clauses show how dual typed links may be connected to form a link.

We write ⇒ * Z for the transitive closure of ⇒ Z . Say a hybrid expression c embeds in a complex [c * ] if c is the prefix of a hybrid expression E obtained from an expression E ≡ c * by replacing some bindings with their corresponding typed links.

Clearly ⇒ * Z c implies that c is connected, and γ(Z) is the set of all classes [c] such that ⇒ * Z c and c has no typed links. Proof (Th. 2, continued). We want γα(X) ⊆ X, supposing X is closed under swap. It is enough to prove that whenever ⇒ * α(X) c, c embeds in some [c * ] ∈ X. Indeed if c ∈ γα(X) embeds in some [c * ] ∈ X, then c ≡ c * , since c has no typed links. We prove this by induction on ⇒ α(X) : -The base case is by definition of α. Using the proof above for the local set γα(X) obtains a stronger statement:

Theorem 3. If ⇒ * α(X) c
, then c embeds in some c * ∈ γα(X).

One may use the grammar ⇒ Z to obtain either an enumeration or a counting of γ(Z), when Z ∈ Im(α) (which is the one case we are interested in in the application). In general, ⇒ Z has either finitely many rewrite sequences or, by a simple combinatorial argument, there must be a sequence of derivations that form a hybrid expression with a path connecting two instances of a typed link b.B. By Theorem 3, any such sequence can be completed so as to produce a complex (with no typed links), so one can effectively decide whether γ(Z) is infinite (and practically stop the enumeration on derivations showing a repeatable pattern). Note that one may also infer from the same theorem that post v (Z) = αpost c γ(Z) when Z ∈ Im(α) (the equation does not hold in general).

Local rule sets

At this stage, we know that local sets can be exactly counted or enumerated via the abstraction if they are finite, and neatly described if they are not. Say a rule set R is local if given any set of disconnected agents, R generates a local set of complexes. Proposition 1. A rule set R is local if the following holds: -(acyclicity) complexes in γα(Γ * ) are acyclic; -(local tests) rules only test the views of the agents they modify; -(non interference) binding rules do not interfere, that is to say: -whenever A(a ι1 , σ 1 ),

B(b ι2 , σ 2 ) → A(a 1 ι1 , σ 1 ), B(b 1 ι2 , σ 2 ) -and A(a ι3 , σ 3 ), B(b ι4 , σ 4 ) → A(a 1 ι3 , σ 3 ), B(b 1 ι4 , σ 4 ) -then A(a ι1 , σ 1 ), B(b ι4 , σ 4 ) → A(a 1 ι1 , σ 1 ), B(b 1 ι4 , σ 4 )
Before we sketch the proof, let us comment on the acyclicity condition which is the only non syntactical one. Define the contact map of a rule set R, written χ(R), and defined as: a graph with nodes the agent names used in R, with sites those occurring in R, and where sites are connected iff they are bound by some r ∈ R. Note that χ(R) is not a (graphical) solution, since sites can be connected more than once; rather it is a constraint on generated complexes.

Say a complex is compatible with χ(R) if it projects to it. Fig. 11 shows the contact map of an early EGF model, and the complex shown Fig. 3 does project to it.

One can test whether a rule set R is acyclic by inspecting χ(R). Proposition 2. Given R, and Γ 0 compatible with χ(R), if Γ * contains a cyclic complex, then there exists s : Z 2n → S such that for all p ∈ Z n : s(2p), s(2p + 1) belong to the same agent in χ(R), s(2p) = s(2p + 1), and s(2p -1), s(2p) is an edge in χ(R).

In Fig. 11, one sees that the contact map may be cyclic, but every cycle has to use twice the same site, so no complex in this model can be cyclic, provided one picks a compatible initial set of complexes. Note also that the non-interference condition is only concerning binding operations and there is no comparable constraint on unbinding rules. The intuition is that both agents that want to connect have to do it on the sole basis of their views and are not allowed to communicate prior to context. This is reminiscent of synchronisation in CCS [START_REF] Milner | Communication and Concurrency[END_REF]. Suppose that E ≡ c 1 ≡ c 2 , then l 1 , l 2 are connected via a unique path in c 1 (by acyclicity). Suppose they have the same orientation along this path, then [c s 1 ] splits in two components, one of them, call it [d 1 ], containing a cycle; on the other hand, [d 1 ] ∈ γα(Γ * ), which contradicts acyclicity. So l 1 , l 2 must have opposite orientations. Pick a copy of [c 1 ], say [c 1 ], with links l 1 , l 2 ; it is easy to see that swapping (l 1 , l 2 ), and (l 1 , l 2 ) obtains two copies of [c s 1 ], so one can reduce that case to the other one where E ≡ c 1 , c 2 .

So suppose that E ≡ c 1 , c 2 and pick separate traces leading to solutions which contains respectively [c 1 ], and [c 2 ] (there must be some, by definition of Γ * ). Because initial complexes are single agents, both l 1 , l 2 have to be created along those traces; consider the last such event in both traces, say [ Fig. 13. Times refer to a run on a 2GHz Intel Centrino Duo, 2G RAM. We also give the number of complexes obtained by using a non-relational analysis to show the loss of precision. We skip the enumeration step when the set of complexes is too large. Recall the GLO model is explicitly designed to be non local.

All the above models can be shown to be acyclic using their contact maps as shown above for the EGF case. Furthermore the rule sets in these models can be made to verify the other assumptions of Prop. 1. This is done by using two transformations on the rule set.

The first transformation is decontextualization. One groups rules that perform the same action. Then, for each group, one computes a Boolean encoding of the set of solutions that 1) may match the left hand side of rules and 2) may be reachable -according to the view-based analysis (Section 3). In good cases redundant conditions in left hand side expressions are revealed and one can simplify the rules. This operation of decontextualization is fully automatic and does not modify the transition system (it does change the kinetics of the system when merged rules have different rates but that is not of concern here).

The second transformation of conjugation comes into play to deal with the few non local rules that may remain. One adds rules that are in the transitive closure of the transition system (so that the set of reachable complexes remains the same) and invoke decontextualization again. More precisely, whenever an action can only be applied in a specific context, one looks for sequences of rules that allows to simulate the same action in any other reachable context. This second stage is not automated at the moment.

As noted in the introduction, the use of the view-based abstraction is not limited to proving that complex sets are local. The inverse operation of contextualization where one enumerates extensions of complexes in a rule is also useful to get rid of non-contextual rule involving agent deletions, or to extract ground rules from a rule set. Another noteworthy application is the approximation of causations and conflict relations between events as static relations between rules; that is useful for simulation [START_REF] Danos | Scalable modelling of biological pathways[END_REF], and abstracting those at the level of views accelerates greatly their computation.

Conclusion

Biological signalling networks are large and generate combinatorial and highdimensional transition systems which are computationally unwieldy. We have presented in this paper an abstraction of such systems, as represented as κ rule sets, which is a prerequisite for a certain number of tasks to become feasible. Perhaps the most intriguing finding is that this leads naturally to the definition of a class of local networks, a rather weak fragment of the set of all κ systems, where one would not a priori expect real models to sit. We could prove that previously and independently constructed models actually fall into that class.

Obviously, more examples need to be studied, before one can claim this is the class of natural signalling networks. Suppose however, for the sake of the argument, that biological networks are indeed predominantly local, one wonders why. Our favourite speculation is that a local network can be brought to process signals reasonably well in a variety of circumstances, placing only low demand on the accuracy of the setup (eg kinetic rates), or the reliability of the signal.

One can unfold the hierarchy of classes which has been left implicit in this paper, by investigating larger radii approximations, which would cover a larger class of networks, although we know that no finite radius approximation can cover all cases (see the GLO example). One has to see if a nice characterisation of say 2-local complex sets can be obtained.

Note that there is no need for our views to be of uniform radii, and one could even refine this classification of dimension sets, using collections of non uniform views. Such a theory, which still needs to be developed, would likely characterize the closure and covering properties one needs for soundness. Our present local views would be just one particularly simple instance that is a good computation trade-off between too poor an abstraction (eg that based on discrete coverings) which is fast but retains little information, and the richer ones we just suggested.

Another tempting avenue for future research is to articulate quantitative extensions of those ideas. Specifically, one can use the multiset version of the abstraction map, and derive an approximate differential or stochastic operational model, to be compared with concrete exact simulations. One is looking for a manifestation of locality at the level of quantitative dynamics.

EFig. 1 .

 1 Fig. 1. Syntax.

Fig. 4 .

 4 Fig. 4. Definition of matching |= (left), and replacement (right).

Fig. 5 .

 5 Fig. 5. Receptor 'cross-phosphorylation' (left): site Y1148 is modified (phosphorylation induced by the receptor kinase domain represented as a solid white circle, and inducing a state change represented as a solid black circle); and receptor 'dimerisation' (right): the dotted edge represent binding, both ends of the link are modified.

Fig. 6 .Fig. 7 .

 67 Fig. 6. Syntax for views.

Fig. 8 .Fig. 9 .

 89 Fig. 8. Abstract semantics.

Fig. 10 .

 10 Fig. 10. The main swap involution (top row); if the names A and B are the same, some agents can be identified (bottom row); orientations are shown for clarity.

  -Suppose c is obtained from c 1 by replacing a typed link b.B with a binding to a view v of type B; by induction we have [c * 1 ], and [v * ] ∈ X containing respectively c 1 and v; we can assume that expressions c 1 and v do not share bindings; therein A, a and B, b must be connected to say B , b, and A , a. One can therefore swap the bindings in the expression c * 1 , v * , and connect A, a and B, b; since c 1 is connected, it is contained in the post-swap connected component of A which is in X (because X is closed under swap), and so is c. -Suppose c is obtained from c 1 by fusing two typed links b.B and a.A in two distinct agents; by induction there is [c * 1 ] which embeds c 1 , if A, a, B, b are connected in [c * 1 ] we are done, else consider B , and A as above (those may be the same agent). Again one can swap the bindings in [c * 1 ], and connect A, a and B, b, and their common component after the swap contains c and is in X. -Suppose c is obtained from c 1 by fusing two typed links b.B and a.A within the same agents; by induction there is [c * 1 ] which embeds c 1 , if A, a is connected to A, b we are done, else A, a, A, b are connected in [c * 1 ] to say A , b, A , a (which may belong to the same agent), so one can swap the bindings, and the resulting connected component of A contains c and is in X.

Fig. 11 .

 11 Fig. 11. The early EGF receptor cascade model contact map; some sites can change their internal states (solid black).

  Proof (Prop. 1 sketch). Given [E] a solution of complexes in Γ * , and a swap s between links l 1 , l 2 in [E], one wants to prove that the obtained [E s ] is still a solution of complexes in Γ * . Call [c 1 ], [c 2 ] the connected components of l 1 , l 2 in [E]; clearly, it is enough to prove it in the cases when E ≡ c 1 , c 2 or when E ≡ c 1 ≡ c 2 .

  T 1 ] → r1 [S 1 ], and [T 2 ] → r2 [S 2 ] creating respectively l 1 , and l 2 . By atomicity the views of the agents involved in l 1 , say [A 1 ], [B 1 ], are the same before and after r 1 , except of course for the typed links associated to l 1 ; the same thing holds of [A 2 ], [B 2 ], therefore in [T 1 , T 2 ], one can permute the bindings and apply r 1 to [A 1 ], [B 2 ], and r 2 to [A 2 ], [B 1 ] (by non interference). Using the final condition namely that

		EGF	FGF SBF GLO
	Number of rules	39	42	66	4
	Abstraction time	0.08 s 0.06 s 0.08 s 0.01 s
	Number of complexes	356	79 080	10 19 ∞
	Complex counting time	<0.01 s 0.09 s 0.04 s <0.01 s
	Enumeration time	0.06 s 85 s	*	*
	Number of complexes (non relational analysis) 14 374 709698 10 25 ∞
	Decontextualization time	0.17 s 0.25 s 0.88 s 0.01
	Local (by conjugation)	true	true	true	false

A trickier example is αγ({[A(a, b a.A )], [A(a b.A , b a.A )]}) = {[A(a b.A , b a.A )]}, since a finite chain with a free a must have a free b at the other end.

The models and relevant outputs of the analysis used in this proof are available at www.di.ens.fr/ ~feret/proplx.

A(au), B(au

A(au) ↔ A(ap) A(au), A(ap

Fig. 12. Rule systems tests are local, it is easy to see that all computation steps onward commute to that permutation.

We illustrate now each condition of Prop. 1 in turn. Local tests: consider the initial complexes A(a u ) and B(a u ) and the rules in Non-interference: consider the initial complex A(a u ) and the rules in Fig. 12.(c), A(a 1 u ), A(a 1 u ) is in γα(Γ * )\Γ * ; indeed the rule set does not verify non-interference, since A(a u ) should also be allowed to bind with A(a u ).

In any of the above examples, the finite interpretation could be made exact by suitably extending the agent view radii. In Fig. 12.(d) gives an example which no finite radius approximation can interpret exactly. Indeed it is easy to see that, with A(l, x u , r) as the only initial complex, all generated chains of length > 1 have exactly one A(x p ); whereas any < n radius abstraction α will have A-chains with no A(x p ), and length ≥ 2n in γα(Γ * ). We shall refer to this model as the GLO model in the next section.

Examples

We have considered three examples: -the early EGF receptor pathway model [START_REF] Blinov | A network model of early events in epidermal growth factor receptor signaling that accounts for combinatorial complexity[END_REF], -the early FGF (fibroblast growth factor) receptor pathway model [START_REF] Kwiatkowska | Simulation and verification for computational modelling of signalling pathways[END_REF], -and the EGF model of Ref. [START_REF] Danos | Rule-based modelling of cellular signalling[END_REF]. Those are referred to hereafter as the EGF, FGF, and SBF models. 7 Proposition 3. The sets of reachable complexes in the EGF, FGF and SBF models are local.