В теории автоматов , автомат Мюллера представляет собой тип из со-автомата . Условие приемки отделяет автомат Мюллера от других ω-автоматов. Автомат Мюллера определяется с помощью условия приемлемости Мюллера , т.е. множество всех состояний, которые посещаются бесконечно часто, должно быть элементом множества приемок. И детерминированные, и недетерминированные автоматы Мюллера распознают ω-регулярные языки . Они названы в честь Дэвида Э. Мюллера , американского математика и компьютерного ученого , который изобрел их в 1963 году [1].
Формальное определение
Формально детерминированный автомат Мюллера - это набор A = ( Q , Σ, δ, q 0 , F ), состоящий из следующей информации:
- Q - конечное множество . Элементы Q называются состояния из A .
- Σ конечное множество называется алфавит из A .
- δ: Q × Σ → Q является функцией, которая называется функцией перехода из A .
- q 0 - элемент Q , называемый начальным состоянием.
- F - это набор наборов состояний. Формально, F ⊆ P ( Q ) , где Р ( Q ) является Powerset из Q . F определяет условие приемки . A принимает именно те прогоны, в которых множество бесконечно часто встречающихся состояний является элементом F
В недетерминированном автомате Мюллера функция перехода δ заменяется отношением перехода Δ, которое возвращает набор состояний, а начальное состояние q 0 заменяется набором начальных состояний Q 0 . Обычно автомат Мюллера относится к недетерминированному автомату Мюллера.
Для более полного формализма взгляните на ω-автомат .
Эквивалентность другим ω-автоматам
Эти автоматы Мюллера в равной степени выразительные , как четности автоматы , Рабин автоматы , Streett автоматы и недетерминированными Бюхи автоматы , упомянуть некоторые, и строго более выразительные , чем детерминированный автомат Бюхи. Эквивалентность вышеупомянутых автоматов и недетерминированных автоматов Мюллера может быть очень легко продемонстрирована, поскольку условия принятия этих автоматов могут быть эмулированы с использованием условия принятия автоматов Мюллера. Теорема Макнотона демонстрирует эквивалентность недетерминированного автомата Бюхи и детерминированного автомата Мюллера. Таким образом, детерминированный и недетерминированный автомат Мюллера эквивалентны в терминах языков, которые они могут принимать.
Преобразование к недетерминированному автомату Мюллера
Ниже приводится список автоматных конструкций, которые преобразуют тип ω-автоматов в недетерминированный автомат Мюллера.
- От Büchi automaton
- Если - множество конечных состояний в автомате Бюхи с множеством состояний , мы можем построить автомат Мюллера с тем же набором состояний, функцией перехода и начальным состоянием с условием принятия Мюллера как F = {X | X ∈ 2 Q ∧ X ∩ B ≠ }
- Из автомата Рабина / Автомат четности
- Аналогично условия Рабина можно смоделировать, построив приемочное множество в автоматах Мюллера, поскольку все множества в которые удовлетворяют , для некоторых j. Обратите внимание, что это также относится и к случаю автомата контроля четности, поскольку условие принятия четности может быть легко выражено как условие принятия Рабина.
- Из автомата Streett
- Условия Streett можно смоделировать, построив приемочное множество в автоматах Мюллера, поскольку все множества в которые удовлетворяют , для всех j.
Преобразование к детерминированному автомату Мюллера
- Объединение двух детерминированных автоматов Мюллера
- От Büchi automaton
Теорема Макнотона предоставляет процедуру преобразования недетерминированного автомата Бюхи в детерминированный автомат Мюллера.
Рекомендации
- ^ Мюллер, Дэвид Э. (1963). «Бесконечные последовательности и конечные машины». 4-й ежегодный симпозиум по теории коммутационных цепей и логическому проектированию (SWCT) : 3–16.
- Слайды « Автоматы на бесконечных словах» для учебного пособия Паритоша К. Пандьи.
- Иде Венема (2008) Лекции по модальному μ-исчислению ; версия 2006 была представлена на 18 - й Европейской летней школы в Logic, языка и информации