Teorema de McNaughton

Em teoria dos autômatos, o teorema de McNaughton refere-se a um teorema que afirma que o conjunto de linguagens ω-regulares é idêntico ao conjunto de linguagens reconhecíveis por autômatos de Muller determinísticos. Este teorema é provado através do fornecimento de um algoritmo para construir um autômato de Muller determinístico para qualquer linguagem ω-regular e vice-versa.

Este teorema tem muitas consequências importantes. Tendo em vista que autômatos de Büchi e linguagens ω-regulares, são expressivos igualmente, o teorema implica que autômatos de Büchi e autômatos de Muller determinísticos também são expressivos igualmente. Visto que a complementação de autômatos de Muller determinísticos é trivial, o teorema implica que autômatos de Büchi/linguagens ω-regulares são fechados sob complementação.

Declaração original

No artigo original de McNaughton, o teorema foi apresentado como:

"Um evento-ω é regular se e somente se tem estados finitos."

Na terminologia moderna,eventos-ω são comumente referidos como linguagens-ω. Seguindo a definição de McNaughton, um evento-ω é um evento de estados finitos se existe um autômato de Muller determinístico que o reconheça.

Construindo uma linguagem ω-regular a partir de uma autômato de Muller determinístico

Uma direção do teorema pode ser provada, mostrando que qualquer autômato de Muller reconhece uma linguagem ω-regular.

Suponha que A = (Q,Σ,δ,q₀,F) é um autômato de Muller determinístico. A união de um número finito de linguagens ω-regulares produz uma linguagem ω-regular, portanto, pode-se assumir sem perda de generalidade que a condição aceitação F do autômato de Muller contém exatamente um conjunto de estados {q₁, ... ,q_n}. Sendo α a linguagem regular em que seus elementos levarão A de q₀ para q₁. Para 1≤i≤n, seja β_i uma linguagem regular cujos elementos levam A de q_i para q_{(i mod n)+1} sem passar por nenhum estado fora de {q₁, ... ,q_n}. Alega-se que α(β₁ ... β_n)^ω é a linguagem ω-regular reconhecida pelo autômato de Muller A. Está provado como segue.

Suponha que w é uma palavra aceita por A. Seja ρ a execução que levou a aceitação de w. Num instante de tempo t, considere que ρ(t) é um estado visitado por ρ num instante t. Nós criamos uma sequência infinita e estritamente crescente de instantes t₁, t₂, ... em que para cada a e b, ρ(t_na+b) = q_b. Tal sequência existe porque todos os estados {q₁, ... ,q_n} aparecem em ρ infinitas vezes. Através das definições anteriores de α e ß's, pode ser facilmente mostrado que a existência de uma tal sequência implica que w é um elemento de α(β₁ ... β_n)^ω.

Suponha que w ∈ α(β₁ ... β_n)^ω. Pela definição de α, existe um segmento inicial de w que é um elemento de α e conduz A ao estado q₁. A partir daí, a execução nunca assume um estado fora de {q₁, ... ,q_n}, devido às definições dos ß's, e todos os estados no conjunto são infinitamente repetidos. Portanto, A aceita a palavra w.

Construindo um autômato de Muller determinístico a partir de uma dada linguagem ω-regular

A outra direção do teorema pode ser provada, mostrando que existe um autômato de Muller que reconhece uma determinada linguagem ω-regular.

A união de um número finito de autômatos de Muller determinísticos pode ser facilmente construída, portanto, sem perda de generalidade, vamos assumir que a linguagem ω-regular dada é da forma αβ^ω. Vamos supor a palavra-ω w=a₁,a₂,... ∈ αβ^ω. Seja w(i,j) o segmento finito a_i+1,...,a_j-1,a_j de w. Para a construção de um autômato de Muller para αβ^ω, apresentamos os dois conceitos seguintes com relação a w.

Favor

Um momento j favorece um momento i se j > i, w(0,i) ∈ αβ*, e w(i,j) ∈ β*.

Equivalência

E(i,j,k), ou i é equivalente a j como julgado no momento k se i,j ≤ k, w(0,i) ∈ αβ*,w(0,j) ∈ αβ*, e para cada palavra x Σ*, w(i,k)x ∈ β* sse w(j,k)x ∈ β*. É fácil notar que se E(i,j,k) então para todo k < l, E(i,j,l). Em outras palavras, se i e j são considerados equivalentes, então eles continuarão equivalentes posteriormente. E também para o mesmo l, l favorece i sse l favorece j. Seja E(i,j) se existe um k tal que E(i,j,k).

Seja p o número de estados do menor autômato finito determinístico A^β* para reconhecer a linguagem ß*. Agora vamos provar dois lemas sobre os dois conceitos acima.

