Skip to main content
SpringerLink
Log in

Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions

  • Conference paper
Computational Methods in Systems Biology (CMSB 2014)

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

Included in the following conference series:

Abstract

A central problem in systems biology is to identify parameter values such that a biological model satisfies some behavioral constraints (e.g., time series). In this paper we focus on parameter synthesis for hybrid (continuous/discrete) models, as many biological systems can possess multiple operational modes with specific continuous dynamics in each mode. These biological systems are naturally modeled as hybrid automata, most often with nonlinear continuous dynamics. However, hybrid automata are notoriously hard to analyze — even simple reachability for hybrid systems with linear differential dynamics is an undecidable problem. In this paper we present a parameter synthesis framework based on δ-complete decision procedures that sidesteps undecidability. We demonstrate our method on two highly nonlinear hybrid models of the cardiac cell action potential. The results show that our parameter synthesis framework is convenient and efficient, and it enabled us to select a suitable model to study and identify crucial parameter ranges related to cardiac disorders.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Liu, B., Thiagarajan, P.: Modeling and analysis of biopathways dynamics. Journal of Bioinformatics and Computational Biology 10(4), 1231001 (2012)

    Article  Google Scholar 

  2. Chen, K.C., Calzone, L., Csikasz-Nagy, A., Cross, F.R., Novak, B., Tyson, J.J.: Integrative analysis of cell cycle control in budding yeast. Mol. Biol. Cell. 15(8), 3841–3862 (2004)

    Article  Google Scholar 

  3. Ghosh, R., Tomlin, C.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: Delta-notch protein signalling. IET Syst. Biol. 1(1), 170–183 (2004)

    Article  Google Scholar 

  4. Hu, J., Wu, W.-C., Sastry, S.S.: Modeling subtilin production in bacillus subtilis using stochastic hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 417–431. Springer, Heidelberg (2004)

    Google Scholar 

  5. Ye, P., Entcheva, E., Smolka, S.A., Grosu, R.: Modelling excitable cells using cycle-linear hybrid automata. IET Syst. Biol. 2(1), 24–32 (2008)

    Article  Google Scholar 

  6. Aihara, K., Suzuki, H.: Theory of hybrid dynamical systems and its applications to biological and medical systems. Phil. Trans. R. Soc. A 368(1930), 4893–4914 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  7. Antoniotti, M., Mishra, B., Piazza, C., Policriti, A., Simeoni, M.: Modeling cellular behavior with hybrid automata: Bisimulation and collapsing. In: Priami, C. (ed.) CMSB 2003. LNCS, vol. 2602, pp. 57–74. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Lincoln, P., Tiwari, A.: Symbolic systems biology: Hybrid modeling and analysis of biological networks. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 660–672. Springer, Heidelberg (2004)

    Google Scholar 

  9. Baldazzi, V., Monteiro, P.T., Page, M., Ropers, D., Geiselmann, J., Jong, H.D.: Qualitative analysis of genetic regulatory networks in bacteria. In: Understanding the Dynamics of Biological Systems, pp. 111–130. Springer (2011)

    Google Scholar 

  10. Tanaka, G., Hirata, Y., Goldenberg, S.L., Bruchovsky, N., Aihara, K.: Mathematical modelling of prostate cancer growth and its application to hormone therapy. Phil. Trans. R. Soc. A 368, 5029–5044 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  11. Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292 (1996)

    Google Scholar 

  12. Gao, S., Avigad, J., Clarke, E.M.: Delta-complete decision procedures for satisfiability over the reals. In: IJCAR, pp. 286–300 (2012)

    Google Scholar 

  13. Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: LICS, pp. 305–314 (2012)

    Google Scholar 

  14. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

  16. Bueno-Orovio, A., Cherry, E.M., Fenton, F.H.: Minimal model for human ventricular action potentials in tissue. J. Theor. Biol. 253, 544–560 (2008)

    Article  MathSciNet  Google Scholar 

  17. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)

    Google Scholar 

  18. Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taLiRo: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Chabrier-Rivier, N., Fages, F., Soliman, S.: The biochemical abstract machine BIOCHAM. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 172–191. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. Bortolussi, L., Policriti, A.: Hybrid systems and biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 424–448. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Brim, L., Češka, M., Šafránek, D.: Model checking of biological systems. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 63–112. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Batt, G., Belta, C., Weiss, R.: Temporal logic analysis of gene networks under parameter uncertainty. IEEE T. Automat. Contr. 53, 215–229 (2008)

    Article  Google Scholar 

  24. Donzé, A., Clermont, G., Langmead, C.J.: Parameter synthesis in nonlinear dynamical systems: Application to systems biology. J. Comput. Biol. 17(3), 325–336 (2010)

    Article  MathSciNet  Google Scholar 

  25. Palaniappan, S.K., Gyori, B.M., Liu, B., Hsu, D., Thiagarajan, P.S.: Statistical model checking based calibration and analysis of bio-pathway models. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 120–134. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

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

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

  28. Koutroumpas, K., Cinquemani, E., Kouretas, P., Lygeros, J.: Parameter identification for stochastic hybrid systems using randomized optimization: A case study on subtilin production by Bacillus subtilis. Nonlinear Anal.-Hybrid Syst. 2, 786–802 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  29. Cinquemani, E., Porreca, R., Ferrari-Trecate, G., Lygeros, J.: Subtilin production by Bacillus subtilis: Stochastic hybrid models and parameter identification. IEEE Trans. Automat. Contr. 53, 38–50 (2008)

    Article  MathSciNet  Google Scholar 

  30. Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: FMCAD, pp. 105–112 (2013)

    Google Scholar 

  31. Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  32. Nabauer, M., Beuckelmann, D.J., Uberfuhr, P., Steinbeck, G.: 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 (1996)

    Article  Google Scholar 

  33. Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  34. Li, C., Donizelli, M., Rodriguez, N., Dharuri, H., Endler, L., Chelliah, V., Li, L., He, E., Henry, A., Stefan, M.I., Snoep, J.L., Hucka, M., Novere, N.L., Laibe, C.: BioModels Database: An enhanced, curated and annotated resource for published quantitative kinetic models. BMC Sys. Biol. 4, 92 (2010)

    Article  Google Scholar 

  35. Matsuno, H., Tanaka, Y., Aoshima, H., Doi, A., Matsui, M., Miyano, S.: Biopathways representation and simulation on hybrid functional petri net. In Silico Biol. 3(3), 389–404 (2003)

    Google Scholar 

  36. Ptolemaeus, C. (ed.): System Design, Modeling, and Simulation using Ptolemy II (2014), Ptolemy.org

  37. Weihrauch, K.: Computable Analysis: An Introduction. Springer (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegie Mellon University, USA

    Bing Liu, Soonho Kong, Sicun Gao & Edmund M. Clarke

  2. School of Computing Science, Newcastle University, UK

    Paolo Zuliani

Authors
  1. Bing Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Soonho Kong
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sicun Gao
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Paolo Zuliani
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Edmund M. Clarke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Manchester Institute of Biotechnology, The University of Manchester, 131 Princess Street, M1 7DN, Manchester, UK

    Pedro Mendes , Joseph O. Dada  & Kieran Smallbone ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M. (2014). Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions. In: Mendes, P., Dada, J.O., Smallbone, K. (eds) Computational Methods in Systems Biology. CMSB 2014. Lecture Notes in Computer Science(), vol 8859. Springer, Cham. https://doi.org/10.1007/978-3-319-12982-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12982-2_8

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12981-5

  • Online ISBN: 978-3-319-12982-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation