@article {, title = {Control and anticontrol of chaos in fractional-order models of Diabetes, HIV, Dengue, Migraine, Parkinson{\textquoteright}s and Ebola virus diseases}, journal = {Chaos, Solitons \& Fractals}, volume = {153}, year = {2021}, month = {12/2021}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:hCrLmN-GePgC}, author = {Manashita Borah and Debanita Das and Antara Gayan and Flavio Fenton and Elizabeth Cherry} } @article {, title = {Interactive 3D Human Heart Simulations on Segmented Human MRI Hearts}, year = {2021}, url = {https://www.cinc.org/2021/Program/accepted/261.pdf}, author = {John P. Berman and FLAVIO H. FENTON and ELIZABETH M. CHERRY and Tinen Iles and Paul A. Iaizzo and Abouzar Kaboudian} } @conference {, title = {MPC-guided Imitation Learning of Bayesian Neural Network Policies for the Artificial Pancreas}, booktitle = {Proceedings of CDC 2021, the 60th IEEE Conference on Decision and Control}, year = {2021}, month = {12/2021}, author = {H. Chen and N. Paoletti and S. A. Smolka and S. Lin} } @article {, title = {Neural Predictive Monitoring and a Comparison of Frequentist and Bayesian Approaches}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2021}, month = {05/2021}, author = {L. Bortolussi and F. Cairoli and N. Paoletti and S. A. Smolka and S. D. Stoller} } @article {, title = {Quantifying arrhythmic long QT effects of hydroxychloroquine and azithromycin with whole-heart optical mapping and simulations}, journal = {Heart Rhythm O2}, volume = {2}, year = {2021}, month = {08/2021}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:Ug5p-4gJ2f0C}, author = {Ilija Uzelac and Abouzar Kaboudian and Shahriar Iravanian and Jimena G Siles-Paredes and James C Gumbart and Hiroshi Ashikaga and Neal Bhatia and Robert F Gilmour Jr and Elizabeth M Cherry and Flavio H Fenton} } @conference {, title = {Verification of Neural ODEs with Stochastic Guarantees}, booktitle = {Proceedings of AAAI-21, 35th AAAI Conference on Artificial Intelligence}, year = {2021}, month = {02/2021}, author = {S. Gruenbacher and J. Cyranka and M. Lechner and S. A. Smolka and R. Grosu} } @article {, title = {Accelerating simulations of cardiac electrical dynamics through a multi-GPU platform and an optimized data structure}, journal = {Concurrency and Computation: Practice and Experience}, volume = {32}, year = {2020}, month = {03/2020}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&cstart=20\&pagesize=80\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:vDijr-p_gm4C}, author = {Eduardo C Vasconcellos and Esteban WG Clua and Flavio H Fenton and Marcelo Zamith} } @conference {, title = {Bayesian Neural Predictive Monitoring}, booktitle = {Proceedings of OVERLAY-20, Second Workshop on Formal Methods for AI}, year = {2020}, month = {09/2020}, author = {L. Bortolussi and F. Cairoli and N. Paoletti and S. A. Smolka and S. D. Stoller} } @article {, title = {Better Automata through Process Algebra}, journal = {arXiv preprint arXiv:2002.07562}, year = {2020}, author = {Cleaveland, Rance} } @article {, title = {Data-Driven Robust Control for a Closed-Loop Artificial Pancreas}, journal = {IEEE/ACM Transactions on Computational Biology and Bioinformatics}, volume = {17}, year = {2020}, month = {11/2020}, chapter = {1981}, author = {N. Paoletti and K. S. Liu and H. Chen and S. A. Smolka and S. Lin} } @article {, title = {Data-Driven Uncertainty Quantification for Cardiac Electrophysiological Models: Impact of Physiological Variability on Action Potential and Spiral Wave Dynamics}, journal = {Frontiers in physiology}, volume = {11}, year = {2020}, month = {11/2020}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:tuHXwOkdijsC}, author = {Pras Pathmanathan and Suran K Galappaththige and Jonathan M Cordeiro and Abouzar Kaboudian and Flavio H Fenton and Richard A Gray} } @article {, title = {Excitable dynamics in neural and cardiac systems}, journal = {Communications in Nonlinear Science and Numerical Simulation}, volume = {86}, year = {2020}, month = {07/2020}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:hMsQuOkrut0C}, author = {Roberto Barrio and Stephen Coombes and Mathieu Desroches and Flavio Fenton and Stefan Luther and Esther Pueyo} } @article {, title = {Fatal arrhythmias: another reason why doctors remain cautious about chloroquine/hydroxychloroquine for treating COVID-19}, journal = {Heart Rhythm}, volume = {17}, year = {2020}, month = {09/2020}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:tYavs44e6CUC}, author = {Ilija Uzelac and Shahriar Iravanian and Hiroshi Ashikaga and Neal K Bhatia and Conner Herndon and Abouzar Kaboudian and James C Gumbart and Elizabeth M Cherry and Flavio H Fenton} } @booklet {, title = {Lagrangian Reachtubes: The Next Generation}, year = {2020}, author = {Sophie Gruenbacher and Jacek Cyranka and Mathias Lechner and Md. Ariful Islam and Scott A. Smolka and Radu Grosu} } @conference {, title = {Next-Generation Lagrangian Reachtubes}, booktitle = {Proceedings of CDC 2020, 59th IEEE Conference on Decision and Control}, year = {2020}, month = {12/2020}, author = {S. Gruenbacher and J. Cyranka and M. Lechner and Md. A. Islam and S. A. Smolka and R. Grosu} } @article {, title = {Single-variable delay-differential equation approximations of the Fitzhugh-Nagumo and Hodgkin-Huxley models}, journal = {Communications in Nonlinear Science and Numerical Simulation}, volume = {82}, year = {2020}, pages = {105066}, doi = {10.1016/j.cnsns.2019.105066}, url = {https://doi.org/10.1016/j.cnsns.2019.105066}, author = {Raffael Bechara Rameh and ELIZABETH M. CHERRY and Rodrigo Weber dos Santos} } @article {, title = {Swarm Model Checking on the GPU}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2020}, author = {R. DeFrancisco and S. Cho and M. Ferdman and S. A. Smolka} } @conference {, title = {Temporal-logic query checking over finite data streams}, booktitle = {International Conference on Formal Methods for Industrial Critical Systems}, year = {2020}, publisher = {Springer, Cham}, organization = {Springer, Cham}, author = {Huang, Samuel and Cleaveland, Rance} } @article {, title = {Timed Automata Benchmark Description}, journal = {arXiv preprint arXiv:2005.13151}, year = {2020}, author = {Fontana, Peter and Cleaveland, Rance} } @conference {, title = {Towards Automated Comprehension and Alignment of Cardiac Models at the System Invariant Level}, booktitle = {CSBio{\textquoteright}20: Proceedings of the Eleventh International Conference on Computational Systems-Biology and Bioinformatics}, year = {2020}, author = {Huang, Samuel and Diep, Madeline and Jang, Kuk and Cherry, Elizabeth M and Fenton, Flavio H and Cleaveland, Rance and Lindvall, Mikael and Mangharam, Rahul and Porter, Adam} } @booklet {, title = {On The Verification of Neural ODEs with Stochastic Guarantees}, year = {2020}, author = {Sophie Gruenbacher and Ramin Hasani and Mathias Lechner and Jacek Cyranka and Scott A. Smolka and Radu Grosu} } @article {, title = {Delay differential equation-based models of cardiac tissue: Efficient implementation and effects on spiral-wave dynamics}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {29}, year = {2019}, pages = {123128}, doi = {10.1063/1.5128240}, url = {https://doi.org/10.1063/1.5128240}, author = {Johnny Moreira Gomes and Marcelo Lobosco and Rodrigo Weber dos Santos and ELIZABETH M. CHERRY} } @booklet {, title = {From Reactive Systems to Cyber-physical Systems: Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday}, year = {2019}, author = {Bartocci, Ezio and Cleaveland, Rance and Grosu, Radu and Sokolsky, Oleg} } @article {, title = {Large-scale interactive numerical experiments of chaos, solitons and fractals in real time via GPU in a web browser}, journal = {Chaos, Solitons \& Fractals}, volume = {121}, year = {2019}, pages = {6{\textendash}29}, doi = {10.1016/j.chaos.2019.01.005}, url = {https://doi.org/10.1016/j.chaos.2019.01.005}, author = {Abouzar Kaboudian and ELIZABETH M. CHERRY and FLAVIO H. FENTON} } @article {, title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans}, journal = {Theoretical Computer Science}, volume = {765}, year = {2019}, pages = {158{\textendash}169}, author = {Islam, Md Ariful and Cleaveland, Rance and Fenton, Flavio H and Grosu, Radu and Jones, Paul L and Smolka, Scott A} } @article {, title = {Real-time interactive simulations of large-scale systems on personal computers and cell phones: Toward patient-specific heart modeling and other applications}, journal = {Science Advances}, volume = {5}, year = {2019}, pages = {eaav6019}, doi = {10.1126/sciadv.aav6019}, url = {https://doi.org/10.1126/sciadv.aav6019}, author = {Abouzar Kaboudian and ELIZABETH M. CHERRY and FLAVIO H. FENTON} } @inbook {, title = {Scott Smolka and Me}, booktitle = {From Reactive Systems to Cyber-Physical Systems}, year = {2019}, pages = {1{\textendash}6}, publisher = {Springer, Cham}, organization = {Springer, Cham}, author = {Cleaveland, Rance} } @article {, title = {Spatiotemporal correlation uncovers characteristic lengths in cardiac tissue}, journal = {Physical Review E}, volume = {100}, year = {2019}, doi = {10.1103/physreve.100.020201}, url = {https://doi.org/10.1103/physreve.100.020201}, author = {Alessandro Loppini and Alessio Gizzi and Christian Cherubini and ELIZABETH M. CHERRY and FLAVIO H. FENTON and Simonetta Filippi} } @article {, title = {A tableau construction for finite linear-time temporal logic}, journal = {arXiv preprint arXiv:1910.09339}, year = {2019}, author = {Huang, Samuel and Cleaveland, Rance} } @conference {, title = {Automated Specification Extraction and Analysis with Specstractor}, booktitle = {Software Engineering and Formal Methods - 16th International Conference, {SEFM} 2018, Held as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings}, year = {2018}, doi = {10.1007/978-3-319-92970-5\_3}, url = {https://doi.org/10.1007/978-3-319-92970-5\_3}, author = {Christoph Schulze and Rance Cleaveland and Mikael Lindvall} } @conference {, title = {Bisimulation in Behavioral Dynamical Systems and Generalized Synchronization Trees}, booktitle = {2018 IEEE Conference on Decision and Control (CDC)}, year = {2018}, publisher = {IEEE}, organization = {IEEE}, author = {Ferlez, James and Cleaveland, Rance and Marcus, Steven I} } @article {, title = {Electromechanical vortex filaments during cardiac fibrillation}, journal = {Nature}, volume = {555}, year = {2018}, pages = {667+}, abstract = {

The self-organized dynamics of vortex-like rotating waves, which are also known as scroll waves, are the basis of the formation of complex spatiotemporal patterns in many excitable chemical and biological systems. In the heart, filament-like phase singularities5,6\ that are associated with three-dimensional scroll waves7\ are considered to be the organizing centres of life-threatening cardiac arrhythmias. The mechanisms that underlie the onset, maintenance and control14,15,16\ of electromechanical turbulence in the heart are inherently three-dimensional phenomena. However, it has not previously been possible to visualize the three-dimensional spatiotemporal dynamics of scroll waves inside cardiac tissues. Here we show that three-dimensional mechanical scroll waves and filament-like phase singularities can be observed deep inside the contracting heart wall using high-resolution four-dimensional ultrasound-based strain imaging. We found that mechanical phase singularities co-exist with electrical phase singularities during cardiac fibrillation. We investigated the dynamics of electrical and mechanical phase singularities by simultaneously measuring the membrane potential, intracellular calcium concentration and mechanical contractions of the heart. We show that cardiac fibrillation can be characterized using the three-dimensional spatiotemporal dynamics of mechanical phase singularities, which arise inside the fibrillating contracting ventricular wall. We demonstrate that electrical and mechanical phase singularities show complex interactions and we characterize their dynamics in terms of trajectories, topological charge and lifetime. We anticipate that our findings will provide novel perspectives for non-invasive diagnostic imaging and therapeutic applications.

}, doi = {https://doi.org/10.1038/nature26001}, author = {Jan Christoph and M. Chebbok and Carl Richter and Johannes Schr{\"o}der-Schetelig and Philip Bittihn and Seth Stein and Ilija Uzelac and FLAVIO H. FENTON and Gerd Hasenfuss and Robert F. Gilmour and Stefan Luther} } @article {, title = {An Optimization-Based Algorithm for the Construction of Cardiac Purkinje Network Models}, journal = {IEEE Transactions on Biomedical Engineering}, volume = {65}, year = {2018}, pages = {2760{\textendash}2768}, doi = {10.1109/tbme.2018.2815504}, url = {https://doi.org/10.1109/tbme.2018.2815504}, author = {Jesuliana N. Ulysses and Lucas A. Berg and ELIZABETH M. CHERRY and Ben R. Liu and Rodrigo W. dos Santos and Bruno G. de Barros and Bernardo M. Rocha and Rafael A. B. de Queiroz} } @article {, title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans}, journal = {Theoretical Computer Science}, year = {2018}, month = {02/2018}, abstract = {

Using a probabilistic reachability-based approach, we present a multi-parameter bifurcation analysis of electrical alternans in the two-current Mitchell{\textendash}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 δ-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.

}, keywords = {Bifurcation analysis, Cardiac alternans, Cardiac modeling, Formal methods, Hybrid systems, Probabilistic reachability}, issn = {0304-3975}, doi = {https://doi.org/10.1016/j.tcs.2018.02.005}, url = {http://www.sciencedirect.com/science/article/pii/S0304397518300823}, author = {Md. Ariful Islam and Rance Cleaveland and FLAVIO H. FENTON and Radu Grosu and Paul L. Jones and Scott A. Smolka} } @inbook {, title = {Process Algebra and Model Checking}, booktitle = {Handbook of Model Checking.}, year = {2018}, pages = {1149{\textendash}1195}, doi = {10.1007/978-3-319-10575-8\_32}, url = {https://doi.org/10.1007/978-3-319-10575-8\_32}, author = {Rance Cleaveland and A. W. Roscoe and Scott A. Smolka} } @conference {, title = {Programming is modeling}, booktitle = {International Symposium on Leveraging Applications of Formal Methods}, year = {2018}, publisher = {Springer, Cham}, organization = {Springer, Cham}, author = {Cleaveland, Rance} } @article {, title = {The role of conductivity discontinuities in design of cardiac defibrillation}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {28}, year = {2018}, pages = {013106}, abstract = {
Fibrillation is an erratic electrical state of the heart, of rapid twitching rather than organized contractions. Ventricular fibrillation is fatal if not treated promptly. The standard treatment, defibrillation, is a strong electrical shock to reinitialize the electrical dynamics and allow a normal heart beat. Both the normal and the fibrillatory electrical dynamics of the heart are organized into moving wave fronts of changing electrical signals, especially in the transmembrane voltage, which is the potential difference between the cardiac cellular interior and the intracellular region of the heart. In a normal heart beat, the wave front motion is from bottom to top and is accompanied by the release of Ca ions to induce contractions and pump the blood. In a fibrillatory state, these wave fronts are organized into rotating scroll waves, with a centerline known as a filament. Treatment requires altering the electrical state of the heart through an externally applied electrical shock, in a manner that precludes the existence of the filaments and scroll waves. Detailed mechanisms for the success of this treatment are partially understood, and involve local shock-induced changes in the transmembrane potential, known as virtual electrode alterations. These transmembrane alterations are located at boundaries of the cardiac tissue, including blood vessels and the heart chamber wall, where discontinuities in electrical conductivity occur. The primary focus of this paper is the defibrillation shock and the subsequent electrical phenomena it induces. Six partially overlapping causal factors for defibrillation success are identified from the literature. We present evidence in favor of five of these and against one of them. A major conclusion is that a dynamically growing wave front starting at the heart surface appears to play a primary role during defibrillation by critically reducing the volume available to sustain the dynamic motion of scroll waves; in contrast, virtual electrodes occurring at the boundaries of small, isolated blood vessels only cause minor effects. As a consequence, we suggest that the size of the heart (specifically, the surface to volume ratio) is an important defibrillation variable.
Fibrillation is an erratic state of the electrical signals in the heart, characterized by twitching rather than organized contractions. It is fatal if not treated promptly. It is a common cause of cardiac arrest, with 350 000 out of hospital US occurrences annually. The recommended treatment is a strong electrical shock, to reset the cardiac electrical activity, and allow resumption of a normal heart beat. The imperfect understanding of defibrillation mechanisms and the high dimensionality of its parameter space are obstacles to optimization of defibrillation treatment protocols. This work focuses on virtual electrodes (VE), which are charges occurring at cardiac boundaries (e.g., cardiac and blood vessel surfaces), due to shock induced alterations in the transmembrane potential. They are of primary importance for defibrillation. We present evidence that a dynamically growing wave front, starting at the heart surface, and aided by the dynamics of the fibrillation scroll waves to be more important than small, isolated blood vessels in terminating fibrillation. This conclusion is important for multiple reasons. It sheds light on mechanisms of virtual electrode formation and defibrillation. It allows a prioritization of experimental, simulation, and modeling focus. It places more emphasis on larger experimental animals for assessing novel low strength defibrillation strategies.
}, doi = {10.1063/1.5019367}, url = {https://doi.org/10.1063/1.5019367}, author = {Lim,Hyunkyung and Cun,Wenjing and Wang,Yue and Gray,Richard A. and Glimm,James} } @article {, title = {Alternans promotion in cardiac electrophysiology models by delay differential equations}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {27}, year = {2017}, pages = {093915}, abstract = {

Cardiac electrical alternans is a state of alternation between long and short action potentials and is frequently associated with harmful cardiac conditions. Different dynamic mechanisms can give rise to alternans; however, many cardiac models based on ordinary differential equations are not able to reproduce this phenomenon. A previous study showed that alternans can be induced by the introduction of delay differential equations (DDEs) in the formulations of the ion channel gating variables of a canine myocyte model. The present work demonstrates that this technique is not model-specific by successfully promoting alternans using DDEs for five cardiac electrophysiology models that describe different types of myocytes, with varying degrees of complexity. By analyzing results across the different models, we observe two potential requirements for alternans promotion via DDEs for ionic gates: (i) the gate must have a significant influence on the action potential duration and (ii) a delay must significantly impair the gate{\textquoteright}s recovery between consecutive action potentials.

}, issn = {1054-1500}, doi = {10.1063/1.4999471}, url = {http://aip.scitation.org/doi/10.1063/1.4999471}, author = {Gomes, Johnny M. and dos Santos, Rodrigo Weber and Cherry, Elizabeth M.} } @conference {, title = {Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees}, booktitle = {Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, {EXPRESS/SOS} 2017, Berlin, Germany, 4th September 2017.}, year = {2017}, doi = {10.4204/EPTCS.255.3}, url = {https://doi.org/10.4204/EPTCS.255.3}, author = {James Ferlez and Rance Cleaveland and Steven I. Marcus} } @article {, title = {Corrections to "A Menagerie of Timed Automata"}, journal = {ACM Comput. Surv.}, volume = {50}, year = {2017}, pages = {42:1{\textendash}42:8}, keywords = {Timed automata, timed transition systems, transition systems}, issn = {0360-0300}, doi = {10.1145/3078809}, url = {http://doi.acm.org/10.1145/3078809}, author = {Keiren, Jeroen J. A. and Fontana, Peter and Cleaveland, Rance} } @conference {, title = {Data assimilation for cardiac electrical dynamics}, booktitle = {Proceedings of the 5th {International} {Conference} on {Computational} and {Mathematical} {Biomedical} {Engineering}}, year = {2017}, address = {Pittsburgh, PA}, abstract = {

New insights into the mechanisms underlying cardiac arrhythmias may be possible from a greater understanding of variables unobserved in experimental settings. When experimental observations are sparse, data assimilation can be effective at recovering a more complete system state estimate. We have recently shown using synthetic observations of one- and three-dimensional cardiac tissue that data assimilation can be used to recover state variables observed sparsely in space and time or unobserved. Here we extend these findings to show that data assimilation remains effective in reconstructing cardiac states with underlying system spatial heterogeneity and in the presence of significant model error.

}, author = {Cherry, E. M. and Cairns, D. I. and Holt, N. and LaVigne, N. S. and Fenton, F. H. and Hoffman, M. J.}, editor = {Nithiarasu, P. and Robertson, A. M.} } @article {, title = {Distinguishing mechanisms for alternans in cardiac cells using constant-diastolic-interval pacing}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {27}, year = {2017}, pages = {093902}, abstract = {

Alternans, a proarrhythmic dynamical state in which cardiac action potentials alternate between long and short durations despite a constant pacing period, traditionally has been explained at the cellular level using nonlinear dynamics principles under the assumption that the action potential duration (APD) is determined solely by the time elapsed since the end of the previous action potential, called the diastolic interval (DI). In this scenario, APDs at a steady state should be the same provided that the preceding DIs are the same. Nevertheless, experiments attempting to eliminate alternans by dynamically adjusting the timing of pacing stimuli to keep the DI constant showed that alternans persisted, contradicting the traditional theory. It is now widely known that alternans also can arise from a different mechanism associated with intracellular calcium cycling. Our goal is to determine whether intracellular calcium dynamics can explain the experimental findings regarding the persistence of alternans despite a constant DI. For this, we use mathematical models capable of producing alternans through both voltage- and calcium-mediated mechanisms. We show that for voltage-driven alternans, action potentials elicited from a constant-DI protocol are always the same. However, in the case of calcium-driven alternans, the constant-DI protocol can result in alternans. Reducing the strength of the calcium instability progressively reduces and finally eliminates constant-DI alternans. Our findings suggest that screening for the presence of alternans using a constant-DI protocol has the potential for differentiating between voltage-driven and calcium-driven alternans.

}, issn = {1054-1500}, doi = {10.1063/1.4999354}, url = {http://aip.scitation.org/doi/10.1063/1.4999354}, author = {Cherry, Elizabeth M.} } @article {, title = {Effects of model error on cardiac electrical wave state reconstruction using data assimilation}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {27}, year = {2017}, pages = {093911}, abstract = {

Reentrant electrical scroll waves have been shown to underlie many cardiac arrhythmias, but the inability to observe locations away from the heart surfaces and the restriction of observations to only one or two state variables have made understanding arrhythmia mechanisms challenging. Recently, we showed that data assimilation from spatiotemporally sparse surrogate observations could be used to reconstruct a reliable time series of state estimates of reentrant cardiac electrical waves including unobserved variables in one and three spatial dimensions. However, real cardiac tissue is unlikely to be described accurately by mathematical models because of errors in model formulation and parameterization as well as intrinsic but poorly described spatial heterogeneity of electrophysiological properties in the heart. Here, we extend our previous work to assess how model error affects the accuracy of cardiac state estimates achieved using data assimilation with the Local Ensemble Transform Kalman Filter. We focus on one-dimensional states of discordant alternans characterized by significant wavelength oscillations. We demonstrate that data assimilation can provide high-quality estimates under a wide range of model error conditions, ranging from varying one or more parameter values to using an entirely different model to generate the truth state. We illustrate how multiplicative and additive inflation can be used to reduce error in the state estimates. Even when the truth state contains underlying spatial heterogeneity, we show that using a homogeneous model in the data assimilation algorithm can achieve good results. Overall, we find data assimilation to be a robust approach for reconstructing complex cardiac electrical states corresponding to arrhythmias even in the presence of model error.

}, issn = {1054-1500}, doi = {10.1063/1.4999603}, url = {http://aip.scitation.org/doi/10.1063/1.4999603}, author = {LaVigne, Nicholas S. and Holt, Nathan and Hoffman, Matthew J. and Cherry, Elizabeth M.} } @article {, title = {Efficient parameterization of cardiac action potential models using a genetic algorithm}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {27}, year = {2017}, pages = {093922}, abstract = {

Finding appropriate values for parameters in mathematical models of cardiac cells is a challenging task. Here, we show that it is possible to obtain good parameterizations in as little as 30{\textendash}40 s when as many as 27 parameters are fit simultaneously using a genetic algorithm and two flexible phenomenological models of cardiac action potentials. We demonstrate how our implementation works by considering cases of {\textquotedblleft}model recovery{\textquotedblright} in which we attempt to find parameter values that match model-derived action potential data from several cycle lengths. We assess performance by evaluating the parameter values obtained, action potentials at fit and non-fit cycle lengths, and bifurcation plots for fidelity to the truth as well as consistency across different runs of the algorithm. We also fit the models to action potentials recorded experimentally using microelectrodes and analyze performance. We find that our implementation can efficiently obtain model parameterizations that are in good agreement with the dynamics exhibited by the underlying systems that are included in the fitting process. However, the parameter values obtained in good parameterizations can exhibit a significant amount of variability, raising issues of parameter identifiability and sensitivity. Along similar lines, we also find that the two models differ in terms of the ease of obtaining parameterizations that reproduce model dynamics accurately, most likely reflecting different levels of parameter identifiability for the two models.

}, issn = {1054-1500}, doi = {10.1063/1.5000354}, url = {http://aip.scitation.org/doi/10.1063/1.5000354}, author = {Cairns, Darby I. and Fenton, Flavio H. and Cherry, E. M.} } @article {, title = {Improving Invariant Mining via Static Analysis}, journal = {ACM Trans. Embed. Comput. Syst.}, volume = {16}, year = {2017}, pages = {167:1{\textendash}167:20}, keywords = {automated test generation, Invariant mining, model-based development, verification and validation}, issn = {1539-9087}, doi = {10.1145/3126504}, url = {http://doi.acm.org/10.1145/3126504}, author = {Schulze, Christoph and Cleaveland, Rance} } @conference {, title = {Lagrangian Reachabililty}, booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017 Proceedings, Part {I}}, year = {2017}, abstract = {

We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

}, doi = {10.1007/978-3-319-63387-9_19}, author = {Jacek Cyranka and Md. Ariful Islam and Greg Byrne and Paul L. Jones and Scott A. Smolka and Radu Grosu} } @article {, title = {Mechanism for amplitude alternans in electrocardiograms and the initiation of spatiotemporal chaos}, journal = {Physical Review Letters}, volume = {118}, year = {2017}, pages = {168101}, abstract = {

It is widely believed that one major life-threatening transition to chaotic fibrillation occurs via spiral-wave breakup that is preceded by spatiotemporal dispersion of refractoriness due to alternations in the duration of the cardiac action potential (AP). However, recent clinical and experimental evidence suggests that other characteristics of the AP may contribute to, and perhaps drive, this dangerous dynamical instability. To identify the relative roles of AP characteristics, we performed experiments in rabbit hearts under conditions to minimize AP duration dynamics which unmasked pronounced AP amplitude alternans just before the onset of fibrillation. We used a simplified ionic cell model to derive a return map and a stability condition that elucidates a novel underlying mechanism for AP alternans and spiral breakup. We found that inactivation of the sodium current is key to developing amplitude alternans and is directly connected to conduction block and initiation of arrhythmias. Simulations in 2D where AP amplitude alternation led to turbulence confirm our hypothesis.

}, author = {Chen, Diandian Diana and Gray, Richard A and Uzelac, Ilija and Herndon, Conner and Fenton, Flavio H} } @article {, title = {A Menagerie of Timed Automata (vol 50, 42, 2017)}, journal = {ACM COMPUTING SURVEYS}, volume = {50}, year = {2017}, author = {Keiren, Jeroen JA and Fontana, Peter and Cleaveland, Rance} } @conference {, title = {Opacity for switched linear systems: Notions and characterization}, booktitle = {2017 IEEE 56th Annual Conference on Decision and Control (CDC)}, year = {2017}, month = {Dec}, keywords = {allowed switching sequences, directed graph, directed graphs, discrete time systems, discrete-time switched linear systems, linear systems, Mathematical model, Power systems, switched linear systems, Switched systems, Switches, switching systems (control)}, doi = {10.1109/CDC.2017.8264445}, author = {B. Ramasubramanian and R. Cleaveland and S. I. Marcus} } @conference {, title = {Query Checking for Linear Temporal Logic}, year = {2017}, month = {25 August 2017}, publisher = {Springer, Cham}, organization = {Springer, Cham}, abstract = {

The query-checking problem for temporal logic may be formulated as follows. Given a Kripke structure\ M\ and a temporal-logic\ query\ of form\ ϕ[var]ϕ[var], which may be thought of as a temporal formula with a missing propositional subformula\ varvar, find the most precise propositional formula\ f\ that, when substituted for\ varvar\ in\ ϕ[var]ϕ[var], ensures\ M\ satisfies the resulting temporal property. Query checking has been used for system comprehension, specification reconstruction, and other related applications in the formal analysis of systems.

In this paper we present an automaton-based methodology for query checking over linear temporal logic (LTL). While this problem is known to be hard in the general case, we show that by exploiting several key observations about the interplay between the input model\ M\ and the query\ ϕ[var]ϕ[var], we can produce results for many problems of interest. In support of this claim, we report on preliminary experimental data for an implementation of our technique.

}, isbn = {978-3-319-67113-0}, doi = {https://doi.org/10.1007/978-3-319-67113-0_3}, url = {https://link.springer.com/chapter/10.1007/978-3-319-67113-0_3}, author = {Samuel Huang and Rance Cleaveland} } @conference {, title = {The role of conductivity discontinuities in design of cardiac de brillation}, year = {2017}, publisher = {Chaos}, organization = {Chaos}, abstract = {

Fibrillation is an erratic electrical state of the heart, of rapid twitching rather than\ organized contractions. Ventricular brillation is fatal if not treated promptly. The\ standard treatment, debrillation, is a strong electrical shock to reinitialize the elec-trical dynamics and allow a normal heart beat. Both the normal and the brillatory\ electrical dynamics of the heart are organized into moving wave fronts of changing electrical signals, especially in the transmembrane voltage, which is the potential dif-ference between the cardiac cellular interior and the intracellular region of the heart.
In a normal heart beat, the wave front motion is from bottom to top and is accom-panied by the release of Ca ions to induce contractions and pump the blood. In a\ brillatory state, these wave fronts are organized into rotating scroll waves, with a\ centerline known as a lament. Treatment requires altering the electrical state of the heart through an externally applied electrical shock, in a manner that precludes the\ existence of the laments and scroll waves. Detailed mechanisms for the success of\ this treatment are partially understood, and involve local shock-induced changes in
the transmembrane potential, known as virtual electrode alterations. These trans-membrane alterations are located at boundaries of the cardiac tissue, including blood vessels and the heart chamber wall, where discontinuities in electrical conductivity\ occur. The primary focus of this paper is the debrillation shock and the subsequent\ electrical phenomena it induces. Six partially overlapping causal factors for debril-lation success are identied from the literature. We present evidence in favor of veof these and against one of them. A major conclusion is that a dynamically growing
wave front, starting at the heart surface appears to play a primary role during deb-rillation by critically reducing the volume required to sustain the dynamic motion of\ scroll waves; in contrast, virtual electrode occurring at boundaries of small, isolated\ blood vessels only cause minor e ects. As a consequence, we suggest that the size\ of the heart (specically, the surface to volume ratio) is an important debrillation\ variable.

Fibrillation is an erratic state of the electrical signals in the heart, character-
ized by twitching rather than organized contractions. It is fatal if not treated
promptly. It is a common cause of cardiac arrest, with 350,000 out of hospital US\ occurrences annually. The recommended treatment is a strong electrical shock,\ to reset the cardiac electrical activity, and allow resumption of a normal heart\ beat. The imperfect understanding of debrillation mechanisms and the high di-mensionality of its parameter space are obstacles to optimization of debrillation treatment protocols. This work focuses on virtual electrodes, which are charges\ occurring at cardiac boundaries, (e. g. cardiac and blood vessel surfaces), due to
shock induced alterations in the transmembrane potential. They are of primary\ importance for debrillation. We present evidence that a dynamically growing\ wave front, starting at the heart surface, and aided by the dynamics of the fib-rillation scroll waves to be more important than small, isolated blood vessels in\ terminating brillation. This conclusion is important for multiple reasons. It\ sheds light on mechanisms of virtual electrode formation and debrillation. It\ allows a prioritization of experimental, simulation and modeling focus, It places\ more emphasis on larger experimental animals for assessing novel low strength\ debrillation strategies.

}, author = {HYUNKYUNG LIM and Wenjing Cun and Richard A. Gray and JAMES GLIMM} } @article {, title = {Simultaneous Quantification of Spatially Discordant Alternans in Voltage and Intracellular Calcium in Langendorff-Perfused Rabbit Hearts and Inconsistencies with Models of Cardiac Action Potentials and Ca Transients}, journal = {Frontiers in Physiology}, volume = {8}, year = {2017}, doi = {10.3389/fphys.2017.00819}, url = {https://doi.org/10.3389/fphys.2017.00819}, author = {Ilija Uzelac and Yanyan C. Ji and Daniel Hornung and Johannes Schr{\"o}der-Scheteling and Stefan Luther and Richard A. Gray and ELIZABETH M. CHERRY and FLAVIO H. FENTON} } @conference {, title = {Bifurcation Analysis of Cardiac Alternans Using δ -Decidability.}, booktitle = {CMSB}, year = {2016}, publisher = {Springer}, organization = {Springer}, keywords = {dblp}, isbn = {978-3-319-45176-3}, url = {http://dblp.uni-trier.de/db/conf/cmsb/cmsb2016.html$\#$IslamBKCCFGJS16}, author = {Islam, Md. Ariful and Byrne, Greg and Kong, Soonho and Clarke, Edmund M. and Cleaveland, Rance and Fenton, Flavio H. and Grosu, Radu and Jones, Paul L. and Smolka, Scott A.}, editor = {Bartocci, Ezio and Li{\`o}, Pietro and Paoletti, Nicola} } @conference {, title = {Cybercardia project: Modeling, verification and validation of implantable cardiac devices}, booktitle = {2016 IEEE International Conference on Bioinformatics and Biomedicine (BIBM)}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, author = {Islam, Md Ariful and Lim, Hyunkyung and Paoletti, Nicola and Abbas, Houssam and Jiang, Zhihao and Cyranka, Jacek and Cleaveland, Rance and Gao, Sicun and Clarke, Edmund and Grosu, Radu and others} } @conference {, title = {Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus}, booktitle = {2016 IEEE 27th International Symposium on Software Reliability Engineering (ISSRE)}, year = {2016}, month = {Oct}, keywords = {aerospace computing, API, application program interfaces, Automation, Computer architecture, Concurrency, Concurrent computing, concurrent design, concurrent flight software bus, concurrent publisher-subscriber architecture style, concurrent system testing, Context, Flight Software, MBT technique, message passing, Microsoft Spec Explorer MBT tool, middleware, Model Based Testing, model-based test automation, NASA, NASA Core Flight Software software bus module, program testing, Publish-Subscribe, safety-critical software, safety-critical system, Software, software architecture, SUT, system-under-test, test case analysis, Testing}, doi = {10.1109/ISSRE.2016.47}, author = {D. Ganesan and M. Lindvall and S. Hafsteinsson and R. Cleaveland and S. L. Strege and W. Moleski} } @article {, title = {An extensible formal semantics for UML activity diagrams}, journal = {arXiv preprint arXiv:1604.02386}, year = {2016}, author = {Daw, Zamira and Cleaveland, Rance} } @conference {, title = {A framework for decentralized opacity in linear systems}, booktitle = {2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton)}, year = {2016}, month = {Sept}, keywords = {adversarial observer, colluding adversary, Computers, cyber-physical system, Cyber-physical systems, decentralized opacity, directed graph, directed graphs, ISO, linear system, linear systems, observers, Power systems, Trajectory}, doi = {10.1109/ALLERTON.2016.7852240}, author = {B. Ramasubramanian and R. Cleaveland and S. I. Marcus} } @conference {, title = {A framework for opacity in linear systems}, booktitle = {2016 American Control Conference, {ACC} 2016, Boston, MA, USA, July 6-8, 2016}, year = {2016}, doi = {10.1109/ACC.2016.7526666}, url = {https://doi.org/10.1109/ACC.2016.7526666}, author = {Bhaskar Ramasubramanian and Rance Cleaveland and Steven I. Marcus} } @article {, title = {SHARP BOUNDARY ELECTROCARDIAC SIMULATIONS}, year = {2016}, address = {Stony Brook}, abstract = {

We present a sharp boundary electrocardiac simulation model based on the finite volume embedded boundary method for the solution of voltage dynamics in irregular domains with anisotropy and a high degree of anatomical detail. This method is second order accurate uniformly up to boundaries and is able to resolve small features without the use of fine meshes. This capability is necessary to enable the repeated simulations required for future verification and validation and uncertainty quantification studies of defibrillation, where fine-scale heterogeneities, such as those formed by small blood vessels, play an important role and require resolution.

}, keywords = {cardiac electrophysiology, embedded boundary method, tensor diffusion}, doi = {10.1137/15M1019283}, author = {SHUAI XUE and HYUNKYUNG LIM and JAMES GLIMM and FLAVIO H. FENTON and ELIZABETH M. CHERRY} } @article {, title = {Abstract Model Repair}, journal = {Logical Methods in Computer Science}, volume = {3:11}, year = {2015}, author = {G. Chatzieleftheriou and B. Bonakdarpour and P. Katsaros and S. A. Smolka} } @article {, title = {Comparing model checkers for timed UML activity diagrams}, journal = {Science of Computer Programming}, volume = {111}, year = {2015}, pages = {277{\textendash}299}, author = {Daw, Zamira and Cleaveland, Rance} } @conference {, title = {An Extensible Operational Semantics for {UML} Activity Diagrams}, booktitle = {Software Engineering and Formal Methods - 13th International Conference, {SEFM} 2015, York, UK, September 7-11, 2015. Proceedings}, year = {2015}, doi = {10.1007/978-3-319-22969-0\_25}, url = {https://doi.org/10.1007/978-3-319-22969-0\_25}, author = {Zamira Daw and Rance Cleaveland} } @article {, title = {Model-Order Reduction of Ion Channel Dynamics Using Approximate Bisimulation}, journal = {Theoretical Computer Science}, volume = {599C}, year = {2015}, month = {09/2015}, chapter = {34}, author = {Md. A. Islam and A. Murthy and E. Bartocci and E. M. Cherry and F. H. Fenton and J. Glimm and S. A. Smolka and R. Grosu} } @article {, title = {Security assurance cases for medical cyber{\textendash}physical systems}, journal = {IEEE Design \& Test}, volume = {32}, year = {2015}, pages = {56{\textendash}65}, author = {Ray, Arnab and Cleaveland, Rance} } @conference {, title = {UML-VT: A Formal Verification Environment for UML Activity Diagrams.}, booktitle = {P\&D@ MoDELS}, year = {2015}, author = {Daw, Zamira and Mangino, John and Cleaveland, Rance} }