nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Quantitative Regular Expressions for Arrhythmia Detection Algorithms

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

Erschienen in: Computational Methods in Systems Biology

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Bio-Curation for Cellular Signalling: The KAMI Project

Nächstes Kapitel Detecting Attractors in Biological Models with Uncertain Parameters

\(p_\sigma = \bar{p}\), \(p_{i<\sigma } = 0\), since we threshold only the spectrogram values at scale \(\bar{s}\). After this initial thresholding, tracing of maxima lines returns the peaks.

Operator \(conn_\delta \) can be defined recursively as follows: \(conn_\delta (X, Y)\,=\,\{y \in Y:\exists x\in X:\, |x-y|\le \delta \},\, conn_\delta (X_{k},..,X_1)\,=\,conn_\delta (conn_\delta (X_k,..,X_2),\, X_1)\).

Alur, R., Fisman, D., Raghothaman, M.: Regular programming for quantitative properties of data streams. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 15–40. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1_2 CrossRef

Alur, R., Freilich, A., Raghothaman, M.: Regular combinators for string transformations. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pp. 9:1–9:10. ACM, New York (2014)

Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)MathSciNetCrossRefMATH

Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23–37. Springer, Cham (2014). doi:10.1007/978-3-319-10512-3_3

Bozzelli, L., Sánchez, C.: Foundations of boolean stream runtime verification. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 64–79. Springer, Cham (2014). doi:10.1007/978-3-319-11164-3_6

Brim, L., Dluhos, P., Safránek, D., Vejpustek, T.: STL-*: extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52–67 (2014)MathSciNetCrossRefMATH

Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 391–403. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_30

Chakarov, A., Sankaranarayanan, S., Fainekos, G.: Combining time and frequency domain specifications for periodic signals. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 294–309. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_22 CrossRef

D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of the 12th International Symposium of Temporal Representation and Reasoning (TIME 2005), pp. 166–174. IEEE Computer Society Press (2005)

10.

Demri, S., Lazic, R., Nowak, D.: On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput. 205(1), 2–24 (2007)MathSciNetCrossRefMATH

11.

Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.A.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92–106. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33386-6_9 CrossRef

12.

Ferrère, T., Maler, O., Ničković, D., Ulus, D.: Measuring with timed patterns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 322–337. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_19 CrossRef

13.

Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of HSCC 2015: The 18th International Conference on Hybrid Systems: Computation and Control, pp. 189–198. ACM (2015)

14.

Harel, E., Lichtenstein, E., Pnueli, A.: Explicit clock temporal logic. IEEE (1990)

15.

Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRef

16.

Krishna, S.N., Madnani, K., Pandya, P.K.: Metric temporal logic with counting. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 335–352. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49630-5_20 CrossRef

17.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12 CrossRef

18.

Mallat, S., Hwang, W.L.: Singularity detection and processing with wavelets. IEEE Trans. Inf. Theor. 38(2), 617–643 (1992)MathSciNetCrossRefMATH

19.

Mallat, S.G.: A Wavelet Tour of Signal Processing, Third Edition: The Sparse Way. Academic Press, Amsterdam (2008)MATH

20.

Mamouras, K., Raghothaman, M., Alur, R., Ives, Z., Khanna, S.: StreamQRE: modular specification and efficient evaluation of quantitative queries over streaming data. In: Proceedings of 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 693–708 (2017)

21.

Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21–37. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_2 CrossRef

22.

Stroobandt, R.X., Barold, S.S., Sinnaeve, A.F.: Implantable Cardioverter - Defibrillators Step by Step. Wiley, Hoboken (2009)CrossRef

23.

Swerdlow, C.D., Asirvatham, S.J., Ellenbogen, K.A., Friedman, P.A.: Troubleshooting implanted cardioverter defibrillator sensing problems I. Circ. Arrhythm. Electrophysiol. 7(6), 1237–1261 (2014)CrossRef

24.

Ulus, D.: Montre: a tool for monitoring timed regular expressions. In: Majumdar, R., Kunĉak, V. (eds.) CAV 2017. LNCS, vol. 10426. Springer, Cham (2017). doi:10.1007/978-3-319-63387-9_16 CrossRef

25.

Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222–236. Springer, Cham (2014). doi:10.1007/978-3-319-10512-3_16

Titel: Quantitative Regular Expressions for Arrhythmia Detection Algorithms
verfasst von: Houssam Abbas
Alena Rodionova
Ezio Bartocci
Scott A. Smolka
Radu Grosu
Verlag: Springer International Publishing
Buch: Computational Methods in Systems Biology
Print ISBN: 978-3-319-67470-4

Electronic ISBN: 978-3-319-67471-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-67471-1_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner