This Article 
 Bibliographic References 
 Add to: 
Component-Based Modeling and Reachability Analysis of Genetic Networks
May/June 2011 (vol. 8 no. 3)
pp. 672-682
Gregor Gössler, INRIA Grenoble, Rhone-Alpes
Genetic regulatory networks usually encompass a multitude of complex, interacting feedback loops. Being able to model and analyze their behavior is crucial for understanding their function. However, state space explosion is becoming a limiting factor in the formal analysis of genetic networks. This paper explores a modular approach for verification of reachability properties. A framework for component-based modeling of genetic regulatory networks, based on a modular discrete abstraction, is introduced. Then a compositional algorithm to efficiently analyze reachability properties of the model is proposed. A case study on embryonic cell differentiation involving several hundred cells shows the potential of this approach.

[1] G. Batt, D. Bergamini, H. de Jong, H. Garavel, and R. Mateescu, "Model Checking Genetic Regulatory Networks Using GNA and CADP," Proc. Spin Workshop (SPIN '04), pp. 158-163, 2004.
[2] G. Bernot, J.-P. Comet, A. Richard, and J. Guespin, "Application of Formal Methods to Biological Regulatory Networks: Extending Thomas' Asynchronous Logical Approach with Temporal Logic," J. Theoretical Biology, vol. 229, no. 3, pp. 339-348, 2004.
[3] G. Bernot and F. Tahi, "Behaviour Preservation of a Biological Regulatory Network when Embedded into a Larger Network," Fundamenta Informaticae, vol. 91, nos. 3/4, pp. 463-485, 2009.
[4] H. Busch, W. Sandmann, and V. Wolf, "A Numerical Aggregation Algorithm for the Enzyme-Catalyzed Substrate Conversion," Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '06), pp. 298-311, 2006.
[5] N. Chabrier and F. Fages, "Symbolic Model Checking of Biochemical Networks," Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '03), 2003.
[6] C. Chaouiya, E. Remy, P. Ruet, and D. Thieffry, "Qualitative Modelling of Genetic Networks: From Logical Regulatory Graphs to Standard Petri Nets," Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN '04), J. Cortadella and W. Reisig, eds., pp. 137-156, 2004.
[7] J.-P. Comet, H. Klaudel, and S. Liauzu, "Modeling Multi-Valued Genetic Regulatory Networks Using High-Level Petri Nets," Proc. Int'l Conf. Application and Theory of Petri Nets (ICATPN '05), G. Ciardo and P. Darondeau, eds., pp. 208-227, 2005.
[8] T. Dang, C.L. Guernic, and O. Maler, "Computing Reachable States for Nonlinear Biological Models," Proc. Seventh Int'l Conf. Computational Methods in Systems Biology (CMSB '09), pp. 126-141, 2009.
[9] H. de Jong, "Modeling and Simulation of Genetic Regulatory Systems: A Literature Review," J. Computational Biology, vol. 9, no. 1, pp. 69-105, 2002.
[10] H. de Jong, J. Geiselmann, C. Hernandez, and M. Page, "Genetic Network Analyzer: Qualitative Simulation of Genetic Regulatory Networks," Bioinformatics, vol. 19, no. 3, pp. 336-344, 2003.
[11] H. de Jong, J.-L. Gouzé, C. Hernandez, M. Page, T. Sari, and J. Geiselmann, "Qualitative Simulation of Genetic Regulatory Networks Using Piecewise-Linear Models," Bull. Math. Biology, vol. 66, pp. 301-340, 2004.
[12] F. Fages and S. Soliman, "Abstract Interpretation and Types for Systems Biology," Theoretical Computer Science, vol. 403, no. 1, pp. 52-70, 2008.
[13] J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu, "CADP: A Protocol Validation and Verification Toolbox," Proc. Int'l Conf. Computer Aided Verification (CAV '96), R. Alur and T.A. Henzinger, eds., pp. 437-440, 1996.
[14] A.F. Filippov, Differential Equations with Discontinuous Righthand Side. Springer, 1988.
[15] R. Ghosh, A. Tiwari, and C. Tomlin, "Automated Symbolic Reachability Analysis; with Application to Delta-Notch Signaling Automata," Proc. Int'l Conf. Hybrid Systems: Computation and Control (HSCC '03), O. Maler and A. Pnueli, eds., pp. 233-248, 2003.
[16] R. Ghosh and C. Tomlin, "Lateral Inhibition through Delta-Notch Signaling: A Piecewise Affine Hybrid Model," Proc. Int'l Conf. Hybrid Systems: Computation and Control (HSCC '01), M. Di Benedetto and A. Sangiovanni-Vincentelli, eds., pp. 232-246, 2001.
[17] R. Ghosh and C. Tomlin, "Symbolic Reachable Set Computation of Piecewise Affine Hybrid Automata and Its Application to Biological Modeling: Delta-Notch Protein Signaling," IEE Trans. Systems Biology, vol. 1, no. 1, pp. 170-183, June 2004.
[18] A. Girard, "Reachability of Uncertain Linear Systems Using Zonotopes," Proc. Int'l Conf. Hybrid Systems: Computation and Control (HSCC '05), pp. 291-305, 2005.
[19] L. Glass and S.A. Kauffman, "The Logical Analysis of Continuous, Non-Linear Biochemical Control Networks," J. Theoretical Biology, vol. 39, no. 1, pp. 103-129, 1973.
[20] G. Gössler, "Component-Based Design of Heterogeneous Reactive Systems in prometheus," Research Report 6057, INRIA, 2006.
[21] G. Gössler, "Compositional Reachability Analysis of Genetic Networks," Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '06), C. Priami, ed., pp. 212-226, 2006.
[22] G. Gössler and J. Sifakis, "Component-Based Construction of Deadlock-Free Systems (Extended Abstract)," Proc. Ann. Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS '03), 2003.
[23] J.-L. Gouzé and T. Sari, "A Class of Piecewise Linear Differential Equations Arising in Biological Models," Dynamical Systems, vol. 17, no. 4, pp. 299-316, 2003.
[24] L.H. Hartwell, J.J. Hopfield, S. Leibler, and A.W. Murray, "From Molecular to Modular Cell Biology," Nature, vol. 402 (supplement), pp. C47-C52, 1999.
[25] H. Kitano, "Looking beyond the Details: A Rise in System-Oriented Approaches in Genetics and Molecular Biology," Current Genetics, vol. 41, pp. 1-10, 2002.
[26] A.G. Gonzalez, A. Naldi, L. Sánchez, D. Thieffry, and C. Chaouiya, "GINsim: A Software Suite for the Qualitative Modelling, Simulation and Analysis of Regulatory Networks," Biosystems, vol. 84, no. 2, pp. 91-100, 2006.
[27] G. Marnellos, G.A. Deblandre, E. Mjolsness, and G. Kintner, "Delta-Notch Lateral Inhibitory Patterning in the Emergence of Ciliated Cells in Xenopus: Experimental Observations and a Gene Network Model," Proc. Pacific Symp. Biocomputing (PSB '00), vol. 5, pp. 326-337, 2000.
[28] A. Naldi, D. Thieffry, and C. Chaouiya, "Decision Diagrams for the Representation and Analysis of Logical Models of Genetic Networks," Proc. Int'l Conf. Computational Methods in Systems Biology (CMSB '06), M. Calder and S.Gilmore, eds., pp. 233-247, 2007.
[29] C. Piazza, M. Antoniotti, V. Mysore, A. Policriti, F. Winkler, and B. Mishra, "Algorithmic Algebraic Model Checking I: Challenges form Systems Biology," Proc. Int'l Conf. Computer Aided Verification (CAV '05), pp. 5-19, 2005.
[30] W. Reisig, Petri Nets: An Introduction. Springer, 1985.
[31] O. Resendis-Antonio, J.A. Freyre-González, R. Menchaca-Méndez, R.M. Gutiérrez-Ríos, A. Martínez-Antonio, C. Avila-Sánchez, and J. Collado-Vides, "Modular Analysis of the Transcriptional Regulatory Network of E. coli," Trends in Genetics, vol. 21, no. 1, pp. 16-20, 2005.
[32] D. Ropers, V. Baldazzi, and H. de Jong, "Model Reduction Using Piecewise-Linear Approximations Preserves Dynamic Properties of the Carbon Starvation Response in Escherichia coli," IEEE/ACM Trans. Computational Biology and Bioinformatics, vol. 8, no. 1, pp. 166-181, Jan./Feb. 2011.
[33] R. Thomas, "Boolean Formalisation of Genetic Control Circuits," J. Theoretical Biology, vol. 42, pp. 565-583, 1973.
[34] R. Thomas and R. d'Ari, Biological Feedback. CRC Press, 1990.
[35] D.M. Wolf and A.P. Arkin, "Motifs, Modules and Games in Bacteria," Current Opinion in Microbiology, vol. 6, pp. 125-134, 2003.
[36] V. Wolf, "Modelling of Biochemical Reactions by Stochastic Automata Networks," Electronic Notes in Theoretical Computer Science, vol. 171, no. 2, pp. 197-208, July 2007.

Index Terms:
Genetic regulatory network, discrete abstraction, component model, formal verification, reachability, modularity.
Gregor Gössler, "Component-Based Modeling and Reachability Analysis of Genetic Networks," IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol. 8, no. 3, pp. 672-682, May-June 2011, doi:10.1109/TCBB.2010.81
Usage of this product signifies your acceptance of the Terms of Use.