ماشین مولر

به‌طور قراردادی ماشین منظم مولر یک تاپل (A = (Q,Σ,δ,q₀,F می‌باشد که از اطلاعات زیر تشکیل شده‌است:

Q یک مجموعه محدود است. مؤلفه‌های Q حالت‌های A نامیده می‌شود.

Σ یک مجموعه محدود است که الفبای A نامیده می‌شود.

δ: Q × Σ → Q یک تابع می‌باشد که تابع انتقال A نامیده می‌شود.

q₀ یک مؤلفه از Q می‌باشد که حالت اولیه نامیده می‌شود.

F مجموعه‌ای از مجموعه حالت‌هاست، به‌طور قراردادی، (F ⊆ P(Q در جایی که (P(Q مجموعه توانی Q می‌باشد. F شرایط پذیرش را مشخص می‌کند. A دقیقاً همان برنامه‌هایی را که مجموعه‌ای از حالت‌های بی‌نهایت اغلب اتفاق می‌افتد را قبول می‌کند که مؤلفه‌ای از F می‌باشد.

در یک ماشین مولر غیرقطعی، تابع انتقال δ با یک رابطه انتقال Δ جایگزین می‌شود که مجموعه‌ای از حالت‌ها را برمی‌گرداند و حالت اولیه که q₀ می‌باشد با مجموعه‌ای از حالت‌های اولیه Q₀ جایگزین می‌شود. به‌طور کلی ماشین مولر به ماشین غیرقطعی مولر اشاره می‌کند.

برای اطلاعات جامع‌تر به ماشین امگا مراجعه کنید.

ماشین مولر به اندازه ماشین parity، ماشین Rabin، ماشین Streett و ماشین غیرقطعی Büchi همانقدر واضح است و به شدت واضح تر از ماشین Büchi. همبستگی ماشین‌های فوق و ماشین غیرقطعی مولر را وقتی می‌توان نشان داد که به راحتی می‌توان شرایط پذیرش این ماشین‌ها را با استفاده از شرایط پذیرش ماشین مولر شبیه‌سازی کرد. نظریه مک ناتون همبستگی ماشین غیرقطعی Büchi با ماشین قطعی مولر را نشان می‌دهد؛ بنابراین ماشین قطعی و غیرقطعی مولر از لحاظ زبان‌هایی که می‌تواند بپذیرد همبستگی دارد.

در ادامه لیستی از ساختمان ماشین‌ها آورده شده که ماشین‌های نوع ω را به ماشین غیرقطعی مولر تبدیل می‌کند:

از ماشین Büchi

اگر B مجموعه‌ای از حالت‌های نهایی در ماشین Büchi با مجموعه‌ای از حالت‌های Q باشد، می‌توانیم ماشین مولر با مجموعه‌ای از همان حالت‌ها، تابع انتقال و حالت اولیه با شرایط پذیرش مولر به صورت {F = { X | X ∈ 2 ∧ X ∩ B ≠ᶲ بسازیم.

از ماشین Rabin یا ماشین Parity

به‌طور مشابه، شرایط(Rabin (E_{j ,} F_j می‌تواند با ساختن مجموعه پذیرش ماشین مولر به صورت همه مجموعه‌ها در که نتیجه می‌شود. توجه داشته باشید که در این مورد برخی از موارد ماشین Parity هم پوشش داده می‌شود، همان‌طور به راحتی می‌شود شرایط پذیرش Parity را به عنوان شرایط پذیرش Rabin بیان کرد.

از ماشین Streett

شرایط (Streett (E_{j ,} F_j می‌تواند با ساختن مجموعه پذیرش ماشین مولر به صورت همه مجموعه‌ها در که نتیجه می‌شود برای همه jها.

اجتماع دو ماشین قطعی مولر از ماشین Büchi

نظریه مک ناتون پروسه تبدیل ماشین غیرقطعی Büchi به ماشین قطعی مولر را ارائه می‌دهد.

1. Muller, David E. (1963). "Infinite sequences and finite machines". 4th Annual Symposium on Switching Circuit Theory and Logical Design (SWCT): 3–16.

• Automata on Infinite Words Slides for a tutorial by Paritosh K. Pandya.
  • Yde Venema (2008) Lectures on the Modal μ-calculus; the 2006 version was presented at The 18th European Summer School in Logic, Language and Information