Quantitative regular expressions for arrhythmia detection algorithms

DOI10.1007/978-3-319-67471-1_2zbMATH Open1416.92097arXiv1612.07770OpenAlexW2751570560MaRDI QIDQ5227312FDOQ5227312

Authors: Houssam Abbas, Alena Rodionova, Ezio Bartocci, Scott A. Smolka, Radu Grosu 

Publication date: 25 July 2019

Published in: Computational Methods in Systems Biology (Search for Journal in Brave)

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' 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'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' 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.

Full work available at URL: https://arxiv.org/abs/1612.07770

Recommendations

• Derivatives of quantitative regular expressions
• On the quantitative semantics of regular expressions over real-valued signals
• Regular Programming for Quantitative Properties of Data Streams
• A method for the classification of QRS-complexes
• Real-time cardiac arrhythmia detection using WOLA filterbank analysis of EGM signals

zbMATH Keywords

peak detectionelectrocardiogramsquantitative regular expressionsarrythmia discriminationICDs

Mathematics Subject Classification ID

Pattern recognition, speech recognition (68T10) Biomedical imaging and signal processing (92C55)

Cited In (3)

• Algebraic quantitative semantics for efficient online temporal monitoring
• Semantic Foundations for Deterministic Dataflow and Stream Processing
• From LTL to rLTL monitoring: improved monitorability through robust semantics

This page was built for publication: Quantitative regular expressions for arrhythmia detection algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5227312)