Автомат Бюхи

Автомат Бюхи с двумя состояниями, q₀ и q₁, где первое состояние q₀ является начальным, а второе состояние q₁ — принимающим. Входные данные представляют собой бесконечные слова над символами $\{a,b\}$. В качестве примера, он принимает бесконечное слово $(ab)^{\omega }$, где $x^{\omega }$ обозначает бесконечное повторение строки. Автомат отвергает бесконечное слово $aaab^{\omega }$.

Автомат Бюхи (англ. 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).

Литература

• 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.