Parameter synthesis for timed automata via path analysis
Zamanlı otomat için yol analizi ile parametre sentezi
- Tez No: 833222
- Danışmanlar: DOÇ. DR. EBRU AYDIN GÖL
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2023
- 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ı: 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
- Hidrolik bir servo sistemde pol atamalı adaptif konum kontrolü
The Pole assignment adaptive position control in a hydraulic servo system
AYHAN KURAL
- Robot kollarda optimum hareket sentezi
Optimal trajectory synthesis for manipulation robots
ÖZGÜR TURHAN
- 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
- Ç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
2020
Elektrik ve Elektronik MühendisliğiTOBB Ekonomi ve Teknoloji ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. COŞKU KASNAKOĞLU
DR. ÖĞR. ÜYESİ RECEP MUHAMMET GÖRGÜLÜARSLAN
- 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
2012
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolYıldız Teknik ÜniversitesiElektrik Mühendisliği Ana Bilim Dalı
DOÇ. DR. KAYHAN GÜLEZ
DOÇ. DR. İBRAHİM BEKLAN KÜÇÜKDEMİRAL