Synthesis of past time signal temporal logic formulas using monotonicity properties

---

Tezin Türü: Yüksek Lisans

Tezin Yürütüldüğü Kurum: Orta Doğu Teknik Üniversitesi, Fen Bilimleri Enstitüsü, Türkiye

Tezin Onay Tarihi: 2020

Tezin Dili: İngilizce

Öğrenci: MERT ERGÜRTUNA

Danışman: Ebru Aydın Göl

Özet:

Due to its expressivity and efficient algorithms, Signal Temporal Logic (STL) is widely used in runtime verification, formal control and analysis of time series data. While it is relatively easy to define an STL formula, simulate the system and mark the unexpected behaviors according to the formula as in the testing process, finding an STL formula that would detect the underlying cause of the errors is a complicated process. The main motivation of this thesis is to find a method that would explain the events that lead to the erroneous behavior in the system in an automated, efficient and human-readable way. Since the aim is to find the events the lead to the error in the system, past time signal temporal logic (ptSTL) which deals with the past events is used in the study. This thesis presents a novel method to find temporal properties that lead to unexpected behaviors from a dataset. The dataset consists of system traces that are labeled at each time point. First, monotonicity properties for ptSTL over the considered dataset is developed. Next using these monotonicity properties, an efficient parameter synthesis method for ptSTL is proposed. Finally, the parameter synthesis method is used in an iterative unguided formula synthesis framework that combines optimized formulas. In addition, the extension of the proposed approach to a dataset with a single label for each trace is developed. In this part, it is shown that the previously defined monotonicity properties hold and the framework is adapted.