Statistical Model Checking-Based Analysis of Biological Networks

  • Bing LiuEmail author
  • Benjamin M. Gyori
  • P. S. Thiagarajan
Part of the Computational Biology book series (COBO, volume 30)


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


  1. 1.
    Abate A, Ames AD, Sastry SS (2005) Stochastic approximations of hybrid systems. In: ACC’05, pp 1557–1562Google Scholar
  2. 2.
    Agrawal M, Stephan F, Thiagarajan PS, Yang S (2006) Behavioural approximations for restricted linear differential hybrid automata. In: HSCC’06, pp 4–18CrossRefGoogle Scholar
  3. 3.
    Alberts B, Johnson A, Lewis J, Raff M, Roberts K, Walter, P (2002) Molecular biology of the cell, 4th edn. Garland Science, New YorkCrossRefGoogle Scholar
  4. 4.
    Aldridge BB, Burke JM, Lauffenburger DA, Sorger PK (2006) Physicochemical modelling of cell signalling pathways. Nat Cell Biol 8(11):1195–1203CrossRefGoogle Scholar
  5. 5.
    Alur R, Henzinger TA, Lafferriere G, Pappas GJ (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971–984CrossRefGoogle Scholar
  6. 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–144Google Scholar
  7. 7.
    Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without bdds. In: TACAS’99. Springer, Berlin, pp 193–207Google Scholar
  8. 8.
    Blom HA, Lygeros J, Everdij M, Loizou S, Kyriakopoulos K (2006) Stochastic hybrid systems: theory and safety critical applications. Springer, HeidelbergCrossRefGoogle Scholar
  9. 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):184CrossRefGoogle Scholar
  10. 10.
    Bueno-Orovio A, Cherry EM, Fenton FH (2008) Minimal model for human ventricular action potentials in tissue. J Theor Biol 253:544–560MathSciNetCrossRefGoogle Scholar
  11. 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–94CrossRefGoogle Scholar
  12. 12.
    Cassandras CG, Lygeros J (2010) Stochastic hybrid systems. CRC PressGoogle Scholar
  13. 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–207Google Scholar
  14. 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–250Google Scholar
  15. 15.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT pressGoogle Scholar
  16. 16.
    De Ferrari GV, Inestrosa NC (2000) Wnt signaling function in Alzheimer’s disease. Brain Res Rev 33:1–12CrossRefGoogle Scholar
  17. 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 reportsGoogle Scholar
  18. 18.
    Donaldson R, Gilbert D (2008) A model checking approach to the parameter estimation of biochemical pathways. CMSB’08. Springer, Berlin/Heidelberg, pp 269–287Google Scholar
  19. 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–192CrossRefGoogle Scholar
  20. 20.
    Elowitz M, Leibler S (2000) A synthetic oscillatory network of transcriptional regulators. Nature 403(6767):335–338CrossRefGoogle Scholar
  21. 21.
    Fenton F, Karma A (1998) Vortex dynamics in 3D continuous myocardium with fiber rotation: filament instability and fibrillation. Chaos 8:20–47CrossRefGoogle Scholar
  22. 22.
    Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: HSCC’05, pp 258–273CrossRefGoogle Scholar
  23. 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–214CrossRefGoogle Scholar
  24. 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–271CrossRefGoogle Scholar
  25. 25.
    Goldberg D (1989) Genetic algorithms in search, optimization, and machine learning. Addison-WesleyGoogle Scholar
  26. 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–585MathSciNetCrossRefGoogle Scholar
  27. 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–411CrossRefGoogle Scholar
  28. 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):954CrossRefGoogle Scholar
  29. 29.
    Gyori BM, Liu B, Paul S, Ramanathan R, Thiagarajan PS (2015) Approximate probabilistic verification of hybrid systems. HSB’15. Springer, Berlin, pp 96–116Google Scholar
  30. 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–257MathSciNetCrossRefGoogle Scholar
  31. 31.
    Henzinger T (1996) The theory of hybrid automata. In: LICS’96, pp 278–292Google Scholar
  32. 32.
    Henzinger T, Kopke P (1999) Discrete-time control for rectangular hybrid automata. Theor Comput Sci 221(1):369–392MathSciNetCrossRefGoogle Scholar
  33. 33.
    Henzinger TA, W. Kopke PW, Puri A, Varaiya P (1998) What’s decidable about hybrid automata? J Comput Syst Sci 57(1):94–124MathSciNetCrossRefGoogle Scholar
  34. 34.
    Hérault T, Lassaigne R, Magniette F, Peyronnet S (2003) Approximate probabilistic model checking. VMCAI’03. Springer, Berlin, pp 73–84Google Scholar
  35. 35.
    Hirsch M, Smale S, Devaney R (2012) Differential equations, dynamical systems, and an introduction to chaos. Academic PressGoogle Scholar
  36. 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–234Google Scholar
  37. 37.
    Julius AA, Pappas GJ (2009) Approximations of stochastic hybrid systems. IEEE Trans Autom Control 54(6):1193–1203MathSciNetCrossRefGoogle Scholar
  38. 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):81CrossRefGoogle Scholar
  39. 39.
    Klipp E, Herwig R, Kowald A, Wierling C, Lehrach H (2005) Systems biology in practice: concepts, implementation and application. Wiley-VCH, WeinheimCrossRefGoogle Scholar
  40. 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–D691CrossRefGoogle Scholar
  41. 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–92CrossRefGoogle Scholar
  42. 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:6245CrossRefGoogle Scholar
  43. 43.
    Liu B, Faeder JR (2016) Parameter estimation of rule-based models using statistical model checking. In: BIBM’16. IEEE, pp 1458–1464Google Scholar
  44. 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–1516CrossRefGoogle Scholar
  45. 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–113Google Scholar
  46. 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):ra70CrossRefGoogle Scholar
  47. 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):17605CrossRefGoogle Scholar
  48. 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–1083CrossRefGoogle Scholar
  49. 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–153CrossRefGoogle Scholar
  50. 50.
    Moles CG, Mendes P, Banga JR (2003) Parameter estimation in biochemical pathways: a comparison of global optimization methods. Genome Res 13(11):2467–2474CrossRefGoogle Scholar
  51. 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–177CrossRefGoogle Scholar
  52. 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–134Google Scholar
  53. 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–57zbMATHGoogle Scholar
  54. 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–268Google Scholar
  55. 55.
    Runarsson T, Yao X (2000) Stochastic ranking for constrained evolutionary optimization. IEEE Trans Evol Comput 4:284–294CrossRefGoogle Scholar
  56. 56.
    Snijder B, Pelkmans L (2011) Origins of regulated cell-to-cell variability. Nat Rev Mol Cell Biol 12(2):119–125CrossRefGoogle Scholar
  57. 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–1358Google Scholar
  58. 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–432CrossRefGoogle Scholar
  59. 59.
    Supplementary information and source code (2018).
  60. 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–847CrossRefGoogle Scholar
  61. 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–338Google Scholar
  62. 62.
    Weiße A, Middleton R, Huisinga W (2010) Quantifying uncertainty, variability and likelihood for ordinary differential equation models. BMC Syst Biol 4(1):144CrossRefGoogle Scholar
  63. 63.
    Wilkinson D (2011) Stochastic modelling for systems biology. CRC PressGoogle Scholar
  64. 64.
    Younes HLS, Kwiatkowska M, Norman G, Parker D (2006) Numerical versus statistical probabilistic model checking. Int J Softw Tools Technol Transf 8:216–228CrossRefGoogle Scholar
  65. 65.
    Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inform Comput 204:1368–1409MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Bing Liu
    • 1
    Email author
  • Benjamin M. Gyori
    • 2
  • P. S. Thiagarajan
    • 2
  1. 1.Department of Computational and Systems BiologyUniversity of PittsburghPittsburghUSA
  2. 2.Laboratory of Systems PharmacologyHarvard Medical SchoolBostonUSA

Personalised recommendations