Synthesis of formal control strategies for traffic systems
Trafik sistemleri için formel kontrol stratejilerinin sentezlenmesi
- Tez No: 489443
- Danışmanlar: YRD. DOÇ. DR. EBRU AYDIN GÖL
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2018
- 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ı: 105
Özet
Trafik sıkışıklığı, dünyadaki metropollerdeki gibi ülkemizde İstanbul ve Ankara gibi büyük şehirlerde insan yaşamını olumsuz etkileyecek seviyelere ulaşmış durumdadır. Trafik sıkışıklığı, sebep olduğu kaybolan zaman, boşa giden yakıt/ para, çevre üzerindeki olumsuz etkilerle insanların yaşam kalitesini düşürmektedir. Bu konuda yapılan araştırmalar, trafik ağı kontrolünün ne denli önemli olduğunu göstermektedir. Çok sayıda araç ve yayanın, farklı yol ve ışık yapılandırmalarındaki etkileşimleri karmaşıklaşmakta, dolayısıyla karmaşık gereksinimleri sağlayacak trafik sistemlerinin oluşturulması gerekmektedir. Bu alanda yapılan çalışmalarla yol ve ışık bazındaki karmaşık gereksinimleri, oluşturulan trafik sistemi modeli üzerinde kontrol edebilecek farklı mekanizmalar geliştirilmeye çalışılmıştır. Bu tezde, büyük bir sinyalize trafik sistemi üzerinde, tanımlanmış karmaşık doğrusal zamansal mantık gereksinimlerini sağlayacak bir kontrolcü sentezleme problemi üzerine çalışmalar yapılmıştır. Yaptığımız çalışmalarda, özellikle büyük trafik sistemlerinin formel kontrolünde ortaya çıkan ölçeklenebilirlik sorunu üzerine odaklanarak, bu sorunu ana problemi daha küçük problemlere ayrıştıracak çözümler üretmekteyiz. Geliştirilen bölüntüleme algoritması ana trafik sistemini alt sistemlere bölüp, ana gereksinimden her bir alt sistem için gereksinim kümesi elde etmektedir. Bunun yanında, alt sistemler arasında eşit ve adil dağılımın garanti edilmesi adına komşu sistemler arasındaki sınır sinyalleri üzerinde ek kısıtlar türetilmektedir. Alt sistemler için kontrol stratejileri üretilmesi sırasında ise soyutlama tekniklerinden yararlanılmaktadır. Bu şartlar altında, her bir alt sistem için kontrolcü üretiliyor olmasının, sistemin bütününün ana gereksinimi sağlamasını garantileyeceği ispatlanmaktadır. Ayrıca, sınırlandırılmış operatörler kullanılarak bunların gereksinimi sağlayan başlangıç durum kümesi üzerindeki etkileri incelenmektedir. Son olarak bu tez, çeşitli optimizasyon kriterlerini kontrol stratejileri üzerinde deneyimlemektedir. Örnek olarak, trafik sistemindeki toplam sinyal değişim sayısının minimize edilmesi, maksimum araç yoğunluğuna sahip yoldaki araç yoğunluğunun minimize edilmesi sayılabilir.
Özet (Çeviri)
The problems caused by traffic congestion affect human life adversely. Wasted amount of time, fuel and money as well as adverse effects to environment are examples of these problems which reduce life quality. Studies on traffic management underline importance of traffic network control mechanisms. Different configurations of roads and signalized intersections complicate interactions among vehicles and pedestrians. Hence, traffic control systems, which need to satisfy complex specifications, should be constructed to serve complex traffic network features. In this dissertation, we study the problem of synthesizing a signal control strategy for a traffic system from Linear Temporal Logic (LTL) specifications. We focus on scalability issue in formal control of large traffic systems and propose to tackle it by decomposing the main problem into smaller problems. The developed decomposition algorithm partitions main traffic system into subsystems and derives a specification for each subsystem from main specification. In addition, we derive additional constraints on the signals lying on boundaries of subsystems to ensure fairness. We employ abstraction based techniques to find control strategies for subsystems by considering dynamics of adjacent subsystems. We show that the controllers found for each system guarantee that overall traffic system satisfies given specification. Moreover, we use bounded LTL, and we analyze effects of bounds on resulting set of satisfying initial states. Furthermore, this dissertation incorporates various optimization criteria into control synthesis. In particular, we developed novel methods to synthesize strategies minimizing the total number of switches and minimizing the maximum vehicle denisty in any link.
Benzer Tezler
- Formal verification and controller synthesis for discrete-time systems
Başlık çevirisi yok
EBRU AYDIN GÖL
Doktora
İngilizce
2014
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoston UniversityPROF. CALIN BELTA
- Avmlerin fijital deneyim merkezlerine dönüşümü ve artırılmış gerçeklik tabanlı bir oyunlaştırılmış ortam önerisi: 'Forus'
The transformation of the malls to the phygital experience centers and as a gamification framework for ar based phygital retail: 'Forus'
ÇAĞIL ÖZALP
Yüksek Lisans
Türkçe
2019
Mimarlıkİstanbul Teknik ÜniversitesiBilişim Ana Bilim Dalı
DOÇ. DR. SEMA ALAÇAM
- Optimizing artistic process: Exploring efficient environment creation workflows in gaming industry
Sanatsal sürecin optimizasyonu: Oyun endüstrisinde verimli çevre oluşturma süreçlerinin incelenmesi
EMRAH ÖZÇİÇEK
Yüksek Lisans
İngilizce
2024
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiOyun ve Etkileşim Teknolojileri Ana Bilim Dalı
PROF. DR. LEMAN FİGEN GÜL
- Kemaliye (Eğin) yerleşme dokusu ve evleri üzerine bir araştırma
Kemaliye (Eğin) a research study of settlement patterns and dwellings
BERRİN ALPER
Doktora
Türkçe
1990
Mimarlıkİstanbul Teknik ÜniversitesiMimarlık Tarihi Ana Bilim Dalı
PROF. DR. METİN SÖZEN
- 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