Skip to main content
SpringerLink
Log in
Book cover

Automated Reasoning for Systems Biology and Medicine pp 63–92Cite as

Statistical Model Checking-Based Analysis of Biological Networks

  • Chapter
  • First Online:

Part of the book series: Computational Biology ((COBO,volume 30))

Abstract

We introduce a framework for analyzing ordinary differential equation  (ODE) models of biological networks using statistical model checking (SMC). A key aspect of our work is the modeling of single-cell variability by assigning a probability distribution to intervals of initial concentration values and kinetic rate constants. We propagate this distribution through the system dynamics to obtain a distribution over the set of trajectories of the ODEs. This in turn opens the door for performing statistical analysis of the ODE system’s behavior. To illustrate this, we first encode quantitative data and qualitative trends as bounded linear time temporal logic (BLTL) formulas. Based on this, we construct a parameter estimation method using an SMC-driven evaluation procedure applied to the stochastic version of the behavior of the ODE system. We then describe how this SMC framework can be generalized to hybrid automata by exploiting the given distribution over the initial states and the—much more sophisticated—system dynamics to associate a Markov chain with the hybrid automaton. We then establish a strong relationship between the behaviors of the hybrid automaton and its associated Markov chain. Consequently, we sample trajectories from the hybrid automaton in a way that mimics the sampling of the trajectories of the Markov chain. This enables us to verify approximately that the Markov chain meets a BLTL specification with high probability. We have applied these methods to ODE-based models of Toll-like receptor signaling and the crosstalk between autophagy and apoptosis, as well as to systems exhibiting hybrid dynamics including the circadian clock pathway and cardiac cell physiology. We present an overview of these applications and summarize the main empirical results. These case studies demonstrate that our methods can be applied in a variety of practical settings.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover 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

