@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} } @article {, title = {Controllability of voltage- and calcium-driven cardiac alternans in a map model}, journal = {Chaos}, year = {2021}, author = {Munoz LM and Ampofo MO and Cherry EM} } @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} } @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 = {A Network-based Cardiac Electrophysiology Simulator with Realistic Signal Generation and Response to Pacing Maneuvers}, journal = {Computing in Cardiology}, year = {2021}, url = {https://www.cinc.org/2021/Program/accepted/294_Preprint.pdf}, author = {Shahriar Iravanian and Ilija Uzelac and Abouzar Kaboudian and Jonathan Langberg and Flavio 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 = {Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems}, journal = {IEEE Access}, year = {2020}, author = {F. Shmarov and S. Soudjani and N. Paoletti and E. Bartocci and S. Lin and S. A. Smolka and P. Zuliani} } @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 = {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} } @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 = {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} } @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} } @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} } @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} } @article {, title = {Simulating waves, chaos and synchronization with a microcontroller}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {29}, year = {2019}, month = {12/2019}, 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:BUYA1_V_uYcC}, author = {Andrea J Welsh and Cristian Delgado and Casey Lee-Trimble and Abouzar Kaboudian and Flavio H Fenton} } @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} } @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 = {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 = {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 = {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 = {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 = {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.} } @conference {, title = {{Data-Driven Robust Control for Type 1 Diabetes Under Meal and Exercise Uncertainties}}, booktitle = {Computational Methods in Systems Biology}, year = {2017}, publisher = {Springer}, organization = {Springer}, abstract = {

We present a fully closed-loop design for an artificial pancreas (AP) which regulates the delivery of insulin for the control of Type I diabetes. Our AP controller operates in a fully automated fashion, without requiring any manual interaction (e.g. in the form of meal announcements) with the patient. A major obstacle to achieving closed-loop insulin control is the uncertainty in those aspects of a patient{\textquoteright}s daily behavior that significantly affect blood glucose, especially in relation to meals and physical activity. To handle such uncertainties, we develop a data-driven robust model-predictive control framework, where we capture a wide range of individual meal and exercise patterns using uncertainty sets learned from historical data. These sets are then used in the controller and state estimator to achieve automated, precise, and personalized insulin therapy. We provide an extensive in silico evaluation of our robust AP design, demonstrating the potential of this approach, without explicit meal announcements, to support high carbohydrate disturbances and to regulate glucose levels in large clusters of virtual patients learned from population-wide survey data.

}, doi = {10.1007/978-3-319-67471-1_13}, author = {Nicola Paoletti and Kin Sum Liu and Scott A. Smolka and Shan Lin} } @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.} } @conference {, title = {A novel ICD morphology discriminator to improve discrimination between Ventricular and Supraventricular tachycardias}, booktitle = {In Heart Rhythm Scientific Sessions, Chicago}, year = {2017}, month = {05/2017}, abstract = {

Implantable\ \  \ Cardioverter\ \  \ Defibrillator\ \  \ (ICD)\ \  \ morphology\ \  \ discriminators\ \  \ (MDs)\ \  \ discriminate\ \  \ ventricular\ \  \ (VT)\ \  \ from\ \  \ supraventricular\ \  \ tachycardias\ \  \ (SVT)\ \  \ by\ \  \ comparing\ \  \ single-beat\ \  \ electrogram\ \  \ (EGM)\ \  \ shape\ \  \ during\ \  \ tachycardia\ \  \ versus\ \  \ sinus\ \  \ rhythm\ \  \ (Fig.\ \  \ A)\ \  \ and\ \  \ counting\ \  \ the\ \  \ matches.\ \  \ \ \  \ 
Objective

}, author = {H. Abbas and K.J. Jang and J. Liang and S. Dixit and R. Mangharam} } @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 = {{SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems}}, booktitle = {Haifa Verification Conference, to appear}, year = {2017}, abstract = {

Abstract. We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitzcontinuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.

}, author = {Fedor Shmarov and Nicola Paoletti and Ezio Bartocci and Shan Lin and Scott Smolka and Paolo Zuliani} } @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} } @conference {, title = {High-level modeling for computer-aided clinical trials of medical devices}, booktitle = {High Level Design Validation and Test Workshop (HLDVT), 2016 IEEE International}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, abstract = {

Medical devices like the Implantable Cardioverter Defibrillator (ICD) are life-critical systems. Malfunctions of the device can cause serious injury or death of the patient. In addition to rigorous testing and verification during the development process, new medical devices often go through clinical trials to evaluate their safety and performance on sample populations. Clinical trials are costly and prone to failure if not planned and executed properly. Evaluating devices on computer models of the relevant physiological systems can provide helpful insights into the safety and efficacy of the device, thus helping to plan and execute a clinical trial. In this paper, we demonstrate how to develop high-level physiological models of cardiac electrophysiology and how to apply them to the Rhythm ID Head to Head Trial (RIGHT), a 5-year long clinical trial for comparing two ICDs. We refer to this as a Computer-Aided Clinical Trial (CACT). We explored two modeling options, a white-box model capturing the mechanisms of the physiological behaviors, and a blackbox model which uses machine learning methods to synthesize physiological input signals. Both models were able to generate physiological inputs to the ICDs and we discuss the challenges and appropriateness of the two modeling options.

}, author = {Abbas, Houssam and Jiang, Zhihao and Jang, Kuk Jin and Beccani, Marco and Liangy, Jackson and Mangharam, Rahul} } @conference {, title = {In-silico pre-clinical trials for implantable cardioverter defibrillators}, booktitle = {Engineering in Medicine and Biology Society (EMBC), 2016 IEEE 38th Annual International Conference of the}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, abstract = {

Regulatory authorities require that the safety and efficacy of a new high-risk medical device be proven in a Clinical Trial (CT), in which the effects of the device on a group of patients are compared to the effects of the current standard of care. Phase III trials can run for several years, cost millions of dollars, and expose patients to an unproven device. In this paper, we demonstrate how to use a large group of synthetic patients based on computer modeling to improve the planning of a CT so as to increase the chances of a successful trial for implantable cardioverter defibrillators (ICDs). We developed a computer model of the electrical generation and propagation in the heart. This model was used to generate a large group of heart instances capable of producing episodes of 19 different arrhythmias. We also implemented two arrhythmia detection algorithms from the literature: Rhythm ID from Boston Scientific and PR Logic + Wavelet from Medtronic. Using this setup, we conducted multiple in-silico trials to compare the ability of the two algorithms to appropriately discriminate between potentially fatal Ventricular Tachy-arrhythmias (VT) and nonfatal Supra-Ventricular Tachy-arrhythmias (SVTs). The results of our in-silico trial indicate that Rhythm ID was less able to discriminate between SVT and VT and so may lead to more cases of inappropriate therapy. This corroborates the findings of the Rhythm ID Going Head to Head Trial (RIGHT), a clinical trial that compared the two algorithms in patients. We further demonstrated that the result continues to hold if we vary the distribution of arrhythmias in the synthetic population. We also used the same in-silico cohort to explore the sensitivity of the outcome to different parameter settings of the device algorithms, which is not feasible in a real clinical trial. In-silico trials can provide early insight into the factors which affect the outcome of a CT at a fraction of the cost and duration and without the ethical issues.

}, author = {Jiang, Zhihao and Abbas, Houssam and Jang, Kuk Jin and Beccani, Marco and Liang, Jackson and Dixit, Sanjay and Mangharam, Rahul} } @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} }