Bifurcation analysis of cardiac alternans using δ-decidability

Md Ariful Islam, Greg Byrne, Soonho Kong, Edmund M. Clarke, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations


We present a bifurcation analysis of electrical alternans in the two-current Mitchell-Schaeffer (MS) cardiac-cell model using the theory of δ-decidability over the reals. Electrical alternans is a phenomenon characterized by a variation in the successive Action Potential Durations (APDs) generated by a single 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 bifurcation analysis we perform determines, for each control parameter τ of the MS model, the bifurcation point in the range of τ such that a small perturbation to this value results in a transition from alternans to non-alternans behavior. To the best of our knowledge, our analysis represents the first formal verification of non-trivial dynamics in a numerical cardiac-cell model. Our approach to this problem rests on encoding alternans-like behavior in the MS model as a 11-mode, multinomial hybrid automaton (HA). For each model parameter, we then apply a sophisticated, guided-searchbased reachability analysis to this HA to estimate parameter ranges for both alternans and non-alternans behavior. The bifurcation point separates these two ranges, but with an uncertainty region due to the underlying δ-decision procedure. This uncertainty region, however, can be reduced by decreasing δ at the expense of increasing the model exploration time. Experimental results are provided that highlight the effectiveness of this method.

Original languageEnglish
Title of host publicationComputational Methods in Systems Biology - 14th International Conference, CMSB 2016, Proceedings
EditorsNicola Paoletti, Ezio Bartocci, Pietro Lio
Number of pages15
ISBN (Print)9783319451763
StatePublished - 2016
Event14th Conference on Computational Methods in Systems Biology, CMSB 2016 - Cambridge, United Kingdom
Duration: Sep 21 2016Sep 23 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9859 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference14th Conference on Computational Methods in Systems Biology, CMSB 2016
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Bifurcation analysis of cardiac alternans using δ-decidability'. Together they form a unique fingerprint.

Cite this