@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 = {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 = {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 = {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 = {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} } @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 = {A tableau construction for finite linear-time temporal logic}, journal = {arXiv preprint arXiv:1910.09339}, year = {2019}, author = {Huang, Samuel and Cleaveland, Rance} } @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 = {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 = {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 = {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} } @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} } @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 = {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 {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} }