اتوماتون بوچی

تعریف 
یک اتوماتون بوچی قطعی ۵ تایی  است که در ان:
 Q مجموعه ای محدود از حالات است.
 Σ مجموعه‌ای محدود از نمادها است که الفبای A یا الفبای ورودی خوانده می‌شود.
  تابع انتقال است.
  عضوی از Q است و حالت ابتدایی نامیده می‌شود
  مجموعه حالات قبول یا پایانی خوانده می‌شود.

فرض کنید  یک اتوماتون بوچی متناهی باشد در این صورت یک تعمیم طبیعی از مفهوم اجرا (نسبت به اتوماتون قطعی متناهی) می‌تواند مطرح شود که به این صورت است که یک اجرا روی یک کلمه نامتناهی  را به صورت دنبالهٔ  تعریف می‌کنیم که از s شروع می‌کنیم و با  به  و سپس با  به  و… می‌رویم.
به عنوان مثال در این اتوماتون:
بندانگشتی|200px|A non-deterministic Büchi automaton that recognizes (0∪۱)*0ω
اگر  در اینصورت  یه اجرای A است.

در این صورت می‌گوییم ماشین A رشته σ را قبول می‌کند اگر اجرایی وجود داشته باشد که در ان حداقل یکی از حالات قبول را به تعداد نامتناهی دیده باشیم.

در اتوماتون بوچی غیرقطعی به‌جای تابع انتقال، رابطهٔ انتفال مطرح است و مانند NFA هر حالت تحت رابطهٔ انتقال به مجموعه ای از حالات منجر می‌شود و به‌جای حالت آغازی مجموعه از حالات ابتدایی در نظر گرفته می‌شود. در حالت کلی وقتی کلمه اتوماتون بوچی را به تنهایی به کار می‌بریم منظورمان اتوماتون بوچی غیرقطعی است.

 زبان‌های قابل تشخیص توسط اتوماتون بوچی 
مجموعه تمام ω-کلمه‌های را که یک بوچی اتوماتون قبول می‌کند زبان ان بوچی اتوماتون می‌گویند. حالا یک زبان  را بوچی تشخیص پذیر می‌گوییم اگر بوچی اتوماتون M ای پیدا شود که  . یک زبان بوچی تشخیص پذیر است اگر و فقط اگر یک زبان امگا‌ی منظم باشد.
مثلاً  .

 ویژگی‌های بستاری 
فرض کنید A,B دو بوچی اتوماتون باشند و C یک اتوماتون متناهی باشد در این داریم:
 اجتماع:بوچی اتوماتونی هست که  را تشخیص می‌دهد
 اشتراک:بوچی اتوماتونی هست که  را تشخیص می‌دهد
 اتصال:بوچی اتوماتونی هست که  را تشخیص می‌دهد
 ω-بستار:اگر کلمهٔ تهی را نداشته باشد بوچی اتوماتونی هست که  را تشخیص می‌دهد
 مکمل:بوچی اتوماتونی هست که  را تشخیص می‌دهد

 انواع 
 اتوماتون Co-Büchi
 اتوماتون بوچی ضعیف
 اتوماتون بوچی نیمه قطعی
 اتوماتون بوچی توسعه یافته

 کاربرد 
از بوچی اتوماتون معمولاً در وارسی مدل به عنوان یه نسخه نظریه ماشینی از یک فرمول در منطق موقت خطی استفاده می‌شود.
 جستارهای وابسته 
 وارسی مدل
 زبان امگا
 مترجم دوگانه
 ماشین بوخی توسعه یافته
 منابع 

 Y. Choueka: “Theories of automata on !-tapes: A simplified approach”, Journal of
Computer and System Sciences 8 (1974) No. 2, 117–141.
 https://faculty.math.illinois.edu/~eid1/ba.pdf

رده:ماشین متناهی
رده:مدل‌های محاسباتی
رده:مقاله‌های ایجادشده توسط ایجادگر
رده:نظریه اتوماتا
رده:وارسی مدل