@booklet {, title = {Adversarial Training is Not Ready for Robot Learning}, year = {2021}, author = {Mathias Lechner and Ramin Hasani and Radu Grosu and Daniela Rus and Thomas A. Henzinger} } @conference {, title = {Collision-Free 3D Flocking Using the Distributed Simplex Architecture}, booktitle = {Proceedings of ISoLA Extra in Rhodes}, year = {2021}, month = {10/2021}, author = {U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller} } @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} } @conference {, title = {Distributed Control for Flocking Maneuvers via Acceleration-Weighted Neighborhooding}, booktitle = {Proceedings of ACC 2021, The 2021 American Control Conference}, year = {2021}, month = {06/2021}, author = {S. Roy and U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller and A. Tiwari} } @conference {, title = {A Distributed Simplex Architecture for Multi-Agent Systems}, booktitle = {Proceedings of SETTA 2021, Symposium on Dependable Software Engineering}, year = {2021}, month = {11/2021}, author = {U. Mehmood and S. D. Stoller and R. Grosu and S. Roy and A. Damare and S. D. Smolka} } @conference {, title = {Model-Checking Support for File System Development}, booktitle = {Proceeding of HotStorage {\textquoteright}21, the 13th ACM Workshop on Hot Topics in Storage and File Systems}, year = {2021}, month = {07/2021}, author = {W. Su and Y. Liu and G. Ganesan and G. Holzmann and G. Kuenning and S. A. Smolka and E. Zadok} } @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 = {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 = {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} } @conference {, title = {Gershgorin Loss Stabilizes the Recurrent Neural Network Compartment of an End-to-end Robot Learning Scheme}, booktitle = {2020 IEEE International Conference on Robotics and Automation (ICRA)}, year = {2020}, doi = {10.1109/ICRA40945.2020.9196608}, author = {Lechner, Mathias and Hasani, Ramin and Rus, Daniela and Grosu, Radu} } @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} } @booklet {, title = {Learning Distributed Controllers for V-Formation}, year = {2020}, author = {Shouvik Roy and Usama Mehmood and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Ashish Tiwari} } @booklet {, title = {Liquid Time-constant Networks}, year = {2020}, author = {Ramin Hasani and Mathias Lechner and Alexander Amini and Daniela Rus and Radu Grosu} } @conference {, title = {A Natural Lottery Ticket Winner: Reinforcement Learning with Ordinary Neural Circuits}, booktitle = {Proceedings of the 37th International Conference on Machine Learning}, year = {2020}, month = {13{\textendash}18 Jul}, publisher = {PMLR}, organization = {PMLR}, abstract = {

We propose a neural information processing system obtained by re-purposing the function of a biological neural circuit model to govern simulated and real-world control tasks. Inspired by the structure of the nervous system of the soil-worm, C. elegans, we introduce ordinary neural circuits (ONCs), defined as the model of biological neural circuits reparameterized for the control of alternative tasks. We first demonstrate that ONCs realize networks with higher maximum flow compared to arbitrary wired networks. We then learn instances of ONCs to control a series of robotic tasks, including the autonomous parking of a real-world rover robot. For reconfiguration of the purpose of the neural circuit, we adopt a search-based optimization algorithm. Ordinary neural circuits perform on par and, in some cases, significantly surpass the performance of contemporary deep learning models. ONC networks are compact, 77\% sparser than their counterpart neural controllers, and their neural dynamics are fully interpretable at the cell-level.

}, url = {http://proceedings.mlr.press/v119/hasani20a.html}, author = {Hasani, Ramin and Lechner, Mathias and Amini, Alexander and Rus, Daniela and Grosu, Radu}, editor = {Hal Daum{\'e} III and Aarti Singh} } @booklet {, title = {Neural Flocking: MPC-based Supervised Learning of Flocking Controllers}, year = {2020}, author = {Shouvik Roy and Usama Mehmood and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Ashish Tiwari} } @booklet {, title = {Neural Simplex Architecture}, year = {2020}, author = {Dung T. Phan and Radu Grosu and Nils Jansen and Nicola Paoletti and Scott A. Smolka and Scott D. Stoller} } @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} } @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} } @inbook {, title = {From Automated MRI Scan to Finite Elements}, year = {2019}, pages = {35-48}, isbn = {978-3-030-31513-9}, doi = {10.1007/978-3-030-31514-6_3}, author = {Glimm, James and Lim, Hyunkyung and Bishop, Martin and Kim, Soojin} } @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 = {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 = {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 = {An Algebraic Framework for Runtime Verification}, journal = {CoRR}, volume = {abs/1802.03775}, year = {2018}, url = {http://arxiv.org/abs/1802.03775}, author = {Stefan Jaksic and Ezio Bartocci and Radu Grosu and Dejan Nickovic} } @conference {, title = {Declarative vs Rule-based Control for Flocking Dynamics}, booktitle = {Proceedings of the 33rd Annual ACM Symposium on Applied Computing}, year = {2018}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, isbn = {978-1-4503-5191-1}, doi = {10.1145/3167132.3167222}, url = {http://doi.acm.org/10.1145/3167132.3167222}, author = {Mehmood, Usama and Paoletti, Nicola and Phan, Dung and Grosu, Radu and Lin, Shan and Stoller, Scott D. and Tiwari, Ashish and Yang, Junxing and Smolka, Scott A.} } @article {, title = {Discordant Alternans as a Mechanism for Initiation of Ventricular Fibrillation In Vitro}, journal = {Journal of the American Heart Association}, volume = {7}, year = {2018}, month = {09}, abstract = {

Background-{\textemdash}Ventricular tachyarrhythmias are often preceded by short sequences of premature ventricular complexes. In a previous study, a restitution-based computational model predicted which sequences of stimulated premature complexes were most likely to induce ventricular fibrillation in canines in vivo. However, the underlying mechanism, based on discordant-alternans dynamics, could not be verified in that study. The current study seeks to elucidate the mechanism by determining whether the spatiotemporal evolution of action potentials and initiation of ventricular fibrillation in in vitro experiments are consistent with model predictions.

Methods and Results-{\textemdash}Optical mapping voltage signals from canine right-ventricular tissue (n=9) were obtained simultaneously from the entire epicardium and endocardium during and after premature stimulus sequences. Model predictions of action potential propagation along a 1-dimensional cable were developed using action potential duration versus diastolic interval data. The model predicted sign-change patterns in action potential duration and diastolic interval spatial gradients with posterior probabilities of 91.1\%, and 82.1\%, respectively. The model predicted conduction block with 64\% sensitivity and 100\% specificity. A generalized estimating equation logistic-regression approach showed that model-prediction effects were significant for both conduction block (P\<191015, coefficient 44.36) and sustained ventricular fibrillation (P=0.0046, coefficient, 1.63) events.

Conclusions-{\textemdash}The observed sign-change patterns favored discordant alternans, and the model successfully identified sequences of premature stimuli that induced conduction block. This suggests that the relatively simple discordant-alternans-based process that led to block in the model may often be responsible for ventricular fibrillation onset when preceded by premature beats. These observations may aid in developing improved methods for anticipating block and ventricular fibrillation. (J Am Heart Assoc. 2018;7:e007898. DOI: 10.1161/JAHA.117.007898.)

}, keywords = {alternans, arrhythmia (mechanisms), computer-based model, electrophysiology, ventricular fibrillation}, doi = {10.1161/JAHA.117.007898}, author = {Munoz, Laura and R. M. Gelzer, Anna and Fenton, Flavio and Qian, Wei and Lin, WeiYe and F. Gilmour, Robert and F. Otani, Niels} } @article {, title = {Dynamic Network Model from Partial Observations}, journal = {CoRR}, volume = {abs/1805.10616}, year = {2018}, url = {http://arxiv.org/abs/1805.10616}, author = {Elahe Ghalebi K. and Baharan Mirzasoleiman and Radu Grosu and Jure Leskovec} } @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} } @conference {, title = {Neural State Classification for Hybrid Systems}, booktitle = {Proc.\ 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018)}, year = {2018}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, author = {Dung Phan and Nicola Paoletti and Timothy Zhang and Radu Grosu and Scott A. Smolka and Scott D. Stoller} } @conference {, title = {OpenUAV: A UAV Testbed for the CPS and Robotics Community}, booktitle = {Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems}, year = {2018}, publisher = {IEEE Press}, organization = {IEEE Press}, address = {Piscataway, NJ, USA}, isbn = {978-1-5386-5301-2}, doi = {10.1109/ICCPS.2018.00021}, url = {https://doi.org/10.1109/ICCPS.2018.00021}, author = {Schmittle, Matt and Lukina, Anna and Vacek, Lukas and Das, Jnaneshwar and Buskirk, Christopher P. and Rees, Stephen and Sztipanovits, Janos and Grosu, Radu and Kumar, Vijay} } @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} } @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} } @conference {, title = {Unsupervised Wafermap Patterns Clustering via Variational Autoencoders}, booktitle = {2018 International Joint Conference on Neural Networks (IJCNN)}, year = {2018}, month = {07/2018}, publisher = {IEEE}, organization = {IEEE}, address = {Rio, Brasil}, author = {Peter Tulala and Hamidreza Mahyar and Elahe Ghalebi and Radu Grosu} } @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.} } @article {, title = {Collision Avoidance for Mobile Robots with Limited Sensing and Limited Information about Moving Obstacles}, journal = {Formal Methods in System Design}, year = {2017}, month = {01/2017}, author = {D. Phan and J. Yang and R. Grosu and S. A. Smolka and S. D. Stoller} } @article {, title = {Dynamics of a human spiral wave}, journal = {Phys. Today}, volume = {70}, year = {2017}, month = {02/2017}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&cstart=20\&pagesize=80\&citation_for_view=jKiNd-0AAAAJ:BrmTIyaxlBUC}, author = {Andrea J Welsh and Edwin F Greco and Flavio H Fenton} } @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 = {Modeling bipolar stimulation of cardiac tissue}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {27}, year = {2017}, pages = {093920}, abstract = {

Unipolar stimulation of cardiac tissue is often used in the design of cardiac pacemakers because of the low current required to depolarize the surrounding tissue at rest. However, the advantages of unipolar over bipolar stimulation are not obvious at shorter coupling intervals when the tissue near the pacing electrode is relatively refractory. Therefore, this paper analyzes bipolar stimulation of cardiac tissue. The strength-interval relationship for bipolar stimulation is calculated using the bidomain model and a recently developed parsimonious ionic current model. The strength-interval curves obtained using different electrode separations and arrangements (electrodes placed parallel to the fibers versus perpendicular to the fibers) indicate that bipolar stimulation results in more complex activation patterns compared to unipolar stimulation. An unusually low threshold stimulus current is observed when the electrodes are close to each other (a separation of 1 mm) because of break excitation. Unlike for unipolar stimulation, anode make excitation is not present during bipolar stimulation, and an abrupt switch from anode break to cathode make excitation can cause dramatic changes in threshold with very small changes in the interval. These results could impact the design of implantable pacemakers and defibrillators.

}, author = {Galappaththige, Suran K and Gray, Richard A and Roth, Bradley J} } @conference {, title = {Quantitative Regular Expressions for Arrhythmia Detection Algorithms}, booktitle = {International Conference on Computational Methods in Systems Biology}, year = {2017}, month = {09/2017}, publisher = {Springer, Cham}, organization = {Springer, Cham}, address = {Darmstadt, Germany }, abstract = {

Motivated by the problem of verifying the correctness of arrhythmia-detection algorithms, we present a formalization of these algorithms in the language of Quantitative Regular Expressions. QREs are a flexible formal language for specifying complex numerical queries over data streams, with provable runtime and memory consumption guarantees. The medical-device algorithms of interest include peak detection (where a peak in a cardiac signal indicates a heartbeat) and various discriminators, each of which uses a feature of the cardiac signal to distinguish fatal from non-fatal arrhythmias. Expressing these algorithms{\textquoteright} desired output in current temporal logics, and implementing them via monitor synthesis, is cumbersome, error-prone, computationally expensive, and sometimes infeasible.

In contrast, we show that a range of peak detectors (in both the time and wavelet domains) and various discriminators at the heart of today{\textquoteright}s arrhythmia-detection devices are easily expressible in QREs. The fact that one formalism (QREs) is used to describe the desired end-to-end operation of an arrhythmia detector opens the way to formal analysis and rigorous testing of these detectors{\textquoteright} correctness and performance. Such analysis could alleviate the regulatory burden on device developers when modifying their algorithms. The performance of the peak-detection QREs is demonstrated by running them on real patient data, on which they yield results on par with those provided by a cardiologist.

}, isbn = {978-3-319-67471-1}, doi = {https://doi.org/10.1007/978-3-319-67471-1_2}, author = {Houssam Abbas and Alena Rodionova and Ezio Bartocci and Scott A. Smolka and Radu Grosu} } @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} } @article {, title = {Computing Compositional Proofs of Input-to-Output Stability Using SOS Optimization and δ-Decidability}, journal = {Nonlinear Analysis: Hybrid Systems}, year = {2016}, month = {05/2016}, author = {A. Murthy and Md. A. Islam, and S. A. Smolka and R. Grosu} } @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} } @article {, title = {Estimability Analysis and Optimal Design in Dynamic Multi-scale Models of Cardiac Electrophysiology}, journal = {Journal of Agricultural, Biological, and Environmental Statistics}, year = {2016}, pages = {1{\textendash}16}, author = {Shotwell, Matthew S and Gray, Richard A} } @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 = {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 = {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} } @conference {21, title = {SpaTeL: A Novel Spatial-temporal Logic and Its Applications to Networked Systems}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, year = {2015}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, keywords = {networked dynamical systems, parameter synthesis, spatial temporal logic, statistical model checking}, isbn = {978-1-4503-3433-4}, doi = {10.1145/2728606.2728633}, url = {http://doi.acm.org/10.1145/2728606.2728633}, author = {Haghighi, Iman and Jones, Austin and Kong, Zhaodan and Bartocci, Ezio and Grosu, Radu and Belta, Calin} }