Geri Dön

Partial order reduction for timed systems

Başlık çevirisi mevcut değil.

  1. Tez No: 402617
  2. Yazar: SERDAR OĞUZ ATA
  3. Danışmanlar: DR. YUSRA ALKHAZRAJI, DR. ROBERT MATTMÜLLER
  4. Tez Türü: Yüksek Lisans
  5. Konular: Matematik, Mathematics
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2014
  8. Dil: İngilizce
  9. Üniversite: Albert-Ludwigs-Universität Freiburg im Breisgau
  10. Enstitü: Yurtdışı Enstitü
  11. Ana Bilim Dalı: Belirtilmemiş.
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

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

    İngilizce

    2000

    Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik Üniversitesi

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

    DOÇ. DR. GÜNEY GÖNENÇ

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

    Türkçe

    2016

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    Makine Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. LEVENT ALİ KAVURMACIOĞLU

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

    Türkçe

    1994

    Endüstri ve Endüstri Mühendisliğiİstanbul Teknik Üniversitesi

    PROF.DR. GÖNÜL YENERSOY

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

    Türkçe

    1998

    Elektrik ve Elektronik Mühendisliğiİstanbul Teknik Üniversitesi

    Elektronik ve Haberleşme Mühendisliği Ana Bilim Dalı

    PROF. DR. AHMET DERVİŞOĞLU