Learning temporal logic formulae from data
MetadataShow full item record
In recent years, there has been a great interest in applying machine learning-based techniques to the formal methods field. In this thesis, we focus on inferring high-level descriptions of a system from its execution traces. The system behaviors are formalized using an appropriate temporal logic language called Signal Temporal Logic (STL). We approach the two-class classification problem first. Given a finite set of pairs of system traces and labels, where each label indicates whether the respective trace exhibits a system property, we devised a decision-tree based framework that outputs an STL formula that can distinguish the traces. Afterward, we tackle the online learning scenario. In this setting, it is assumed that new signals may arrive over time, and the previously inferred formula should be updated to accommodate the new data. Later, we propose a hierarchical clustering algorithm for producing formulae even when the input labels are not available (unsupervised learning). Finally, we extend this work to the multi-class case and drastically improve the execution time by introducing smooth cost functions. The proposed framework, while retaining many qualities of traditional classifiers, presents some additional advantages. In particular, the produced formulae have a precise meaning that is interpretable by users. They can be used to acquire knowledge about the system under analysis. The formulae usage is not restricted to signal classification or knowledge acquisition but they can be used in other phases of the system's operation, such as monitoring and control. We present three case studies to illustrate the characteristics and effectiveness of the proposed algorithms: 1) a maritime surveillance problem; 2) an anomaly detection problem in an automotive powertrain subsystem; and 3) a fault classification problem in an automatic transmission.