{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:47:24Z","timestamp":1725864444872},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319451763"},{"type":"electronic","value":"9783319451770"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45177-0_9","type":"book-chapter","created":{"date-parts":[[2016,9,3]],"date-time":"2016-09-03T01:42:38Z","timestamp":1472866958000},"page":"132-146","source":"Crossref","is-referenced-by-count":3,"title":["Bifurcation Analysis of Cardiac Alternans Using $$\\delta $$ -Decidability"],"prefix":"10.1007","author":[{"given":"Md. Ariful","family":"Islam","sequence":"first","affiliation":[]},{"given":"Greg","family":"Byrne","sequence":"additional","affiliation":[]},{"given":"Soonho","family":"Kong","sequence":"additional","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[]},{"given":"Flavio H.","family":"Fenton","sequence":"additional","affiliation":[]},{"given":"Radu","family":"Grosu","sequence":"additional","affiliation":[]},{"given":"Paul L.","family":"Jones","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,4]]},"reference":[{"issue":"6","key":"9_CR1","doi-asserted-by":"crossref","first-page":"1196","DOI":"10.1161\/01.CIR.76.6.1196","volume":"76","author":"A Shrier","year":"1987","unstructured":"Shrier, A., Dubarsky, H., Rosengarten, M., Guevara, M.R., Nattel, S., Glass, L.: Prediction of complex atrioventricular conduction rhythms in humans with use of the atrioventricular nodal recovery curve. Circulation 76(6), 1196\u20131205 (1987)","journal-title":"Circulation"},{"issue":"3","key":"9_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid Systems, pp. 209\u2013229 (1992)","DOI":"10.1007\/3-540-57318-6_30"},{"issue":"3","key":"9_CR4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181\u2013201 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 145\u2013154. ACM (2016)","DOI":"10.1145\/2883817.2883849"},{"issue":"4","key":"9_CR6","doi-asserted-by":"crossref","first-page":"982","DOI":"10.1016\/j.automatica.2007.08.004","volume":"44","author":"G Batt","year":"2008","unstructured":"Batt, G., De Jong, H., Page, M., Geiselmann, J.: Symbolic reachability analysis of genetic regulatory networks using discrete abstractions. Automatica 44(4), 982\u2013989 (2008)","journal-title":"Automatica"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-319-26916-0_4","volume-title":"Hybrid Systems Biology","author":"L Brim","year":"2015","unstructured":"Brim, L., Demko, M., Pastva, S., \u0160afr\u00e1nek, D.: High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Abate, A., et al. (eds.) HSB 2015. LNCS, vol. 9271, pp. 58\u201374. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26916-0_4"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Bryce, D., Gao, S., Musliner, D.J., Goldman, R.P.: SMT-based nonlinear PDDL+ planning. In: 29th AAAI Conference on Artificial Intelligence, p. 3247","DOI":"10.1609\/aaai.v29i1.9646"},{"issue":"3","key":"9_CR9","first-page":"852","volume":"12","author":"FH Fenton","year":"2002","unstructured":"Fenton, F.H., Cherry, E.M., Hastings, H.M., Harold, M., Evans, S.J.: Multiple mechanisms of spiral wave breakup in a model of cardiac electrical activity. chaos: an interdisciplinary. J. Nonlinear Sci. 12(3), 852 (2002)","journal-title":"J. Nonlinear Sci."},{"issue":"8","key":"9_CR10","doi-asserted-by":"crossref","first-page":"1868","DOI":"10.4249\/scholarpedia.1868","volume":"3","author":"FH Fenton","year":"2008","unstructured":"Fenton, F.H., Cherry, E.M.: Models of cardiac cell. Scholarpedia 3(8), 1868 (2008)","journal-title":"Scholarpedia"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Feret, J.: Reachability analysis of biological signalling pathways by abstract interpretation. In: Computation in Modern Science and Engineering, vol. 2, Part A (AIP Conference Proceedings vol. 963), pp. 619\u2013622 (2007)","DOI":"10.1063\/1.2836158"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$ -complete decision procedures for satisfiability\u00a0over\u00a0the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Chen, W., Clarke, E.M.: Delta-complete analysis for bounded reachability of hybrid systems. CoRR, abs\/1404.7171 (2014)","DOI":"10.21236\/ADA613813"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"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\u2013214. Springer, Heidelberg (2013)"},{"key":"9_CR15","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3389\/fphys.2013.00071","volume":"4","author":"A Gizzi","year":"2013","unstructured":"Gizzi, A., Cherry, E.M., Gilmour, R.F., Luther, S., Filippi, S., Fenton, F.H.: Effects of pacing site and stimulation history on alternans dynamics and the development of complex spatiotemporal patterns in cardiac tissue. Front. Physiol. 4, 71 (2013)","journal-title":"Front. Physiol."},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/978-3-319-08867-9_25","volume-title":"Computer Aided Verification","author":"Z Huang","year":"2014","unstructured":"Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 373\u2013390. Springer, Heidelberg (2014)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Islam, M.A., De Francisco, R., Fan, C., Grosu, R., Mitra, S., Smolka, S.A.: Model checking tap withdrawal in C. Elegans. In: Hybrid Systems Biology, p. 195","DOI":"10.1007\/978-3-319-26916-0_11"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Islam, M.A., Murthy, A., Girard, A., Smolka, S.A., Grosu, R.: Compositionality results for cardiac cell dynamics. In: Proceedings of the 17th international conference on Hybrid systems: computation and control, pp. 243\u2013252. ACM (2014)","DOI":"10.1145\/2562059.2562138"},{"issue":"10","key":"9_CR19","doi-asserted-by":"crossref","first-page":"1244","DOI":"10.1161\/01.RES.0000224540.97431.f0","volume":"98","author":"JN Weiss","year":"2006","unstructured":"Weiss, J.N., Alain, S., Shiferaw, Y., Chen, P., Garfinkel, A., Qu, Z.: From pulsus to pulseless the saga of cardiac alternans. Circ. Res. 98(10), 1244\u20131253 (2006). WOS: 000237812200006","journal-title":"Circ. Res."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Hybrid Systems: Computation and Control (HSCC), pp. 133\u2013142. ACM Press (2014)","DOI":"10.1145\/2562059.2562139"},{"key":"9_CR21","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.M.: dReach: $$\\delta $$ -reachability analysis for hybrid systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS, London, UK, April 11\u201318, 2015, pp. 200\u2013205 (2015)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M.: Towards personalized prostate cancer therapy using delta-reachability analysis. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 227\u2013232. ACM (2015)","DOI":"10.1145\/2728606.2728634"},{"issue":"4527","key":"9_CR23","doi-asserted-by":"crossref","first-page":"1350","DOI":"10.1126\/science.7313693","volume":"214","author":"M Guevara","year":"1981","unstructured":"Guevara, M., Glass, L., Shrier, A.: Phase locking, period-doubling bifurcations, and irregular dynamics in periodically stimulated cardiac cells. Science 214(4527), 1350\u20131353 (1981)","journal-title":"Science"},{"issue":"5","key":"9_CR24","doi-asserted-by":"crossref","first-page":"767","DOI":"10.1016\/S0092-8240(03)00041-7","volume":"65","author":"CC Mitchell","year":"2003","unstructured":"Mitchell, C.C., Schaeffer, D.G.: A two-current model for the dynamics of cardiac membrane. Bull. Math. Biol. 65(5), 767\u2013793 (2003)","journal-title":"Bull. Math. Biol."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Murthy, A., Islam, M.A., Smolka, S.A., Grosu, R.: Computing bisimulation functions using SOS optimization and $$\\delta $$ -decidability over the reals. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 78\u201387. ACM (2015)","DOI":"10.1145\/2728606.2728609"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Murthy, A., Islam, M.A., Smolka, S.A., Grosu, R.: Computing compositional proofs of input-to-output stability using SOS optimization and $$\\delta $$ -decidability. Hybrid Systems, Nonlinear Analysis (2016)","DOI":"10.1016\/j.nahs.2016.03.008"},{"issue":"8","key":"9_CR27","doi-asserted-by":"crossref","first-page":"1087","DOI":"10.1111\/j.1540-8167.1999.tb00281.x","volume":"10","author":"RF Gilmour","year":"1999","unstructured":"Gilmour, R.F., Chialvo, D.R.: Electrical restitution, critical mass, and the riddle of fibrillation. J. Cardiovas. Electrophysiol. 10(8), 1087\u20131089 (1999)","journal-title":"J. Cardiovas. Electrophysiol."},{"issue":"2","key":"9_CR28","doi-asserted-by":"crossref","first-page":"021903","DOI":"10.1103\/PhysRevE.71.021903","volume":"71","author":"Y Shiferaw","year":"2005","unstructured":"Shiferaw, Y., Sato, D., Karma, A.: Coupled dynamics of voltage and calcium in paced cardiac cells. Phys. Rev. E 71(2), 021903 (2005)","journal-title":"Phys. Rev. E"},{"issue":"30","key":"9_CR29","doi-asserted-by":"crossref","first-page":"9358","DOI":"10.1073\/pnas.1424320112","volume":"112","author":"T Quail","year":"2015","unstructured":"Quail, T., Shrier, A., Glass, L.: Predicting the onset of period-doubling bifurcations in noisy cardiac systems. Proc. Nat. Acad. Sci. 112(30), 9358\u20139363 (2015)","journal-title":"Proc. Nat. Acad. Sci."},{"issue":"2","key":"9_CR30","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1046\/j.1540-8167.2001.00196.x","volume":"12","author":"MA Watanabe","year":"2001","unstructured":"Watanabe, M.A., Fenton, F.H., Evans, S.J., Hastings, H.M., Karma, A.: Mechanisms for discordant alternans. J. Cardiovasc. Electrophysiol. 12(2), 196\u2013206 (2001)","journal-title":"J. Cardiovasc. Electrophysiol."},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Yang, Y., Lin, H.: Reachability analysis based model validation in systems biology. In: 2010 IEEE Conference on Cybernetics and Intelligent Systems (CIS), pp. 14\u201319. IEEE (2010)","DOI":"10.1109\/ICCIS.2010.5518589"}],"container-title":["Lecture Notes in Computer Science","Computational Methods in Systems Biology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45177-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,7]],"date-time":"2022-07-07T14:18:11Z","timestamp":1657203491000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45177-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319451763","9783319451770"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45177-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}