ECCB 2002 Poster sorted by: Author | Number

Next | Previous poster (in order of the view you have selected)
Title: Symbolic model checking of biological systems
P20
Chabrier, Nathalie; Fages, François

Nathalie.Chabrier@inria.fr, Francois.Fages@inria.fr
INRIA Rocquencourt, BP 105, F-78153 Le Chesnay Cedex, France.

Model checking is an automatic method for deciding if a circuit, a program or a system, expressed as a concurrent transition system, satisfies a specification or a property, expressed in a temporal logic. A biological system can be modeled as a concurrent transition system, i.e. a triple (S,S0, R) where S is the set of states, S0 is a subset of initial states and R is a relation over SxS. A state is a finite vector of numerical or boolean values expressing the concentrations or simply the presence/absence of molecules. The transition relation is specified by a set of rules condition modification. The temporal evolution of the system is modeled by the transition steps. The different transiton paths model the non-deterministic behavior of the system.

The Computation Tree Logic CTL is a logic for describing properties of computation trees [2]. CTL basically extends first-order logic with both path quantifiers: A "for all transition paths" and E "for some transition path", and temporal operators: F "eventually in the future" and G "always". By duality we have EFf=¬AG¬f and EGf=¬AF¬f for any formula f. DMC is a symbolic model checker based on constraint logic programming [4]. It performs a backward reachability analysis, starting from a constrained state expressing the CTL property to prove, up to the computation of a state belonging to the initial state. We have used DMC to prove properties of a quantitative model of gene interactions [3] and of a qualitative model of the cell cycle [5]. Inageneinteractionnetwork,theconcentrationsofproteins,RNAorothermolecules are modeled by positive real numbers and evolve according to conditional differential equations [3]. In a pedagogical example given in [1], a gene 1 activates the expression of gene 2, but above some threshold, gene 2 inhibits the expression of gene 1. This can be modeled with the two following rules:
y1<0.8 -> x2=x1-0.02x1 + 0.01, y2=y1+0.01x1,
y1>=0.8 -> x2=x1-0.02x1 , y2=y1+0.01x1.
This system is deterministic. A query like "is the concentration of x always less than 0.5?" is expressed by the CTL formula AG(x<0.5)=¬EF(x 0.5). By reasoning backward, DMC instantly proves this property by checking that any predecessor state S1 of a state S2 with x2 0.5 also satisfies x1 0.5, S1 is thus subsumed by state S2 and is not initial. The query AG(x<0.45) is disproved by exhibiting a counter-example with a backward simulation involving 117 states. The query AG(x+y<1.3) is proved in 179 steps. The property AF(AG(x<0.1)) expresses that after some time the concentration of x is always less than 0.1 and is proved with a greatest fixpoint computation.

Our second example modelizes molecular interactions during the cellular cycle [5]. The lack of data concerning the kinetics of the concentrations led us to make a purely qualitative model with boolean variables denoting the presence or absence of molecules or genes. A state is thus a vector of boolean variables denoting the absence or presence in the cell of particular molecules or proteins, noted A, B, C,..., and complexes noted AB, AC,. etc. The transition rules can be classified into four rule schemas:
- Complexation: A1 and B1 -> AB2, two molecules A and B interact to form a complexe AB.
- (De)Phosphorylation: C1 and A1 -> C2 Ap2, a molecule C adds (resp. withdraws) a grouping phosphate on a molecule A which becomes phosphatic.
- Synthesis: G1 -> G2 and A2, an active gene G synthesizes a molecule A.
- Degradation: C1 and A1 -> C2, a molecule C degrades another molecule A.
Our modeling of the cyclin box with transcription and replication [5] involves 416 rules. The states which satisfy EF(¬cyclineA) provide the possible explanations for the disappearance (or diminution) of cycline A in the cell model. The possible causes are its degradation by the complex Skp1-Skp2, its complexation with cdk1 with participation of the complex Cycline H-cdk7, and other complexations. The states which satisfy EF(SL1p) exhibit the different molecules which participate to the phosphorylation of the promoter selectivity factor SL1. The 118 computed states indicate possible states leading to a mitose.

Symbolic model checking methods show some advantages over simulation. Constraint reasoning makes it possible to group large or infinite sets of states into small constrained state expressions which provide formal proofs of safety or liveness properties. In some cases the properties can be checked by computing a fewer number of states than by simulation. It is possible also to reason with infinite sets of initial states finitely represented by constraints. Moreover the proof method applies to non-deterministic systems. For these reasons we believe that, beyond simulation, verification tools such as model checking will be indispensable for querying and validating complex models in systems biology.
[1] A. Bockmayr and A. Courtois. Modeling biological systems in hybrid concurrent constraint programming (poster). In Proc. 2nd Int. Conf. Systems Biology,ICSB'01, Pasadena, CA, 2001.
[2] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
[3] H. de Jong. Modeling and simulation of genetic regulatory systems: A literature review. Journal of Computational Biology, 9(1):69­105, 2001.
[4] G. Delzanno and A. Podelski. Model checking in clp. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems TACAS'99, volume 1579 of LNCS, pages 223­239. Springer-Verlag, January 1999.
[5] K. Khon. Molecular interaction map of the mammalian cell cycle control and dna repair systems. Molecular Biology of Cell, 10(8):703­2734, August 1999.