Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Safety Verification of Deep Neural Networks Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Logical Clustering and Learning for Time-Series Data

verfasst von : Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

In order to effectively analyze and build cyberphysical systems (CPS), designers today have to combat the data deluge problem, i.e., the burden of processing intractably large amounts of data produced by complex models and experiments. In this work, we utilize monotonic parametric signal temporal logic (PSTL) to design features for unsupervised classification of time series data. This enables using off-the-shelf machine learning tools to automatically cluster similar traces with respect to a given PSTL formula. We demonstrate how this technique produces interpretable formulas that are amenable to analysis and understanding using a few representative examples. We illustrate this with case studies related to automotive engine testing, highway traffic analysis, and auto-grading massively open online courses.

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 Data-Driven Synthesis of Full Probabilistic Programs
Nächstes Kapitel Montre: A Tool for Monitoring Timed Regular Expressions
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
If \(X\) is obvious from context (or does not matter), we write \(\mathcal {V} (\varphi (\mathbf {p}), X)\) as \(\mathcal {V} (\varphi )\).
 
2
For canonicity, \(\pi \) need not be a function from timed traces to \({\mathcal {D}_\mathcal {P}}\). For example, it may be expedient to project a trace to a subset of \({\mathcal {D}_\mathcal {P}}\). For simplicity, we defer more involved projections to future exposition.
 
3
For simplicity, we have omitted a number of optimizations in Algorithm 1. For example, one can replace the iterative loop through parameters with a binary search over parameters.
 
4
A GMM assumes that the given parameter space can be modeled as a random variable distributed according to a set of Gaussian distributions with different mean and variance values. A given parameter valuation is labeled l if the probability of the valuation belonging to the \(l^{th}\) Gaussian distribution exceeds the probability of the valuation belonging to other distributions. Another way to visualize clusters in the parameter space is by level-sets of the probability density functions associated with the clusters. For example, for the \(l^{th}\) cluster, we can represent it using the smallest level-set that includes all given points labeled l.
 
5
As the discrete-time derivative can introduce considerable noise, we remark that the discrete-time derivative can often be approximated by a noise-robust operation (such as the difference from a rolling mean/median.).
 
Literatur
1.
2.
3.
Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356–374. Springer, Cham (2015). doi:10.​1007/​978-3-319-21668-3_​21 CrossRef
4.
5.
Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 147–160. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-29860-8_​12 CrossRef
6.
Bartocci, E., Bortolussi, L., Sanguinetti, G.: Learning temporal logical properties discriminating ECG models of cardiac arrhytmias. arXiv preprint arXiv:​1312.​7523 (2013)
7.
Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Proceedings of HSCC, pp. 1–10 (2016)
8.
Colyar, J., Halkias, J.: US highway 101 dataset. Federal Highway Administration (FHWA), Technical report FHWA-HRT-07-030 (2007)
9.
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​17 CrossRef
10.
Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 92–106. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33386-6_​9 CrossRef
11.
Pedregosa, F., et al.: Scikit-learn: machine learning in python. J. Mach. Learn. Res. 12, 2825–2830 (2011)MathSciNetMATH
12.
Hoxha, B., Dokhanchi, A., Fainekos, G.: Mining parametric temporal logic properties in model-based design for cyber-physical systems. Int. J. Softw. Tools Technol. Transf. 1–15 (2017)
13.
Kapinski, J., et al.: ST-lib: a library for specifying and classifying model behaviors. In: SAE Technical Paper. SAE (2016)
14.
Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. IEEE TCAD ICS 34(11), 1704–1717 (2015)MATH
15.
Jones, A., Kong, Z., Belta, C.: Anomaly detection in cyber-physical systems: a formal methods approach. In: Proceedings of CDC, pp. 848–853 (2014)
16.
Juniwal, G., Donzé, A., Jensen, J.C., Seshia, S.A.: CPSGrader: synthesizing temporal logic testers for auto-grading an embedded systems laboratory. In: Proceedings of EMSOFT, p. 24 (2014)
17.
Keogh, E.J., Pazzani, M.J.: Scaling up dynamic time warping for data mining applications. In: Proceedings of KDD, pp. 285–289 (2000)
18.
Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of HSCC, pp. 273–282 (2014)
19.
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRef
20.
Legriel, J., Guernic, C., Cotton, S., Maler, O.: Approximating the pareto front of multi-criteria optimization problems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 69–83. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-12002-2_​6 CrossRef
21.
Li, W., Forin, A., Seshia, S.A.: Scalable specification mining for verification and diagnosis. In: Proceedings of the Design Automation Conference (DAC), pp. 755–760, June 2010
22.
Lin, J., Keogh, E., Truppel, W.: Clustering of streaming time series is meaningless. In: Proceedings of the 8th ACM SIGMOD Workshop on Research Issues in Data Mining and Knowledge Discovery, pp. 56–65. ACM (2003)
23.
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
24.
Metadaten
Titel
Logical Clustering and Learning for Time-Series Data
verfasst von
Marcell Vazquez-Chanlatte
Jyotirmoy V. Deshmukh
Xiaoqing Jin
Sanjit A. Seshia
Copyright-Jahr
2017
Buch
Computer Aided Verification

Print ISBN: 978-3-319-63386-2

Electronic ISBN: 978-3-319-63387-9

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63387-9_15

Premium Partner

    Bildnachweise