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ı: Belirtilmemiş.
Ö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
- Şehirsel yerleşmelerde fraktal ve hücresel otomata yöntemi ile gelişme alanlarının belirlenmesi
Determination of urban development area by fractal and cellular automata method
MEHMET ALİ YÜZER
Doktora
Türkçe
2001
Şehircilik ve Bölge Planlamaİstanbul Teknik ÜniversitesiPROF. DR. CENGİZ GİRİTLİOĞLU
- Hidrolik bir servo sistemde pol atamalı adaptif konum kontrolü
The Pole assignment adaptive position control in a hydraulic servo system
AYHAN KURAL
- An FPGA-accelerated string-matching engine
FPGA ile hızlandırılmış bir dizi-eşleme donanımı
SÜLEYMAN SAMET YALÇIN
Yüksek Lisans
İngilizce
2024
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. ŞENAN ECE SCHMİDT
- Nanofiberlerin elektron mikroskobu görüntülerinin derin öğrenme yöntemleri kullanılarak sınıflandırılması
Classification of nanofibers' electron microscope images using the deep learning methods
ÇAĞRI YARDIMCI
Doktora
Türkçe
2026
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolSüleyman Demirel ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
DOÇ. DR. MEVLÜT ERSOY
- Hydrothermal synthesis and characterization of single crystalline CeO2 nanoparticles for catalytic applications.
Katalitik uygulamalar için tek kristal CeO2 nanoparçacıklarının hidrotermal sentezi ve karakterizasyonu.
TAYLAN MEŞİN
Yüksek Lisans
İngilizce
2012
Kimyaİzmir Yüksek Teknoloji EnstitüsüKimya Ana Bilim Dalı
DOÇ. DR. MEHTAP EMİRDAĞ EANES
YRD. DOÇ. DR. ALİ ÇAĞIR