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₀,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

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

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

Um exemplo de um autômato não determinístico de büchi

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 ω

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