Linguagem Omega-regular

As Linguagens ω-regulares são uma classe de linguagens-ω que generalizam a definição de linguagens regulares para palavras infinitas. Büchi mostrou em 1962 que linguagens ω-regulares são precisamente aquelas definidas numa particular lógica monádica de segunda ordem chamada S1S.

Definição Formal

Uma linguagem-ω L é ω-regular se tem a forma

A^ω onde A é uma linguagem regular não vazia que não contém a string vazia
AB, a concatenação da linguagem regular A e uma linguagem ω-regular B (Note que BA não é bem definida)
A∪B onde A e B são linguagens ω-regulares (essa regra só pode ser aplicada um número finito de vezes)

Os elementos de A^ω são obtidos concatenando palavras de A infinitamente muitas vezes. Note que se A é regular, A^ω não é necessariamente ω-regular, já que A poderia ser {ε}, o conjunto contendo apenas a string vazia, onde neste caso A^ω=A, que não é uma ω-language e portanto não é uma linguagem ω-regular.

Equivalência com o autômato de Büchi

Teorema: Uma linguagem-ω é reconhecida por um Autômato de Büchi se e somente se for uma linguagem ω-regular.

Prova: Toda linguagem ω-regular é reconhecida por um Autômato de Büchi não-determinístico ; a interpretação é construtiva. Usando as propriedades de fechamento do Autômato de Büchi e indução estrutural sobre a definição da linguagem ω-regular, pode ser demonstrado facilmente que um Autômato de Büchi pode ser construído para uma dada liguagem ω-regular.

Reciprocamente, para um dado Autômato de Büchi A = (Q,Σ,Δ,I,F), nos construímos uma linguagem ω-regular e então mostraremos que esta linguagem é reconhecida por A. Para uma palavra-ω w=a₁,a₂,... , seja w(i,j) o segmento finito a_i+1,...,a_j-1,a_j de w. Para todo q,q'∈ Q, nós definimos uma Linguagem regular L_q,q' que é aceita pelo autômato finito (Q,Σ,Δ,{q},{q'}).

Lema: Nós afirmamos que o Autômato de Büchi A reconhece a linguagem ⋃_q∈I,q'∈F L_q,q' (L_q',q' - {ε} )^ω.

Prova: Vamos supor a palavra w ∈ L(A) e q₀,q₁,q₂,... é uma configuração de aceitação de A sobre w. Portanto, q₀ está em I e deve have um estado q' em F tal que q' ocorre com uma frequência infinita na configuração de aceitação. Tendo em mãos a crescente sequência infinita de índices i₀,i₁,i₂... tal que, para todo k≥0, q_{i_k} é q'. Por isso, w(0,i₀)∈L_q₀,q' e, para todo k≥0, w(i_k,i_k+1)∈L_q',q' . Assim, w ∈ L_q₀,q' (L_q',q' )^ω.

Agora, suponha w ∈ L_q,q' (L_q',q' - {ε} )^ω para algum q∈I e q'∈F. Então, há uma infinita e estrita sequência crescente i₀,i₁,i₂... tal que w(0,i₀) ∈ L_q,q' e, para todo k≥0,w(i_k,i_k+1)∈L_q',q' . Por definição de L_q,q', existe uma configuração finita de A a partir de q até q' sobre a palavra w(0,i₀). Para todo k≥0, existe uma configuração finita de A até q até q' sobre a palavra w(i_k,i_k+1). Através desta construção, temos uma configuração de A, que começa a partir de q e na qual q' ocorre com frequência infinita. Por isso, w ∈ L(A).

Bibliografia

W. Thomas, "Automata on infinite objects." Em Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, páginas 133-192. Elsevier Science Publishers, Amsterdam, 1990.