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
[editar | editar código-fonte]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
[editar | editar código-fonte]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=a1,a2,... , seja w(i,j) o segmento finito ai+1,...,aj-1,aj de w. Para todo q,q'∈ Q, nós definimos uma Linguagem regular Lq,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 Lq,q' (Lq',q' - {ε} )ω.
- Prova: Vamos supor a palavra w ∈ L(A) e q0,q1,q2,... é uma configuração de aceitação de A sobre w. Portanto, q0 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 i0,i1,i2... tal que, para todo k≥0, qik é q'. Por isso, w(0,i0)∈Lq0,q' e, para todo k≥0, w(ik,ik+1)∈Lq',q' . Assim, w ∈ Lq0,q' (Lq',q' )ω.
- Agora, suponha w ∈ Lq,q' (Lq',q' - {ε} )ω para algum q∈I e q'∈F. Então, há uma infinita e estrita sequência crescente i0,i1,i2... tal que w(0,i0) ∈ Lq,q' e, para todo k≥0,w(ik,ik+1)∈Lq',q' . Por definição de Lq,q', existe uma configuração finita de A a partir de q até q' sobre a palavra w(0,i0). Para todo k≥0, existe uma configuração finita de A até q até q' sobre a palavra w(ik,ik+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
[editar | editar código-fonte]- 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.