Автомат Бюхи

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