Skip to main content
SpringerLink
Log in

Signal Clustering Using Temporal Logics

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10548))

Included in the following conference series:

Abstract

This paper introduces a new method for clustering signals using their temporal logic properties. Specifically, we propose a hierarchical clustering algorithm for efficiently processing a set of input signals. The input data is unlabeled, that is, no further information about properties of the signals are available to the learning algorithm other than the signals themselves. The algorithm produces a hierarchical structure where the internal nodes test some temporal properties of the data, and each terminal node contains a cluster (i.e., a group of similar signals). Each cluster can be mapped to a Signal Temporal Logic (STL) formula that describes its signals. The obtained formulae can be used directly for monitoring purposes but also, more generally, to acquire knowledge about the system under analysis. We present two case studies to illustrate the characteristics of our proposed algorithm. The first case study is related to a maritime surveillance problem, and the second is a fault classification problem in an automatic transmission system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    A more general definition of the set \(\mathcal {F}\) is used in [19].

  2. 2.

    If the original sampling times of \(s^1\) and \(s^2\) are not the same, the signals can be re-interpolated to obtain values for matching sampling times.

  3. 3.

    We ran our experiments on a Windows PC with an Intel 5920K CPU.

References

  1. Aggarwal, C.C., Reddy, C.K.: Data Clustering: Algorithms and Applications Chapman & Hall/CRC, 1st edn. CRC Press, Boca Raton (2013)

    Google Scholar 

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

    Chapter  Google Scholar 

  3. Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoret. Comput. Sci. 587, 3–25 (2015)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  5. Bishop, C.M.: Pattern Recognition and Machine Learning. Information Science and Statistics. Springer, New York (2006)

    MATH  Google Scholar 

  6. 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 the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 1–10. ACM, New York (2016)

    Google Scholar 

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

    Google Scholar 

  8. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  9. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15297-9_9

    Chapter  Google Scholar 

  10. Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: American Control Conference (ACC), vol. 2012, pp. 3567–3572, June 2012

    Google Scholar 

  11. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262–4291 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  12. Färber, I., Günnemann, S., Kriegel, H.P., Kröger, P., Müller, E., Schubert, E., Seidl, T., Zimek, A.: On using class-labels in evaluation of clusterings. In: MultiClust: 1st International Workshop on Discovering, Summarizing and Using Multiple Clusterings Held in Conjunction with KDD 2010 (2010)

    Google Scholar 

  13. Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009)

    Article  MATH  Google Scholar 

  14. Hoxha, B., Abbas, H., Fainekos, G.: Benchmarks for temporal logic requirements for automotive systems. In: Proceedings of Applied Verification for Continuous and Hybrid Systems (2014)

    Google Scholar 

  15. Hoxha, B., Dokhanchi, A., Fainekos, G.: Mining parametric temporal logic properties in model-based design for cyber-physical systems. Int. J. Softw. Tools Technol. Transfer, 1–15 (2017)

    Google Scholar 

  16. Jin, X., Donzé, A., Deshmukh, J., Seshia, S.A.: Mining requirements from closed-loop control models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. PP(99), 1 (2015)

    MATH  Google Scholar 

  17. Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, pp. 273–282. ACM, New York (2014)

    Google Scholar 

  18. Kowalska, K., Peel, L.: Maritime anomaly detection using Gaussian Process active learning. In: 2012 15th International Conference on Information Fusion (FUSION), pp. 1164–1171, July 2012

    Google Scholar 

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

    Chapter  Google Scholar 

  20. Ratanamahatana, C.A., Keogh, E.: Everything you know about dynamic time warping is wrong. In: Third Workshop on Mining Temporal and Sequential Data. Citeseer (2004)

    Google Scholar 

  21. Ripley, B.D.: Pattern Recognition and Neural Networks. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  22. Shokoohi-Yekta, M., Wang, J., Keogh, E.: On the non-trivial generalization of dynamic time warping to the multi-dimensional case. In: Proceedings of the 2015 SIAM International Conference on Data Mining, Proceedings, Society for Industrial and Applied Mathematics, pp. 289–297, June 2015

    Google Scholar 

  23. The MathWorks Inc: MATLAB and Simulink R2017a. Natick, Massachusetts (2017)

    Google Scholar 

  24. Zhao, Q., Krogh, B.H., Hubbard, P.: Generating test inputs for embedded control systems. IEEE Control Syst. 23(4), 49–57 (2003)

    Article  Google Scholar 

Download references

Acknowledgments

This work was partially supported by DENSO CORPORATION and by the Office of Naval Research under grant N00014-14-1-0554. The authors would like to acknowledge Hirotoshi Yasuoka (DENSO CORPORATION) and Rachael Ivison (Boston University) for providing valuable feedback during this research. We also thank the anonymous reviewers for their comments.

Author information

Authors and Affiliations

  1. Boston University, Boston, USA

    Giuseppe Bombara & Calin Belta

Authors
  1. Giuseppe Bombara
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Calin Belta
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giuseppe Bombara .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bombara, G., Belta, C. (2017). Signal Clustering Using Temporal Logics. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation