{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:04Z","timestamp":1763468224946,"version":"3.40.4"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319088662"},{"type":"electronic","value":"9783319088679"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_25","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:37:30Z","timestamp":1403955450000},"page":"373-390","source":"Crossref","is-referenced-by-count":20,"title":["Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells"],"prefix":"10.1007","author":[{"given":"Zhenqi","family":"Huang","sequence":"first","affiliation":[]},{"given":"Chuchu","family":"Fan","sequence":"additional","affiliation":[]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"25_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"25_CR2","doi-asserted-by":"publisher","first-page":"1386","DOI":"10.1109\/TAC.2009.2015561","volume":"54","author":"D. Angeli","year":"2009","unstructured":"Angeli, D.: Further results on incremental input-to-state stability. IEEE Transactions on Automatic Control\u00a054(6), 1386\u20131391 (2009)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"3","key":"25_CR3","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1109\/9.989067","volume":"47","author":"D. Angeli","year":"2002","unstructured":"Angeli, D.: A lyapunov approach to incremental stability properties. IEEE Transactions on Automatic Control\u00a047(3), 410\u2013421 (2002)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"6","key":"25_CR4","doi-asserted-by":"publisher","first-page":"1082","DOI":"10.1109\/9.863594","volume":"45","author":"D. Angeli","year":"2000","unstructured":"Angeli, D., Sontag, E.D., Wang, Y.: A characterization of integral input-to-state stability. IEEE Transactions on Automatic Control\u00a045(6), 1082\u20131097 (2000)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Annpureddy","year":"2011","unstructured":"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.\u00a06605, pp. 254\u2013257. Springer, Heidelberg (2011)"},{"issue":"1","key":"25_CR6","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1016\/j.brainresrev.2006.01.007","volume":"52","author":"N. Axmacher","year":"2006","unstructured":"Axmacher, N., Mormann, F., Fern\u00e1ndez, G., Elger, C.E., Fell, J.: Memory formation by neuronal synchronization. Brain Research Reviews\u00a052(1), 170\u2013182 (2006)","journal-title":"Brain Research Reviews"},{"key":"25_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511791383","volume-title":"Dynamical processes on complex networks","author":"A. Barrat","year":"2008","unstructured":"Barrat, A., Barthelemy, M., Vespignani, A.: Dynamical processes on complex networks, vol.\u00a01. Cambridge University Press, Cambridge (2008)"},{"issue":"33-34","key":"25_CR8","doi-asserted-by":"publisher","first-page":"3149","DOI":"10.1016\/j.tcs.2009.02.042","volume":"410","author":"E. Bartocci","year":"2009","unstructured":"Bartocci, E., Corradini, F., Berardini, M.R.D., Entcheva, E., Smolka, S.A., Grosu, R.: Modeling and simulation of cardiac tissue using hybrid I\/O automata. Theor. Comput. Sci.\u00a0410(33-34), 3149\u20133165 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"25_CR9","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/j.physrep.2005.10.009","volume":"424","author":"S. Boccaletti","year":"2006","unstructured":"Boccaletti, S., Latora, V., Moreno, Y., Chavez, M., Hwang, D.-U.: Complex networks: Structure and dynamics. Physics Reports\u00a0424(4), 175\u2013308 (2006)","journal-title":"Physics Reports"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Bouissou, O., Martel, M.: Grklib: A guaranteed runge kutta library. In: 12th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, SCAN 2006, p. 8. IEEE (2006)","DOI":"10.1109\/SCAN.2006.20"},{"issue":"3","key":"25_CR11","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1016\/j.jtbi.2008.03.029","volume":"253","author":"A. Bueno-Orovio","year":"2008","unstructured":"Bueno-Orovio, A., Cherry, E.M., Fenton, F.H.: Minimal model for human ventricular action potentials in tissue. Journal of Theoretical Biology\u00a0253(3), 544\u2013560 (2008)","journal-title":"Journal of Theoretical Biology"},{"key":"25_CR12","unstructured":"CAPD. Computer assisted proofs in dynamics (2002)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X. Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A. Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 167\u2013170. Springer, Heidelberg (2010)"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: EMSOFT (2013)","DOI":"10.1109\/EMSOFT.2013.6658604"},{"issue":"1","key":"25_CR16","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1063\/1.166311","volume":"8","author":"F. Fenton","year":"1998","unstructured":"Fenton, F., Karma, A.: Vortex dynamics in three-dimensional continuous myocardium with fiber rotation: filament instability and fibrillation. Chaos: An Interdisciplinary Journal of Nonlinear Science\u00a08(1), 20\u201347 (1998)","journal-title":"Chaos: An Interdisciplinary Journal of Nonlinear Science"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Garz\u00f3n, A., Grigoriev, R.O., Fenton, F.H.: Model-based control of cardiac alternans on a ring. Physical Review E\u00a080 (2009)","DOI":"10.1103\/PhysRevE.80.021932"},{"issue":"9","key":"25_CR18","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/10.245605","volume":"40","author":"S. Greenhut","year":"1993","unstructured":"Greenhut, S., Jenkins, J., MacDonald, R.: A stochastic network model of the interaction between cardiac rhythm and artificial pacemaker. IEEE Transactions on Biomedical Engineering\u00a040(9), 845\u2013858 (1993)","journal-title":"IEEE Transactions on Biomedical Engineering"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R. Grosu","year":"2011","unstructured":"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.\u00a06806, pp. 396\u2013411. Springer, Heidelberg (2011)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R. Grosu","year":"2011","unstructured":"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.\u00a06806, pp. 396\u2013411. Springer, Heidelberg (2011)"},{"issue":"3","key":"25_CR21","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R. Grosu","year":"2009","unstructured":"Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM\u00a052(3), 97\u2013105 (2009)","journal-title":"Commun. ACM"},{"key":"25_CR22","unstructured":"Guevara, M.R., Ward, G., Shrier, A., Glass, L.: Electrical alternans and period-doubling bifurcations. In: Computers in Cardiology, pp. 167\u2013170 (1984)"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In. In: ACM Symposium on Theory of Computing, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Hespanha, J.P., Morse, A.: Stability of switched systems with average dwell-time. In: Proceedings of 38th IEEE Conference on Decision and Control, pp. 2655\u20132660 (1999)","DOI":"10.1109\/CDC.1999.831330"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Huang, Z., Fan, C., Mitra, S., Mereacre, A., Kwiatkowska, M.: Invariant verification of nonlinear hybrid automata networks of cardiac cells, Online supporting material: Models, code, and data (2014), https:\/\/wiki.cites.illinois.edu\/wiki\/display\/MitraResearch\/Complex+Networks+of+Nonlinear+Modules","DOI":"10.1007\/978-3-319-08867-9_25"},{"key":"25_CR26","unstructured":"Huang, Z., Mitra, S.: Proofs from simulations and modular annotations. In: In 17th International Conference on Hybrid Systems: Computation and Control. ACM Press, Berlin"},{"issue":"6","key":"25_CR27","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1161\/CIRCULATIONAHA.106.644765","volume":"114","author":"R.E. Ideker","year":"2006","unstructured":"Ideker, R.E., Rogers, J.M.: Human ventricular fibrillation: Wandering wavelets, mother rotors, or both? Circulation\u00a0114(6), 530\u2013532 (2006)","journal-title":"Circulation"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Jee, E., Wang, S., Kim, J.-K., Lee, J., Sokolsky, O., Lee, I.: A safety-assured development approach for real-time software. In: RTCSA, pp. 133\u2013142 (2010)","DOI":"10.1109\/RTCSA.2010.42"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Jiang, Z., Pajic, M., Connolly, A., Dixit, S., Mangharam, R.: Real-Time Heart model for implantable cardiac device validation and verification. In: ECRTS, pp. 239\u2013248. IEEE Computer Society (2010)","DOI":"10.1109\/ECRTS.2010.36"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z. Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 188\u2013203. Springer, Heidelberg (2012)"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I\/O Automata. Synthesis Lectures on Computer Science. Morgan Claypool, Also available as Technical Report MIT-LCS-TR-917 (November 2005)","DOI":"10.1007\/978-3-031-01794-0"},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"Hybrid Systems: Computation and Control","author":"G. Lafferriere","year":"1999","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 137\u2013151. Springer, Heidelberg (1999)"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Lian, J., Kr\u00e4tschmer, H., M\u00fcssig, D.: Open source modeling of heart rhythm and cardiac pacing. The Open Pacing, Electrophysiology & Therapy Journal, 28\u201344 (2010)","DOI":"10.2174\/1876536X01003010028"},{"issue":"1","key":"25_CR34","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N. Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid I\/O automata. Information and Computation\u00a0185(1), 105\u2013157 (2003)","journal-title":"Information and Computation"},{"key":"25_CR35","unstructured":"Mitra, S.: A Verification Framework for Hybrid Systems. PhD thesis. Massachusetts Institute of Technology, Cambridge, MA 02139 (September 2007)"},{"issue":"1","key":"25_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1457246.1457249","volume":"8","author":"S. Mitra","year":"2008","unstructured":"Mitra, S., Liberzon, D., Lynch, N.: Verifying average dwell time of hybrid systems. ACM Trans. Embed. Comput. Syst.\u00a08(1), 1\u201337 (2008)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"1","key":"25_CR37","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0096-3003(98)10083-8","volume":"105","author":"N.S. Nedialkov","year":"1999","unstructured":"Nedialkov, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Applied Mathematics and Computation\u00a0105(1), 21\u201368 (1999)","journal-title":"Applied Mathematics and Computation"},{"issue":"1","key":"25_CR38","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/JPROC.2006.887293","volume":"95","author":"R. Olfati-Saber","year":"2007","unstructured":"Olfati-Saber, R., Fax, J.A., Murray, R.M.: Consensus and cooperation in networked multi-agent systems. Proceedings of the IEEE\u00a095(1), 215\u2013233 (2007)","journal-title":"Proceedings of the IEEE"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: From verification to implementation: A model translation tool and a pacemaker case study. In: IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 173\u2013184 (2012)","DOI":"10.1109\/RTAS.2012.25"},{"key":"25_CR40","doi-asserted-by":"crossref","unstructured":"Romualdo Pastor-Satorras and Alessandro Vespignani. Epidemic dynamics and endemic states in complex networks. Physical Review E\u00a063(6), 066117 (2001)","DOI":"10.1103\/PhysRevE.63.066117"},{"key":"25_CR41","unstructured":"Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing sostools: A general purpose sum of squares programming solver. In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002, vol.\u00a01, pp. 741\u2013746. IEEE (2002)"},{"issue":"1-2","key":"25_CR42","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0167-6911(98)00003-6","volume":"34","author":"E.D. Sontag","year":"1998","unstructured":"Sontag, E.D.: Comments on integral variants of iss. Systems & Control Letters\u00a034(1-2), 93\u2013100 (1998)","journal-title":"Systems & Control Letters"},{"issue":"6825","key":"25_CR43","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1038\/35065725","volume":"410","author":"S.H. Strogatz","year":"2001","unstructured":"Strogatz, S.H.: Exploring complex networks. Nature\u00a0410(6825), 268\u2013276 (2001)","journal-title":"Nature"},{"key":"25_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-70583-3_12","volume-title":"Automata, Languages and Programming","author":"V. Vladimerou","year":"2008","unstructured":"Vladimerou, V., Prabhakar, P., Viswanathan, M., Dullerud, G.: Stormed hybrid systems. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 136\u2013147. Springer, Heidelberg (2008)"},{"key":"25_CR45","unstructured":"Ye, P., Entcheva, E., Grosu, R., Smolka, S.A.: Efficient Modeling of Excitable Cells Using Hybrid Automata. In: CMSB, pp. 216\u2013227 (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T14:01:50Z","timestamp":1746280910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}