Бюши автоматтары – автоматтар теориясының маңызды құралы. Детерминистік және недетерминистік түрлері бар, шексіз кірістерді қабылдау/қабылдамау үшін қолданылады.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Компьютерлік ғылым мен автоматтар теориясында детерминистік Бюхи автоматы – шексіз кірістерді қабылдайтын немесе қабылдамайтын теориялық машина. Мұндай машинаның күйлер жиынтығы және ауысу функциясы бар, ол келесі кіріс символын оқыған кезде машинаның ағымдағы күйінен қай күйге өту керектігін анықтайды. Кейбір күйлер қабылдаушы, ал біреуі бастапқы күй болып табылады. Машина кірісті қабылдайды, егер және тек қана ол кірісті оқыған кезде қабылдаушы күйден шексіз көп рет өтетін болса. Детерминистік емес Бюхи автоматы, кейіннен жай ғана Бюхи автоматы деп аталатын, ауысу функциясы бірнеше нәтижелер бере алады, соның салдарынан бір кіріс үшін көптеген мүмкін жолдар пайда болады; ол шексіз кірісті қабылдайды, егер және тек қана кейбір мүмкін жол қабылдаушы болса. Детерминистік және детерминистік емес Бюхи автоматтары детерминистік шекті автоматтар мен детерминистік емес шекті автоматтарды шексіз кірістерге дейін жалпылайды. Олардың әрқайсысы ω автоматтарының түрі. Бюхи автоматтары ω-тұрақты тілдерді таниды, бұл тұрақты тілдердің шексіз сөздерге арналған нұсқасы. Олар швейцариялық математик Юлиус Ричард Бюхидің құрметіне аталған, ол оларды 1962 жылы ойлап тапқан. Бюхи автоматтары көбінесе модельді тексеруде сызықтық уақыт логикасындағы формуланың автоматтар теориялық түрі ретінде қолданылады.
In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machine should move to from its current state when it reads the next input character. Some states are accepting states and one state is the start state. The machine accepts an input if and only if it will pass through an accepting state infinitely many times as it reads the input. A non deterministic Büchi automaton, later referred to just as a Büchi automaton, has a transition function which may have multiple outputs, leading to many possible paths for the same input; it accepts an infinite input if and only if some possible path is accepting. Deterministic and non deterministic Büchi automata generalize deterministic finite automata and nondeterministic finite automata to infinite inputs. Each are types of ω automata. Büchi automata recognize the ω regular languages, the infinite word version of regular languages. They are named after the Swiss mathematician Julius Richard Büchi, who invented them in 1962. Büchi automata are often used in model checking as an automata theoretic version of a formula in linear temporal logic.
Тануға болатын тілдер
Büchi автоматтары ω-тұрақты тілдерді таниды. ω-тұрақты тілдің анықтамасы мен Büchi автоматтарының жоғарыдағы жабылу қасиеттерін қолданып, кез келген ω-тұрақты тілді танитын Büchi автоматын құрастыру оңай екенін көрсетуге болады. Керісіне, Büchi автоматы үшін ω-тұрақты тілді құруға қараңыз.
Büchi automata recognize the ω regular languages. Using the definition of ω regular language and the above closure properties of Büchi automata, it can be easily shown that a Büchi automaton can be constructed such that it recognizes any given ω regular language. For converse, see construction of a ω regular language for a Büchi automaton.
Детерминистік және детерминистік емес Бючи автоматтары
Детерминистік Büchi автоматтары класы барлық омега-тұрақты тілдерді қамтуға жеткіліксіз. Атап айтқанда, 1 саны тек шекті ретте ғана кездесетін сөздерді қамтитын (0∪1)^* 0^ω тілін танитын детерминистік Büchi автоматы жоқ. Мұндай детерминистік Büchi автоматының жоқ екенін қайшылық арқылы дәлелдеуге болады. А – соңғы күйлер жиыны F болатын (0∪1)^* 0^ω тілін танитын детерминистік Büchi автоматы болсын. А, 0^ω сөзін қабылдайды. Демек, А, 0^ω сөзінің кейбір шекті префиксін оқығаннан кейін F жиынындағы бір күйге жетеді, мысалы, i-інші 0-дан кейін. А, ω сөзін де қабылдайды. Сондықтан, кейбір i үшін, префикстен кейін автомат F жиынындағы бір күйге жетеді. Осы құрылымды жалғастыра отырып, ω сөзі құрылады, бұл А-ның F жиынындағы бір күйге шексіз көп рет келуіне себеп болады, ал сөз (0∪1)^* 0^ω тіліне жатпайды. Қайшылық. Детерминистік Büchi автоматтарымен танылатын тілдер класы келесі леммамен сипатталады. Лемма: Егер ω тілі, кейбір тұрақты тілдің лимит тілі болса, онда ол детерминистік Büchi автоматымен танылады. Дәлел: Кез келген детерминистік Büchi автоматын А, детерминистік шекті автомат А' ретінде қарастыруға болады, және керісінше, өйткені автоматтың екі түрі де бірдей компоненттердің 5-тік түрі ретінде анықталады, тек қабылдау шартының интерпретациясы ғана әртүрлі. L(A) – L(A') лимит тілі екенін көрсетеміз. Егер ω сөзін А қабылдаса, онда ол А-ны соңғы күйге шексіз көп рет келуге мәжбүрлейді. Осылайша, осы ω сөзінің шексіз көп шекті префикстері А' арқылы қабылданады. Сондықтан L(A) – L(A') лимит тілі болады.
The class of deterministic Büchi automata does not suffice to encompass all omega regular languages. In particular, there is no deterministic Büchi automaton that recognizes the language (0\cup 1)^* 0^\omega, which contains exactly words in which 1 occurs only finitely many times. We can demonstrate it by contradiction that no such deterministic Büchi automaton exists. Let us suppose A is a deterministic Büchi automaton that recognizes (0\cup 1)^* 0^\omega with final state set F. A accepts 0^\omega. So, A will visit some state in F after reading some finite prefix of 0^\omega, say after the i {0} th letter. A also accepts the ω word Therefore, for some i {1} , after the prefix the automaton will visit some state in F. Continuing with this construction the ω word is generated which causes A to visit some state in F infinitely often and the word is not in (0\cup 1)^* 0^\omega. Contradiction. The class of languages recognizable by deterministic Büchi automata is characterized by the following lemma. Lemma: An ω language is recognizable by a deterministic Büchi automaton if it is the limit language of some regular language. Proof: Any deterministic Büchi automaton A can be viewed as a deterministic finite automaton A' and vice versa, since both types of automaton are defined as 5 tuple of the same components, only the interpretation of acceptance condition is different. We will show that L(A) is the limit language of L(A'). An ω word is accepted by A if it will force A to visit final states infinitely often. Thus, infinitely many finite prefixes of this ω word will be accepted by A'. Hence, L(A) is a limit language of L(A').