François Fages
email: francois.fages@inria.fr

Sylvain Soliman
email: sylvain.soliman@inria.fr

Abstract Interpretation and Types for Systems Biology

Keywords: SBML, type inference, hierarchy of semantics, ordinary differential equations, Markov chains

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

Systems biology aims at elucidating the high-level functions of the cell from their biochemical basis at the molecular level [START_REF] Ideker | A new approach to decoding life: Systems biology[END_REF]. A lot of work has been done for collecting genomic and post-genomic data and making them available in databases [START_REF] Ashburner | Gene ontology: tool for the unification of biology[END_REF][START_REF] Kanehisa | KEGG: Kyoto encyclopedia of genes and genomes[END_REF], and for organizing the knowledge on pathways and interaction networks into models of cell metabolism, signaling, cycle, apoptosis, etc. now published in model repositories (e.g. http://biomodels.net/). Furthermore the Systems Biology Markup Language (SBML) [START_REF] Hucka | The systems biology markup language (SBML): A medium for representation and exchange of biochemical network models[END_REF] provides a common exchange format for reaction models, which is nowadays supported by the majority of modeling tools [START_REF] Hlavacek | Rules for modeling signal-transduction systems[END_REF][START_REF] Soliman | CMBSlib: a library for comparing formalisms and models of biological systems[END_REF].

Models of biological processes are built with two somewhat contradictory perspectives that are worth clarifying. The first perspective is a perspective of knowledge representation. In this perspective, the more concrete the better: models aim at gathering in a consistent way current knowledge on particular systems, and at representing the interactions participating in a system with the maximum of details. The second perspective for building models is to make predictions and answer particular questions about a system. Yet in this perspective, the more abstract the better: models for making predictions should get rid of useless details and should represent the minimum information that is sufficient for answering the questions at hand; the minimum the information the more powerful and efficient the tools available.

One way to reconcile these two perspectives is to put more focus on the issue of abstraction in systems biology, and to develop not only models but also their relationships to other models at different abstraction levels. In this paper we propose a formal ground for this issue by transposing the concepts of abstract interpretation and types borrowed from programming theory to systems biology. Abstract interpretation is a theory of abstraction, introduced by Cousot and Cousot in [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] as a framework for reasoning about programs, their semantics [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF], and for designing static analyzers, among which type inference systems [START_REF] Cousot | Types as abstract interpretation[END_REF]. Type checking and type inference are important concepts and methods in programming languages and software engineering [START_REF] Cardelli | Typeful programming[END_REF]. Type checking is a way to ensure some level of consistency, depending on the type system, in large programs and in complex assemblies of software components. Type inference provides powerful static analyzes of pre-existing programs without types, and facilitates the use of type systems by freeing the user from entering type information.

In this paper, we investigate the application of these concepts to systems biology formalisms. More specifically, we consider the Systems Biology Markup Language SBML [START_REF] Hucka | The systems biology markup language (SBML): A medium for representation and exchange of biochemical network models[END_REF] and the Biochemical Abstract Machine BIOCHAM [START_REF] Calzone | BIOCHAM: An environment for modeling biological systems and formalizing experimental knowledge[END_REF][START_REF] Fages | Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM[END_REF] with its differential, stochastic, discrete and boolean semantics [START_REF] Calzone | Machine learning biochemical networks from temporal logic properties[END_REF][START_REF] Fages | From syntax to semantics in systems biology -towards automated reasoning tools[END_REF]. We first show how these different semantics can be formally related by simple Galois connections, as required in the theory of abstract interpretation, with the noticeable exception of the differential semantics that is discussed with some details.

Then we study three type systems:

(1) one for checking or inferring the protein functions in a reaction model, [START_REF] Borghans | Complex intracellular calcium oscillations: a theoretical exploration of possible mechanisms[END_REF] one for checking or inferring the activation and inhibition effects in a reaction model, (3) and another one for checking or inferring the topology of compartments or locations in reaction models with space considerations.

We show that the framework of abstract interpretation elegantly applies to the formalization of these type abstractions, and to the implementation of linear or quadratic time complexity type checking as well as type inference algorithms. Furthermore, when comparing the inference of the activation and inhibition effects from the syntax of the reaction rules with their inference from the differential semantics, we show a theorem of independence of the graph of activation and inhibition effects from the kinetic expressions, under general conditions.

Through some examples of reaction models coming from the BioModels and BIOCHAM repositories [START_REF] Soliman | CMBSlib: a library for comparing formalisms and models of biological systems[END_REF], we show that the analysis of biochemical models by type inference provides accurate and useful information. Interestingly, we show that such a mathematical formalization of abstractions commonly used in systems biology already provides some guidelines for the extensions of biochemical reaction rule languages.

2 Preliminaries on Abstract Interpretation, Type Checking and Type Inference

Domains, Abstractions and Galois Connections

In the algebraic setting of abstract interpretation, a domain is a lattice L( , ⊥, , , ) defined by a partial order (L, ), where ⊥ and , elements of L and , , binary operators on L, respectively denote the least element, the greatest element, the least upper bound and the greatest lower bound. Intuitively, the partial ordering represents the information loss: the lesser the more informative, the greater the bigger loss of information.

As it is often the case in program analysis, the concrete domain and the abstract domains considered for analyzing biochemical models, will be powersets, i.e. set lattices P(S)(⊆, ∅, S, ∪, ∩) ordered by inclusion, with the empty set as ⊥ element, and the base set S as element. For instance, in the syntactical domain of reaction rule sets ordered by inclusion, the base set of all possible reactions makes all behaviors possible and thus contains no information, while the empty set is the most precise in this information ordering.

An abstraction is formalized by a Galois connection between a concrete domain C and an abstract domain A, as follows [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]:

Definition 1 A Galois connection C -→ α ←-γ A between two lattices (C, C
) and (A, A ) is defined by an abstraction function α : C → A, and a concretization function γ : A → C, that are monotonic:

• ∀ c, c ∈ C : c C c ⇒ α(c) A α(c ), • ∀ a, a ∈ A : a A a ⇒ γ(a) C γ(a ),
and are adjoint:

• ∀c ∈ C, ∀a ∈ A : c C γ(a) ⇔ α(c) A a.
For any Galois connection, we have the following properties:

(1) γ • α is extensive (i.e. c C γ • α(c)) and represents the information lost by the abstraction (2) α • γ is contracting (i.e. α • γ(a) A a) (3) γ • α is the identity iff γ is onto iff α is one-to-one (4) α preserves , and γ preserves [START_REF] Cardelli | Typeful programming[END_REF] If γ • α is the identity, the abstraction α loses no information, and C and A are isomorphic from the information standpoint (although α may be not onto and γ not one-to-one). It is equivalent in the definition of Galois connections to replace the condition of adjointness by conditions 1 and 2, or by condition 5 which also entails the monotonicity of γ.

γ(a) = max α -1 (↓ a) = α -1 (↓ a) (6) α(c) = min γ -1 (↑ c) = γ -1 (↑ c) (7)
Furthermore we shall use the fact that in powerset domains, the pointwise extension of any function from the base set of the concrete domain to the abstract domain forms a Galois connection: Lemma 2 Let C and A be two sets, and α : P(C) -→ P(A) be a function such that α(c) = e∈c α({e}). Then the function γ(a) = ∪α -1 (↓ a) forms a Galois connection P(C) -→ α ←γ P(A) between (P(C), ⊆) and (P(A), ⊆).

Proof. We show that α is monotonic and γ(a) = max α -1 (↓ a).

The monotonicity of α is immediate since if c ⊆ c we have c i ∈c α({c i }) ⊆

c i ∈c α({c i }).
Now, let us consider c = γ(a) = ∪α -1 (↓ a), we need to prove that c ∈ α -1 (↓ a), i.e. α(c) ∈↓ a. We know that α(c) = e∈c α({e}) = e∈∪α -1 (↓a) α({e}). For each e in ∪α -1 (↓ a) there exists d ∈ P(C) such that e ∈ d and α(d) ⊆ a, therefore α({e}) ⊆ a. Hence e∈∪α -1 (↓a) α({e}) ⊆ a and thus α(c) ⊆ a. 2

In this paper, we will consider the syntactical domain of reaction models ordered by the inclusion of rule sets as concrete domain, and four semantical domains for respectively:

• the stochastic semantics, in which the reaction rules are interpreted by a continuous time Markov chain; • the discrete semantics, in which the rules are interpreted by a Petri net;

• the boolean semantics, in which the rules are interpreted by a boolean asynchronous transition system; • and the differential semantics, in which the rules are interpreted by a system of ordinary differential equations.

We will show in Sect. 3 that, with the noticeable exception of the differential semantics, all these domains are formally related by simple Galois connections.

Type Checking and Type Inference by Abstract Interpretation

Types provide further abstractions for reasoning about programs. In the setting of abstract interpretation, a type system A for a concrete domain C is

nothing but a Galois connection C -→ α ←-γ A.
The type inference problem is, given a concrete element x ∈ C (e.g. a reaction model), to compute α(x) (e.g. the protein functions that can be inferred from the reactions). The type checking problem is, given a concrete element x ∈ C and a typing y ∈ A (e.g. a set of protein functions), to determine whether x C γ(y) (i.e. whether the reactions are compatible with the information given on the protein functions) which is equivalent to α(x) A y (i.e. whether the given typing contains the inferred types).

Most of the type systems considered in this paper will be implemented with type checking and type inference algorithms that basically browse the set of reactions, and check or collect the type information for each rule or pair of rules independently, thus in linear time or quadratic time respectively.

In this paper, we will consider three abstract domains for types:

• one for protein functions, where molecules are abstracted into categories such as kinases and phosphatases (Sect. 4), • one for the influence graph, where the biochemical reaction rules are abstracted by binary relations of activation and inhibition between molecular species (Sect. 5), • and one for location topologies, where reaction and transport rules are abstracted by retaining only the neighborhood information between locations (Sect. 6).

These domains will be defined by abstractions from the syntactical domain of reaction models. The syntactical domain indeed suffices to define the abstractions necessary for these analyses. It is worth noting that a similar situation also occurs in program analysis when the syntax of programs captures enough of the semantics for the needs of the analysis. For the analysis of influences between species, we will compare in section 5 the results obtained by abstraction from the syntactical domain, with the information obtained by abstraction from the differential semantics.

3 Domains for Reaction Models and Hierarchy of Semantics

Syntactical Domain of Reaction Models

Following SBML and BIOCHAM conventions, a model of a biochemical system is a set of reaction rules of the form e for l => r where l is a multiset of molecule names given with stoichiometric coefficients, called a solution, r is the transformed solution, and e is a kinetic expression, i.e. a positive arithmetic expression on the concentrations of the molecules in i (plus possibly of some other molecules that have for instance an inhibitory effect on the reaction).

We will use the BIOCHAM operators + and * to denote solutions as 2*A + B, as well as the syntax of catalyzed reactions e for 2*A+B =[C]=> D as an abbreviation for e for 2*A+B+C => C+D. By abuse of notation, assuming a finite set of molecules M, we shall also see a solution l as an |M|-dimensional vector of integers, and will denote by l(A) the stoichiometric coefficient of A in solution l.

Formally, the concrete domain of reaction models is the powerset of all possible reaction rules ordered by set inclusion :

Definition 3 Given a finite set M of molecule names, the universe of reactions is the set of rules R = {e for l => r | e is a kinetic expression, and l and r are solutions of molecules in M}.

The concrete domain D R = (P(R), ⊆) of reaction models is the power-set of reaction rules ordered by inclusion.

Note that in this domain, the composition of two reaction models is naturally the union of the sets of reactions. A reaction appearing in two reaction sets is thus not duplicated when composing two models by set union.

In the SBML exchange format, no particular semantics is defined, and this syntactical domain is the natural one to consider. In BIOCHAM, reaction models are interpreted under four semantics that correspond to four different abstraction levels : the boolean semantics, the discrete semantics, the differential semantics and the stochastic semantics [START_REF] Calzone | Machine learning biochemical networks from temporal logic properties[END_REF][START_REF] Fages | From syntax to semantics in systems biology -towards automated reasoning tools[END_REF]. In the following subsections, we formalize these semantical domains and study their formal relationship by Galois connections within a hierarchy of semantics.

It is worth noting that in the context of programming languages, it is not usual (and generally not possible) to include the syntactical domain ordered y set inclusion within the hierarchy of semantics. It is possible here however for the rule-based language of reactions, and should be possible as well for other rule-based languages in which programs can be ordered by set inclusion, like Prolog for instance [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF].

Stochastic Semantics

The most realistic interpretation of biochemical reaction models is provided by the stochastic semantics. In that semantics, a reaction model is interpreted as a (continuous time) Markov chain, and the kinetic expressions as transition rates. This interpretation is correct w.r.t. the Master Chemical Equation if we suppose that the reactions happen in a well stirred environment (i.e. "instantaneous" diffusion) with constant pressure, temperature and volume [START_REF] Daniel | Exact stochastic simulation of coupled chemical reactions[END_REF].

For a given volume V k of the location where the compound x k resides, a concentration

C k for x k is translated into a molecule number N k = C k ×V k ×N A ,
where N A is Avogadro's number. A state in the stochastic semantics will be a vector of integers indicating the numbers of molecules for each species.

Formally, given a fixed finite set M of molecule names, the stochastic transition semantics is defined by the following domain :

Definition 4 Let a discrete state be a vector of positive integers of dimension |M|. The universe S of stochastic transitions is the set of triplets (S, S , τ ) where S and S are discrete states and τ ∈ R + is a weight. The domain D S = (P(S), ⊆) of stochastic transition models is the power-set of stochastic transitions ordered by inclusion.

Note first that discrete states have the same mathematical structure as solutions in reaction rules, and can both be represented by |M|-dimensional vectors of positive integers. In the following, we will identify states and solutions and will sum them (see definition of S → i S below and theorem 13).

Note also that in a stochastic transition model s, there can be more than one transition from one state to another one, labelled with different real numbers.

We define the weight in s of a transition from state S i to S j as the sum of the weights τ ij = (S i ,S j ,τ )∈s τ .

Now, an element s of the domain precisely defines a Markov chain where the probability p ij of having a transition from state S i to state S j is obtained by normalizing the transition weights into

p ij = τ ij k τ ik
. Then the transition time can be computed as usual. Stochastic simulation techniques like Gillespie's algorithm [START_REF] Daniel | General method for numerically simulating stochastic time evolution of coupled chemical-reactions[END_REF] compute realizations of the processes described by models in the stochastic domain, where random variables range over the probability and the time of transition. The results of those simulations are generally noisy versions of the simulation obtained by the interpretation of the reaction rules by a system of ordinary differential equations (see section 3.5). However, in models with for instance, very few molecules of some kind, qualitatively different behaviors may appear in the stochastic simulation, and thus justify the recourse to that semantics in such cases. A classical example is the model of the lambda phage virus [START_REF] Gibson | A probabilistic model of a prokaryotic gene and its regulation[END_REF] in which a small number of molecules, promotion factors of two genes, can generate an explosive multiplication (lysis) after a more or less long period of passive wait (lysogeny). Now, in order to relate the stochastic semantics domain to the syntactical domain of reaction rules, let us consider a reaction rule model {e i for l i =>r i } i∈I , and denote by S → i S the fact that rule i fires in state S resulting in state S , i.e. if S ≥ l i (pointwise) and S = S -l i + r i .

In a given state S, the numbers of molecules are fixed integer values and the kinetic expression e i evaluates into a (positive) real valued reaction rate, noted e i (S). This allows us to relate the stochastic transition domain to the syntactical domain of reaction rules by the following Galois connection : Proposition 5 Let α RS : D R → D S be the function associating to a reaction model {e i for l i =>r i } i∈I the stochastic transition model {(S, S , e i (S))

∈ S | i ∈ I, S → i S }. Let γ RS (s) = ∪α RS -1 (↓ s). D R -→ α RS ←-γ RS D S is a Galois connection.
Proof. Simply note that α RS is defined by its union on each rule of the concrete model and apply Lemma 2.

2

Proposition 6 α RS is not one-to-one.

Proof. For instance, the reaction models m1 = { e for A => B} and m2 = m1 ∪ { e for 2*A => A+B} have the same set of stochastic transitions. γ • α is thus not the identity, the information lost by the stochastic abstraction is the elimination of redundant rules in the reaction model.

2
α RS is neither onto as the stochastic transitions obtained from a reaction model enjoy some particular properties, such as for instance the following stability property w.r.t. the number of molecules in the states:

Proposition 7 If two states S 1 , S 2 are such that S 1 ≤ S 2 pointwise, then for any reaction model m and any stochastic transition

(S 1 , S, τ ) ∈ α RS (m), we have (S 2 , (S + S 2 -S 1 ), τ ) ∈ α RS (m), i.e.
all the rules that apply in S 1 apply in S 2 with the same effect.

Proof. By definition of α RS . 2

Corollary 8 α RS is not onto.

Discrete Semantics

The discrete semantics of reaction models can be defined as the trivial abstraction of the stochastic semantics that simply forgets the transition rates.

(d) = ∪α SD -1 (↓ d). D S -→ α SD ←-γ SD D D is a Galois connection.
Proof. Here again it suffices to note that α SD is defined by its union on each single stochastic transition of the concrete model and to apply Lemma 2. 2

Remark that α SD is this time onto, but obviously not one-to-one as the transition rates are simply forgotten.

It is worth noticing that the discrete semantics corresponds to the classical Petri net semantics of reaction models [START_REF] Reddy | Petri net representations in metabolic pathways[END_REF][START_REF] Sackmann | Application of petri net based analysis techniques to signal transduction pathways[END_REF][START_REF] Chaouiya | Petri net modelling of biological networks[END_REF][START_REF] Gilbert | A unifying framework for modelling and analysing biochemical pathways using petri nets[END_REF]. As a consequence, classical Petri net analysis tools can be used for the analysis of reaction models at this abstraction level. For instance, the elementary mode analysis of metabolic networks [START_REF] Schuster | Exploring the pathway structure of metabolism: decomposition into subnetworks and application to mycoplasma pneumoniae[END_REF] has been shown in [START_REF] Zevedei-Oancea | Topological analysis of metabolic networks based on petri net theory[END_REF] to be equivalent to the classical analysis of Petri nets by T-invariants. These analyses apply to the discrete semantics of reaction models in all generality.

Boolean Semantics

The boolean semantics is purely qualitative, and provides somehow the most abstract semantics of reaction models. The boolean semantics forgets the kinetic expressions and interprets the rules as a (non-deterministic) asynchronous transition system but this time over boolean states representing the absence or presence of molecules. It can be applied to large models for which the kinetic data may be not available.

(b) = ∪α DB -1 (↓ b). D D -→ α DB ←-γ DB D B is a Galois connection.
Proof. As before, note that α DB is defined by its union on each transition of the concrete model and apply Lemma 2.

2

In BIOCHAM, the boolean semantics of reaction models is computed by associating to each reaction rule a set of boolean transition rules that take into account the possible complete consumption or not of the reactants by the reaction [START_REF] Chabrier | Symbolic model cheking of biochemical networks[END_REF]. For instance, a reaction rule like A+B=>C+D is interpreted by four boolean transition rules :

• A ∧ B -→ A ∧ B ∧ C ∧ D • A ∧ B -→ ¬A ∧ B ∧ C ∧ D • A ∧ B -→ A ∧ ¬B ∧ C ∧ D • A ∧ B -→ ¬A ∧ ¬B ∧ C ∧ D
Given a reaction model R, let us denote by S BB the set of boolean transitions obtained by applying these boolean transition rules to each state. The following theorem shows that the BIOCHAM boolean semantics of reaction models over-approximates the boolean semantics obtained from the quantitative semantics. The non-existence of a behaviour in the BIOCHAM boolean semantics thus entails its non-existence in the quantitative semantics of the rules whatever the kinetic expressions are.

Theorem 13 For any reaction model R, α DB (α SD (α RS (R))) ⊆ S BB .

Proof. Since all our abstractions are defined pointwise, it is enough to prove it for only one rule in R. Let us consider e for l => r. By abuse of notation we will denote by l and r the discrete states corresponding to solutions of same name. We have

α RS (R) = {(S i , S j , e)|S i ≥ l, S j = S i -l + r} and thus α SD (α RS (R)) = {(S i , S j )|S i ≥ l, S j = S i -l + r}, which leads to α DB (α SD (α RS (R))) = {(S i , S j )|S i ≥ l, S j = S i -l + r, S i = α N B (S i ), S j = α N B (S j )}. Since S BB = {(T, T )|T ≥ α N B (l), α N B (r) ∨ (T ∧ ¬α N B (l)) ≤ T ≤ α N B (T ) ∨ α N B (r)
} we can see that the property holds as S i ≥ l implies S i ≥ α N B (l), and since S i ≥ l we have

S j = S i -l + r ⇒ S i -l + r ≤ S j ≤ S i +r ⇒ α N B (S i -l+r) = α N B (r)∨(α N B (S i )∧¬α N B (l)) ≤ S j ≤ α N B (S i +r) = α N B (S i ) ∨ α N B (r). 2
It is worth noticing that this property does not hold for the boolean semantics of reaction models that always assume either incomplete consumption, or complete consumption, like in Pathway Logic [START_REF] Eker | Pathway logic: Symbolic analysis of biological signaling[END_REF] or in boolean Petri nets [START_REF] Gilbert | A unifying framework for modelling and analysing biochemical pathways using petri nets[END_REF]. In these formalisms, the correctness of the boolean interpretation w.r.t. a quantitative interpretation is thus left to the modeler who is in charge of explicitly adding reaction rules for the different cases of consumption of the reactants.

Differential Semantics

The differential semantics of reaction models interprets a set of reaction rules {e i for l i => r i } i=1,...,n over molecular concentration variables {x 1 , ..., x m }, by the following system of Ordinary Differential Equations (ODE):

dx k /dt = n i=1 r i (x k ) * e i - n j=1 l j (x k ) * e j
where r i (x k ) (resp. l i ) is the stoichiometric coefficient of x k in the right (resp. left) member of rule i. Thanks to its wide range of mathematical tools, this semantics is the most commonly used in mathematical biology [START_REF] Segel | Modeling dynamic phenomena in molecular and cellular biology[END_REF].

The study of the relationship between the differential and the stochastic semantics dates back to the seminal work of Boltzmann in the XIXth century who created the domain of statistical physics. In this setting, the differential semantics is obtained from the stochastic semantics by limit operations where the number of molecules tends to the infinity and the time steps tend to zero. under several assumptions such as perfect diffusion.

In the setting of abstract interpretation, the differential semantics is however difficult to formally relate to the previous semantics for several reasons. The differential semantics is a synchronous semantics in the sense that it specifies the evolution of variables in parallel, whereas all the other semantics are asynchronous in the sense that the interleaving semantics is considered where one reaction is fired at a time. Hence the notion of time is not the same in both categories of semantics, having infinitesimal time steps in the differential semantics, and time for one transition in the other semantics. Furthermore the differential semantics is deterministic and produces an average trace, whereas the other semantics produce sets of possible traces representing the competition between reactions.

For these reasons, the differential semantics does not belong to our hierarchy of syntactical, stochastic, discrete and boolean semantics. In section 5, we will come back to it however for comparing the analysis of the influence graph between molecules obtained from the differential semantics, with the one obtained from the syntax of the reaction rules, and for establishing equivalence results under some general conditions on the kinetics.

A Type System for Protein Functions

In this section, we investigate the use of types for formally relating information on the biological function of some proteins to reaction models. For the sake of simplicity, we restrict ourselves to two simple enzymatic functions: kinase and phosphatase. These functions correspond to the action of adding (resp. removing) a phosphate group to (resp. from) a compound with a covalent binding. We do not consider other categories such as protease in degradation rules, nor acetylase and deacetylase in modification rules, etc. This choice is in accordance with the BIOCHAM syntax which permits to mark the sites of a protein where a group is added, with the operator ~, as in P~{p,q} where protein P is modified on its sites p and q, without distinguishing however between phosphorylation, acetylation, methylation, ubiquitination, etc. We thus consider BIOCHAM models containing compounds with different levels of phosphorylation or acetylation, etc. without distinguishing the different forms of modification, and call them phosphorylation by abuse of terminology.

The inference of protein functions in a reaction model is interesting for several reasons. First, the kind of information (kinase activity) collected on proteins can be checked using online databases like for instance GO, the Gene Ontology [START_REF] Ashburner | Gene ontology: tool for the unification of biology[END_REF]. Second, in the context of the machine learning techniques implemented in BIOCHAM for completing or revising a model w.r.t. a temporal logic specification [START_REF] Calzone | Machine learning biochemical networks from temporal logic properties[END_REF], the information that an enzyme acts as a kinase or as a phosphatase drastically reduces the search space for adding reactions, and helps to directly find rules and model revisions that are biologically plausible. The abstraction function from the syntactical domain, α F : D R → D F , associates to a reaction model R the union of the abstractions defined for each single rule and each pair of rules as follows:

Abstract Domain of Protein Functions

α F (A =[B]=> C) = {kinase(B,A)} if C is more phosphorylated than A (i.
e. its set of active phosphorylation sites strictly includes that of A), in which case B has kinase function w.r.t. A;

α F (A + B => D, D => C + B) = {kinase(B,A)} if similarly C is more phos- phorylated than A; α F (A =[B]=> C) = {phosphatase(B,A)} if, on the contrary, A is more phos- phorylated than C; α F (A + B => D, D => C + B) = {phosphatase(B,A)} if A is more phospho- rylated than C.
Note that as the abstraction function is not defined pointwise but also on pairs of reaction rules, the time complexity for computing the set of protein functions from the reactions is quadratic in the number of rules. One can easily check that:

Proposition 15 Let γ F (f ) = ∪α F -1 (↓ f ), D R -→ α F ←-γ F D F is a Galois con- nection.
This typing for protein functions is very precise as it refers to particular molecules. On the other hand, keeping only the kinase or phosphatase function in an unary predicate without the information on the transformed molecules might be too loose. Between these two extreme choices, one could also consider a hierarchical type structure such as the one defined by the following grammar:

τ ::= kinase|phosphatase|kinase(τ )|phosphatase(τ )|T
where T denotes some basic types of proteins, with the subtyping relations kinase(τ ) kinase and phosphatase(τ ) phosphotase. This kind of typing relation stems from models like the MAPK cascade shown in next section where the common denomination for the function of MEK is "MAPK kinase" (i.e. kinase(M AP K)) and that of RAF is "MAPK kinase kinase" (i.e. kinase(kinase(M AP K))). It is worth noting that such typings are supported by type systems already defined for rule based languages as in [START_REF] Fages | Typing constraint logic programs[END_REF], using solvers for subtyping constraints in general ordering structures such as quasilattices [START_REF] Coquery | Subtyping constraints in quasilattices[END_REF] for instance. These considerations are however beyond the scope of this paper and will not be further developed here.

Evaluation Results

MAPK model.

On a simple example of the MAPK cascade originally based on [START_REF] Levchenko | Scaffold proteins may biphasically affect the levels of mitogen-activated protein kinase signaling and reduce its threshold properties[END_REF] and imported into BIOCHAM, the type inference algorithm determines that RAFK, RAF~{p1} and MEK~{p1,p2} have a kinase function; RAFPH, MEKPH and MAPKPH have a phosphatase function; and the other compounds have no function inferred.

If the family of MAPK molecules is given as a basic type, one would moreover infer that the active form of MEK is a MAPKK (a kinase for the MAPK family), and that the active form of RAF is a MAPKKK (a MAPKK kinase).

If we wanted to type-check such a model, we would correctly check all phosphatases but would miss an example of the kinase function of MAPK~{p1,p2}, since its action is not visible in the above model.

Kohn's Map.

Kohn's map of the mammalian cell cycle control [START_REF] Kohn | Molecular interaction map of the mammalian cell cycle control and DNA repair systems[END_REF] has been transcribed in BIOCHAM to serve as a large benchmarking example of 500 species and 800 rules [START_REF] Chabrier-Rivier | Modeling and querying biochemical interaction networks[END_REF]. This example shows that this abstraction scales up efficiently as the computation of influences requires less than one second CPU time (on a PC 1,7GHz) in this model. Here is an excerpt of the output of the type inference, where it was restricted to the unary functions kinase and phosphatase as explained at the end of section 4.1:

cdk7-cycH is a kinase Wee1 is a kinase Myt1 is a kinase cdc25C~{p1} is a phosphatase cdc25C~{p1,p2} is a phosphatase Chk1 is a kinase C-TAK1 is a kinase Raf1 is a kinase cdc25A~{p1} is a phosphatase cycA-cdk1~{p3} is a kinase cycA-cdk2~{p2} is a kinase cycE-cdk2~{p2} is a kinase cdk2~{p2}-cycE~{p1} is a kinase cycD-cdk46~{p3} is a kinase cdk46~{p3}-cycD~{p1} is a kinase cycA-cdk1~{p3} is a kinase cycB-cdk1~{p3} is a kinase cycA-cdk2~{p2} is a kinase cycD-cdk46~{p3} is a kinase cdk46~{p3}-cycD~{p1} is a kinase Plk1 is a kinase pCAF is a kinase p300 is a kinase HDAC1 is a phosphatase
On the other hand in these results, no compound is both a kinase and a phosphatase. The protein cdc25A, cdc25C and HDAC1 are the only phosphatases found in the whole map. The type inference also tells us that the cyclindependant kinases have a kinase function when in complex with a cyclin, which is correct. Finally the acetylases pCAF, p300 and the deacetylase HDAC1 are detected but as expected identified to kinases and phosphatases respectively, since the BIOCHAM syntax does not distinguish between phosphorylation and acetylation.

A Type System for Activation and Inhibitory Influences

Abstract Domain of Influences

Influence networks for activation and inhibition have been introduced for the analysis of gene expression in the setting of gene regulatory networks [START_REF] Thomas | A complex control circuit : regulation of immunity in temperate bacteriophages[END_REF], they basically define graphs where vertices are genes and oriented edges are labelled either with activates or inhibits, representing the supposed regulation of one gene by another one. Such influence networks are in fact an abstraction of complex reaction networks, and can be applied as such to protein interaction networks. However the distinction between the influence network and the reaction network is crucial for the application of Thomas's conditions of multistationarity and oscillations [START_REF] Thomas | A complex control circuit : regulation of immunity in temperate bacteriophages[END_REF][START_REF] Soulé | Graphic requirements for multistationarity[END_REF] to protein interaction networks, and there has been some confusion between the two kinds of networks [START_REF] Markevich | Signaling switches and bistability arising from multisite phosphorylation in protein kinase cascades[END_REF]. Here we precisely define influence networks as an abstraction (a type system) of reaction networks.

α RI (x) = {A activates B | ∃(e i for l i ⇒ r i ) ∈ x, l i (A) > 0 and r i (B) -l i (B) > 0} ∪{A inhibits B | ∃(e i for l i ⇒ r i ) ∈ x, l i (A) > 0 and r i (B) -l i (B) < 0}
In particular, we have the following influences for elementary reactions of complexation, modification, synthesis and degradation:

α RI ({A + B => C}) = { A inhibits B, A inhibits A, B inhibits A, B inhibits B, A activates C, B activates C} α RI ({A = [C] => B}) = { C inhibits A, A inhibits A, A activates B, C activates B} α RI ({A = [B] => }) = { B inhibits A, A inhibits A} α RI ({ = [B] => A}) = { B activates A}
The inhibition loops on the reactants are justified by the negative sign in the differential semantics of the reactions (see theorem 21 of the next section). These loops are however often omitted in the influence graphs considered in the literature, together with some other influences, according to functionality, kinetics and non-linearity considerations [30].

The abstraction function α RI allows us either to type check a reaction model w.r.t. a given influence typing of molecules, or to infer the influence types from the reaction rules. As α RI is defined pointwise, it can be computed very efficiently in linear time, and we have by lemma 2:

Proposition 18 Let γ RI (f ) = ∪α RI -1 (↓ f ), D R -→ α RI ←-γ RI D I is a Galois connection.

Abstraction from the differential semantics of reaction rules

In the differential semantics of a reaction rule model {e i for l i =>r i | i ∈ I} we have ẋk = dx k /dt = n i=1 (r i (x k ) -l i (x k )) * e i . The Jacobian matrix J is formed of the partial derivatives J ij = ∂ ẋi /∂x j , and one can define the domain D J of Jacobians ordered by the pointwise inclusion of codomains. Let us denote by β the mapping from D R to D J that extracts ẋk (by the equation given at the beginning of this paragraph) and hence the Jacobian from the kinetic expressions in the reaction rules.

Definition 19

The differential influence abstraction α J I : D J → D I is the function

α J I (x) = {A activates B | ∂ ẋB /∂x A > 0 in some point of the space} ∪{A inhibits B | ∂ ẋB /∂x A < 0 in some point of the space}
The comparison between the differential influences, represented by the function α J I • β, and the syntactical influences, represented by the abstraction function α RI , requires that the information in the kinetic expressions and in the reaction rules are compatible. This motivates the following definition where, intuitively, the first property forbids the absence of purely kinetic inhibitors not represented in the rules, and the second property enforces that reactants and enzymes do appear in rules where they are used.

Definition 20 In a reaction model x ={e i for l i =>r i | i ∈ I}, we say that a kinetic expression e i is monotonic iff for all molecules x k we have (1) ∂e i /∂x k ≥ 0 in all points of the space, (2) l i (x k ) > 0 whenever ∂e i /∂x k > 0 in some point of the space.

A reaction model x has a monotonic kinetics iff all its reaction rules have monotonic kinetics.

Note that the mass action law kinetics, e i = k * Πx i l i , are monotonic and that Hill's kinetics (of which Michaelis-Menten kinetics are a special case with n = 1) e i = V m * x s n /(K m + x s n ) where V m = k * (x e + x e * x s /K m ) for an enzymatic reaction x s = [x e ] => x p , are also monotonic1 . On the other hand, inhibitions with negative Hill kinetics of the form e i = V m /(K m + x s n ) are not monotonic, and are not reflected in the syntax of the reactants of the rules.

Theorem 21 For any reaction model x with monotonic kinetics,

α J I •β(x) ⊆ α RI (x). Proof. If (A activates B) ∈ α J I • β(x) then ∂ Ḃ/∂A > 0.
Hence there exists a term in the differential semantics, of the form (r i (B) -l i (B)) * e i with ∂e i /∂A of the same sign as r i (B) -l i (B).

Let us suppose that r i (B) -l i (B) > 0 then ∂e i /∂A > 0 and since e i is monotonic we get that l i (A) > 0 and thus that (A activates B) ∈ α RI (x). If on the contrary r i (B) -l i (B) < 0 then ∂e i /∂A < 0, which is not possible for a monotonic kinetics.

If (A inhibits B) ∈ α J I • β(x) then ∂ Ḃ/∂A < 0. Hence there exists a term in the differential semantics, of the form (r i (B) -l i (B)) * e i with ∂e i /∂A of sign opposite to that of r i (B) -l i (B). Let us suppose that r i (B) -l i (B) > 0 then ∂e i /∂A < 0, which is not possible for a monotonic kinetics. If on the contrary r i (B) -l i (B) < 0 then ∂e i /∂A > 0 and since e i is monotonic we get that l i (A) > 0 and thus that (A activates B) ∈ α RI (x).

2

It is worth noticing that even in the simple case of mass action law kinetics, there is no equality between α J I •β and α RI . For instance let x be the following model :

k 1 * A for A => B k 2 * A for = [A] => A
We have α RI (x) = {A activates B, A activates A, A inhibits A}, however Ȧ = (k 2 -k 1 ) * A, hence ∂ Ȧ/∂A can be made always positive or always negative or always null, resulting in the absence from α J I • β(x) of, respectively, A inhibits A, A activates A or both.

Actually in the general case, β is not monotonic since adding rules can compensate an existing rule in the differential expression and eliminate terms in the differential equations. The differential semantics is thus not an abstraction of the reaction models ordered by set inclusion in the formal sense of abstract interpretation. The above case shows that α J I • β applied to the first rule contains A inhibits A, whereas its application to the set of two rules (greater in D R ) may not. A sufficient condition for β to be monotonic is that in the model no kinetic expression can compensate another one in the Jacobian. That is :

∀x i , x j ∃?k s.t. r k (x i ) = l k (x i
) and ∂e k /∂x j = 0. This condition is used in the forthcoming corollary 25. Furthermore, under some hypotheses about the adequateness between the kinetic expressions and the rules, shown to be quite general in the following section, the equality holds between both abstractions.

Definition 22

In a reaction model x ={e i for l i =>r i | i ∈ I}, a kinetic expression e i is strongly monotonic iff for all molecules x k we have

(1) ∂e i /∂x k ≥ 0 in all points of the space, (2) l i (x k ) > 0 iff there exists a point in the space s.t. ∂e i /∂x k > 0 A reaction model x has a strongly monotonic kinetics iff all its reaction rules have a strongly monotonic kinetics.

Note that strongly monotonic implies monotonic.

Proposition 23 Mass action law, Michaelis Menten, and Hill kinetics are strongly monotonic.

Proof.

For the case of Mass action law, the kinetics are of the form:

e i = k i m l=1 x l i (x l ) l
This theorem shows that for standard kinetic expressions, the syntactical influences coincide with the differential influences based on the signs of the coefficients in the Jacobian matrix, when no molecule is at the same time an activator and an inhibitor of the same molecule. The theorem thus provides a linear time algorithm for computing the differential influences in these cases, simply by computing the syntactical influences. It shows also that the graph of differential influences is independent of the kinetic expressions:

Corollary 26 The graph of differential influences of a reaction model of n rules with strongly monotonic kinetics is computable in time O(n) if no molecule is at the same time an activator and an inhibitor.

Corollary 27

The graph of differential influences of a reaction model is independent of the kinetic expressions as long as they are strongly monotonic, if no molecule is at the same time an activator and an inhibitor.

Evaluation Results

MAPK model.

Let us first consider the MAPK signalling model of [START_REF] Levchenko | Scaffold proteins may biphasically affect the levels of mitogen-activated protein kinase signaling and reduce its threshold properties[END_REF]. Fig. 6 depicts the reaction graph as a bipartite graph with round boxes for molecules and rectangular boxes for rules. Fig. 7 depicts the inferred influence graph, where activation (resp. inhibition) is materialized by plain (resp. dashed) arrows. The graph layouts of the figures have been computed in BIOCHAM by the Graphviz suite 2 .

Since this model verifies the hypotheses of corollary 25 we know that abstracting from the kinetics would give the same result.

Interestingly, this influence graph of the MAPK cascade exhibits inhibition feedback loops although in this model, the reaction graph is a pure cascade containing no feedback reaction. The interpretation of these inhibition feedback loops by sequestration in complexes at the different levels of the cascade is analyzed in [START_REF] Ventura | A hidden feedback in signaling cascades is revealed[END_REF]. The possibility to obtain (damped) oscillations in such "cascades" has been observed in [START_REF] Qiao | Bistability and oscillations in the huang-ferrell model of mapk signaling[END_REF] showing the relevance of our automatic analysis in this example.

p53-Mdm2 model.

In the p53-Mdm2 model of [START_REF] Ciliberto | Steady states and oscillations in the p53/mdm2 network[END_REF], the protein M dm2 is localized explicitly in two possible locations: the nucleus and in the cytoplasm, and transport rules are considered. Fig. 2 depicts the reaction graph of the model.

Fig. 1 depicts the inferred influence graph. Note that M dm2 in the nucleus has both an activation and an inhibitory effect on p53 ∼ {u}. This corresponds to different influences in different regions of the space and one can check that the two influences also appear in α J I .

Fig. 3 depicts the core influence graph considered for the logical analysis of this model [30]. In the core influence graph, some influence are neglected, as expected, however some inhibitions, such the inhibitory effect of p53 on M dm2 in the nucleus, are considered while they do not appear in the inferred influence graph. The reason for these omissions is the way the reaction model is written. Some inhibitory effects are indeed expressed in the kinetic expression by subtraction of, or division by, the molecular concentration of some compounds that do not appear in the rule itself. Those non-monotonic inhibitions are thus missed by the type inference algorithm. An example of such a rule is the following one for the inhibition of M dm2 by p53:

macro(p53tot,[p53]+[p53~{u}]+[p53~{uu}]).
(kph*[Mdm2::c]/(Jph+p53tot),MA(kdeph)) for Mdm2::c <=> Mdm2~{p}::c.

Obviously, one cannot expect to infer such inhibitory effects from the reaction rules. Such a situation suggests to extend the syntax of reaction rules in order to indicate the inhibitors of the reaction, in a somewhat symmetric fashion to what is done for catalysts.

Kohn's Map.

On the quite big model of Kohn's map, the type inference of activation and inhibition influences from reaction rules takes less than one second CPU time (on a PC 1,7GHz) for the complete model, showing again the efficiency of the type inference algorithm.

As kinetic data is typically missing for such a large model, the influence analysis from the syntactical domain is the only one available.

A Type System for Location Topologies

To date, models of biochemical systems generally abstract from space considerations. Models taking into account cell compartments and transport phenomena are thus much less common. Nevertheless, with the advent of systems biology computational tools, more and more models are refined with space considerations and transport delays, e.g. [START_REF] Ciliberto | Steady states and oscillations in the p53/mdm2 network[END_REF]. In SBML [START_REF] Hucka | The systems biology markup language (SBML): A medium for representation and exchange of biochemical network models[END_REF] level 1 version 1, locations have been introduced as purely symbolic compartments without precise topology. We show in this section how the topology can be inferred

In the first case (model BIOMD0000000039.xml), three locations are defined: the cytosol, the endoplasmic reticulum and a mitochondria, from the reactions the inferred topology is that the cytosol is neighbor of the two other locations. This correspond exactly to the information obtained from the outside annotations (the cytosol being marked as the outside of the two other locations).

In the second case (models BIOMD0000000043.xml to BIOMD0000000045.xml) we focused on the last model (two-pool) since it is the only one with 4 different locations: the extracellular space, the cytosol and two internal vesiculae.

The location inference produces a topology where the cytosol is neighbor of all other locations. Once again this is correct w.r.t. the outside information provided in the SBML file: both vesiculae have the cytosol as outside location and the cytosol itself has the extracellular space as outside location.

These considerations show that there is some mismatch between the SBML reaction models and the choice of expressing outside vs neighborhood properties of locations. In the perspective of type checking and type inference, neighborhood relations should be preferred as they can be checked, or inferred from the reaction model, whereas the outside relation contain more information that, while helpful for the modeler as meta-data, cannot be handled automatically without abstracting it first in neighbors properties. Note however that the SBML v. 3 effort rather goes in the opposite direction w.r.t. spatial information (see http://sbml.org/wiki/Spatial Features) since it will allow a complete geometrical description of the compartments, which is of course very informative but is not amenable to automatic checking or inference.

Note also that in calculi where the topology of the network evolves, like the Brane calculus [START_REF] Cardelli | Brane calculi -interactions of biological membranes[END_REF] and its derivatives, the outside and inside relationships change much more radically than the neighborhood relationship. For instance an exocytosis followed by an endocytosis might reverse the outside relationship whereas it would not change the neighborhood relation. Moreover, as shown in the second example below the neighborhood relation can easily be applied to cell (or compartment) populations to represent the topology, while defining only one "outside" for each cell makes the topology disappear.

P53/Mdm2.

The first example comes from [START_REF] Ciliberto | Steady states and oscillations in the p53/mdm2 network[END_REF]: a model of the p53/Mdm2 interaction with two locations (see Fig. 2) where the transport between cytoplasm and nucleus is necessary to explain some time delays observed in the mutual repression of these proteins. We restricted the output to the neighborhood between compartments rather than compounds for clarity.

In this precise case, the model as published does not systematically use the volume ratio in the kinetics. The transcription and type-checking of the model showed that if one wanted to keep the background degradation rate of M dm2 (without DNA damage) independent of the location, one obtains different kinetics than those of the published model. In this case a formal transcription in BIOCHAM (or SBML) provided a supplementary model-validation step. ... Note that in this example, as most of the information is in the kinetics of the rules, the analysis of influences should be done with the Jacobian of the differential semantics, instead of the syntactic domain of reaction rules, as described in section 5. However, for the analysis of location topology, the abstraction defined in this section provides the expected result, as depicted in figure 4. This illustrates the fact that lots of published reaction models rely extensively on the ODEs derived from the rules, the rules themselves being not always carefully written, but rather as compact as possible.

Conclusion

We have shown that the framework of abstract interpretation applies, on the one hand, to the organization of major semantics of biochemical reaction rules into a hierarchy of semantics related by abstraction functions, and on the other hand, to the formalization of some further abstractions commonly used in systems biology as type systems. In the three type systems studied in this paper for, respectively, protein functions, activation and inhibitory influences, and location topologies, the analyses are based on static information gained directly from the syntax of reaction rules, without considering their formal semantics, nor their precise dynamics.

It is worth noting that this situation also occurs in program analysis where the syntax of programs may capture a sufficient part of the semantics for many analyses. Here, it is remarkable that such simple analyses already provide useful information on biological models, independently from their dynamics for which different definitions are considered (discrete, continuous, stochastic, etc.).

The formal definition of the influence graph as an abstraction of the reaction model eliminates some confusion that exists in the use of Thomas's conditions [START_REF] Thomas | A complex control circuit : regulation of immunity in temperate bacteriophages[END_REF][START_REF] Soulé | Graphic requirements for multistationarity[END_REF] for the analysis of reaction models [START_REF] Markevich | Signaling switches and bistability arising from multisite phosphorylation in protein kinase cascades[END_REF]. Such a formalization shows also that the influence graphs usually considered in the literature are further abstractions obtained by forgetting some influences, based on non-linearity considerations [START_REF] Thomas | Multistationarity, the basis of cell differentiation and memory[END_REF]. Some inhibitions may also be missing in the inferred influences when they are hidden in the kinetic expressions of the reactions and do not appear explicitly in the reactants. This suggests either to refine the abstraction function to take into account the kinetic expression when possible, or to extend the syntax of reactions in order to make explicit such inhibitory effects, in a symmetric fashion to catalysts for activations. In SBML there is actually an unique symmetrical notion of Modifiers which is not sufficient to infer the influence graph since it does not make any difference between activators and inhibitors.

Furthermore, we have shown that under general monotonicity conditions sat-isfied by standard kinetics, such as the mass action law, Michaelis-Menten or Hill kinetics, the influences inferred from the syntax of reactants and products in the rules, include the influences inferred from the signs of the coefficient of the Jacobian matrix, and the equality holds when no molecule is both an activator and an inhibitor of a same molecule. This shows, perhaps surprisingly, that the Jacobian influences can be easily computed in linear time from the rule syntax, and that they are independent of the precise kinetic expressions under general conditions.

Similarly, the inference of protein functions and of location neighborhood have shown that the static analysis of reaction models by type inference provides both accurate and useful information. They also provide some guidelines for the extensions of biochemical reaction languages, like for instance in BIOCHAM, differentiating phosphorylation from other forms of modifications like acetylation, methylation, ubiquitination, etc. and in SBML, considering neighborhood rather than outside properties, and introducing a syntax for compound modifications.

Although the analyses done from the differential semantics of reaction rules have been compared to the analyses done from the syntax of reaction rules, the differential semantics itself is the only one that has not been related by Galois connections to the other semantics for several reasons explained in the corresponding section of this paper. These difficulties obviously provide an interesting subject for future work, from both the systems biology and the abstract interpretation theory standpoints.

  the composition of two Galois connections is a Galois connection. where ↓ a = {b | b a} and ↑ a = {b | a b}.

Definition 9

 9 The universe D of discrete transitions is the set of pairs of discrete states. The domain D D of discrete transitions is the power-set of discrete transitions ordered by inclusion D D = (P(D), ⊆). Proposition 10 Let α SD : D S → D D be the function associating to a set of stochastic transitions the discrete transitions obtained by projection on the two first components, and γ SD

Definition 11

 11 Let a boolean state be a vector of booleans of dimension |M| indicating the presence of each molecule in the state. The universe B of boolean transitions is the set of pairs of boolean states. The domain D B of boolean transitions is the power-set of boolean transitions ordered by inclusion D B = (P(B), ⊆). This semantical domain is related to the discrete transitions semantics domain by the zero/non-zero abstraction from the integers to the booleans, and its pointwise extension from discrete states to boolean states α N B : N |M| → B |M| . Proposition 12 Let α DB : D D → D B be the function associating to a set of discrete transitions the set of boolean transitions obtained by applying α N B to the discrete states. Let γ DB

Definition 14

 14 Let kinase(A,B) and phosphatase(A,B) be relations in M × M denoting the kinase (resp. phosphatase) function of A on B. The abstract domain of protein functions D F = P({kinase(A,B) | A, B ∈ M} ∪ {phosphatase(A,B) | A, B ∈ M}) is the powerset of these expressions, ordered by inclusion.

Definition 16

 16 The abstract domain of influences is the powerset of the binary relations of activation and inhibition between compounds D I = P({A activates B | A, B ∈ M} ∪ {A inhibits B | A, B ∈ M}), ordered by inclusion. 5.2 Abstraction from the syntax of the reaction rules Definition 17 The influence abstraction α RI : D R → D I is the function

Fig. 1 .Fig. 2 .

 12 Fig. 1. Inferred influence graph of the p53-Mdm2 model

Fig. 3 .

 3 Fig.3. Core influence graph[30].

6. 2 . 3

 23 Delta and Notch Model.The Delta and Notch proteins are crucial to the cell fate in different organisms. A population of neighboring cells is represented through locations, chosen here to be on a square grid. The model of Gosh and Tomlin[START_REF] Ghosh | Lateral inhibition through delta-notch signaling: A piecewise affine hybrid model[END_REF] for the activation and inhibition of Delta and Notch proteins reproduce the salt-and-pepper coloring of the cells corresponding to high Delta-low Notch and low Deltahigh Notch differentiation. This is typical of the Delta-Notch lateral inhibition based differentiation. The signaling pathways are simplified to the extreme to take into account only the direct effect of Delta and Notch expression in the cell and on the neighboring cells, with rules like : biocham: load_biocham('EXAMPLES/locations/notch4n36c.bc'). (if [D::c21]+[D::c23]+[D::c12]+[D::c32] < 0.2 then 0 else ka,MA(kd)) for _ <=> N::c22.(if [N::c22] > 0.5 then 0 else ka,MA(kd)) for _ <=> D::c22.

Fig. 4 .Figure 5

 45 Fig. 4. Delta-Notch square cell grid inferred by α N in a 6x6 model.This example also illustrates a subtlety in the definition of the abstraction function α N . Indeed, it could be tempting to define the abstraction in the following simpler manner :

Fig. 5 .

 5 Fig. 5. Delta-Notch square cell grid inferred by α N in a 6x6 model.

Fig. 6 .Fig. 7 .

 67 Fig. 6. Reaction graph of the MAPK cascade model

x e * x s /K m is the concentration of the enzyme-substrate complex, supposed constant in the Michaelian approximation and x e + x e * x s /K m is thus the total amount of enzyme

http://www.graphviz.org/

Acknowledgement.

We gracefully acknowledge Monika Heiner for interesting discussions on the modeling of biochemical networks with Petri nets. This work benefited from partial support of the Network of Excellence REWERSE of the European Union and of the INRIA ARC MOCA.

with k i > 0 and l i (x l ) ≥ 0. We thus have ∂e i /∂x k = 0 if l i (x k ) = 0 and ∂e i /∂x k = k i * l i (x k ) * x l i (x k )-1 k l =k x l i (x l ) l otherwise, which clearly satisfies [START_REF] Ashburner | Gene ontology: tool for the unification of biology[END_REF] and [START_REF] Borghans | Complex intracellular calcium oscillations: a theoretical exploration of possible mechanisms[END_REF].

In the case of Hill kinetics (of which Michaelis Menten is a subcase), we have:

for the reaction x s + x e => x p + x e and where

) from the steady state approximation. It is obvious that ∂e i /∂x k = 0 for all x k other than x s and x e since they do not appear in e i and one can easily check that with all the constants n, k 1 , k -1 , k 2 strictly positive, both ∂e i /∂x e and ∂e i /∂x s are greater than 0 at some point in the space.

2

Lemma 24 Let x be a reaction model with strongly monotonic kinetics, and A and B be two molecules.

and all e i are monotonic we get that

then all rule such that l i (A) > 0 verify r i (B) -l i (B) ≥ 0 and there is at least one rule for which the inequality is strict. We thus get that ∂ Ḃ/∂A is a sum of positive numbers, amongst which one is such that r i (B) -l i (B) > 0 and l i (A) > 0 which, since x is strongly monotonic, implies that there exists a point in the space for which ∂e i /∂A > 0 thus ∂ Ḃ/∂A > 0 at that point and

For inhibition the same reasoning applies with the opposite sign for the r i (B)l i (B) and thus for the finale partial derivative.

2

This lemma establishes the following equivalence result:

Theorem 25 Let x be a reaction model with strongly monotonic kinetics and where no molecule is at the same time an activator and an inhibitor of the same target molecule, then α RI (x) = α J I • β(x).

from the reaction rules, and checked in different models.

Abstract Domain of Location Topologies

We will here focus on the notion of neighbor that is supposed to represent the fact that two compounds live in two compartments that are next to each other. In SBML level 2, an outside relation can optionally be given for two compartments, stating that one is the outside of the other one. We should have, from our definition, that if A is the outside of B, then any compound living in and any compound living in B are neighbors.

Definition 28

The domain of neighborhood relations D N = P(M × M) is about pairs of molecules. α N : D R → D N is defined by the union of its definition on single rules:

The concretization of a positive neighborhood between two locations is the set of all possible rules linking those compartments, i.e. transport rules or rules influencing one compartment from another one. It describes in some sense the interface between the two locations. The neighborhood relation is inferred in these models imported in BIOCHAM, and then checked consistent with the provided outside relation.

For instance for calcium oscillations, we tried both the Marhl et al. model of [START_REF] Marhl | Complex calcium oscillations and the role of mitochondria and cytosolic proteins[END_REF] and the Borghans et al. model of [START_REF] Borghans | Complex intracellular calcium oscillations: a theoretical exploration of possible mechanisms[END_REF].