Автомат Бюхи
Автомат Бюхи (англ. Büchi automaton) — это теоретическая машина, которая либо принимает, либо отвергает бесконечные входные данные. У такой машины есть набор состояний и функция перехода, которая определяет, в какое состояние машина должна перейти из текущего состояния при чтении со входа следующего символа. Некоторые состояния являются принимающими, а одно состояние — начальным. Машина принимает входные данные тогда и только тогда, когда она будет бесконечное количество раз проходить через принимающее состояние при чтении ввода.
![Автомат Бюхи](http://upload.wikimedia.org/wikipedia/commons/thumb/5/56/Automate_de_Buchi2.jpg/220px-Automate_de_Buchi2.jpg)
Недетерминированный автомат Бюхи, позже называемый просто автоматом Бюхи, имеет функцию перехода, которая может иметь несколько выходов, что приводит к множеству возможных путей для одного и того же ввода; он принимает бесконечный ввод тогда и только тогда, когда некоторый возможный путь является принимающим. Детерминированные и недетерминированные автоматы Бюхи обобщают детерминированные конечные автоматы и недетерминированные конечные автоматы на случай бесконечных входов. Оба являются видами ω-автоматов. Автоматы Бюхи распознают ω-регулярные языки, бесконечную версию регулярных языков. Они названы в честь швейцарского математика Юлиуса Ричарда Бюхи[англ.], который изобрел их в 1962 году.
Автоматы Бюхи часто используются при проверке моделей формулы в логике линейного времени.
Формальное определение
правитьАвтомат Бюхи (недетерменированный) — это кортеж (Q, Σ, T, I, F), где
- Q — конечное множество состояний.
- Σ — конечное множество, называемое алфавитом.
- T ⊂ Q × Σ × Q — отношение переходов.
- I ⊆ Q — начальные состояния, подмножество состояний.
- F⊆Q — конечные состояния.
Детерминированный автомат Бюхи представляет собой кортеж A = (Q, Σ, δ, q0, F), в котором отношение переходов становится функцией, а начальное состояние только одно:
- Q — конечное множество состояний.
- Σ — конечное множество, называемое алфавитом.
- δ: Q × Σ → Q — функция перехода.
- q0 — элемент множества 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.