Автомат Мюллера - Muller automaton

В теории автоматов , автомат Мюллера представляет собой тип из со-автомата . Условие приемки отделяет автомат Мюллера от других ω-автоматов. Автомат Мюллера определяется с помощью условия приемлемости Мюллера , т. Е. Множество всех состояний, которые посещаются бесконечно часто, должно быть элементом приемочного множества. И детерминированные, и недетерминированные автоматы Мюллера распознают ω-регулярные языки . Они названы в честь Дэвида Э. Мюллера , американского математика и компьютерного ученого , который изобрел их в 1963 году.

Формальное определение

Формально детерминированный автомат Мюллера - это набор A  = ( Q , Σ, δ, q ₀ , F ), состоящий из следующей информации:

• Q - конечное множество . Элементы Q называются состояния из A .
• Σ конечное множество называется алфавит из A .
• δ:  Q  × Σ →  Q является функцией, которая называется функцией перехода из A .
• q ₀ - элемент Q , называемый начальным состоянием.
• F - это набор наборов состояний. Формально, F ⊆ P ( Q ) , где Р ( Q ) является Powerset из Q . F определяет условие приемки . A принимает именно те прогоны, в которых множество бесконечно часто встречающихся состояний является элементом  F

В недетерминированном автомате Мюллера функция перехода δ заменяется отношением перехода Δ, которое возвращает набор состояний, а начальное состояние q ₀ заменяется набором начальных состояний Q ₀ . Обычно автомат Мюллера относится к недетерминированному автомату Мюллера.

Для более полного формализма взгляните на ω-автомат .

Эквивалентность другим ω-автоматам

Эти автоматы Мюллера в равной степени выразительные , как четности автоматы , Рабин автоматы , Streett автоматы и недетерминированными Бюхи автоматы , упомянуть некоторые, и строго более выразительные , чем детерминированный автомат Бюхи. Эквивалентность вышеупомянутых автоматов и недетерминированных автоматов Мюллера может быть продемонстрирована очень легко, поскольку условия принятия этих автоматов могут быть эмулированы с использованием условия принятия автоматов Мюллера. Теорема Макнотона демонстрирует эквивалентность недетерминированного автомата Бюхи и детерминированного автомата Мюллера. Таким образом, детерминированный и недетерминированный автомат Мюллера эквивалентны в терминах языков, которые они могут принимать.

Преобразование к недетерминированному автомату Мюллера

Ниже приводится список автоматных конструкций, которые преобразуют тип ω-автоматов в недетерминированный автомат Мюллера.

От Büchi automaton

Если - набор конечных состояний в автомате Бюхи с набором состояний , мы можем построить автомат Мюллера с тем же набором состояний, функцией перехода и начальным состоянием с условием принятия Мюллера как F = {X | X ∈ 2 ^Q ∧ X ∩ B ≠ }${\ displaystyle B}$${\ displaystyle Q}$${\ displaystyle \ emptyset}$

Из автомата Рабина / Автомат четности

Точно так же условия Рабина могут быть эмулированы путем построения приемлемого множества в автоматах Мюллера, поскольку все множества, которым удовлетворяют , для некоторого j. Обратите внимание, что это также относится и к случаю автомата контроля четности, поскольку условие принятия четности может быть легко выражено как условие принятия Рабина.${\ displaystyle (E_ {j}, F_ {j})}$${\ Displaystyle F \ substeq 2 ^ {Q}}$${\ Displaystyle F \ cap E_ {j} = \ emptyset \ land F \ cap F_ {j} \ neq \ emptyset}$

Из автомата Streett

Условия Стритта могут быть эмулированы путем построения набора приемлемости в автоматах Мюллера, так как все наборы, которым удовлетворяют , для всех j.${\ displaystyle (E_ {j}, F_ {j})}$${\ Displaystyle F \ substeq 2 ^ {Q}}$${\ Displaystyle F \ cap E_ {j} = \ emptyset \ rightarrow F \ cap F_ {j} = \ emptyset}$

Преобразование к детерминированному автомату Мюллера

Объединение двух детерминированных автоматов Мюллера

От Büchi automaton

Теорема Макнотона предоставляет процедуру преобразования недетерминированного автомата Бюхи в детерминированный автомат Мюллера.

Рекомендации

• Слайды « Автоматы на бесконечных словах» для учебника Паритоша К. Пандьи.
• Иде Венема (2008) Лекции по модальному μ-исчислению ; версия 2006 была представлена на 18 - й Европейской летней школы в Logic, языка и информации