Synthesis of signal temporal logic formulas with genetic algorithms
Sinyal zamansal mantık formüllerinin sentezlenmesinde genetik algoritmaların kullanımı
- Tez No: 548438
- Danışmanlar: DR. ÖĞR. ÜYESİ EBRU AYDIN GÖL
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Bilim ve Teknoloji, Computer Engineering and Computer Science and Control, Science and Technology
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2019
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 86
Özet
Sinyal zamansal mantık(Signal Temporal Logic, STL), devamlı sinyallerin davranışlarını anlamlandırmak için kullanılır. Anlatım gücü ve algoritmaları sayesinde, sinyal izleme prosedürleri için, donanım ve yazılım sistemlerinde kullanılacak izleme kurallarını tanımlamada kullanılır. Yine de, bir sistemin davranışını tanımlayan STL formülünü yazmak basit bir iş değildir. İzlenilecek sistemin bir uzmanının formülü üretip, ürettiği bu formülün parametrelerini, izleme anında doğabilecek hataları(yanlış ya da kaçırılan alarmlar) asgariye indirecek şekilde optimize etmesi gerekir. Dolayısıyla, formel izlemeyi basitleştirmek ve yaygınlaştırmak adına, formül oluşturma sürecinin otomatize edilme ihtiyacı vardır, ki bu çalışmanın temel motivasyonunu da bu ihtiyaç oluşturur. Farklı alanlardan gelen farklı veri kümeleri birbirlerinden boyutça farklılıklar gösterirler, ve hatta çok çok büyüyebilirler de. Bu tip durumları da düşünerek, genetik algoritma bazlı paralel bir formül sentezleme metodu üzerine çalıştık. Sunduğumuz çözüm, bir uzman yardımına ihtiyaç duymaksızın, gerekli formülü türetip parametreleri optimize edebilmekte. Dahası her bir formül yapısına ait lokal optimum parametreleri bulabilmek adına, parametre uzayı üzerinde çalışan rastlantısal bir arama metodu geliştirdik, ve bu sayede önerilen formülün daha az tekrarda amaçlanan formüle yakınsamasını sağladık.
Özet (Çeviri)
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.
Benzer Tezler
- Synthesis of past time signal temporal logic formulas using monotonicity properties
Monotonluk özelliklerı kullanılarak geçmiş zamanlı sinyal zamansal mantık formülleri sentezlenmesi
MERT ERGÜRTUNA
Yüksek Lisans
İngilizce
2020
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. EBRU AYDIN GÖL
- Synthesis of formal control strategies for traffic systems
Trafik sistemleri için formel kontrol stratejilerinin sentezlenmesi
KEMAL ÇAĞRI BARDAKÇI
Yüksek Lisans
İngilizce
2018
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. EBRU AYDIN GÖL
- Düşük bir hızlarında konuşma kodlama ve uygulamaları
Low bit rate speech coding and applications
TARIK AŞKIN
Doktora
Türkçe
1999
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. GÜNSEL DURUSOY
- Variable sized input multi layer perceptrons for speech recognition
Değişken boyutlu girdili çok katmanlı perceptronlar ile ses tanıma
OLCAY KURŞUN
Yüksek Lisans
İngilizce
2000
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
DOÇ. DR. ETHEM ALPAYDIN
- Analysis of GRACE L2 data globally and regionally with PCA
Global ve bölgesel olarak GRACE L2 verilerinin PCA ile analizi
CEREN ALTUNAL PODLECH
Yüksek Lisans
İngilizce
2015
Jeodezi ve Fotogrametriİstanbul Teknik ÜniversitesiGeomatik Mühendisliği Ana Bilim Dalı
DOÇ. DR. HAYRİ HAKAN DENLİ