Synthesis of Controllable ptSTL Formulas

Date

2020-01-01

Author

Saglam, Irmak
Aydın Göl, Ebru

Metadata

Show full item record

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

Item Usage Stats

140
views

0
downloads

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, the results are shown on an example.

URI

https://hdl.handle.net/11511/93831

DOI

https://doi.org/10.1109/siu49456.2020.9302190

Conference Name

28th Signal Processing and Communications Applications Conference (SIU)

Collections

Department of Computer Engineering, Conference / Seminar

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...
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...
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 ...
Assessment of alternative simulation techniques in nonlinear time history analyses of multi-story frame buildings: A case study Karim Zadeh Naghshineh, Shaghayegh; Askan Gündoğan, Ayşegül; Yakut, Ahmet (2017-07-01) In regions with sparse ground motion data, simulations provide alternative acceleration time series for evaluation of the dynamic response of a structure. Different ground motion simulation methods provide varying levels of goodness of fit between observed and synthetic data. Before using the seismologically acceptable synthetic records for engineering purposes, it is critical to investigate the efficiency of synthetics in predicting observed seismic responses of structures. For this purpose, in this study ...
Implementation Studies of Robot Swarm Navigation Using Potential Functions and Panel Methods Merheb, Abdel-Razzak; GAZİ, VEYSEL; Sezer Uzol, Nilay (2016-10-01) This paper presents a practical swarm navigation algorithm based on potential functions and properties of inviscid incompressible flows. Panel methods are used to solve the flow equations around complex shaped obstacles and to generate the flowlines, which provide collision-free paths to the goal position. Safe swarm navigation is achieved by following the generated streamlines. Potential functions are used to achieve and maintain group cohesion or a geometric formation during navigation. The algorithm is i...

Citation Formats

I. Saglam and E. Aydın Göl, “Synthesis of Controllable ptSTL Formulas,” presented at the 28th Signal Processing and Communications Applications Conference (SIU), ELECTR NETWORK, 2020, Accessed: 00, 2021. [Online]. Available: https://hdl.handle.net/11511/93831.