Signal Temporal Logic (STL) [1] is a formalism used in robotics to specify complex tasks and to characterize (desired) behaviours of systems in a machine-interpretable way. However, designing a temporal logic formula is usually a tedious task, often requiring manual tuning. To automate the inference of temporal logic formulae, recent approaches learn specifications from datasets which include positive (i.e. complying with the specification) and negative signals (i.e. violating the specification) of the target specification [2-6]. To obtain accurate and tight results, this process usually requires that the signals only belong to a single target specification. Nevertheless, in reality, signals are recorded from multiple specifications during the operation of a system. For instance, an autonomous vehicle performs different manoeuvres during its operation, depending on the current traffic situation. Each of these manoeuvres usually adheres to a different target specification. If the provided dataset contains signals of multiple target specifications, inference algorithms may not be able to determine a tight specification or even no specification at all. Another example spans different driving styles one can encounter while driving: from careful driving styles to more aggressive ones.
Your task will be to develop a hierarchical clustering approach that allows one to separate the recorded signals into distinct subsets. Each of these subsets should belong to a different target specification. Therefore, you need to determine suitable metrics [7] and identify clustering approaches to separate the signals, e.g., using their frequency spectrum. Subsequently, an inference algorithm should learn the target specification of each of the distinct subsets. These subsets can be updated in case this update results in tighter target specifications. Moreover, subsets can be further split, and the relation of each of the subsets can be modelled in a tree structure.
References
[1] O. Maler and D. Nickovic, “Monitoring temporal properties of continuous signals,” in Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 2004, pp. 152–166.
[2] E. Asarin, A. Donze, O. Maler, and D. Nickovic, “Parametric identification of temporal properties,” in Proc. of the Int. Conf. on Runtime Verification. Springer, 2011, pp. 147–160.
[3] A. Bakhirkin, T. Ferrere, and O. Maler, “Efficient parametric identification for STL,” in Proc. of the 21st Int. Conf. on Hybrid Systems: Computation and Control. ACM, 2018, pp. 177–186.
[4] G. Bombara, C.-I. Vasile, F. Penedo, H. Yasuoka, and C. Belta, “A decision tree approach to data classification using signal temporal logic,” in Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. ACM, 2016, pp. 1–10.
[5] A. Jones, Z. Kong, and C. Belta, “Anomaly detection in cyber-physical systems: A formal methods approach,” in Proc. of the IEEE Int. Conf. on Decision and Control (CDC). 2014, pp. 848–853.
[6] G. Bombara and C. Belta, “Online learning of temporal logic formulae for signal classification,” in European Control Conference (ECC). IEEE, 2018, pp. 2057–2062.
[7] C. Madsen, P. Vaidyanathan, S. Sadraddini, C.-I. Vasile, N. A. De-Lateur, R. Weiss, D. Densmore, and C. Belta, “Metrics for signal temporal logic formulae,” in Proc. of the IEEE Int. Conf. on Decision and Control (CDC). 2018, pp. 1542–1547.