[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Formal Cell Biology in Biocham

  • Conference paper
Formal Methods for Computational Systems Biology (SFM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5016))

Abstract

Biologists use diagrams to represent interactions between molecular species, and on the computer, diagrammatic notations are also employed in interactive maps. These diagrams are fundamentally of two types: reaction graphs and activation/inhibition graphs. In this tutorial, we study these graphs with formal methods originating from programming theory. We consider systems of biochemical reactions with kinetic expressions, as written in the Systems Biology Markup Language (SBML), and interpreted in the Biochemical Abstract Machine (Biocham) at different levels of abstraction, by either an asynchronous boolean transition system, a continuous time Markov chain, or a system of Ordinary Differential Equations over molecular concentrations. We show that under general conditions satisfied in practice, the activation/inhibition graph is independent of the precise kinetic expressions, and is computable in linear time in the number of reactions. Then we consider the formalization of the biological properties of systems, as observed in experiments, in temporal logics. We show that these logics are expressive enough to capture semi-qualitative semi-quantitative properties of the boolean and differential semantics of reaction models, and that model-checking techniques can be used to validate a model w.r.t. its temporal specification, complete it, and search for kinetic parameter values. We illustrate this modelling method with examples on the MAPK signalling cascade, and on Kohn’s map of the mammalian cell cycle.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Kohn, K.W.: Molecular interaction map of the mammalian cell cycle control and DNA repair systems. Molecular Biology of the Cell 10, 2703–2734 (1999)

    Google Scholar 

  2. Hucka, M., et al.: The systems biology markup language (SBML): A medium for representation and exchange of biochemical network models. Bioinformatics 19, 524–531 (2003)

    Article  Google Scholar 

  3. Thomas, R., Gathoye, A.M., Lambert, L.: A complex control circuit: regulation of immunity in temperate bacteriophages. European Journal of Biochemistry 71, 211–227 (1976)

    Article  Google Scholar 

  4. Kaufman, M., Soulé, C., Thomas, R.: A new necessary condition on interaction graphs for multistationarity. Journal of Theoretical Biology 248, 675–685 (2007)

    Article  Google Scholar 

  5. Soulé, C.: Mathematical approaches to differentiation and gene regulation. C.R. Biologies 329, 13–20 (2006)

    Article  Google Scholar 

  6. Soulé, C.: Graphic requirements for multistationarity. ComplexUs 1, 123–133 (2003)

    Article  Google Scholar 

  7. Snoussi, E.: Necessary conditions for multistationarity and stable periodicity. J. Biol. Syst. 6, 3–9 (1998)

    Article  MATH  Google Scholar 

  8. Gouzé, J.L.: Positive and negative circuits in dynamical systems. J. Biol. Syst. 6, 11–15 (1998)

    Article  MATH  Google Scholar 

  9. Calzone, L., Fages, F., Soliman, S.: BIOCHAM: An environment for modeling biological systems and formalizing experimental knowledge. BioInformatics 22, 1805–1807 (2006)

    Article  Google Scholar 

  10. Fages, F., Soliman, S., Chabrier-Rivier, N.: Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. Journal of Biological Physics and Chemistry 4, 64–73 (2004)

    Article  Google Scholar 

  11. Hlavacek, W.S., Faeder, J.R., Blinov, M.L., Posner, R.G., Hucka, M., Fontana, W.: Rules for modeling signal-transduction systems. Science STKE 344, 6 (2006)

    Google Scholar 

  12. Soliman, S., Fages, F.: CMBSlib: a library for comparing formalisms and models of biological systems. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 231–235. Springer, Heidelberg (2005)

    Google Scholar 

  13. Fages, F., Soliman, S.: Abstract interpretation and types for systems biology. In: Theoretical Computer Science (to appear, 2008)

    Google Scholar 

  14. Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 68–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Fages, F.: From syntax to semantics in systems biology - towards automated reasoning tools. Transactions on Computational Systems Biology IV 3939, 68–70 (2006)

    Article  MathSciNet  Google Scholar 

  16. Chabrier-Rivier, N., Chiaverini, M., Danos, V., Fages, F., Schächter, V.: Modeling and querying biochemical interaction networks. Theoretical Computer Science 325, 25–44 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Levchenko, A., Bruck, J., Sternberg, P.W.: Scaffold proteins biphasically affect the levels of mitogen-activated protein kinase signaling and reduce its threshold properties. PNAS 97, 5818–5823 (2000)

    Article  Google Scholar 

  18. Ventura, A.C., Sepulchre, J.A., Merajver, S.D.: A hidden feedback in signaling cascades is revealed. In: PLoS Computational Biology (to appear, 2008)

    Google Scholar 

  19. Markevich, N.I., Hoek, J.B., Kholodenko, B.N.: Signaling switches and bistability arising from multisite phosphorylation in protein kinase cascades. Journal of Cell Biology 164, 353–359 (2005)

    Article  Google Scholar 

  20. Kolch, W., Kotwaliwale, A., Vass, K., Janosch, P.: The role of raf kinases in malignant transformation. In: Expert Reviews in Molecular Medicine, vol. 25, Cambridge University Press, Cambridge (2002)

    Google Scholar 

  21. Shapiro, B.E., Levchenko, A., Meyerowitz, E.M., Wold, B.J., Mjolsness, E.D.: Cellerator: extending a computer algebra system to include biochemical arrows for signal transduction simulations. Bioinformatics 19, 677–678 (2003)

    Article  Google Scholar 

  22. Regev, A., Silverman, W., Shapiro, E.Y.: Representation and simulation of biochemical processes using the pi-calculus process algebra. In: Proceedings of the sixth Pacific Symposium of Biocomputing, pp. 459–470 (2001)

    Google Scholar 

  23. Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry 81, 2340–2361 (1977)

    Article  Google Scholar 

  24. Gillespie, D.T.: General method for numerically simulating stochastic time evolution of coupled chemical-reactions. Journal of Computational Physics 22, 403–434 (1976)

    Article  MathSciNet  Google Scholar 

  25. Gibson, M.A., Bruck, J.: A probabilistic model of a prokaryotic gene and its regulation. In: Bolouri, H., Bower, J. (eds.) Computational Methods in Molecular Biology: From Genotype to Phenotype, MIT press, Cambridge (2000)

    Google Scholar 

  26. Reddy, V.N., Mavrovouniotis, M.L., Liebman, M.N.: Petri net representations in metabolic pathways. In: Hunter, L., Searls, D.B., Shavlik, J.W. (eds.) Proceedings of the 1st International Conference on Intelligent Systems for Molecular Biology (ISMB, pp. 328–336. AAAI Press, Menlo Park (1993)

    Google Scholar 

  27. Sackmann, A., Heiner, M., Koch, I.: Application of petri net based analysis techniques to signal transduction pathways. BMC Bioinformatics 7 (2006)

    Google Scholar 

  28. Chaouiya, C.: Petri net modelling of biological networks. Briefings in Bioinformatics (2007)

    Google Scholar 

  29. Gilbert, D., Heiner, M., Lehrack, S.: A unifying framework for modelling and analysing biochemical pathways using petri nets. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Schuster, S., Pfeiffer, T., Moldenhauer, F., et al.: Exploring the pathway structure of metabolism: decomposition into subnetworks and application to mycoplasma pneumoniae. Bioinformatics 18, 51–61 (2002)

    Article  Google Scholar 

  31. Zevedei-Oancea, I., Schuster, S.: Topological analysis of metabolic networks based on petri net theory. Silico Biology 3 (2003)

    Google Scholar 

  32. Chabrier, N., Fages, F.: Symbolic model cheking of biochemical networks. In: Priami, C. (ed.) CMSB 2003. LNCS, vol. 2602, pp. 149–162. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  33. Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sönmez, M.K.: Pathway logic: Symbolic analysis of biological signaling. In: Proceedings of the seventh Pacific Symposium on Biocomputing, pp. 400–412 (2002)

    Google Scholar 

  34. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proceedings of the 6th ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 238–252. ACM Press, New York (1977)

    Chapter  Google Scholar 

  35. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science 277, 47–103 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  36. Cousot, P.: Types as abstract interpretation. In: POP 1997: Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pp. 316–331. ACM Press, New York (1997)

    Chapter  Google Scholar 

  37. Qiao, L., Nachbar, R.B., Kevrekidis, I.G., Shvartsman, S.Y.: Bistability and oscillations in the huang-ferrell model of mapk signaling. PLoS Computational Biology 3, 1819–1826 (2007)

    Article  MathSciNet  Google Scholar 

  38. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  39. Bernot, G., Comet, J.P., Richard, A., Guespin, J.: A fruitful application of formal methods to biological regulatory networks: Extending thomas’ asynchronous logical approach with temporal logic. Journal of Theoretical Biology 229, 339–347 (2004)

    Article  MathSciNet  Google Scholar 

  40. Batt, G., Bergamini, D., de Jong, H., Garavel, H., Mateescu, R.: Model checking genetic regulatory networks using gna and cadp. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, Springer, Heidelberg (2004)

    Google Scholar 

  41. Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using the continuous time markow chains. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 44–67. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  42. Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol. 4210, pp. 32–47. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  43. Antoniotti, M., Policriti, A., Ugel, N., Mishra, B.: Model building and model checking for biochemical processes. Cell Biochemistry and Biophysics 38, 271–286 (2003)

    Article  Google Scholar 

  44. Fages, F.: Temporal logic constraints in the biochemical abstract machine biocham (invited talk). In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol. 3901, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  45. Cardelli, L.: Brane calculi - interactions of biological membranes. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 257–280. Springer, Heidelberg (2005)

    Google Scholar 

  46. Regev, A., Panina, E.M., Silverman, W., Cardelli, L., Shapiro, E.: Bioambients: An abstraction for biological compartments. Theoretical Computer Science 325, 141–167 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  47. Danos, V., Laneve, C.: Formal molecular biology. Theoretical Computer Science 325, 69–110 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  48. Phillips, A., Cardelli, L.: A correct abstract machine for the stochastic pi-calculus. Transactions on Computational Systems Biology Special issue of BioConcur (to appear, 2004)

    Google Scholar 

  49. Fages, F., Soliman, S.: Type inference in systems biology. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol. 4210, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  50. Cimatti, A., Clarke, E., Enrico Giunchiglia, F.G., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  51. Fages, F., Rizk, A.: On the analysis of numerical data time series in temporal logic. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 48–63. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  52. Fages, F., Soliman, S.: Model revision from temporal logic properties in systems biology. In: Probabilistic Inductive Logic Programming. LNCS, vol. 4911, pp. 287–304. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  53. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1994)

    Article  MATH  Google Scholar 

  54. Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: st International Conference on Quantitative Evaluation of Systems (QEST 2004), pp. 322–323. IEEE Computer Society, Los Alamitos (2004)

    Chapter  Google Scholar 

  55. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004)

    Google Scholar 

  56. Gibson, M.A., Bruck, J.: Efficient exact stochastic simulation of chemical systems with many species and many channels. Journal of Physical Chemistry 104, 1876–1889 (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Projet Contraintes, INRIA Rocquencourt, BP105, 78153, Le Chesnay Cedex, France

    François Fages & Sylvain Soliman

Authors
  1. François Fages
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sylvain Soliman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marco Bernardo Pierpaolo Degano Gianluigi Zavattaro

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fages, F., Soliman, S. (2008). Formal Cell Biology in Biocham. In: Bernardo, M., Degano, P., Zavattaro, G. (eds) Formal Methods for Computational Systems Biology. SFM 2008. Lecture Notes in Computer Science, vol 5016. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68894-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-68894-5_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-68892-1

  • Online ISBN: 978-3-540-68894-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation