Geri Dön

Synthesis of signal temporal logic formulas with genetic algorithms

Sinyal zamansal mantık formüllerinin sentezlenmesinde genetik algoritmaların kullanımı

  1. Tez No: 548438
  2. Yazar: SERTAÇ KAĞAN AYDIN
  3. Danışmanlar: DR. ÖĞR. ÜYESİ EBRU AYDIN GÖL
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Bilim ve Teknoloji, Computer Engineering and Computer Science and Control, Science and Technology
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2019
  8. Dil: İngilizce
  9. Üniversite: Orta Doğu Teknik Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

  1. 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

    İngilizce

    2020

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. EBRU AYDIN GÖL

  2. 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

    İngilizce

    2018

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. EBRU AYDIN GÖL

  3. Düşük bir hızlarında konuşma kodlama ve uygulamaları

    Low bit rate speech coding and applications

    TARIK AŞKIN

  4. 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

    İngilizce

    2000

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    DOÇ. DR. ETHEM ALPAYDIN

  5. 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

    İngilizce

    2015

    Jeodezi ve Fotogrametriİstanbul Teknik Üniversitesi

    Geomatik Mühendisliği Ana Bilim Dalı

    DOÇ. DR. HAYRİ HAKAN DENLİ