Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
Synthesis of signal temporal logic formulas with genetic algorithms
Download
index.pdf
Date
2019
Author
Aydın, Sertaç Kağan
Metadata
Show full item record
This work is licensed under a
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License
.
Item Usage Stats
162
views
87
downloads
Cite This
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 formal monitors, its necessary to automate the formula writing process, which motivates this study. In this dissertation, we study the problem of synthesizing STL formulas from a labeled set of system traces. The datasets from different fields may vary in size and can be quite large. In order to handle such cases, we developed a parallel formula synthesis method based on genetic algorithms. The proposed method does not require any expertise guidance; it generates formula structure and optimizes the formula parameters simultaneously. In addition, in order to find the local optimum around an individual, we developed a randomized search over the parameter space, which is shown to speed up the convergence of the proposed method.
Subject Keywords
Signal Temporal Logic.
,
Keywords: Formal Methods
,
STL
,
Requirement Mining
,
Genetic Algorithms.
URI
http://etd.lib.metu.edu.tr/upload/12623224/index.pdf
https://hdl.handle.net/11511/43404
Collections
Graduate School of Natural and Applied Sciences, Thesis
Suggestions
OpenMETU
Core
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...
Synthesis of past time signal temporal logic formulas using monotonicity properties
Ergürtuna, Mert.; Aydın Göl, Ebru; Department of Computer Engineering (2020)
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 event...
Synthesis of Controllable ptSTL Formulas
Saglam, Irmak; Aydın Göl, Ebru (2020-01-01)
In this work, we develop an approach to anomaly detection and prevention problem using Signal Temporal Logic (STL). This approach consists of two steps: detection of the causes of the anomalities as STL formulas and prevention of the satisfaction of the formula via controller synthesis. This work focuses on the first step and proposes a formula template such that any controllable cause can be represented in this template. An efficient algorithm to synthesize formulas in this template is presented. Finally, ...
Properly Handling Complex Differentiation in Optimization and Approximation Problems
Candan, Çağatay (Institute of Electrical and Electronics Engineers (IEEE), 2019-03-01)
Functions of complex variables arise frequently in the formulation of signal processing problems. The basic calculus rules on differentiation and integration for functions of complex variables resemble, but are not identical to, the rules of their real variable counterparts. On the contrary, the standard calculus rules on differentiation, integration, series expansion, and so on are the special cases of the complex analysis with the restriction of the complex variable to the real line. The goal of this lect...
On the use of genetic algorithms for synthesis of signal temporal logic formulas
Aydin, Sertac Kagan; Aydın Göl, Ebru (2018-07-09)
In this work, we studied use of genetic algorithms to synthesize Signal Temporal Logic formulas from a labeled data set. In the synthesis problem, the goal is to generate the best STL formula representing the labeled signals in the set. To use genetic algoritms in this domain, the basic genetic algoritm processes are defined for STL formulas. The developed synthesis method produces a formula from the data set efficiently in a fully automated way. In particular, the proposed approach does not require an expe...
Citation Formats
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
S. K. Aydın, “Synthesis of signal temporal logic formulas with genetic algorithms,” Thesis (M.S.) -- Graduate School of Natural and Applied Sciences. Computer Engineering., Middle East Technical University, 2019.