@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 = {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 = {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} }