Autômato de Muller

Na teoria dos autômatos, um Autômato de Muller é um tipo de ω-autômato. A condição de aceitação separa o autômato de Muller de outros ω-autômatos. Os autômatos de Muller são definidos usando a condição de aceitação de Muller, i.e. o conjunto de todos os estados viditados infinitamente comuns devem ser um elemento do conjunto de aceitação. Os autômatos de Muller determinísticos e não determinísticos reconhecem as linguagens ω-regulares.

Definição formal

Formalmente, um autômato determinístico de Muller é uma tupla A = (Q,Σ,δ,q0,F) que consiste das seguintes informações:

• Q é um conjunto finito. Os elementos de Q são são chamados estados de Q.
• Σ é um conjunto finito chamado alfabeto de A.
• δ: Q × Σ → Q é uma função, chamada função de transação de A.
• q0 é um elemento de Q, chamado de estado inicial
• F é um conjunto de estados. Formalmente, F ⊆ P(Q) onde P(Q) é o conjunto das partes de Q. F define a condição de aceitação. A aceita exatamente o conjunto de infinitalidade geralmente ocorre estados de um elemento F.

Em um automato de Mulle não determinístico', a função de transação δ é substituída pela relação de transição Δ que retorna um conjunto de estados e o estado inicial q0 é substituído por um conjunto de estados iniciais Q0. De modo geral, autômato de Muller refere aos autômatos de Muller não determinísticos.

Para uma maior compreensão do formalismo veja ω-autômatos.

Equivalência com outros autômatos ω

Os autômatos de Muller são igualmente expressivos como autômatos de paridade, autômatos de Rabin, autômatos de Streett e autômatos de Büchi não determinísticos, para mencionar alguns, e estritamente mais expressivos que os autômatos de Büchi determinísticos. A equivalência do autômato acima e do autômato de Muller não determinístico pode ser visto muito facilmente como as condições de aceitação desses autômatos poderem ser simulados usando a condição de aceitação dos autômatos de Muller. O teorema de McNaughton's demonstra a equivalência do autômato de Büchi não determinísticos com o autômato de Muller determinístico. Assim, autômatos de Muller determinísticos e não determinísticos são equivalentes em termos das linguagens que eles aceitam.

Transformação para um autômato de Muller não determinísticos

Seguindo a lista de construção de autômatos que transformam um tipo de ω-autômato em um autômato de Muller não determinísticos.

A partir do autômato de Büchi

Se B é o conjunto de estados finais em um autômato de Büchi com o conjunto de estados Q, nós podemos construit um auômato de Muller com o mesmo conjunto de estados, funções de transição e estado inicial com condição de aceitação F = { X | X ∈ 2^Q ∧ X ∩ B ≠ $\emptyset$}.

A partir do autômato de Rabin/ autômato de paridade

Similarmente, as condições de Rabin $(E_{j},F_{j})$ podem ser simuladas pela construção do conjunto de aceitação em um autômato de Muller como todos os conjuntos em $F\subseteq 2^{Q}$ que satisfazem $F\cap E_{j}=\emptyset \land F\cap F_{j}\neq \emptyset$

, para algum j. Note que assim é também coberto o caso do autômato de paridade, como a condição de aceitação de paridade pode ser facilmente expressada como a condição de aceitação de Rabin.

A partir do autômato de Streett

A condição de Streett $(E_{j},F_{j})$ pode ser simulada pela construção de um conjunto de aceitação no autômato de Muller como todos os conjuntos $F\subseteq 2^{Q}$ que satisfazem $F\cap E_{j}=\emptyset \rightarrow F\cap F_{j}=\emptyset$ para todo j.

Transformação de um autômato de Muller determinístico

União de dois autômatos de Muller determinísticos

A partir do autômato de Büchi

O teorema de McNaughton fornece um procedimento para transformar um autômato não determinístico de Büchi em um autômato determinístico de Muller.

Referências

• Automata on Infinite Words Slides for a tutorial by Paritosh K. Pandya.
• Yde Venema (2008) Lectures on the Modal μ-calculus; the 2006 version was presented at The 18th European Summer School in Logic, Language and Information