Partial order reduction for timed systems
Başlık çevirisi mevcut değil.
- Tez No: 402617
- Danışmanlar: DR. YUSRA ALKHAZRAJI, DR. ROBERT MATTMÜLLER
- Tez Türü: Yüksek Lisans
- Konular: Matematik, Mathematics
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2014
- Dil: İngilizce
- Üniversite: Albert-Ludwigs-Universität Freiburg im Breisgau
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 41
Özet
Özet yok.
Özet (Çeviri)
In this work, an application of a partial order reduction method for the reachability analysis of timed systems using local-time semantics is presented. Reachability analysis of timed systems requires exploring an excessive size of the state-space. The size of the statespa. ce can be reduced by using partial order reduction methods. Partial order reduction methods make use of the independence relation between transitions. Two transitions are independent if they lead to the same state with any execution order. Exploring one of the two possible execution order is sufficient to rea.ch the same states. Partia.l order reduction methods choose one of the two paths and prune the other one to decrease the size of the state space to be explored. Application of partial order reduction methods to timed systems is not straightforward, since all of the transitions which include a clock variable are implicitly synchronized. Thus local-time semantics is proposed to enable the application of partial order reduction methods to timed automata. The idea of local-time semantics is to remove the implicit clock synchroniza.tion between the loca.l clocks of different processes to a.llow loca.l clocks to a.dva. nce with different time sca.les. Using loca.l-time sema.ntics allows usage of independence of transitions in different processes thus allowing application of pa.rtial order reduction techniques to timed automata. In this paper, stubborn sets are used as the partial order reduction method. Local-time sernantics and stubborn sets are implemented in MCTA, a model checking tool for timed automata. The implementation is tested with the benchmarks available for MCTA and test results showing the size of explored state-space with global time semantics, wit h local time semantics and with local time semantics and stubborn sets are added. 3
Benzer Tezler
- Static partial order reduction and model checking of hardware/software co-design systems
Durağan kısmi sıra eksiltme ve donanım/yazılım birleşik sistemlerin model kontrolü
HÜSNÜ YENİGÜN
Doktora
İngilizce
2000
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
DOÇ. DR. GÜNEY GÖNENÇ
- Eksenel gaz türbini kanat ucu geometrisinin hesaplamalı akışkanlar dinamiği ile aerotermal tasarımı
Aerothermal design of axial gas turbine blade tip using computational fluid dynamics
CEM BERK ŞENEL
Yüksek Lisans
Türkçe
2016
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. LEVENT ALİ KAVURMACIOĞLU
- Esnek imalat sistemleri ve alternatif rotaları göz önünde bulundurarak esnek ortamlar için üretim hücrelerinin dizaynı
Flexible manufacturing systems and design of manufacturing cells for flexible environmental
GİRAY İLKER ÇELİK
Yüksek Lisans
Türkçe
1994
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. GÖNÜL YENERSOY
- Buhar difüzyonunun dış duvarların nem ile ilgili ve ısıl performansına etkilerinin değerlendirilmesinde kullanılabilecek bir yaklaşım
Başlık çevirisi yok
M.CEM ALTUN
Doktora
Türkçe
1997
Mimarlıkİstanbul Teknik ÜniversitesiMimarlık Ana Bilim Dalı
PROF. DR. İMER SUNGUROĞLU
- VHDL ile lojik devre tasarımı ve DSP uygulamaları için çarpma bloklarının modellenmesi
Başlık çevirisi yok
SIDDIKA BERNA ÖRS
Yüksek Lisans
Türkçe
1998
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiElektronik ve Haberleşme Mühendisliği Ana Bilim Dalı
PROF. DR. AHMET DERVİŞOĞLU