Synthesis of past time signal temporal logic formulas using monotonicity properties

Download

index.pdf

Date

2020

Author

Ergürtuna, Mert.

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

345
views

118
downloads

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.

Subject Keywords

Signal Temporal Logic., Keywords: Signal Temporal Logic, Formal Methods, Formula Synthesis, Monotonicity, Classification.

URI

http://etd.lib.metu.edu.tr/upload/12625448/index.pdf
https://hdl.handle.net/11511/45668

Collections

Graduate School of Natural and Applied Sciences, Thesis

Suggestions

OpenMETU
Core

Synthesis of signal temporal logic formulas with genetic algorithms Aydın, Sertaç Kağan; Aydın Göl, Ebru; Department of Computer Engineering (2019) Signal Temporal Logic (STL) is used to reason about the behavior of continuous signals. Due to its expressivity and algorithms to generate signal monitors, it is used to define monitoring rules for hardware and software systems. However, it is a hard task to define an STL formula that describes the system behavior. An expert of the monitored system should write the formula and optimize its parameters to minimize the monitoring errors (false alarms and missed alarms). To simplify and disseminate the use of f...
Analysis of Face Recognition Algorithms for Online and Automatic Annotation of Personal Videos Yılmaztürk, Mehmet; Ulusoy Parnas, İlkay; Çiçekli, Fehime Nihan (Springer, Dordrecht; 2010-05-08) Different from previous automatic but offline annotation systems, this paper studies automatic and online face annotation for personal videos/episodes of TV series considering Nearest Neighbourhood, LDA and SVM classification with Local Binary Patterns, Discrete Cosine Transform and Histogram of Oriented Gradients feature extraction methods in terms of their recognition accuracies and execution times. The best performing feature extraction method and the classifier pair is found out to be SVM classification...
Optimizing Parameters of Signal Temporal Logic Formulas with Local Search Aydin, Sertac Kagan; Aydın Göl, Ebru (2019-08-22) Signal temporal logic (STL) is a formal language for expressing temporal and real-time properties of real valued signals. In this paper, we study the problem of generating an STL formula from a labeled dataset. We propose a local search algorithm to synthesize parameters of a template formula. Starting from a random initial point, the parameter space is explored in the directions improving the formula evaluation. In addition, the local search method is integrated to the genetic algorithms developed for form...
A Formal Methods Approach to Pattern Recognition and Synthesis in Reaction Diffusion Networks Bartocci, Ezio; Aydın Göl, Ebru; Haghighi, Iman; Belta, Calin (2018-03-01) We introduce a formal framework for specifying, detecting, and generating spatial patterns in reaction diffusion networks. Our approach is based on a novel spatial superposition logic, whose semantics is defined over the quad-tree representation of a partitioned image. We demonstrate how to use rule-based classifiers to efficiently learn spatial superposition logic formulas for several types of patterns from positive and negative examples. We implement pattern detection as a model-checking algorithm and we ...
MODELLING OF KERNEL MACHINES BY INFINITE AND SEMI-INFINITE PROGRAMMING Ozogur-Akyuz, S.; Weber, Gerhard Wilhelm (2009-06-03) In Machine Learning (ML) algorithms, one of the crucial issues is the representation of the data. As the data become heterogeneous and large-scale, single kernel methods become insufficient to classify nonlinear data. The finite combinations of kernels are limited up to a finite choice. In order to overcome this discrepancy, we propose a novel method of "infinite" kernel combinations for learning problems with the help of infinite and semi-infinite programming regarding all elements in kernel space. Looking...

Citation Formats

M. Ergürtuna, “Synthesis of past time signal temporal logic formulas using monotonicity properties,” Thesis (M.S.) -- Graduate School of Natural and Applied Sciences. Computer Engineering., Middle East Technical University, 2020.