В информатике и теории автоматов , детерминированный автомат Бюхи теоретический аппарат , который принимает или отклоняет бесконечные входы. Такая машина имеет набор состояний и функцию перехода, которая определяет, в какое состояние машина должна перейти из своего текущего состояния при чтении следующего входного символа. Некоторые состояния принимают состояния, и одно состояние является начальным. Машина принимает ввод тогда и только тогда, когда она будет проходить через состояние приема бесконечно много раз при чтении ввода.
Недетерминированная Бюхи автомат , далее по тексту просто как автомат Бюхи , имеет функцию перехода , которая может иметь несколько выходов, ведущую к многим возможным путям для того же вход; он принимает бесконечный ввод тогда и только тогда, когда принимает некоторый возможный путь. Детерминированные и недетерминированные автоматы Бюхи обобщают детерминированные конечные автоматы и недетерминированные конечные автоматы на бесконечные входы. Каждый из них является типом ω-автоматов . Автоматы Бюхи распознают ω-регулярные языки , бесконечнословную версию обычных языков . Они названы в честь швейцарского математика Юлиуса Рихарда Бючи , который изобрел их в 1962 году [1].
Автоматы Бюхи часто используются при проверке моделей как теоретико-автоматная версия формулы в линейной темпоральной логике .
Формальное определение
Формально детерминированный автомат Бюхи - это набор A = ( Q , Σ, δ, q 0 , F ), состоящий из следующих компонентов:
- Q - конечное множество . Элементы Q называются состояния из A .
- Σ конечное множество называется алфавит из A .
- δ: Q × Σ → Q является функцией, которая называется функцией перехода из A .
- д 0 является элементом Q , называется начальное состояние из A .
- F ⊆ Q - условие приемки . Принимает именно те пробеги , в которых по крайней мере один из бесконечно часто встречающихся состояний является в F .
В ( недетерминированном ) автомате Бюхи функция перехода δ заменяется отношением перехода Δ, которое возвращает набор состояний, а единственное начальное состояние q 0 заменяется набором I начальных состояний. Как правило, термин автомат Бюхи без квалификатора относится к недетерминированным автоматам Бюхи.
Для более полного формализма см. Также ω-автомат .
Свойства закрытия
Множество автоматов Бюхи замыкается при выполнении следующих операций.
Позволять а также быть автоматами Бюхи и - конечный автомат .
- Союз : есть автомат Бюхи, который распознает язык
- Доказательство: если предположить, что wlog , тогда пусто распознается автоматом Бюхи
- Пересечение : есть автомат Бюхи, который распознает язык
- Доказательство: автомат Бюхи. признает где
- По конструкции, является запуском автомата A 'по входному слову w, если выполняется из A на w и выполняется из B по w . принимает и принимается, если r 'является объединением бесконечной серии конечных сегментов 1-состояний (состояний с третьим компонентом 1) и 2-состояний (состояний с третьим компонентом 2) поочередно. Вот такая серия отрезков r ', если r' принимается A '.
- Конкатенация : есть автомат Бюхи, который распознает язык
- Доказательство: если предположить, что wlog , пусто, то автомат Бюхи признает , где
- ω-замыкание : если не содержит пустого слова, то существует автомат Бюхи, распознающий язык
- Доказательство: автомат Бюхи, распознающий строится в два этапа. Сначала построим конечный автомат A 'такой, что A' также распознает но нет входящих переходов в начальные состояния A '. Так, где Обратите внимание, что так как не содержит пустой строки. Во-вторых, мы построим автомат Бюхи A ", распознающий добавив петлю к исходному состоянию A '. Так, , где
- Дополнение : есть автомат Бюхи, который распознает язык.
- Доказательство: здесь представлено доказательство .
Узнаваемые языки
Автоматы Бюхи распознают ω-регулярные языки . Используя определение ω-регулярного языка и указанные выше свойства замыкания автоматов Бюхи, легко показать, что автомат Бюхи может быть построен так, что он распознает любой заданный ω-регулярный язык. Обратно, см. Построение ω-регулярного языка для автомата Бюхи.
Детерминированные и недетерминированные автоматы Бюхи
Класса детерминированных автоматов Бюхи недостаточно для охвата всех омега-регулярных языков. В частности, не существует детерминированного автомата Бюхи, распознающего язык, который содержит ровно слова, в которых 1 встречается только конечное число раз. Мы можем показать от противного, что такого детерминированного автомата Бюхи не существует. Предположим, что A - детерминированный автомат Бюхи, распознающийс конечным состоянием множества F . принимает. Итак, A посетит некоторое состояние в F после чтения некоторого конечного префикса, скажи после ое письмо. A также принимает ω-слово Поэтому для некоторых , после префикса автомат будет посетить какое - то состояние в F . Продолжая эту конструкцию, ω-словогенерируется, что заставляет A посещать какое-либо состояние в F бесконечно часто, и слово не находится в Противоречие.
Класс языков, распознаваемых детерминированными автоматами Бюхи, характеризуется следующей леммой.
- Лемма: ω-язык распознается детерминированным автоматом Бюхи, если он является предельным языком некоторого регулярного языка .
- Доказательство: любой детерминированный автомат Бюхи A можно рассматривать как детерминированный конечный автомат A ' и наоборот, поскольку оба типа автоматов определены как набор из пяти одинаковых компонентов, только интерпретация условия приемки различна. Мы покажем, что это предел языка . Ω-слово принимается A, если оно заставляет A посещать конечные состояния бесконечно часто. если бесконечно много конечных префиксов этого со-слова будет принимать А ' . Следовательно, это язык ограничения .
Алгоритмы
Проверка моделей систем с конечным числом состояний часто может быть преобразована в различные операции над автоматами Бюхи. Помимо операций замыкания, представленных выше, ниже приведены некоторые полезные операции для приложений автоматов Бюхи.
- Детерминизация
Поскольку детерминированные автоматы Бюхи строго менее выразительны, чем недетерминированные автоматы, не может быть алгоритма для детерминизации автоматов Бюхи. Но теорема Макнотона и конструкция Сафры предоставляют алгоритмы, которые могут переводить автомат Бюхи в детерминированный автомат Мюллера или детерминированный автомат Рабина . [2]
- Проверка пустоты
Язык, распознаваемый автоматом Бюхи, непустой тогда и только тогда, когда существует конечное состояние, которое одновременно достижимо из начального состояния и лежит в цикле.
Эффективный алгоритм, который может проверить пустоту автомата Бюхи:
- Рассмотрим автомат как ориентированный граф и разложим его на сильно связные компоненты (ССС).
- Выполните поиск (например, поиск в глубину ), чтобы определить, какие SCC достижимы из начального состояния.
- Проверьте, существует ли нетривиальный SCC, достижимый и содержащий конечное состояние.
Каждый из шагов этого алгоритма может быть выполнен за линейное время по размеру автомата, поэтому алгоритм явно оптимален.
- Минимизация
Алгоритм минимизации недетерминированного конечного автомата также правильно минимизирует автомат Бюхи. Алгоритм не гарантирует минимального количества автоматов Бюхи [ требуется пояснение ] . Однако алгоритмы минимизации детерминированного конечного автомата не работают для детерминированного автомата Бюхи.
Варианты
Переход от других моделей описания к недетерминированным автоматам Бюхи
Из обобщенных автоматов Бюхи (GBA)
- Множественные наборы состояний в состоянии приемки могут быть переведены в один набор состояний с помощью конструкции автомата, которая известна как «конструкция подсчета». Скажем, A = (Q, Σ, ∆, q 0 , {F 1 , ..., F n }) - это GBA, где F 1 , ..., F n - множества принимающих состояний, тогда эквивалентный автомат Бюхи есть A ' = (Q', Σ, ∆ ', q' 0 , F '), где
- Q '= Q × {1, ..., n}
- q ' 0 = (q 0 , 1)
- ∆ '= {((q, i), a, (q', j)) | (q, a, q ') ∈ ∆, и если q ∈ F i, то j = ((i + 1) mod n) else j = i}
- F '= F 1 × {1}
Из формулы линейной темпоральной логики
- Перевод с временной логикой формулы линейной обобщенным Бюх автоматом приведен здесь . А перевод от обобщенного автомата Бюхи к автомату Бюхи представлен выше.
От автоматов Мюллера
- Данный автомат Мюллера можно преобразовать в эквивалентный автомат Бюхи с помощью следующей конструкции автомата. Предположим, что A = (Q, Σ, ∆, Q 0 , {F 0 , ..., F n }) - автомат Мюллера, где F 0 , ..., F n - множества принимающих состояний. Эквивалентным автоматом Бюхи является A ' = (Q', Σ, ∆ ', Q 0 , F'), где
- Q '= Q ∪ ∪ n i = 0 {i} × F i × 2 F i
- ∆ '= ∆ ∪ ∆ 1 ∪ ∆ 2 , где
- ∆ 1 = {(q, a, (i, q ', ∅)) | (q, a, q ') ∈ ∆ и q' ∈ F i }
- ∆ 2 = {((i, q, R), a, (i, q ', R')) | (q, a, q ') ∈∆ и q, q' ∈ F i, и если R = F i, то R '= ∅, иначе R' = R∪ {q}}
- F '= ∪ n i = 0 {i} × F i × {F i }
- A ' сохраняет исходный набор состояний из A и добавляет к ним дополнительные состояния. Автомат Бюхи A ' моделирует автомат Мюллера A следующим образом: в начале входного слова выполнение A' следует за выполнением A , так как начальные состояния такие же и ∆ 'содержит ∆. В некоторой недетерминированно выбранной позиции во входном слове A ' решает перейти в новые добавленные состояния через переход в ∆ 1 . Тогда переходы в Δ 2 раза посетить все штаты F я и продолжают расти R . Как только R становится равным F i, он сбрасывается в пустой набор, и ∆ 2 пытается снова и снова посещать все состояния состояний F i . Итак, если состояния R = F i посещаются бесконечно часто, то A ' принимает соответствующий ввод, и A тоже . Эта конструкция близко следует первой части доказательства теоремы Макнотона .
Из структур Крипке
- Пусть данная структура Крипке определяется M = ⟨ Q , I , R , L , А.П. ⟩ , где Q представляет собой набор состояний, я есть множество начальных состояний, R представляет собой отношение между двумя состояниями , также интерпретируются как ребра, L это метка для государства и AP является множеством атомарных предложений , которые образуют L .
- Автомат Бюхи будет иметь следующие характеристики:
- если ( q , p ) принадлежит R и L ( p ) = a
- и инициализация q, если q принадлежит I и L ( q ) = a .
- Заметим, однако, что существует разница в интерпретации между структурами Крипке и автоматами Бюхи. В то время как в первом случае явно указывается полярность каждой переменной состояния для каждого состояния, во втором просто объявляется текущий набор переменных, имеющих или не поддерживающих истину. Он абсолютно ничего не говорит о других переменных, которые могут присутствовать в модели.
Рекомендации
- ^ Бюхи, JR (1962). «О методе решения в ограниченной арифметике второго порядка». Proc. Международный конгресс по логике, методу и философии науки. 1960 . Стэнфорд: Издательство Стэнфордского университета: 425–435. DOI : 10.1007 / 978-1-4613-8928-6_23 . ISBN 978-1-4613-8930-9.
- ^ Сафра, С. (1988), «О сложности ω-автоматов», Труды 29-го ежегодного симпозиума по основам компьютерных наук (FOCS '88) , Вашингтон, округ Колумбия, США: IEEE Computer Society, стр. 319–327, DOI : 10,1109 / SFCS.1988.21948 , S2CID 206559211.
- Бахадыр Хусаинов; Анил Нероде (6 декабря 2012 г.). Теория автоматов и ее приложения . Springer Science & Business Media. ISBN 978-1-4612-0171-7.
- Томас, Вольфганг (1990). «Автоматы на бесконечных объектах». В Ван Леувен (ред.). Справочник по теоретической информатике . Эльзевир. С. 133–164.
Внешние ссылки
- «Конечные автоматы на бесконечных входах» (PDF) . Цитировать журнал требует
|journal=
( помощь ) - Варди, Моше Ю. "Теоретико-автоматный подход к линейной темпоральной логике". CiteSeerX 10.1.1.125.8126 . Цитировать журнал требует
|journal=
( помощь )