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

**اتوماتون بوچی** (زبان انگلیسی: Büchi automaton) را می‌توان به عنوان اتوماتونی در نظر گرفت که می‌توانند رشته‌های نامتناهی الفبا را بپذیرد. این اتوماتون اولین بار توسط ژولیوس ریچارد بوچی (Julius Richard Büchi) منطق‌دان سوئیسی در سال ۱۹۶۲ معرفی شد. اگر ω را به عنوان مجموعه اعداد طبیعی و Σ رابه عنوان الفبا در نظر بگیریم یک کلمه نامتناهی (یا یک ω-کلمه) را می‌توان به عنوان یک تابع از ω به Σ در نظر گرفت به این ترتیب مجموعه تمام کلمه‌های نامتناهی را با \Sigma^\omega  نشان می‌دهیم.بندانگشتی|Julius Richard Büchi

## تعریف
یک اتوماتون بوچی قطعی ۵ تایی A = (Q, \Sigma, \delta, q_0, F) است که در ان:
* Q مجموعه ای محدود از حالات است.
* Σ مجموعه‌ای محدود از نمادها است که الفبای A یا الفبای ورودی خوانده می‌شود.
*  \delta : Q \times \Sigma \rightarrow Q  تابع انتقال است.
* q_0 عضوی از Q است و حالت ابتدایی نامیده می‌شود
* F\subset Q مجموعه حالات قبول یا پایانی خوانده می‌شود.

فرض کنید A = (Q, \Sigma, \delta, q_0, F) یک اتوماتون بوچی متناهی باشد در این صورت یک تعمیم طبیعی از مفهوم اجرا (نسبت به اتوماتون قطعی متناهی) می‌تواند مطرح شود که به این صورت است که یک اجرا روی یک کلمه نامتناهی \sigma = a_1a_2a_3... را به صورت دنبالهٔ r = sq_1q_2q_3... تعریف می‌کنیم که از s شروع می‌کنیم و با a_1 به q_1 و سپس با a_2 به q_2 و… می‌رویم.
به عنوان مثال در این اتوماتون:
بندانگشتی|200px|A non-deterministic Büchi automaton that recognizes (0∪۱)*0<sup>ω</sup>
اگر \sigma = 100^\omega.. در اینصورت r = q_0q_1q_1^\omega یه اجرای A است.

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

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

## زبان‌های قابل تشخیص توسط اتوماتون بوچی
مجموعه تمام ω-کلمه‌های را که یک بوچی اتوماتون قبول می‌کند زبان ان بوچی اتوماتون می‌گویند. حالا یک زبان A\subset \Sigma^\omega را بوچی تشخیص پذیر می‌گوییم اگر بوچی اتوماتون M ای پیدا شود که  L(M) = A  . یک زبان بوچی تشخیص پذیر است اگر و فقط اگر یک زبان امگا‌ی منظم باشد.
مثلاً  A=\Sigma^* a^\omega \bigcup \Sigma^* (ab)^\omega  .

## ویژگی‌های بستاری
فرض کنید A,B دو بوچی اتوماتون باشند و C یک اتوماتون متناهی باشد در این داریم:
# اجتماع:بوچی اتوماتونی هست که L(A) \cup L(B) را تشخیص می‌دهد
# اشتراک:بوچی اتوماتونی هست که L(A) \cap L(B) را تشخیص می‌دهد
# اتصال:بوچی اتوماتونی هست که L(C).L(A) را تشخیص می‌دهد
# ω-بستار:اگرL(C) کلمهٔ تهی را نداشته باشد بوچی اتوماتونی هست که L(C)^\omega را تشخیص می‌دهد
# مکمل:بوچی اتوماتونی هست که \Sigma^\omega/L(A) را تشخیص می‌دهد

## انواع
* اتوماتون 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

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