References

  1. Abate A, Ames AD, Sastry SS (2005) Stochastic approximations of hybrid systems. In: ACC’05, pp 1557–1562

    Google Scholar 

  2. Agrawal M, Stephan F, Thiagarajan PS, Yang S (2006) Behavioural approximations for restricted linear differential hybrid automata. In: HSCC’06, pp 4–18

    Chapter  Google Scholar 

  3. Alberts B, Johnson A, Lewis J, Raff M, Roberts K, Walter, P (2002) Molecular biology of the cell, 4th edn. Garland Science, New York

    Book  Google Scholar 

  4. Aldridge BB, Burke JM, Lauffenburger DA, Sorger PK (2006) Physicochemical modelling of cell signalling pathways. Nat Cell Biol 8(11):1195–1203

    Article  Google Scholar 

  5. Alur R, Henzinger TA, Lafferriere G, Pappas GJ (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971–984

    Article  Google Scholar 

  6. Ballarini P, Djafri H, Duflot M, Haddad S, Pekergin N (2011) COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: QEST’11, pp 143–144

    Google Scholar 

  7. Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without bdds. In: TACAS’99. Springer, Berlin, pp 193–207

    Google Scholar 

  8. Blom HA, Lygeros J, Everdij M, Loizou S, Kyriakopoulos K (2006) Stochastic hybrid systems: theory and safety critical applications. Springer, Heidelberg

    Book  Google Scholar 

  9. Brown KS, Hill CC, Calero GA, Myers CR, Lee KH, Sethna JP, Cerione RA (2004) The statistical mechanics of complex signaling networks: nerve growth factor signaling. Phys Biol 1(3):184

    Article  Google Scholar 

  10. Bueno-Orovio A, Cherry EM, Fenton FH (2008) Minimal model for human ventricular action potentials in tissue. J Theor Biol 253:544–560

    Article  MathSciNet  Google Scholar 

  11. Calzone L, Chabrier-Rivier N, Fages F, Soliman S (2006) Machine learning biochemical networks from temporal logic properties. In: Transactions on computational systems biology VI, pp 68–94

    Chapter  Google Scholar 

  12. Cassandras CG, Lygeros J (2010) Stochastic hybrid systems. CRC Press

    Google Scholar 

  13. Clarke EM, Fehnker A, Han Z, Krogh BH, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexample-guided abstraction refinement. In: TACAS’03, pp 192–207

    Google Scholar 

  14. Clarke EM, Faeder JR, Langmead CJ, Harris LA, Jha SK, Legay A (2008) Statistical model checking in BioLab: applications to the automated analysis of T-cell receptor signaling pathway. CMSB’08. Springer, Berlin/Heidelberg, pp 231–250

    Google Scholar 

  15. Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT press

    Google Scholar 

  16. De Ferrari GV, Inestrosa NC (2000) Wnt signaling function in Alzheimer’s disease. Brain Res Rev 33:1–12

    Article  Google Scholar 

  17. Donaldson R, Gilbert D (2008) A Monte Carlo model checker for probabilistic LTL with numerical constraints. University of Glasgow, Department of computer science, Technical reports

    Google Scholar 

  18. Donaldson R, Gilbert D (2008) A model checking approach to the parameter estimation of biochemical pathways. CMSB’08. Springer, Berlin/Heidelberg, pp 269–287

    Google Scholar 

  19. Drouin E, Charpentier F, Gauthier C, Laurent K, Le Marec H (1995) Electrophysiologic characteristics of cells spanning the left ventricular wall of human heart: evidence for presence of M cells. J Am Coll Cardiol 26:185–192

    Article  Google Scholar 

  20. Elowitz M, Leibler S (2000) A synthetic oscillatory network of transcriptional regulators. Nature 403(6767):335–338

    Article  Google Scholar 

  21. Fenton F, Karma A (1998) Vortex dynamics in 3D continuous myocardium with fiber rotation: filament instability and fibrillation. Chaos 8:20–47

    Article  Google Scholar 

  22. Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: HSCC’05, pp 258–273

    Chapter  Google Scholar 

  23. Gao S, Kong S, Clarke EM (2013) dReal: an SMT solver for nonlinear theories over the reals. In: CADE’13. Springer, Berlin, pp 208–214

    Chapter  Google Scholar 

  24. Girard A, Le Guernic C, Maler O (2006) Efficient computation of reachable sets of linear time-invariant systems with inputs. In: HSCC’06, pp 257–271

    Chapter  Google Scholar 

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

    Google Scholar 

  26. Goldbeter A, Pourquie O (2008) Modeling the segmentation clock as a network of coupled oscillations in the Notch, Wnt and FGF signaling pathways. J Theor Biol 252:574–585

    Article  MathSciNet  Google Scholar 

  27. Grosu R, Batt G, Fenton FH, Gilmm J, Guernic CL, Smolka SA, Bartocci E (2011) From cardiac cells to genetic regulatory networks. In: CAV’11, pp 396–411

    Chapter  Google Scholar 

  28. Gyori BM, Bachman JA, Subramanian K, Muhlich JL, Galescu L, Sorger PK (2017) From word models to executable models of signaling networks using automated assembly. Mol Syst Biol 13(11):954

    Article  Google Scholar 

  29. Gyori BM, Liu B, Paul S, Ramanathan R, Thiagarajan PS (2015) Approximate probabilistic verification of hybrid systems. HSB’15. Springer, Berlin, pp 96–116

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  31. Henzinger T (1996) The theory of hybrid automata. In: LICS’96, pp 278–292

    Google Scholar 

  32. Henzinger T, Kopke P (1999) Discrete-time control for rectangular hybrid automata. Theor Comput Sci 221(1):369–392

    Article  MathSciNet  Google Scholar 

  33. Henzinger TA, W. Kopke PW, Puri A, Varaiya P (1998) What’s decidable about hybrid automata? J Comput Syst Sci 57(1):94–124

    Article  MathSciNet  Google Scholar 

  34. Hérault T, Lassaigne R, Magniette F, Peyronnet S (2003) Approximate probabilistic model checking. VMCAI’03. Springer, Berlin, pp 73–84

    Google Scholar 

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

    Google Scholar 

  36. Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P (2009) A Bayesian approach to model checking biological systems. CMSB. Springer, Berlin/Heidelberg, pp 218–234

    Google Scholar 

  37. Julius AA, Pappas GJ (2009) Approximations of stochastic hybrid systems. IEEE Trans Autom Control 54(6):1193–1203

    Article  MathSciNet  Google Scholar 

  38. Kagan VE, Mao G, Qu F, Angeli JPF, Doll S, St Croix C, Dar HH, Liu B, Tyurin VA, Ritov VB et al (2017) Oxidized arachidonic and adrenic PEs navigate cells to ferroptosis. Nat Chem Biol 13(1):81

    Article  Google Scholar 

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

    Book  Google Scholar 

  40. 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 (2006) BioModels database: a free, centralized database of curated, published, quantitative kinetic models of biochemical and cellular systems. Nucl Acids Res 34:D689–D691

    Article  Google Scholar 

  41. Li C, Nagasaki M, Koh CH, Miyano S (2011) 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–92

    Article  Google Scholar 

  42. Liu B, Bhatt D, Oltvai ZN, Greenberger JS, Bahar I (2014) Significance of p53 dynamics in regulating apoptosis in response to ionizing radiation, and polypharmacological strategies. Sci Rep 4:6245

    Article  Google Scholar 

  43. Liu B, Faeder JR (2016) Parameter estimation of rule-based models using statistical model checking. In: BIBM’16. IEEE, pp 1458–1464

    Google Scholar 

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

    Article  Google Scholar 

  45. Liu B, Kong S, Gao S, Zuliani P, Clarke EM (2014) Parameter synthesis for cardiac cell hybrid models using \(\delta \)-decisions. In: CMSB’14, pp 99–113

    Google Scholar 

  46. Liu B, Liu Q, Palaniappan S, Bahar I, Thiagarajan PS, Ding JL (2016) Innate immune memory and homeostasis may be conferred through TLR3-TLR7 pathway crosstalk. Sci Signal 9(436):ra70

    Article  Google Scholar 

  47. Liu B, Oltvai ZN, Bayır H, Silverman GA, Pak SC, Perlmutter DH, Bahar I (2017) Quantitative assessment of cell fate decision between autophagy and apoptosis. Sci Rep 7(1):17605

    Article  Google Scholar 

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

    Article  Google Scholar 

  49. Matsuno H, Inouye ST, Okitsu Y, Fujii Y, Miyano S (2006) A new regulatory interaction suggested by simulations for circadian genetic control mechanism in mammals. J Bioinform Comput Biol 4(1):139–153

    Article  Google Scholar 

  50. Moles CG, Mendes P, Banga JR (2003) Parameter estimation in biochemical pathways: a comparison of global optimization methods. Genome Res 13(11):2467–2474

    Article  Google Scholar 

  51. Nabauer M, Beuckelmann DJ, Uberfuhr P, Steinbeck G (1996) Regional differences in current density and rate-dependent properties of the transient outward current in subepicardial and subendocardial myocytes of human left ventricle. Circulation 93:169–177

    Article  Google Scholar 

  52. Palaniappan SK, Gyori BM, Liu B, Hsu D, Thiagarajan PS (2013) Statistical model checking based calibration and analysis of bio-pathway models. CMSB’13. Springer, Berlin, pp 120–134

    Google Scholar 

  53. Ramanathan R, Zhang Y, Zhou J, Gyori BM, Wong WF, Thiagarajan PS (2015) Parallelized parameter estimation of biological pathway models. Springer, Berlin, pp 37–57

    MATH  Google Scholar 

  54. Rizk A, Batt G, Fages F, Soliman S (2008) On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. CMSB. Springer, Berlin/Heidelberg, pp 251–268

    Google Scholar 

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

    Article  Google Scholar 

  56. Snijder B, Pelkmans L (2011) Origins of regulated cell-to-cell variability. Nat Rev Mol Cell Biol 12(2):119–125

    Article  Google Scholar 

  57. Somlyo AP, Somlyo AV (2003) Ca\(^{2+}\) sensitivity of smooth muscle and nonmuscle myosin ii: modulated by g proteins, kinases, and myosin phosphatase. Physiol Rev 83:1325–1358

    Google Scholar 

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

    Article  Google Scholar 

  59. Supplementary information and source code (2018). http://www.pitt.edu/~liubing/smc/

  60. Tanaka K, Zlochiver S, Vikstrom K, Yamazaki M, Moreno J, Klos M, Zaitsev A, Vaidyanathan R, Auerbach D, Landas S, Guiraudon G, Jalife J, Berenfeld O, Kalifa J (2007) Spatial distribution of fibrosis governs fibrillation wave dynamics in the posterior left atrium during heart failure. Circ Res 8(101):839–847

    Article  Google Scholar 

  61. Vardi M (1985) Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of 26th IEEE symposium on foundations of computer science. IEEE, pp 327–338

    Google Scholar 

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

    Article  Google Scholar 

  63. Wilkinson D (2011) Stochastic modelling for systems biology. CRC Press

    Google Scholar 

  64. Younes HLS, Kwiatkowska M, Norman G, Parker D (2006) Numerical versus statistical probabilistic model checking. Int J Softw Tools Technol Transf 8:216–228

    Article  Google Scholar 

  65. Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inform Comput 204:1368–1409

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

This work was partly supported by the NIH awards P41GM103712, U19AI068021, and P30DA035778 (to BL) and DARPA grants W911NF-15-1-0544 and W911NF-18-1-0014 (to BMG and PST).

Author information

Authors and Affiliations

  1. Department of Computational and Systems Biology, University of Pittsburgh, Pittsburgh, PA, 15237, USA

    Bing Liu

  2. Laboratory of Systems Pharmacology, Harvard Medical School, Boston, MA, 02115, USA

    Benjamin M. Gyori & P. S. Thiagarajan

Authors
  1. Bing Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benjamin M. Gyori
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. P. S. Thiagarajan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bing Liu .

Editor information

Editors and Affiliations

  1. Department of Computer Science and Technology, University of Cambridge, Cambridge, UK

    Pietro Liò

  2. School of Computing, Newcastle University, Newcastle, UK

    Paolo Zuliani

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Liu, B., Gyori, B.M., Thiagarajan, P.S. (2019). Statistical Model Checking-Based Analysis of Biological Networks. In: Liò, P., Zuliani, P. (eds) Automated Reasoning for Systems Biology and Medicine. Computational Biology, vol 30. Springer, Cham. https://doi.org/10.1007/978-3-030-17297-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-17297-8_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-17296-1

  • Online ISBN: 978-3-030-17297-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation