# Autômato ω

Na teoria de autômatos, um ramo da teoria da computação, um autômato ω é uma variação do autômato finito que roda sobre cadeias infinitas como entrada, ao invés de finitas. Uma vez que um ω-autômato não para, eles têm uma variedade de condições de aceitação, em vez de simplesmente um conjunto de estados de aceitação.
ω-autômatos são úteis para a especificação de comportamento de sistemas que não são esperados para terminar, como hardware, sistemas operacionais e sistemas de controle. Para tais sistemas, você pode querer especificar uma propriedade, como "para cada pedido, uma confirmação, eventualmente, segue", ou sua negação "existe um pedido que não é seguido por uma confirmação". O último é uma propriedade das palavras infinitas: nada se pode dizer de uma sequência finita que satisfaz esta propriedade.
Classes de ω-autômatos incluem o autômatos de Büchi, 'Rabin de autômatos', 'autômatos de Streett, 'autômatos de paridade e Muller autômatos, determinístico ou não determinístico. Essas classes de ω-autômatos diferem apenas em termos de condicionar a aceitação. Todos eles reconhecem precisamente a linguagens ω regulares , excepto pelos autômatos do Büchi determinísticos, que são estritamente mais fracos do que todos os outros. Embora todos estes tipos de autômatos reconhecem o mesmo conjunto de linguagens ω, eles ainda diferem em concisão de representação para uma dada linguagem ω.

## Autômato ω determinístico

Formalmente, um autômato ω determinístico é uma tupla A = (Q,Σ,δ,q$_0$,Acc) que consiste nos seguintes componentes:
* Q é um conjunto finito. Os elementos de Q são chamados de estados de A.
* Σ é um conjunto finito chamado de alfabeto de A.
* δ: Q × Σ → Q é uma função, chamada de função de transição de A.
* q$_0$ é um elemento de Q, chamado de estado inicial.
* Acc é a condição de aceitação, formalmente um subconjunto de Q$^ω$
Uma entrada para A é uma string infinita sobre o alfabeto Σ, i.e. é uma sequencia infinita α = (a$_1$,a$_2$,a$_3$,...). A execução de A em tal entrada é uma sequencia infinita ρ = (r$_0$,r$_1$,r$_2$,...) de estados, definidos da seguinte forma:
* r$_0$ = q$_0$.
* r$_1$ = δ(r$_0$,a$_1$).
* r$_2$ = δ(r$_1$,a$_2$).
* r$_n$ = δ(r$_{n-1}$,a$_n$).
A finalidade principal de um autômato ω é definir um subconjunto do conjunto de todas as entradas: O conjunto de entradas aceitas. Considerando que, no caso de um simples autômato finito cada corrida termina com um estado r$_n$ e a entrada é aceita se e somente se r$_n$ é um estado de aceitação, a definição do conjunto de entradas aceitas é mais complicado para autômatos ω. Aqui devemos olhar para a execução completa de ρ. A entrada é aceita se a execução correspondente está em Acc. Oconjunto de entradas de palavras ω aceitas é chamado de linguagem ω reconhecida por um autômato, que é denotado como L(A).
A definição de Acc como subconjunto de Q$^ω$ é puramente formal e não adequado pra prática porque normalmente tais conjuntos são infinitos. A diferença entre vários tipos de autômatos ω (Büchi, Rabin etc.) consiste em como eles codificam determinados subconjuntos Acc de Q$^ω$ como conjuntos finitos, e portanto em quais subconjuntos eles podem codificar.

## Autômatos ω não-determinísticos

Formalmente, um autômato ω não-determinístico é uma tupla A = (Q,Σ,Δ,Q$_0$,Acc) que consiste dos seguintes componentes:
* Q é um conjunto finito. Os elementos de Q são chamados de estados de A.
* Σ é um conjunto finito chamado de alfabeto de A.
* Δ é um subconjunto de Q × Σ × Q e é chamado de relação de transição de A.
* Q$_0$ é um subconjunto de Q, conjunto inicial de estados.
* Acc é a condição de aceitação, um subconjunto de Q$^ω$.
Ao contrário de um autômato ω determinístico que tem uma função de transição δ, a versão não-determinística tem uma transição relação Δ. Note-se que Δ pode ser considerada como uma função : Q × Σ → P(Q) de Q × Σ para o conjunto das partes P(Q). Assim, dado o estado q$_n$ e o símbolo a$_n$, o próximo estado q$_{n+1}$ não é necessariamente determinada de forma exclusiva, uma vez que há um conjunto de estados possíveis próximos. A execução de A sobre a entrada α = (a$_1$,a$_2$,a$_3$,...) é qualquer sequencia infinita ρ = (r$_0$,r$_1$,r$_2$,...) de estados que satifaz as seguinte condições
* r$_0$ é um elemento de Q$_0$.
* r$_1$ é um elemento de Δ(r$_0$,a$_1$).
* r$_2$ é um elemento de Δ(r$_1$,a$_2$).
* r$_n$ é um elemento de Δ(r$_{n-1}$,a$_n$).
Um autômato ω não-determinístico pode admitir muitas execuções diferentes em qualquer dada entrada, ou mesmo nenhuma. A entrada é aceita se, pelo menos, uma das execuções possíveis aceitar. Se uma execução é aceita, depende apenas de Acc, como por autômato ω determinístico. Cada autômato ω determinístico pode ser considerada como um autômato ω não-determinístico tomando Δ para ser o grafo de δ. As definições de execuções e de aceitação para autômatos ω determinísticos são, então, os casos especiais dos casos não determinísticos.

## Condições de aceitação

Condição de aceitação pode ser um conjunto infinito de palavras ômega. Assim, as pessoas em sua maioria estudam as condições de aceitação que são apenas finitamente representáveis. A seguir listamos uma variedade de condições de aceitação popular.
Antes de discutir a lista, vamos fazer seguinte observação. No caso de sistemas infinitamente em funcionamento, muitas vezes tem-se interesse em se certo comportamento é repetido muitas vezes infinitamente. Por exemplo, se uma placa de rede recebe pedidos de ping infinitos, então pode deixar de responder a alguns dos pedidos, mas deve responder a um subconjunto infinito de solicitações de ping recebidas. Isto motiva a seguinte definição: Para qualquer execução ρ, deixe Inf(ρ) ser o conjunto de estados que ocorrem frequente e infinitamente em ρ. Esta noção de certos estados a ser visitado infinitas vezes será útil na definição das condições de aceitação a seguir.
* Um autômato de Büchi é um autômato ω A que usa as seguintes condições de aceitação, para algum subconjunto F de Q:

   ### condição de Büchi

       A aceita exatamente aquelas execuções de ρ pelas quais Inf(ρ) ∩ F não é vazia, i.e. existe um estado de aceitação que ocorre frequente e infinitamente in ρ.
    Uma vez que F é finito, isso é equivalente a condição que ρ$_n$ é aceita por uma quantidade infinita de números naturais n.
* Um autômato de Rabin é um autômato ω A que usa a seguinte condição de aceitação, para algum conjunto Ω de pares (E$_i$,F$_i$) de conjunto de estados:

   ### Condição de Rabin

       A aceita exatamente aquelas execuções ρ pelas quais existem um par (E$_i$,F$_i$) em Ω tal que E$_i$ ∩ Inf(ρ) é vazio e F$_i$ ∩ Inf(ρ) não é vazio.
* Um autômato de Streett é um autômato ω A que usa as seguinte condição de aceitação, para algum conjunto Ω de pares (E$_i$,F$_i$) de conjuntos de estados:

   ### Condição de Streett

       A aceita exatamente aquelas execuções ρ pelas quais para todos os pares (E$_i$,F$_i$) em Ω, E$_i$ ∩ Inf(ρ) não é vazio ou F$_i$ ∩ Inf(ρ) é vazio.
A condição de Streett é a negação da condição de Rabin. Portanto, um autômato determinístico de Streett aceita exatamente o complemento d linguagem aceita pelo autômato determinístico de Rabin composto pelos mesmos dados com todos os L$_i$ e U$_i$ trocados.
* Um autômato de paridade é um autômato A cujo conjunto de estados é Q = {0,1,2,...,k} para algum número natural k, e que tem a seguinte condição de aceitação:

   ### Condição de paridade

       A aceita ρ se e somente se é ainda o menor número em Inf(ρ).
