# 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:
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$_0$,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$_1$, ... ,q$_n$}. Sendo α a linguagem regular em que seus elementos levarão A de q$_0$ para q$_1$. Para 1≤i≤n, seja β$_i$ uma linguagem regular cujos elementos levam A de q$_i$ para q$_{(imodn)+1}$ sem passar por nenhum estado fora de {q$_1$, ... ,q$_n$}. Alega-se que α(β$_1$ ... β$_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$_1$, t$_2$, ... em que para cada a e b, ρ(t$_{na+b}$) = q$_b$. Tal sequência existe porque todos os estados {q$_1$, ... ,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 α(β$_1$ ... β$_n$)$^ω$.
Suponha que w ∈ α(β$_1$ ... β$_n$)$^ω$. Pela definição de α, existe um segmento inicial de w que é um elemento de α e conduz A ao estado q$_1$. A partir daí, a execução nunca assume um estado fora de {q$_1$, ... ,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$_1$,a$_2$,... ∈ αβ$^ω$. 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$_1$,...,i$_{p+1}$ de tal forma que não existem dois deles que são equivalentes. Para l > max(i$_1$,...,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$_0$,i$_1$,i$_2$,... em que w(0,i$_0$) ∈ α 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$_0$,i$_1$,i$_2$, em que w(0,i$_0$) ∈ αβ* 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$_0$=i. Nós montamos i$_1$ de forma que i$_1$ favoreça i$_0$ e E(i$_0$,i$_1$). Então w(i$_0$,i$_1$) ∈ β*.
    Passo indutivo: Vamos supor E(i$_0$,i$_n$). Então, existe um momento i' em que E(i$_0$,i$_n$,i'). Nós montamos i$_{n+1}$ de forma que i$_{n+1}$ > i', i$_{n+1}$ favoreça i$_0$, e E(i$_0$,i$_{n+1}$). Então, w(i$_0$,i$_{n+1}$) ∈ β* e, visto que i$_{n+1}$ > i' nós temos por definição de E(i$_0$,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ãoacondiçãodeaceitaçãodeMulleréF={S|∃nμn⊆S⊆νn}.IssoterminaaconstruçãodoautômatodeMullerdesejado.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.

## Reference list

* ↑ McNaughton, R.: "Testing and generating infinite sequences by a finite automaton", Information and control 9, pp. 521–530, 1966.
* ↑ B. Le Saëc , J. Pin , P. Weil, A Purely Algebraic Proof of McNaughton's Theorem on Infinite Words, Foundations of Software Technology and Theoretical Computer Science, p. 141–151