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 ∈ 2Q ∧ X ∩ B ≠ {\displaystyle \emptyset } }.
A partir do autômato de Rabin/ autômato de paridade
Similarmente, as condições de Rabin ( E j , F j ) {\displaystyle (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 2 Q {\displaystyle F\subseteq 2^{Q}} que satisfazem F E j = F F j {\displaystyle 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 ) {\displaystyle (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 2 Q {\displaystyle F\subseteq 2^{Q}} que satisfazem F E j = F F j = {\displaystyle 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