Автомат Бюхи

Автомат Бюхи (англ. Büchi automaton) — это теоретическая машина, которая либо принимает, либо отвергает бесконечные входные данные. У такой машины есть набор состояний и функция перехода, которая определяет, в какое состояние машина должна перейти из текущего состояния при чтении со входа следующего символа. Некоторые состояния являются принимающими, а одно состояние — начальным. Машина принимает входные данные тогда и только тогда, когда она будет бесконечное количество раз проходить через принимающее состояние при чтении ввода.

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

Автоматы Бюхи часто используются при проверке моделей формулы в логике линейного времени.

Автомат Бюхи (недетерменированный) — это кортеж (Q, Σ, T, I, F), где

• Q — конечное множество состояний.
• Σ — конечное множество, называемое алфавитом.
• T ⊂ Q × Σ × Q — отношение переходов.
• I ⊆ Q — начальные состояния, подмножество состояний.
• F⊆Q — конечные состояния.

Детерминированный автомат Бюхи представляет собой кортеж A = (Q, Σ, δ, q₀, F), в котором отношение переходов становится функцией, а начальное состояние только одно:

• Q — конечное множество состояний.
• Σ — конечное множество, называемое алфавитом.
• δ: Q × Σ → Q — функция перехода.
• q₀ — элемент множества Q, называемый начальным состоянием.
• F⊆Q — условие принятия. Aвтомат A принимает ровно те запуски, в которых хотя бы одно из бесконечно часто встречающихся состояний находится в F.

Хотя определение автомата Бюхи не отличается определением конечного автомата, главным отличием является то, что автоматы Бюхи работают с бесконечными строками, тогда как конечные автоматы — со строками конечной длины.

Множество автоматов Бюхи замкнуто для следующих операций.

Пусть A и B — автоматы Бюхи, а C — конечный автомат. Через L(X) обозначим язык, который этот автомат распознаёт.

Существует автомат Бюхи, распознающий язык L(A) ∪ L(B).

Существует автомат Бюхи, распознающий язык L(A) ∩ L(B).

Cуществует автомат Бюхи, распознающий язык L(C) ⋅ L(A).

Если L(C) не содержит пустого слова, то существует автомат Бюхи, который распознаёт язык L(C)^ω.

Существует автомат Бюхи, распознающий язык Σ^ω/L(A).

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

Класс детерминированных автоматов Бюхи не охватывает все ω-регулярные языки. В частности, не существует детерминированного автомата Бюхи, распознающего язык ${\displaystyle (0\cup 1)^{*}0^{\omega }}$, состоящий из всех слов, в которых символ «1» встречается лишь конечное число раз.

Это можно показать от противного. Пусть A — детерминированный автомат Бюхи, распознающий ${\displaystyle (0\cup 1)^{*}0^{\omega }}$ с множеством принимающих состояний F. Автомат A принимает ${\displaystyle 0^{\omega }}$. Значит, после чтения некоторого конечного префикса ${\displaystyle 0^{\omega }}$, скажем, после ${\displaystyle i_{0}}$-го символа, A посетит состояние из F. Тогда A также примет слово ${\displaystyle 0^{i_{0}}10^{\omega }}$. Следовательно, для некоторого ${\displaystyle i_{1}}$ после префикса ${\displaystyle 0^{i_{0}}10^{i_{1}}}$ автомат снова посетит состояние из F. Продолжая это построение, мы получаем ω-слово ${\displaystyle 0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots }$, при чтении которого автомат будет бесконечно часто посещать состояния из F. Однако это слово не принадлежит языку ${\displaystyle (0\cup 1)^{*}0^{\omega }}$. Противоречие.

Класс языков, распознаваемых детерминированными автоматами Бюхи, характеризуется следующей леммой:

Лемма. Ω-язык распознаётся детерминированным автоматом Бюхи тогда и только тогда, когда он является предельным языком некоторого регулярного языка.

Доказательство. Любой детерминированный автомат Бюхи A можно рассматривать как детерминированный конечный автомат A' и наоборот, так как оба вида автоматов задаются одной и той же пятёркой множеств и функций, различается лишь условие приёма. Покажем, что ${\displaystyle L(A)}$ является предельным языком для ${\displaystyle L(A')}$. Ω-слово принимается автоматом A тогда и только тогда, когда оно заставляет A бесконечно часто посещать принимающие состояния. Следовательно, бесконечно много конечных префиксов этого ω-слова принимаются автоматом A' . Таким образом, ${\displaystyle L(A)}$ является предельным языком для ${\displaystyle L(A')}$.

• Bakhadyr Khoussainov. Automata Theory and its Applications / Bakhadyr Khoussainov, Anil Nerode. — Springer Science & Business Media, 6 December 2012. — ISBN 978-1-4612-0171-7.
• Automata on infinite objects // Handbook of Theoretical Computer Science. — Elsevier, 1990. — P. 133–164.