@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} } @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 = {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 = {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 = {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 = {Automated Closed-Loop Model Checking of Implantable Pacemakers using Abstraction Trees}, booktitle = {Medical Cyber Physical Systems Workshop 2016}, year = {2016}, abstract = {

Autonomous medical devices such as implantable cardiac pacemakers are capable of diagnosing the patient condition and delivering therapy without human intervention. Their ability to autonomously affect the physiological state of the patient makes them safety-critical. Sufficient evidence for the safety and efficacy of the device software, which makes these autonomous decisions, should be provided before these devices can be released on the market. Formal methods like model checking can provide safety evidence that the devices can safely operate under a large variety of physiological conditions. The challenge is to develop physiological models that are general enough to cover the large variability of human physiology, and also expressive enough to provide physiological contexts to counter-examples returned by the model checker. In this paper, the authors develop a set of physiological abstraction rules that introduce physiological constraints to heart models. By applying these abstraction rules to a initial set of heart models, an abstraction tree is created. The root model covers all possible inputs to a pacemaker and derived models cover inputs from different heart conditions. If a counter-example is returned by the model checker, the abstraction tree is traversed so that the most concrete counter-example(s) with physiological contexts can be returned to the domain experts for validity check. The abstraction tree framework replaces the manual abstraction and refinement framework, which reduced the amount of domain knowledge required to perform closed-loop model checking. It encourages the use of model checking during the development of autonomous medical devices, and identifies safety risks earlier in the design process.

}, author = {Zhihao Jiang and Houssam Abbas and Pieter J Mosterman and Rahul Mangharam} } @article {, title = {The Challenges of High-Confidence Medical Device Software}, journal = {IEEE Computer January Outlook}, year = {2016}, author = {Z. Jiang and H. Abbas and K. Jang and R. Mangharam} } @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 = {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} } @conference {, title = {Towards Model Checking of Implantable Cardioverter Defibrillators}, booktitle = {Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control}, year = {2016}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, abstract = {

Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It usually ends in death within a minute. A common way to treat the symptoms of fibrillation is to implant a medical device, known as an Implantable Cardioverter Defibrillator (ICD), in the patient{\textquoteright}s body. Model-based verification can supply rigorous proofs of safety and efficacy. In this paper, we build a hybrid system model of the human heart+ICD closed loop, and show it to be a STORMED system, a class of o-minimal hybrid systems that admit finite bisimulations. In general, it may not be possible to compute the bisimulation. We show that approximate reachability can yield a finite simulation for STORMED systems, and that certain compositions respect the STORMED property. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.

}, keywords = {heart modeling, icds, life-critical cps, medical devices, stormed systems}, isbn = {978-1-4503-3955-1}, doi = {10.1145/2883817.2883841}, url = {http://doi.acm.org/10.1145/2883817.2883841}, author = {Abbas, Houssam and Jiang, Kuk Jin and Jiang, Zhihao and Mangharam, Rahul} }