×

Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans. (English) Zbl 1427.92054

Summary: Using a probabilistic reachability-based approach, we present a multi-parameter bifurcation analysis of electrical alternans in the two-current Mitchell-Schaeffer (MS) cardiac-cell model. Electrical alternans is a phenomenon characterized by a variation in successive action potential durations generated by a cardiac cell or tissue. Alternans are known to initiate re-entrant waves and are an important physiological indicator of an impending life-threatening arrhythmia such as ventricular fibrillation. The multi-parameter bifurcation analysis we perform identifies a bifurcation hypersurface in the MS model parameter space, such that a small perturbation to this region results in a transition from highly likely alternans to highly likely non-alternans behavior.
Our approach to this problem rests on encoding alternans-like behavior in the MS model as a five-mode, multinomial hybrid automaton. To perform multi-parameter bifurcation analysis of cardiac alternans, we first treat the parameters in question as bounded random variables. We then apply a sophisticated guided-search-based probabilistic reachability analysis to compute a bounded bifurcation region (possibly very tight) that contains the bifurcation hypersurface (BH). Our probabilistic reachability analysis uses a technique that combines a \(\delta\)-decision procedure with statistical tests. In the process of computing the bifurcation region, we further partition the parameter space into two more regions such that any valuation chosen from one of the regions will either produce alternans or non-alternans behavior with a probability greater than a user-defined threshold.

MSC:

92C55 Biomedical imaging and signal processing
34C23 Bifurcation theory for ordinary differential equations
93B03 Attainable sets, reachability

Software:

