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[editar | editar código-fonte]

Formalmente, um autômato ω determinístico é uma tupla A = (Q,Σ,δ,q₀,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₀ é 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₁,a₂,a₃,...). A execução de A em tal entrada é uma sequencia infinita ρ = (r₀,r₁,r₂,...) de estados, definidos da seguinte forma:

r₀ = q₀.
r₁ = δ(r₀,a₁).
r₂ = δ(r₁,a₂).

...

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[editar | editar código-fonte]

Formalmente, um autômato ω não-determinístico é uma tupla A = (Q,Σ,Δ,Q₀,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₀ é 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₁,a₂,a₃,...) é qualquer sequencia infinita ρ = (r₀,r₁,r₂,...) de estados que satifaz as seguinte condições

r₀ é um elemento de Q₀.
r₁ é um elemento de Δ(r₀,a₁).
r₂ é um elemento de Δ(r₁,a₂).

...

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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₀ (o estado inicial) e q₁. Δ consiste das triplas (q₀,0,q₀), (q₀,1,q₀), (q₀,0,q₁) e (q₁,0,q₁). F = {q₁}. Para qualquqer entrada α em que 1 ocorre apenas um quantidade finita de vezes, existe uma execução que fica no estado q₀ enquanto tiverem 1s para ler, e vai para o estado q₁ 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₀. (Uma vez que a máquina tenha deixado q₀ e alcançado q₁, 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 ω[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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