Lema 1

Para qualquer momento k, entre os momentos i, j < k tal que w (0, i) e w(0,j) ∈ αβ*, o número de classes de equivalência induzidas por E(i,j,k) é delimitada por p. O número de classes de equivalência induzidas por E(i,j) também é delimitada por p.

Prova:O autômato finito A^ß* é mínimo, portanto, não contêm estados equivalentes. Seja i e j be tal que w(0,i) e w(0,j) ∈ αβ* e E(i,j,k). Então, as palavras w(i,k) e w(j,k) terão que levar A^ß* para o mesmo estado, iniciando a partir do estado inicial. Portanto, primeira parte do lema é verdadeira. A segunda parte é provada por contradição. Vamos supor que existem p+1 momentos i₁,...,i_p+1 de tal forma que não existem dois deles que são equivalentes. Para l > max(i₁,...,i_p+1), teríamos, para cada m e n, não-E(i_m,i_n,l). Portanto, existiriam p+1 classes de equivalência, como julgado em l, contradizendo a primeira parte do lema.

Lema 2

w ∈ αβ^ω sse existe um momento i tal qual existe um número infinito de momentos equivalentes a i e favorecendo i.

Prova: Vamos supor que w ∈ αβ^ω, então existe uma sequência estritamente crescente de momentos i₀,i₁,i₂,... em que w(0,i₀) ∈ α e w(i_n,i_n+1) ∈ β. Então, para todo n > m, w(i_m,i_n) ∈ β* e i_n favorece i_m. Então, todos os i's são membros de uma das finitas classes de equivalência (mostradas no Lema 1). Assim, deve haver um subconjunto infinito de todos os i's que pertencem a mesma classe. O menor membro deste subconjunto satisfaz o lado direito deste lema.

Por outro lado, suponha que em w, há um número infinito de momentos que são equivalentes a i e favorecem i. A partir desses momentos, nós vamos construir uma sequência estritamente crescente e infinita de momentos i₀,i₁,i₂, em que w(0,i₀) ∈ αβ* e w(i_n,i_n+1) ∈ β*. Logo, w estaria em αβ^ω. Essa sequência é definida por indução:

Caso Base: w(0,i) ∈ αβ* porque i está em uma classe de equivalência. Então, montamos i₀=i. Nós montamos i₁ de forma que i₁ favoreça i₀ e E(i₀,i₁). Então w(i₀,i₁) ∈ β*.

Passo indutivo: Vamos supor E(i₀,i_n). Então, existe um momento i' em que E(i₀,i_n,i'). Nós montamos i_n+1 de forma que i_n+1 > i', i_n+1 favoreça i₀, e E(i₀,i_n+1). Então, w(i₀,i_n+1) ∈ β* e, visto que i_n+1 > i' nós temos por definição de E(i₀,i_n,i'), w(i_n,i_n+1) ∈ β*.

Construção do autômato de Muller

Usamos os conceitos de "favor" e "equivalência no lema 2. Agora, nós usaremos o lema para a construção de um autômato de Muller para a linguagem αβ^ω. O autômato proposto aceitará uma palavra sse exista um momento i que satisfará o lado direito do lema 2. A máquina abaixo é descrita informalmente. Note que essa máquina será um autômato de Muller determinístico.

A máquina contém p+2 autômatos finitos determinísticos e um controlador mestre, onde p é o tamanho de αβ^ω. Uma das p+2 máquinas pode reconhecer aß* e esta máquina recebe uma entrada a cada ciclo. E, ela comunica em qualquer momento i para o controlador mestre se w(0,i) ∈ αβ*. O resto das p+1 máquinas são cópias um A^ß*. O mestre pode definir as máquinas A^ß* como inativas ou ativas. Se o mestre define uma máquina A^ß* como inativa ela permanece em seu estado inicial e se torna alheia a entrada. Se o mestre ativa uma máquina A^ß* ela então lê a entrada e se move, até que o mestre a torne inativa e a force de volta ao estado inicial. O mestre pode tornar uma máquina A^ß* ativa ou inativa quantas vezes quiser. O mestre guarda as seguintes informações sobre as máquinas A^ß* a cada instante.

• Estados atuais das máquinas A^ß*,
• Lista das máquinas A^ß* ativas por ordem de momento de ativação.
• Para cada máquina A^ß* M ativa, o conjunto das outras máquinas A^ß* ativas que estavam em um estado de aceitação no momento da ativação de M. Em outras palavras, se uma máquina é ativada na ocasião i e algumas outras máquinas foram ativadas na ocasião j < i e continuam ativos até i, então o mestre mantém o registro se i favorece j ou não. Este registro é descartado se a outra máquina entra em estado inativo antes de M.

Inicialmente, o mestre pode se comportar de duas maneiras diferentes, dependendo de a. Se a contém uma palavra vazia então, apenas uma das máquinas A^ß* está ativa, caso contrário, nenhuma das máquinas A^ß* estão ativas no início. Mais tarde, em algum momento i, se w(0,i) ∈ αβ* e nenhuma das máquinas A^ß* estão no estado inicial, então o mestre ativa uma das máquinas inativas e a máquina A^ß* que foi ativada começa a receber a entrada a partir do momento i + 1. Em algum momento, se duas máquinas A^ß* chegarem ao mesmo estado, o mestre inativa a máquina que foi ativada por último. Note que o mestre pode tomar as decisões acima usando as informações que ele armazena.

Para a saída, o mestre também tem um par de luzes vermelhas e verdes correspondente a cada uma das máquinas A^ß*. Se uma máquina A^ß* vai do estado ativo para o estado inativo, a correspondente luz vermelha pisca. A luz verde de uma A máquina A^ß* M, que foi ativada em j, pisca no momento i nas duas situações seguintes:

• M está em estado inicial, portanto, E (j, i, i) e i favorece j(o estado inicial tem que ser um estado de aceitação).
• Para alguma outra máquina A^ß* M' ativada em k, onde j <k <i, k favorece j (o mestre tem registro disso) e i é o primeiro momento em que E (j, k, i) (M' entra em estado inativo no momento i).