dReal; SReach; dReach; BFComp
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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-1205 (Dec. 1987)
[2] Alpern, B.; Schneider, F. B., Recognizing safety and liveness, Distrib. Comput., 2, 3, 117-126 (1987) · Zbl 0641.68039
[3] 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, Theoret. Comput. Sci., 138, 1, 3-34 (1995) · Zbl 0874.68206
[4] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P., Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, (Hybrid Systems (1992)), 209-229
[5] Alur, R.; Henzinger, T. A.; Ho, P.-H., Automatic symbolic verification of embedded systems, IEEE Trans. Softw. Eng., 22, 3, 181-201 (1996)
[6] Bae, K.; Ölveczky, P. C.; Kong, S.; Gao, S.; Clarke, E. M., SMT-based analysis of virtually synchronous distributed hybrid systems, (Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (2016), ACM), 145-154 · Zbl 1364.68258
[7] Batt, G.; De Jong, H.; Page, M.; Geiselmann, J., Symbolic reachability analysis of genetic regulatory networks using discrete abstractions, Automatica, 44, 4, 982-989 (2008) · Zbl 1283.93046
[8] Billman, G. E., Cardiac autonomic neural remodeling and susceptibility to sudden cardiac death: effect of endurance exercise training, Am. J. Physiol. Heart Circ. Physiol., 297, 4, H1171-H1193 (2009)
[9] Brim, L.; Demko, M.; Pastva, S.; Šafránek, D., High-performance discrete bifurcation analysis for piecewise-affine dynamical systems, (Hybrid Systems Biology (2015), Springer), 58-74 · Zbl 1412.92115
[10] Bryce, D.; Gao, S.; Musliner, D. J.; Goldman, R. P., SMT-based nonlinear PDDL+ planning, (29th AAAI Conference on Artificial Intelligence (2015)), 3247
[11] Cao, J.-M.; Qu, Z.; Kim, Y.-H.; Wu, T.-J.; Garfinkel, A.; Weiss, J. N.; Karagueuzian, H. S.; Chen, P.-S., Spatiotemporal heterogeneity in the induction of ventricular fibrillation by rapid pacing, Circ. Res., 84, 11, 1318-1331 (1999)
[12] Chen, D. D.; Gray, R. A.; Uzelac, I.; Herndon, C.; Fenton, F. H., Mechanism for amplitude alternans in electrocardiograms and the initiation of spatiotemporal chaos, Phys. Rev. Lett., 118, 16, Article 168101 pp. (2017)
[13] Connolly, S. J.; Gent, M.; Roberts, R. S.; Dorian, P.; Roy, D.; Sheldon, R. S.; Mitchell, L. B.; Green, M. S.; Klein, G. J.; O’brien, B., Canadian implantable defibrillator study (CIDS), Circulation, 101, 11, 1297-1302 (2000)
[14] Cram, A. R.; Rao, H. M.; Tolkacheva, E. G., Toward prediction of the local onset of alternans in the heart, Biophys. J., 100, 4, 868-874 (2011)
[15] 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, 12, 3, 852 (2002)
[16] Fenton, F. H.; Cherry, E. M., Models of cardiac cell, Scholarpedia, 3, 8, 1868 (2008)
[17] Feret, J., Reachability analysis of biological signalling pathways by abstract interpretation, (Computation in Modern Science and Engineering, Volume 2, Part A. Computation in Modern Science and Engineering, Volume 2, Part A, AIP Conference Proceedings, vol. 963 (2007)), 619-622
[18] Gao, S.; Avigad, J.; Clarke, E. M., Delta-complete decision procedures for satisfiability over the reals, (Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR’12 (2012), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 286-300 · Zbl 1358.03028
[19] Gao, S.; Kong, S.; Chen, W.; Clarke, E. M., Delta-complete analysis for bounded reachability of hybrid systems (2014), CoRR
[20] Gao, S.; Kong, S.; Clarke, E. M., dReal: an SMT solver for nonlinear theories over the reals, (Automated Deduction - CADE-24 (2013), Springer), 208-214 · Zbl 1381.68268
[21] Gao, S.; Kong, S.; Clarke, E. M., dReal: an SMT solver for nonlinear theories over the reals, (Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction. Proceedings. Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction. Proceedings, Lake Placid, NY, USA, June 9-14, 2013 (2013)), 208-214 · Zbl 1381.68268
[22] 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)
[23] Henderson, M. E., Multiple parameter continuation: computing implicitly defined k-manifolds, Internat. J. Bifurc. Chaos, 12, 03, 451-476 (2002) · Zbl 1044.37053
[24] Huang, Z.; Fan, C.; Mereacre, A.; Mitra, S.; Kwiatkowska, M., Invariant verification of nonlinear hybrid automata networks of cardiac cells, (Proceedings of 26th International Conference on Computer Aided Verification (CAV). Proceedings of 26th International Conference on Computer Aided Verification (CAV), Lecture Notes in Comput. Sci., vol. 8559 (2014), Springer), 373-390
[25] Ikeda, T.; Saito, H.; Tanno, K.; Shimizu, H.; Watanabe, J.; Ohnishi, Y.; Kasamaki, Y.; Ozawa, Y., T-wave alternans as a predictor for sudden cardiac death after myocardial infarction, Am. J. Cardiol., 89, 1, 79-82 (2002)
[26] Islam, M. A.; Byrne, G.; Kong, S.; Clarke, E. M.; Cleaveland, R.; Fenton, F. H.; Grosu, R.; Jones, P. L.; Smolka, S. A., Bifurcation analysis of cardiac alternans using \(δ\)-decidability, (International Conference on Computational Methods in Systems Biology (2016), Springer), 132-146
[27] Islam, M. A.; De Francisco, R.; Fan, C.; Grosu, R.; Mitra, S.; Smolka, S. A., Model checking tap withdrawal in C. Elegans, (Hybrid Systems Biology (2015)), 195 · Zbl 1412.92039
[28] Islam, M. A.; Murthy, A.; Girard, A.; Smolka, S. A.; Grosu, R., Compositionality results for cardiac cell dynamics, (Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (2014), ACM), 243-252 · Zbl 1362.92017
[29] Nolasco, J. B.; Dahlen, R. W., A graphic method for the study of alternation in cardiac action potentials, J. Appl. Physiol., 25, 2, 191-196 (Aug. 1968)
[30] 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-1253 (May 2006), WOS:000237812200006
[31] Kapinski, J.; Deshmukh, J. V.; Sankaranarayanan, S.; Arechiga, N., Simulation-guided Lyapunov analysis for hybrid dynamical systems, (Hybrid Systems: Computation and Control (HSCC) (2014), ACM Press), 133-142 · Zbl 1362.93108
[32] Kong, S.; Gao, S.; Chen, W.; Clarke, E. M., dReach: \(δ\)-reachability analysis for hybrid systems, (Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS. Proceedings. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS. Proceedings, London, UK, April 11-18, 2015 (2015)), 200-205
[33] Kuck, K.-H.; Cappato, R.; Siebels, J.; Rüppel, R., Randomized comparison of antiarrhythmic drug therapy with implantable defibrillators in patients resuscitated from cardiac arrest, Circulation, 102, 7, 748-754 (2000)
[34] Legay, A.; Delahaye, B.; Bensalem, S., Statistical model checking: an overview, (RV, vol. 10 (2010)), 122-135
[35] Liu, B.; Kong, S.; Gao, S.; Zuliani, P.; Clarke, E. M., Towards personalized prostate cancer therapy using delta-reachability analysis, (Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (2015), ACM), 227-232
[36] Guevara, M.; Glass, L.; Shrier, A., Phase locking, period-doubling bifurcations, and irregular dynamics in periodically stimulated cardiac cells, Science, 214, 4527, 1350-1353 (Dec. 1981)
[37] McAnulty, J.; Halperin, B.; Kron, J.; Larsen, G.; Rait, M.; Swenson, R.; Floreck, R.; Marchant, C.; Hamlin, M.; Heywood, G., A comparison of antiarrhythmic-drug therapy with implantable defibrillators in patients resuscitated from near-fatal ventricular arrhythmias, N. Engl. J. Med., 337, 22, 1576-1583 (1997)
[38] Fuster, V.; Rydén, L. E.; Cannom, D. S.; Crijns, H. J.; Curtis, A. B.; Ellenbogen, K. A.; Halperin, J. L.; Le Heuzey, J.-Y.; Kay, G. N., ACC/AHA/ESC 2006 guidelines for the management of patients with atrial fibrillation—executive summary: a report of the American College of Cardiology/American Heart Association Task Force on practice guidelines and the European Society of Cardiology Committee for Practice Guidelines (writing committee to revise the 2001 guidelines for the management of patients with atrial fibrillation) developed in collaboration with the European Heart Rhythm Association and the Heart Rhythm Society, Eur. Heart J., 27, 16, 1979-2030 (2006)
[39] Mitchell, C. C.; Schaeffer, D. G., A two-current model for the dynamics of cardiac membrane, Bull. Math. Biol., 65, 5, 767-793 (2003) · Zbl 1334.92097
[40] Moss, A. J.; Hall, W. J.; Cannom, D. S.; Daubert, J. P.; Higgins, S. L.; Klein, H.; Levine, J. H.; Saksena, S.; Waldo, A. L.; Wilber, D., Improved survival with an implanted defibrillator in patients with coronary disease at high risk for ventricular arrhythmia, N. Engl. J. Med., 335, 26, 1933-1940 (1996)
[41] Murthy, A.; Islam, M. A.; Smolka, S. A.; Grosu, R., Computing bisimulation functions using SOS optimization and \(δ\)-decidability over the reals, (Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (2015), ACM), 78-87 · Zbl 1364.93728
[42] Murthy, A.; Islam, M. A.; Smolka, S. A.; Grosu, R., Computing compositional proofs of input-to-output stability using SOS optimization and \(δ\)-decidability, Nonlinear Anal. Hybrid Syst., 23, 272-286 (2017) · Zbl 1351.93133
[43] Narayan, S. M.; Krummen, D. E.; Shivkumar, K.; Clopton, P.; Rappel, W.-J.; Miller, J. M., Treatment of atrial fibrillation by the ablation of localized sources: confirm (conventional ablation for atrial fibrillation with or without focal impulse and rotor modulation) trial, J. Am. Coll. Cardiol., 60, 7, 628-636 (2012)
[44] Pastore, J. M.; Girouard, S. D.; Laurita, K. R.; Akar, F. G.; Rosenbaum, D. S., Mechanism linking t-wave alternans to the genesis of cardiac fibrillation, Circulation, 99, 10, 1385-1394 (1999)
[45] Gilmour, R. F.; Chialvo, D. R., Electrical restitution, critical mass, and the riddle of fibrillation, J. Cardiovasc. Electrophysiol., 10, 8, 1087-1089 (Aug. 1999)
[46] Shiferaw, Y.; Sato, D.; Karma, A., Coupled dynamics of voltage and calcium in paced cardiac cells, Phys. Rev. E, 71, 2, Article 021903 pp. (2005)
[47] Quail, T.; Shrier, A.; Glass, L., Predicting the onset of period-doubling bifurcations in noisy cardiac systems, Proc. Natl. Acad. Sci., 112, 30, 9358-9363 (July 2015)
[48] Vakulenko, L., Features of bioelectrical activity of the heart in children with chronic pyelonephritis, Med. Perspect., 19, 2, 85-92 (2014)
[49] Wang, Q.; Zuliani, P.; Kong, S.; Gao, S.; Sreach, E. M. Clarke, A probabilistic bounded delta-reachability analyzer for stochastic hybrid systems, (International Conference on Computational Methods in Systems Biology (2015), Springer)
[50] Watanabe, M. A.; Fenton, F. H.; Evans, S. J.; Hastings, H. M.; Karma, A., Mechanisms for discordant alternans, J. Cardiovasc. Electrophysiol., 12, 2, 196-206 (2001)
[51] Yang, Y.; Lin, H., Reachability analysis based model validation in systems biology, (Cybernetics and Intelligent Systems (CIS), 2010 IEEE Conference on (2010), IEEE), 14-19
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.