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