Talks and Poster Presentations (with Proceedings-Entry):
A. Islam, G. Byrne, S. Kong, E. Clarke, R. Cleaveland, F. Fenton, R. Grosu, P. Jones, S. Smolka:
"Bifurcation Analysis of Cardiac Alternans using Delta-Decidability";
Talk: CMSB 2016: 14th International Conference on Computational Methods in Systems Biology,
Cambridge, UK;
2016-09-21
- 2016-09-23; in: "Proceedings of CMSB'16, the 14th International Conference on Computational Methods in Systems Biology",
LNCS, Springer,
Lecture Notes in Computer Science, Vol. 9859, Cambridge, UK
(2016),
ISBN: 978-3-319-45176-3;
132
- 146.
English abstract:
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-search-based 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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-45177-0_9
Electronic version of the publication:
http://link.springer.com/chapter/10.1007%2F978-3-319-45177-0_9