اتوماتای بوچی (Buchi Automaton)

اتوماتای بوچی (Buchi Automaton)

اسلاید 1: اتوماتای بوچی

اسلاید 2: مقدمهماشین بوچی، ماشین متناهی‌ای است که عبارات نامتناهی را می‌پذیرد.در ادامه خواهیم دید که ماشین بوچی، خواصی دارد که می‌تواند برای ساخت الگوریتم‌های کنترل مدل (Model Checking Algorithm) برای LTL (Linear Temporal Logic) موثر واقع شود.

اسلاید 3: زبان‌های امگا(𝜔)یک زبان امگا معادل با اتوماتای بوچی استاگر و تنها اگرعضو کلاس زبان‌های منظم امگا باشدزبان منظم امگا یک بخش از تعریف بالاستمجموعه زبان‌هایی که منظم‌اند اما لزوماً متناهی نیستندهر مجموعه از رشته‌های به طول نامتناهی از یک الفبای مشخص، یک زبان امگا بر روی آن الفبا می‌باشد𝛚

اسلاید 4: مشکلات تشخیص زبان‌های امگایکی از مشکلاتی که در تشخیص این زبان‌ها وجود دارد این است که برای تشخیص آن‌ها در زمان اجرا، ما تنها می‌توانیم تعداد محدودی واژه را در هر زمان خوانده باشیم ولی طول رشته‌های این زبان می‌تواند نامتناهی باشد.

اسلاید 5: ماشین امگا و کاربردهای آنماشین امگا، گونه‌ای از ماشین‌های حالت متناهی است که ورودی آن رشته‌های نامتناهی به جای رشته‌های متناهی می‌باشد. از آنجایی که رشته‌های ورودی نامتناهی می‌باشند، ماشین‌های امگا به جای مجموعه وضعیت‌های قبول، شرایط قبول دارند.با توجه به ورودی ماشین‌های امگا که نامتناهی است، می‌توان از آن‌ها برای توصیف وضعیت سامانه‌هایی از قبیل سخت‌افزارها، سیستم‌های عامل، سیستم‌های کنترلی، تصدیق سیستم‌ها و محاسبات استفاده کرد.

اسلاید 6: منطق موقت خطی(Linear temporal logic)یک مساله در منطق موقت خطی، می‌تواند بررسی فرموله کردن آینده یک مسیر باشد؛ مثلاً این که یک شرط در نهایت درست خواهد شد یا اصلاً درست نخواهد شد یا … منطق موقت یک فرمالیسم مناسب برای مشخص کردن و تصدیق ویژگی‌های یک سیستم واکنش‌گرا است.یک فرمول از منطق موقت، یک مجموعه از دنباله‌های نامتناهی را که برای تشخیص درست بودن هر یک از فرمول‌ها به کار می‌رود، توصیف می‌کند که به آن خواص موقت (Temporal Property) نیز گفته می‌شود.یک سیستم پیشنهادی، یک خاصیت را زمانی تأیید می‌کند که تمامی محاسباتش مربوط به این مجموعه باشد.

اسلاید 7: ماشین بوچی چیست؟ماشین بوچی را می‌توان ماشینی در نظر گرفت که می‌تواند رشته‌های نامتناهی الفبا را بپذیرد. این ماشین اولین بار توسط ریچارد بوچی منطق‌دان سوئیسی در سال 1962 معرفی شد.اگر𝜔 را به عنوان مجموعه اعداد طبیعی و Σ را به عنوان الفبا در نظر بگیریم یک کلمه نامتناهی (یا یک 𝜔-کلمه) را می‌توان به عنوان یک تابع از 𝜔 به Σ در نظر گرفت. به این ترتیب مجموعه تمام کلمه‌های نامتناهی را با Σ 𝜔 نشان می‌دهیم.

اسلاید 8: تعاریفمجموعه اعداد صحیح نامنفی را با 𝜔 نشان می‌دهیم؛ یعنی 𝜔={0,1,2,…} . الفبای ورودی متناهی را نیز با Σ نمایش می‌دهیم؛ در حالی که Σ ∗ مجموعه‌ی تمام کلمات متناهی بر روی الفبای Σ است، Σ 𝜔 مجموعه‌ی تمام کلمات نامتناهی بر روی الفبای مذکور می‌باشد.زبان 𝐿 را یک زبان 𝜔 گوییم هرگاه کلمات آن، زیرمجموعه‌ای از Σ 𝜔 باشند؛ یعنی 𝐿⊆ Σ 𝜔 .