Top

International Journal on Software Tools for Technology Transfer

Published in:

29-06-2021 | General

Specifying and detecting temporal patterns with shape expressions

Authors: Dejan Ničković, Xin Qin, Thomas Ferrère, Cristinel Mateis, Jyotirmoy Deshmukh

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2021

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Modern cyber-physical systems (CPS) and the Internet of things (IoT) are data factories generating, measuring and recording huge amounts of time series. The useful information in time series is usually present in the form of sequential patterns. We propose shape expressions as a declarative language for specification and extraction of rich temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We associate with shape expressions novel noisy semantics that combines regular expression matching semantics with statistical regression. We study essential properties of the language and propose an efficient heuristic for approximate matching of shape expressions. We demonstrate the applicability of this technique on two case studies from the health and the avionics domains.

previous article An extension of first-order LTL with rules with application to runtime verification

next article What can we monitor over unreliable channels?

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

The signal with the empty time domain is equivalent to the empty word in the classical language theory

We use \(\underline{l}\) instead of \(\underline{l}_{\sigma ,x}\) whenever its association to \(\sigma _{x}\) is clear from the context and omit \(\underline{l}_{\sigma ,x}\) altogether when not interested in the duration of the shape.

We omit the duration variable \(\underline{l}\) whenever we are not interested in the duration of a shape—for instance, we then use the notation \(\textsf {sin}(a,b,c,d)\).

We abuse the notation and replace a parameter variable by a constant, for instance, \(\textsf {lin}_x(0,b)\), as a shortcut for \(\textsf {lin}_x(a_1,b)~:~a_1 = 0\).

We also assume that the SMA \(\hat{\mathcal {A}}\), the signal w, the noise tolerance threshold \(\nu \) and the minimum match length \(\uplambda \) are given as global parameters to the main procedure \(\textsf {policy\_scheduler}\) and are implicitly propagated to all the other methods

Recall that we require atomic matches of minimum length \(\uplambda \).

The figure is under copyright by A. Rad.

We recall that \(\nu = 0\) denotes zero noise tolerance and \(\nu = 1\) allows arbitrary level of noise.

IEEE standard on pulse measurement and analysis by objective techniques. In: ANSI/IEEE Std 181–1977 (1977). https://doi.org/10.1109/IEEESTD.1977.81097

Abbas H., Rodionova A., Bartocci E., Smolka S. A., Grosu R. Quantitative regular expressions for arrhythmia detection algorithms. In International Conference on Computational Methods in Systems Biology, pages 23–39. Springer, 2017

Alur R., Fisman D., Raghothaman M. Regular programming for quantitative properties of data streams. In European Symposium on Programming, pages 15–40. Springer, 2016

Alur, R., Mamouras, K., Stanford, C.: Modular quantitative monitoring. Proceedings of the ACM on Programming Languages 3(POPL), 50 (2019)CrossRef

Étienne André, Hasuo I., Waga M. Offline timed pattern matching under uncertainty. In 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018, pages 10–20, 2018

Asarin E., Caspi P., Maler O. A Kleene theorem for timed automata. In Logic in Computer Science (LICS), pages 160–171, 1997

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

Bakhirkin A., Ferrère T., Maler O., Ulus D. On the quantitative semantics of regular expressions over real-valued signals. In Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings, pages 189–206, 2017

Bakhirkin A., Ferrère T., Nickovic D., Maler O., Asarin E. Online timed pattern matching using automata. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 215–232. Springer, 2018

10.

D’Angelo B., Sankaranarayanan S., César Sánchez, Robinson W., Finkbeiner B., Sipma H. B., Mehrotra S., Manna Z. LOLA: runtime monitoring of synchronous systems. In 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pages 166–174, 2005

11.

Faymonville P., Finkbeiner B., Schirmer S., Torfah H. A stream-based specification language for network monitoring. In Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, pages 152–168, 2016

12.

Geurts P. Pattern extraction for time series classification. In European Conference on Principles of Data Mining and Knowledge Discovery, pages 115–127. Springer, 2001

13.

Ghidella J. , Mosterman P. Requirements-based testing in aircraft control design. In AIAA Modeling and Simulation Technologies Conference and Exhibit, page 5886, 2005