Note que a luz verde para a M não pisca toda vez que uma máquina entra em estado inativo devido a M.

Lema 3

Se existe um momento equivalente a um número infinito de momentos que favorecem ele e i é o mais antigo desses momentos, então uma máquina A^ß* M é ativada em i, se mantendo sempre ativa (sem flash de luz vermelha correspondente depois disso), e faz a luz verde piscar infinitas vezes.

Prova Vamos supor que uma máquina A^ß* foi ativada no momento j tal que j < i e esta máquina vai para o estado inicial no tempo i. Portanto, se a qualquer momento é equivalente e favorece i então esse momento deve ter a mesma relação com j. Isto contradiz a hipótese de que i é o primeiro momento de um número infinito de momentos equivalente ao i e favorecendo i. Assim, no momento i, nenhuma máquina ativa pode estar no estado inicial. Daí, o mestre tem que ativar uma nova máquina A^ß* no momento i, que é a nossa M. Essa máquina nunca vai ficar inativa porque se alguma outra máquina, que foi ativada no momento l, a torna inativa no momento k então E (l, i, k). Mais uma vez, a mesma contradição está implícita. Pela construção e devido a um número infinito de momentos equivalentes a i e favorecendo i, a luz verde irá piscar infinitas vezes.

Lema 4

Por outro lado, se há uma máquina A^ß* M, cuja luz verde piscou em infinitos momentos e luz vermelha apenas em finitos momentos, então, há um número infinito de momentos equivalente a e favorecendo a última vez em que M se tornou ativa.

Prova: Verdade por construção.

Lema 5

w ∈ αβ^ω sse, para alguma máquina A^ß*, a luz verde pisca em infinitos momentos e a luz vermelha pisca somente em finitos momentos.

Prova: Devido ao lema 2-4.

A descrição anterior de uma máquina completa pode ser visualizada como um grande autômato determinístico. Agora, só precisa definir a condição de aceitação de Muller. Neste grande autômato, definimos µ_n para ser o conjunto de estados em que a de luz verde pisca e a luz vermelha não pisca correspondente a máquina n^th A^ß*. Sendo ν_n o conjunto de estados em que a luz vermelha não pisca correspondente a n-ésima máquina A^{ß*. Então a condição de aceitação de Muller é F = { S | ∃n μ_n ⊆ S ⊆ ν_n }. Isso termina a construção do autômato de Muller desejado. C.Q.D.}

Outras provas

Desde a prova de McNaughton, várias outras provas foram propostas. A seguir, algumas delas.

• Uma linguagem ω-regular pode ser mostrada equiv-expressiva a um autômatos de Büchi. Autômatos de Büchi podem ser mostrados equiv-expressivos a autômatos de Büchi semi-determinísticos. Um autômato de Büchi semi-determinístico pode ser mostrado equiv-expressivo a um autômato de Muller determinístico. Esta prova segue as mesmas linhas que a prova acima.
• A construção de Safra transforma um autômato de Büchi não-determinístico em um autômato de Muller. Esta construção é considerada ótima.
• Existe uma prova puramente algébrica para o teorema de McNaughton.