Skip to main content

Statistical Model Checking Based Calibration and Analysis of Bio-pathway Models

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNBI,volume 8130))

Abstract

We present a statistical model checking (SMC) based framework for studying ordinary differential equation (ODE) models of bio-pathways. We address cell-to-cell variability explicitly by using probability distributions to model initial concentrations and kinetic rate values. This implicitly defines a distribution over a set of ODE trajectories, the properties of which are to be characterized. The core component of our framework is an SMC procedure for verifying the dynamical properties of an ODE system accompanied by such prior distributions. To cope with the imprecise nature of biological data, we use a formal specification logic that allows us to encode both qualitative properties and experimental data. Using SMC, we verify such specifications in a tractable way, independent of the system size. This further enables us to develop SMC based parameter estimation and sensitivity analysis procedures. We have evaluated our method on two large pathway models, namely, the segmentation clock network and the thrombin-dependent MLC phosphorylation pathway. The results show that our method scales well and yields good parameter estimates that are robust. Our sensitivity analysis framework leads to interesting insights about the underlying dynamics of these systems.

This research was partially supported by the Singapore MOE ARC grant MOE2011-T2- 2-012.

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

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. De Ferrari, G.V., Inestrosa, N.C.: Wnt signaling function in Alzheimer’s disease. Brain Res. Rev. 33, 1–12 (2000)

    Article  Google Scholar 

  2. Aldridge, B.B., Burke, J.M., Lauffenburger, D.A., Sorger, P.K.: Physicochemical modelling of cell signalling pathways. Nat. Cell Biol. 8(11), 1195–1203 (2006)

    Article  Google Scholar 

  3. Wilkinson, D.: Stochastic modelling for systems biology. CRC Press (2011)

    Google Scholar 

  4. Klipp, E., Herwig, R., Kowald, A., Wierling, C., Lehrach, H.: Systems biology in practice: concepts, implementation and application. Wiley-VCH, Weinheim (2005)

    Book  Google Scholar 

  5. Spencer, S., Gaudet, S., Albeck, J., Burke, J., Sorger, P.: Non-genetic origins of cell-to-cell variability in TRAIL-induced apoptosis. Nature 459(7245), 428–432 (2009)

    Article  Google Scholar 

  6. Snijder, B., Pelkmans, L.: Origins of regulated cell-to-cell variability. Nature Reviews Molecular Cell Biology 12(2), 119–125 (2011)

    Article  Google Scholar 

  7. Weiße, A., Middleton, R., Huisinga, W.: Quantifying uncertainty, variability and likelihood for ordinary differential equation models. BMC Systems Biology 4(1), 144 (2010)

    Article  Google Scholar 

  8. Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer 8, 216–228 (2006)

    Article  Google Scholar 

  9. Moles, C.G., Mendes, P., Banga, J.R.: Parameter estimation in biochemical pathways: A comparison of global optimization methods. Genome Res. 13(11), 2467–2474 (2003)

    Article  Google Scholar 

  10. Runarsson, T., Yao, X.: Stochastic ranking for constrained evolutionary optimization. IEEE T. Evolut. Comput. 4, 284–294 (2000)

    Article  Google Scholar 

  11. Saltelli, A., Ratto, M., Andres, T., Campolongo, F., Cariboni, J., Gatelli, D., Saisana, M., Tarantola, S.: Global sensitivity analysis: the primer. Wiley-Interscience (2008)

    Google Scholar 

  12. Cho, K.H., Shin, S.Y., Kolch, W., Wolkenhauer, O.: Experimental design in systems biology, based on parameter sensitivity analysis using a Monte Carlo method: A case study for the TNFα-mediated NF-κB signal transduction pathway. Simulation 79(12), 726–739 (2003)

    Article  Google Scholar 

  13. Le Novere, N., Bornstein, B., Broicher, A., Courtot, M., Donizelli, M., Dharuri, H., Li, L., Sauro, H., Schilstra, M., Shapiro, B., Snoep, J., Hucka, M.: BioModels Database: A free, centralized database of curated, published, quantitative kinetic models of biochemical and cellular systems. Nucleic Acids Res. 34, D689–D691 (2006)

    Article  Google Scholar 

  14. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci. 391(3), 239–257 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  16. Li, C., Nagasaki, M., Koh, C.H., Miyano, S.: Online model checking approach based parameter estimation to a neuronal fate decision simulation model in Caenorhabditis elegans with hybrid functional Petri net with extension. Mol. Biosyst. 7(5), 1576–1592 (2011)

    Article  Google Scholar 

  17. Liu, B., Hagiescu, A., Palaniappan, S.K., Chattopadhyay, B., Cui, Z., Wong, W., Thiagarajan, P.S.: Approximate probabilistic analysis of biopathway dynamics. Bioinformatics 28(11), 1508–1516 (2012)

    Article  Google Scholar 

  18. Donaldson, R., Gilbert, D.: A monte carlo model checker for probabilistic ltl with numerical constraints. University of Glasgow, Dep. of CS, Tech. Rep. (2008)

    Google Scholar 

  19. Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269–287. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in BioLab: Applications to the automated analysis of T-cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 231–250. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Maler, O.: On under-determined dynamical systems. In: Proceedings of the Ninth ACM International Conference on Embedded Software, pp. 89–96. ACM (2011)

    Google Scholar 

  22. Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. T. Comput. Syst. Biol. VI, 68–94 (2006)

    Google Scholar 

  23. Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 251–268. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Batt, G., Page, M., Cantone, I., Goessler, G., Monteiro, P., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18), i603–i610 (2010)

    Article  Google Scholar 

  25. Barnat, J., Brim, L., Krejci, A., Streck, A., Safranek, D., Vejnar, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE/ACM T. Comput. Bi. 9(3), 693–705 (2012)

    Article  Google Scholar 

  26. Supplementary information and source code, http://www.comp.nus.edu.sg/~rpsysbio/SMC/

  27. Hirsch, M., Smale, S., Devaney, R.: Differential equations, dynamical systems, and an introduction to chaos. Academic Press (2012)

    Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inform. Comput. 204, 1368–1409 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  30. Goldberg, D.: Genetic algorithms in search, optimization, and machine learning. Addison-Wesley (1989)

    Google Scholar 

  31. Hindmarsh, A., Brown, P., Grant, K., Lee, S., Serban, R., Shumaker, D., Woodward, C.: SUNDIALS: Suite of nonlinear and differential/algebraic equation solvers. ACM T. Math. Software 31(3), 363–396 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  32. Vanlier, J., Tiemann, C., Hilbers, P., van Riel, N.: An integrated strategy for prediction uncertainty analysis. Bioinformatics 28(8), 1130–1135 (2012)

    Article  Google Scholar 

  33. Maedo, A., Ozaki, Y., Sivakumaran, S., Akiyama, T., Urakubo, H., Usami, A., Sato, M., Kaibuchi, K., Kuroda, S.: Ca2 + -independent phospholipase A2-dependent sustained Rho-kinase activation exhibits all-or-none response. Genes Cells 11, 1071–1083 (2006)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Palaniappan, S.K., Gyori, B.M., Liu, B., Hsu, D., Thiagarajan, P.S. (2013). Statistical Model Checking Based Calibration and Analysis of Bio-pathway Models. In: Gupta, A., Henzinger, T.A. (eds) Computational Methods in Systems Biology. CMSB 2013. Lecture Notes in Computer Science(), vol 8130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40708-6_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40708-6_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40707-9

  • Online ISBN: 978-3-642-40708-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics