Monotonluk özelliklerı kullanılarak geçmiş zamanlı sinyal zamansal mantık formülleri sentezlenmesi

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.