Geri Dön

Parameter synthesis for timed automata via path analysis

Zamanlı otomat için yol analizi ile parametre sentezi

  1. Tez No: 833222
  2. Yazar: BURKAY SUCU
  3. Danışmanlar: DOÇ. DR. EBRU AYDIN GÖL
  4. Tez Türü: Doktora
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2023
  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ı: 83

Özet

Zamanlı otomatların zamanlı kısıtlamalarda sabit değerler yerine parametreler kullanılarak genişletilmesiyle elde edilen parametrik zamanlı otomatlar, belirsizliklerin tasarım aşamasında uygun biçimde ele alınabilmesi için esneklik sağlar. Parametrik model elde edildikten sonra, ortaya çıkacak zamanlı otomatın verilen tanımlamaları sağlayacağı en uygun parametre değerlerini bulmak için parametre sentez yöntemleri bu modele uygulanır. Bu tezde, parametrik zamanlı otomatlar için parametre sentezi stratejileri geliştirilmiştir. Sunulan yaklaşımlar, otomat grafiğinin derin öncelikli aranması sırasında parametre kısıtlamalarının toplanmasını içerir. Derin öncelikli arama sırasında karşılaşılan yolların gerçekleştirilebilirlik problemleri, Karma Tamsayılı Doğrusal Programlama (MILP) veya Doğrusal Olmayan Programlama (NLP) problemleri olarak kodlanır; daha sonra, bu problemler verilen tanımlamalara bağlı olarak farklı şekillerde değerlendirilir. Ulaşılabilirlik gibi tek bir tanığın yeterli olduğu tanımlamalar için, derin öncelikli arama, kabul eden bir konumda biten bir yolu gerçekleştirilebilir kılan ilk parametre kısıtlamasını döndürür. Güvenlik gibi hiçbir tanığın olmaması gereken tanımlamalar için, parametre kısıtlamaları, kodlanmış problemlere niceleme eleme uygulanarak bulunur ve derin öncelikli arama boyunca toplanır. Derin öncelikli arama, gerçekleştirilemez dalların kesilmesiyle iyileştirilir ve döngüsel yolların analizi için sunulan yeni yöntemlerle bu aramanın sona erdirilmesi garanti edilir. Derin öncelikli arama aracılığıyla toplanan kısıtlamalar, bu kısıtlamaları karşılayan bir parametre değerlemesinin sentez problemini çözeceğini garanti eder. Daha sonra, geliştirilen algoritmalar, belirli bir kriter için en iyi parametre değerlerini bulmak üzere genişletilmiştir. Önerilen algoritmaların doğruluğu ve eksiksizliği gösterilmiştir. Tüm sonuçlar örneklerle açıklanmıştır.

Özet (Çeviri)

Parametric timed automata (PTA) extends timed automata (TA) with parameters instead of fixed timing constraints, providing the flexibility to accommodate uncertainties during the design phase. Once the parametric model is obtained, parameter synthesis methods are applied to find the optimal parameter values such that the resulting timed automaton satisfies the specifications. In this thesis, parameter synthesis strategies for parametric timed automata are developed. The proposed approaches involve accumulating parameter constraints while exploring the automata graph in a depth-first manner. Realizability problems of encountered paths during the graph search are encoded as Mixed Integer Linear Programming (MILP) or Non-Linear Programming (NLP) problems; then, those problems are evaluated in different ways depending on the given specifications. For specifications where a single witness is enough, e.g., reachability, the depth-first search returns the first parameter constraint that makes a path ending in an accepting state realizable. For specifications where no witness must exist, e.g., safety, parameter constraints are found by applying quantifier elimination on encoded problems and accumulated along the depth-first traversal. Depth-first traversal is optimized via pruning unrealizable branches and guaranteed to terminate via the proposed novel cycle analysis methods. The collected constraints through the depth-first search guarantee that a parameter valuation satisfying these constraints solves the synthesis problem. The developed algorithms are extended to generate the optimal parameter values for a given criteria. The correctness and completeness of the proposed algorithms are presented. All the results are depicted via examples.

Benzer Tezler

  1. Hidrolik bir servo sistemde pol atamalı adaptif konum kontrolü

    The Pole assignment adaptive position control in a hydraulic servo system

    AYHAN KURAL

    Yüksek Lisans

    Türkçe

    Türkçe

    1992

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    DOÇ. DR. CAN ÖZSOY

  2. Robot kollarda optimum hareket sentezi

    Optimal trajectory synthesis for manipulation robots

    ÖZGÜR TURHAN

    Doktora

    Türkçe

    Türkçe

    1990

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    PROF.DR. FUAT PASİN

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

  4. Çok hedefli optimizasyon yöntemleri ile uçuş kontrol algoritma tasarımı

    Flight control algorithm design with multiobjective parameter synthesis

    SAMET USLU

    Yüksek Lisans

    Türkçe

    Türkçe

    2020

    Elektrik ve Elektronik MühendisliğiTOBB Ekonomi ve Teknoloji Üniversitesi

    Elektrik-Elektronik Mühendisliği Ana Bilim Dalı

    PROF. DR. COŞKU KASNAKOĞLU

    DR. ÖĞR. ÜYESİ RECEP MUHAMMET GÖRGÜLÜARSLAN

  5. Doğrusal parametre değişimli sistemlerin ileri beslemeli kontrol tasarımı ve kalıcı mıknatıslı senkron motora uygulanması

    Feedforward control synthesis of linear parameter varying systems and application to permanent magnet synchronous motor

    YUSUF ALTUN

    Doktora

    Türkçe

    Türkçe

    2012

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolYıldız Teknik Üniversitesi

    Elektrik Mühendisliği Ana Bilim Dalı

    DOÇ. DR. KAYHAN GÜLEZ

    DOÇ. DR. İBRAHİM BEKLAN KÜÇÜKDEMİRAL