अनंत वस्तुओं पर ऑटोमेटा

अनंत वस्तुओं पर ऑटोमेटा ऐसे इनपुट पढ़ते हैं जो कभी समाप्त नहीं होते, जैसे कि अनंत शब्द या अनंत वृक्ष, और इस आधार पर स्वीकार करते हैं कि कौन सी अवस्थाएँ या संक्रमण अनंत बार देखे जाते हैं, जो चल रही, गैर-समाप्त होने वाली प्रणालियों के बारे में तर्क करने के लिए गणितीय मशीनरी प्रदान करते हैं।

Definition

एक ओमेगा-ऑटोमेटन (omega-automaton) एक परिमित-अवस्था मशीन है जिसकी रन अनंत होती हैं, जिसमें स्वीकृति अनंत बार देखी गई अवस्थाओं के सेट पर एक शर्त द्वारा परिभाषित की जाती है; ऐसे ऑटोमेटा अनंत शब्दों या वृक्षों के सेट को पहचानते हैं जिन्हें ओमेगा-रेगुलर भाषाएँ (omega-regular languages) कहा जाता है।

Scope

यह विषय अनंत शब्दों पर बूची (Büchi), मुलर (Muller), राबिन (Rabin), और पैरिटी (parity) ऑटोमेटा, उन्हें अलग करने वाली स्वीकृति शर्तें, निर्धारणीकरण (determinization) और पूरकता (complementation) परिणाम, अनंत वृक्षों पर ऑटोमेटा, और इन ऑटोमेटा, एकात्मक द्वितीय-क्रम तर्क (monadic second-order logic), तथा संश्लेषण और सत्यापन में उपयोग किए जाने वाले अनंत खेलों के बीच गहरे संबंधों को शामिल करता है।

Core questions

• एक परिमित मशीन ऐसे इनपुट को कैसे स्वीकार या अस्वीकार कर सकती है जिसका कोई अंत न हो?
• गैर-निर्धारणात्मक (nondeterministic) और निर्धारणात्मक (deterministic) बूची ऑटोमेटा की अभिव्यंजक शक्ति (expressive power) में अंतर क्यों होता है?
• अनंत वस्तुओं पर ऑटोमेटा प्रणाली के व्यवहार को निर्दिष्ट करने वाले तर्क (logics) से कैसे संबंधित हैं?
• इन ऑटोमेटा की पूरकता (complementation) को क्या मुश्किल बनाता है, और यह क्यों मायने रखता है?

Key theories

बूची स्वीकृति और ओमेगा-रेगुलर भाषाएँ

एक बूची ऑटोमेटन एक अनंत शब्द को तब स्वीकार करता है जब कोई स्वीकृत अवस्था अनंत बार देखी जाती है, और इस प्रकार पहचानी गई भाषाएँ, ओमेगा-रेगुलर भाषाएँ, प्राकृतिक संख्याओं पर एकात्मक द्वितीय-क्रम तर्क में परिभाषित की जा सकने वाली भाषाओं के साथ मेल खाती हैं।

निर्धारणीकरण और पैरिटी शर्त

गैर-निर्धारणात्मक बूची ऑटोमेटा को सामान्यतः स्वीकृति शर्त को बदले बिना निर्धारणात्मक नहीं बनाया जा सकता है, लेकिन सफरा का निर्माण (Safra's construction) उन्हें निर्धारणात्मक राबिन या पैरिटी ऑटोमेटा में परिवर्तित करता है, जो पूरकता और खेलों को हल करने के लिए आवश्यक है।

Clinical relevance

ओमेगा-ऑटोमेटा मॉडल चेकिंग (model checking) की एल्गोरिथम रीढ़ हैं: एक प्रतिक्रियाशील प्रणाली और एक अस्थायी-तर्क गुण (temporal-logic property) प्रत्येक को अनंत शब्दों पर ऑटोमेटा में अनुवादित किया जाता है, और गुण की जाँच एक शून्यता परीक्षण (emptiness test) तक कम हो जाती है, जिससे हार्डवेयर, प्रोटोकॉल और समवर्ती सॉफ्टवेयर (concurrent software) का स्वचालित सत्यापन संभव हो पाता है।

History

बूची ने लगभग 1960 में प्राकृतिक संख्याओं के एकात्मक द्वितीय-क्रम सिद्धांत (monadic second-order theory) का निर्णय करने के लिए अनंत शब्दों पर ऑटोमेटा प्रस्तुत किया, मैकनॉटन (McNaughton) ने दिखाया कि उन्हें मजबूत स्वीकृति शर्तों के साथ कैसे निर्धारणीकृत किया जाए, और राबिन ने सिद्धांत को अनंत वृक्षों तक विस्तारित किया, ये परिणाम 1970 के दशक के अंत में अस्थायी तर्क के कंप्यूटर विज्ञान में प्रवेश करने के बाद सत्यापन के लिए केंद्रीय बन गए।

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

एक मशीन अनंत इनपुट को कैसे स्वीकार कर सकती है?

स्वीकृति अंत में अंतिम अवस्था तक पहुँचने से परिभाषित नहीं होती है, क्योंकि कोई अंत नहीं होता है, बल्कि इस बात से परिभाषित होती है कि कौन सी अवस्थाएँ बार-बार आती हैं। उदाहरण के लिए, एक बूची ऑटोमेटन तब स्वीकार करता है जब वह अपनी अंतहीन रन के दौरान एक निर्दिष्ट स्वीकृत अवस्था से अनंत बार गुजरता है।

ये ऑटोमेटा सत्यापन के लिए क्यों महत्वपूर्ण हैं?

ऑपरेटिंग सिस्टम और नेटवर्क प्रोटोकॉल जैसी गैर-समाप्त होने वाली प्रणालियों को स्वाभाविक रूप से अनंत व्यवहारों द्वारा मॉडल किया जाता है। 'सिस्टम कभी डेडलॉक नहीं होता' या 'प्रत्येक अनुरोध अंततः पूरा होता है' जैसे गुण ओमेगा-रेगुलर भाषाएँ बन जाते हैं, इसलिए उनकी जाँच ऑटोमेटा संचालन तक कम हो जाती है जिसे एक मॉडल चेकर स्वचालित रूप से कर सकता है।