Введение

В информатике и теории автоматов детерминированный автомат Бюхи – это теоретическая машина, которая принимает или отвергает бесконечные входные последовательности. Такая машина имеет набор состояний и функцию перехода, определяющую, в какое состояние машина переходит из текущего при чтении следующего входного символа. Некоторые состояния являются принимающими, а одно из них – начальным. Машина принимает входную последовательность тогда и только тогда, когда она проходит через принимающее состояние бесконечное число раз в процессе чтения входных данных. Недетерминированный автомат Бюхи, далее именуемый просто автоматом Бюхи, имеет функцию перехода, которая может иметь несколько выходных значений, что приводит к множеству возможных путей для одной и той же входной последовательности; он принимает бесконечную входную последовательность, если и только если хотя бы один из возможных путей является принимающим. Детерминированные и недетерминированные автоматы Бюхи обобщают детерминированные конечные автоматы и недетерминированные конечные автоматы для бесконечных входных последовательностей. Каждый из них является типом ω-автомата. Автоматы Бюхи распознают ω-регулярные языки, бесконечную версию регулярных языков. Они названы в честь швейцарского математика Юлиуса Ричарда Бюхи, который изобрел их в 1962 году. Автоматы Бюхи часто используются в верификации моделей как автоматическое представление формулы в линейной темпоральной логике.

Признаваемые языки

Автоматы Бюхи распознают ω-регулярные языки. Используя определение ω-регулярного языка и вышеуказанные свойства замкнутости автоматов Бюхи, можно легко показать, что можно построить автомат Бюхи, распознающий любой заданный ω-регулярный язык. Для доказательства обратного утверждения, обратитесь к построению ω-регулярного языка для автомата Бюхи.

Детерминированные и недетерминированные автоматики Бючи

Класс детерминированных автоматов Бюхи не позволяет охватить все омега-регулярные языки. В частности, не существует детерминированного автомата Бюхи, распознающего язык (0 ∪ 1)^* 0^ω, который содержит ровно те слова, в которых 1 встречается лишь конечное число раз. Мы можем доказать это от противного, показав, что такого детерминированного автомата Бюхи не существует. Пусть A – детерминированный автомат Бюхи, распознающий (0 ∪ 1)^* 0^ω, с множеством конечных состояний F. A принимает 0^ω. Следовательно, A посетит некоторое состояние из F после прочтения конечного префикса 0^ω, скажем, после i-го нуля. A также принимает ω-слово. Таким образом, для некоторого i, после префикса автомат посетит некоторое состояние из F. Продолжая эту конструкцию, мы получим ω-слово, которое заставит A бесконечно часто посещать некоторое состояние из F, и это слово не принадлежит (0 ∪ 1)^* 0^ω. Противоречие. Класс языков, распознаваемых детерминированными автоматами Бюхи, характеризуется следующей леммой. Лемма: Омега-язык распознается детерминированным автоматом Бюхи, если он является предельным языком некоторого регулярного языка. Доказательство: Любой детерминированный автомат Бюхи A можно рассматривать как детерминированный конечный автомат A', и наоборот, поскольку оба типа автоматов определены как 5-кортежи из одних и тех же компонентов, различаясь лишь интерпретацией условия принятия. Мы покажем, что L(A) является предельным языком L(A'). Ω-слово принимается A, если оно заставляет A бесконечно часто посещать конечные состояния. Следовательно, бесконечно много конечных префиксов этого ω-слова будут приняты A'. Таким образом, L(A) является предельным языком L(A').