Co-Büchi otomat - Co-Büchi automaton

İçinde otomata teorisi, bir co-Büchi otomat bir çeşididir Büchi otomat. Tek fark, kabul etme koşuludur: bir Co-Büchi otomatı sonsuz bir kelimeyi kabul eder Çalıştırmada sonsuz sıklıkla meydana gelen tüm durumlar son durum kümesinde olacak şekilde bir çalıştırma varsa . Aksine, bir Büchi otomat bir kelimeyi kabul eder bir çalıştırma varsa, en az bir durum son durum kümesinde sonsuz sıklıkta meydana gelir .

(Deterministik) Co-Büchi otomatları, (kesin olmayan) Büchi otomatlarından kesinlikle daha zayıftır.

Resmi tanımlama

Resmen, bir deterministik ortak Büchi otomat bir demet aşağıdaki bileşenlerden oluşur:

  • bir Sınırlı set. Unsurları denir eyaletler nın-nin .
  • adı verilen sonlu bir kümedir alfabe nın-nin .
  • ... geçiş işlevi nın-nin .
  • bir unsurdur , başlangıç ​​durumu olarak adlandırılır.
  • ... son durum seti. tam olarak bu kelimeleri kabul eder koşarak içinde sonsuz sıklıkla meydana gelen tüm durumların içeride .

İçinde deterministik olmayan ortak Büchi otomatgeçiş işlevi bir geçiş ilişkisi ile değiştirilir . İlk durum bir başlangıç ​​durum kümesiyle değiştirilir . Genel olarak, ortak Büchi otomat terimi, deterministik olmayan ortak Büchi otomatını ifade eder.

Daha kapsamlı biçimcilik için ayrıca bkz. ω-otomat.

Kabul Koşulu

Ortak Büchi otomatının kabul koşulu resmi olarak

Büchi kabul koşulu, ortak Büchi kabul koşulunun tamamlayıcısıdır:

Özellikleri

Co-Büchi otomatları, birleşim, kavşak, projeksiyon ve belirleme altında kapatıldı.