14.

Goldberger, A.L., Amaral, L.A.N., Glass, L., Hausdorff, J.M., Ivanov, P.C., Mark, R.G., Mietus, J.E., Moody, G.B., Peng, C.-K., Stanley, H.E.: Physiobank, physiotoolkit, and physionet: components of a new research resource for complex physiologic signals. Circulation 101(23), e215–e220 (2000)CrossRef

15.

Gorostiaga F. and César Sánchez. Striver: Stream runtime verification for real-time event-streams. In Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings, pages 282–298, 2018

16.

Hallé S. , Khoury R. Event stream processing with beepbeep 3. In RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, September 15, 2017, Seattle, WA, USA, pages 81–88, 2017

17.

Leucker M., César Sánchez, Scheffel T., Schmitz M., Schramm A. Tessla: runtime verification of non-synchronized real-time streams. In Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018, pages 1925–1933, 2018

18.

Maler O., Nickovic D. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, pages 152–166, 2004

19.

Mamouras, K., Raghothaman, M., Alur, R., Ives, Z.G., Khanna, S.: StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data. ACM SIGPLAN Notices 52, 693–708 (2017)CrossRef

20.

Nickovic D., Qin X., Ferrère T., Mateis C., Deshmukh J. V. Shape expressions for specifying and extracting signal features. In Runtime Verification - 19th International Conference, RV 2019, Porto, Portugal, October 8-11, 2019, Proceedings, pages 292–309, 2019

21.

Olszewski R. T. Generalized feature extraction for structural pattern recognition in time-series data. Technical report, Carnegie-Mellon Univ. School of Computer Science, 2001

22.

Rakthanmanon T., Campana B., Mueen A., Batista G., Westover B., Zhu Q., Zakaria J., Keogh E. Searching and mining trillions of time series subsequences under dynamic time warping. In Proceedings of the 18th ACM SIGKDD international conference on Knowledge discovery and data mining, pages 262–270. ACM, 2012

23.

Dogan Ulus. Montre: A tool for monitoring timed regular expressions. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, pages 329–335, 2017

24.

Ulus D., Ferrère T., Asarin E., Maler O. Timed pattern matching. In Formal Modeling and Analysis of Timed Systems (FORMATS), pages 222–236, 2014

25.

Ulus D., Ferrère T., Asarin E., Maler O. Online timed pattern matching using derivatives. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 736–751, 2016

26.

Waga, M., Hasuo, I.: Moore-machine filtering for timed and untimed pattern matching. IEEE Trans. on CAD of Integrat. Circuit. Syst. 37(11), 2649–2660 (2018)CrossRef

27.

Waga M., Hasuo I., Suenaga K. Efficient online timed pattern matching by automata-based skipping. In Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings, pages 224–243, 2017

28.

Waga M., Hasuo I., Suenaga K. MONAA: A tool for timed pattern matching with automata-based acceleration. In 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, pages 14–15, 2018

29.

Wenig F., Klanatsky P., Heschl C., Mateis C., Dejan N. Exponential pattern recognition for deriving air change rates from CO2 data. In 26th IEEE International Symposium on Industrial Electronics, ISIE 2017, Edinburgh, United Kingdom, June 19-21, 2017, pages 1507–1512, 2017

30.

Ye L., Keogh E. J. Time series shapelets: a new primitive for data mining. In Proceedings of the 15th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, Paris, France, June 28 - July 1, 2009, pages 947–956, 2009

Title: Specifying and detecting temporal patterns with shape expressions
Authors: Dejan Ničković
Xin Qin
Thomas Ferrère
Cristinel Mateis
Jyotirmoy Deshmukh
Publication date: 29-06-2021
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 4/2021
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-021-00627-x

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 4/2021

Compositional learning of mutually recursive procedural systems

What can we monitor over unreliable channels?

Quantitative estimation of side-channel leaks with neural networks

Neural predictive monitoring and a comparison of frequentist and Bayesian approaches

Introduction to the special issue of the 19th International Conference on Runtime Verification

An extension of first-order LTL with rules with application to runtime verification

Premium Partner