* Um Autômato de Muller é um autômato ω A que usa as seguinte condição de aceitação, para um subconjunto F de P(Q) (o conjunto das partes de Q):

   ### Condição de Muller

       A aceita exatamente aquelas execuções ρ pelas quais Inf(ρ) é um elemento de F.
Cada autômato de Büchi pode ser considerado um autômato de Muller. é suficiente substituir F por F' consistindo de todos os subconjuntos de Q que contêm pelo menos um elemento de F. Similarmente cada autômato de Rabin, Streett ou Paridade pode também ser considerado um autômato de Muller.

## Exemplo

A seguinte linguagem ω L sobre o alfabetoΣ = {0,1} que pode ser conhecida por um autômato não determinístico de Büchi: L consiste de todas as palavras ω em Σ$^ω$ em que 1 ocorre apenas um número finito de vezes. Um autômato não determinístico de Büchi que reconhece L precisa apenas de dois estados q$_0$ (o estado inicial) e q$_1$. Δ consiste das triplas (q$_0$,0,q$_0$), (q$_0$,1,q$_0$), (q$_0$,0,q$_1$) e (q$_1$,0,q$_1$). F = {q$_1$}. Para qualquqer entrada α em que 1 ocorre apenas um quantidade finita de vezes, existe uma execução que fica no estado q$_0$ enquanto tiverem 1s para ler, e vai para o estado q$_1$ depois. Essa execução é bem sucessida. Se existe infinitos 1s, então existe apenas uma possível execução: A que sempre fica no estado q$_0$. (Uma vez que a máquina tenha deixado q$_0$ e alcançado q$_1$, não pode retornar. Se outro 1 é lido, não há nenhum estado sucessor.)
Observe que a línguagem acima não pode ser reconhecida por um autômato determinístico de Büchi, que pode ser demonstrado utilizando o facto de que existem apenas um número finito de estados no autômato.

## Poder expressivo de um autômato ω

Uma linguagem ω sobre um alfabeto finito Σ é o conjunto de palavras ω sobre Σ, i.e. é um subconjunto de Σ$^ω$. Uma linguagem ω sobre Σ é conhecida por um autômato ω A (com o mesmo alfabeto) se é o conjunto de todas as palavras ω aceitas por A. O expressivo poder da classe do autômatos ω é medido pela classe de todas as linguagens ω, que podem ser reconhecidas por algum autômato na classe.
Os autômatos não determinísticos de Büchi, paridade, Rabin, Streett e Muller, respectivamente, todos reconhecem exatamente a mesma classe de linguagens ω. Esses são conhecidos como fechamento de ω-Kleene para linguagens regulares ou como as linguagens ω regulares. Usando provas diferentes também pode ser mostrado que os autômatos determinísticos de paridade, Rabin, Streett e Muller reconhencem as linguagens ω regulares. Daqui decorre que a classe das linguagens ω regulares é fechada sob complementação. No entanto, o exemplo acima mostra que a classe de autômatos determinísticos de Büchi é estritamente mais fraco.

## Referencias

* Farwer, Berndt (2002), «ω-Automata», in: Grädel, Erich; Thomas, Wolfgang; Wilke, Thomas, Automata, Logics, and Infinite Games, ISBN 978-3-540-00388-5, Lecture Notes in Computer Science, Springer, pp. 3–21 .
* Automata on Infinite Words Slides for a tutorial by Paritosh K. Pandya.

## Leitura complementar

* Perrin, Dominique; Pin, Jean-Éric (2004), Infinite Words: Automata, Semigroups, Logic and Games, ISBN 978-0-12-532111-2, Elsevier
* Thomas, Wolfgang (1990), «Automata on infinite objects», in: van Leeuwen, Jan, Handbook of Theoretical Computer Science, vol. B, ISBN 978-0-262-22039-2, MIT Press, pp. 133–191