Abstract
In this work, we introduce a supervised learning framework for inferring temporal logic specifications from labelled patterns in signals, so that the formulae can then be used to correctly detect the same patterns in unlabelled samples. The input patterns that are fed to the training process are labelled by a Boolean signal that captures their occurrences. To express the patterns with quantitative features, we use parametric specifications that are increasing, which we call Increasing Parametric Pattern Predictor (IPPP). This means that augmenting the value of the parameters makes the predicted pattern true on a larger set. A particular class of parametric specification formalisms that we use is Parametric Signal Temporal Logic (PSTL). One of the main contributions of this paper is the definition of a new measure, called \(\epsilon \)-count, to assess the quality of the learned formula. This measure enables us to compare two Boolean signals and, hence, quantifies how much the labelling signal induced by the formula differs from the true labelling signal (e.g. given by an expert). Therefore, the \(\epsilon \)-count can measure the number of mismatches (either false positives or false negatives) up to some error tolerance \(\epsilon \). Our supervised learning framework can be expressed by a multicriteria optimization problem with two objective functions: the minimization of false positives and false negatives given by the parametric formula on a signal. We provide an algorithm to solve this multi-criteria optimization problem. Our approach is demonstrated on two case studies involving characterization and classification of labeled ECG (electrocardiogram) data.
This work has been partially supported by the ANR Project ANR-15-IDEX-02.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A subset of \(\mathbb {R}\) is compact if and only if it is closed and bounded.
- 2.
Here and in the rest of the paper we slightly simplified the syntax of [8] by replacing \((\mathop {\mathrm {On}_{[a,b]}} \mathop {\mathrm {Max}}s)\) by \((\mathop {\mathrm {Max_{[a,b]}}} s)\) whose value in t is \(\max _{t'\in [t+a,t+b]} s(t')\).
- 3.
where \((\mathop {\mathrm {F}_{[-\sigma ,\sigma ]}}\lambda _s)(t)=1\) iff \(\exists t'\in [t-\delta ,t+\delta ], s(t')=1\).
- 4.
\(\bigtriangleup \) is the symmetric difference of two sets.
References
ECGFiveDays data set. http://www.timeseriesclassification.com/description.php?Dataset=ECGFiveDays
Implementation of Pareto front intersection algorithm. https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/tempo/multidimensional_search/-/tree/intersectionAkshay
Implementation of the StlEval \(\epsilon \)-count operator. https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/tempo/StlEval/-/tree/akshayTest
Learning specifications for labelled patterns (technical report). http://www-verimag.imag.fr/TR/TR-2020-1.pdf
Abbas, H., Rodionova, A., Mamouras, K., Bartocci, E., Smolka, S.A., Grosu, R.: Quantitative regular expressions for arrhythmia detection. IEEE/ACM Trans. Comput. Biol. Bioinform. 16(5), 1586–1597 (2019)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
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). https://doi.org/10.1007/978-3-642-29860-8_12
Bakhirkin, A., Basset, N.: Specification and efficient monitoring beyond STL. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 79–97. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_5
Bakhirkin, A., Basset, N., Maler, O., Requeno, J.I.: Learning pareto front from membership queries. Working paper or preprint (2019). https://hal.archives-ouvertes.fr/hal-02125140
Bakhirkin, A., Basset, N., Maler, O., Jarabo, J.-I.R.: ParetoLib: a python library for parameter synthesis. In: André, É., Stoelinga, M. (eds.) FORMATS 2019. LNCS, vol. 11750, pp. 114–120. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29662-9_7
Bakhirkin, A., Ferrére, T., Maler, O.: Efficient parametric identification for STL. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018, pp. 177–186. ACM, New York (2018)
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, pages 1–10. ACM, New York (2016)
Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: A Simulink hybrid heart model for quantitative verification of cardiac pacemakers. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 131–136. ACM, New York (2013)
Cutulenco, G., Joshi, Y., Narayan, A., Fischmeister, S.: Mining timed regular expressions from system traces. In: Proceedings of the 5th International Workshop on Software Mining, Software Mining 2016, pp. 3–10. ACM, New York (2016)
Dau, H.A.: et al.: The UCR time series classification archive, October 2018. https://www.cs.ucr.edu/~eamonn/time_series_data_2018/
Goldberger, A.L., et al.: PhysioBank, physiotoolkit, and physionet: components of a new research resource for complex physiologic signals. Circulation 101(23), e215–e220 (2000)
Jha, S., Tiwari, A., Seshia, S.A., Sahai, T., Shankar, N.: TeLEx: learning signal temporal logic from positive examples using tightness metric. Formal Methods Syst. Des. 54(3), 364–387 (2019). https://doi.org/10.1007/s10703-019-00332-1
Kolmogorov, A.N., Tikhomirov, V.M.: \(\varepsilon \)-entropy and \(\varepsilon \)-capacity of sets in function spaces. Uspekhi Matematicheskikh Nauk, 14(2(86)), 386 (1959)
Kong, Z., Jones, A., Ayala, A.M., Gol, E.A., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2014, pp. 273–282. ACM, New York (2014)
Kong, Z., Jones, A., Belta, C.: Temporal logics for learning and detection of anomalous behavior. IEEE Trans. Automatic Control 62(3), 1210–1222 (2017)
Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining (T). In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, pp. 81–92. IEEE (2015)
Maler, O.: Learning monotone partitions of partially-ordered domains (work in progress). Working paper or preprint (2017) https://hal.archives-ouvertes.fr/hal-01556243
Mohammadinejad, S., Deshmukh, J.V., Puranic, A.G.: Mining environment assumptions for cyber-physical system models. In: Proceedings of the 11th ACM/IEEE International Conference on Cyber-Physical Systems (to appear), ICCPS 2020. IEEE (2020)
Mohammadinejad, S., Deshmukh, J.V., Puranic, A.G., Vazquez-Chanlatte, M., Donzé, A.: Interpretable classification of time-series data using efficient enumerative techniques. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (to appear), HSCC 2020. ACM, New York (2020)
Moody, G.B., Mark, R.G.: The impact of the MIT-BIH arrhythmia database. IEEE Eng. Med. Biol. Mag. 20(3), 45–50 (2001)
Neider, D., Gavran, I.: Learning linear temporal properties. In: Proceedings of the 18th International Conference on Formal Methods in Computer Aided Design, FMCAD 2011, pp. 1–10. ACM, Austin (2018)
Ničković, D., Qin, X., Ferrère, T., Mateis, C., Deshmukh, J.: Shape expressions for specifying and extracting signal features. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 292–309. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_17
Vazquez-Chanlatte, M., Deshmukh, J.V., Jin, X., Seshia, S.A.: Logical clustering and learning for time-series data. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 305–325. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_15
Vazquez-Chanlatte, M., Ghosh, S., Deshmukh, J.V., Sangiovanni-Vincentelli, A., Seshia, S.A.: Time-series learning using monotonic logical properties. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 389–405. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_22
von Birgelen, A., Niggemann, O.: Using self-organizing maps to learn hybrid timed automata in absence of discrete events. In: Proceedings of the 22nd IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2017, pp. 1–8. IEEE (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Basset, N., Dang, T., Mambakam, A., Jarabo, J.I.R. (2020). Learning Specifications for Labelled Patterns. In: Bertrand, N., Jansen, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2020. Lecture Notes in Computer Science(), vol 12288. Springer, Cham. https://doi.org/10.1007/978-3-030-57628-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-57628-8_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-57627-1
Online ISBN: 978-3-030-57628-8
eBook Packages: Computer ScienceComputer Science (R0)