Autômato de Büchi

Em ciência da computação e teoria dos autômatos, um Autômato de Büchi é um tipo de autômato ω, que estende um autómato finito para entradas infinitas. Ele aceita como entrada uma sequência infinita sse existe uma execução do autômato que visita (pelo menos) um dos estados finais infinitas vezes. Autômato de Büchi reconhece a linguagem Omega-regular, a versão da palavra infinita das linguagens regulares. Foi assim denominada por causa do matemático suíço Julius Richard Büchi que inventou esse tipo de autômato em 1962.

Autômatos de Büchi são frequentemente utilizados em verificação de modelos como uma versão da teoria dos autômatos de uma fórmula em lógica temporal linear.

Definição formal

Formalmente, um Autômato de Büchi determinístico é uma tupla A = (Q,S,d,q₀,F) que consiste nos seguintes componentes:

• Q é um conjunto finito. Os elementos de Q são chamados estados de A.
• S é um conjunto finito chamado alfabeto de A.
• d: Q × S ? Q é uma função, chamada de função de transição de A.
• q₀ é um elemento de Q, chamado estado inicial.
• F⊆Q é o estado de aceitação. A aceita exatamente aquelas execuções em que pelo menos um dos estados infinitos frequentes ocorrem em  F.

No autômato de Büchi não-determinístico, a função de transição δ é substituída com uma relação de transição Δ que retorna um conjunto e estados. Geralmente, o autômato de Büchi refere-se ao autômato de Büchi não-determinístico.

Para um formalismo mais abrangente, veja também autômato ω.

Propriedades de fechamento

O conjunto dos autômatos de Büchi é fechado em relação a algumas das seguintes operações.

Seja A=(Q_A,Σ,Δ_A,I_A,F_A) e B=(Q_B,Σ,Δ_B,I_B,F_B) autômatos de Büchi e C=(Q_C,Σ,Δ_C,I_C,F_C) seja um autômato finito.

• União: Existe um autômato de Büchi que reconhece L(A)∪L(B).

Prova: Se nós assumirmos, w.l.o.g., Q_A∩Q_B é vazio então L(A)∪L(B) é reconhecido pelo autômato de Büchi (Q_A∪Q_B, Σ, Δ_A∪Δ_B, I_A∪I_B, F_A∪F_B).

• Intersecção: Existe um autômato de Büchi que reconhece a linguagem L(A)∩L(B).

Prova: O autômato de Büchi A'=(Q',Σ,Δ',I',F') reconhece L(A)∩L(B), onde

• Q' = Q_A × Q_B × {1,2}
• Δ' = Δ₁ ∪ Δ₂
  • Δ₁ = {( (q_A,q_B,1), a, (q'_A,q'_B,i) ) | (q_A,a,q'_A)∈Δ_A e(q_B,a,q'_B)∈Δ_B e se q_A∈F_A então i=2 ou então i=1 }
  • Δ₂ = {( (q_A,q_B,2), a, (q'_A,q'_B,i) ) | (q_A,a,q'_A)∈Δ_A e (q_B,a,q'_B)∈Δ_B e se q_B∈F_B então i=1 ou então i=2 }
• I' = I_A × I_B × {1}
• F' = { (q_A,q_B,2) | q_B∈F_B }

Por construção, r'=(q_A⁰,q_B⁰,i⁰),(q_A¹,q_B¹,i¹),... é uma execução do autômato A' numa cadeia de entrada w sse r_A=q_A⁰,q_A¹,... é executado A emw e r_B=q_B⁰,q_B¹,... é executado B em w. r_A aceita e r_B aceita sse r' é a concatenação de uma séria infinita de segmentos finitos de 1-estados(estados com um terceiro componente 1) e 2-estados(estados com um terceiro componente 2) alternativamente. Não existe uma série de segmentos de r' sse r' aceita por A'.

• Concatenação: Existe um autômato de Büchi que reconhece a linguagem L(C)⋅L(A).

Prova: Se assumirmos, w.l.o.g., Q_C∩Q_A é vazio, então autômato de Büchin A'=(Q_C∪Q_A,Σ,Δ',I',F_A) reconhece L(C)⋅L(A), onde

• Δ' = Δ_A ∪ Δ_C ∪ { (q,a,q') | q'∈I_A e  ∃f∈F_C. (q,a,f)∈Δ_C }
• se I_C∩F_C é vazio, então I' = I_C caso contrário I' = I_C ∪ I_A

• Fechamento-ω: Se L(C) não contém a cadeia vazia então existe um autômato de Büchi que reconhece a linguagem (C)^ω.

Prova: O autômato de Büchi que reconhece L(C)^ω é construído em duas etapas. Primeiro, nós construímos um autômato finito A' tal que A' também reconhece L(C) mas não há transições de entrada para os estados iniciais de A'. Então, A'=(Q_C ∪ {q_novo},Σ,Δ',{q_novo},F_C), onde Δ' = Δ_C ∪ { (q_novo,a,q') | ∃q∈I_C. (q,a,q')∈Δ_C}. Note que L(C)=L(A') porque L(C) não contém a cadeia vazia. Segundo, nós iremos construir o autômato de Büchi A" que reconhece L(C)^ω pela adição de um loop de volta ao estado inicial de A'. Então, A"=(Q_C ∪ {q_novo},Σ,Δ",{q_novo},{q_novo}), onde Δ" = Δ' ∪ { (q,a,q_novo) | ∃q'∈F_C. (q,a,q')∈Δ'}.

• Complemento:Existe um autômato de Büchi que reconhece a linguagem Σ*/L(A).

Prova: A prova é apresentada aqui.

Linguagens Reconhecíveis

O autômato de Büchi reconhece as linguagens ω-regulares. Utilizando a definição de linguagem ω-regular e as propriedades de fechamento do autômato de Büchi mostradas acima, pode ser facilmente demonstrado que um autômato de Büchi pode ser construído de tal forma a reconhecer qualquer linguagem ω-regular dada. Para mais, veja construção de uma linguagem w-regular por um autômato de Büchi.

Autômato de Büchi determinístico e não-determinístico

Um autômato de Büchi que reconhece (0+1)*0^ω

A classe de autômatos de Büchi determinísticos não é suficiente para abranger todas as línguagens ω-regulares. Em particular, não existe um autômato de Büchi determinístico que reconheça a linguagem (0+1)*0^ω (Qualquer palavra que possui um sufixo infinito consistindo apenas de 0's). Podemos demonstrar por contradição que nenhum autômato de Büchi determinístico como esse existe. Vamos supor A como um autômato de Büchi determinístico que reconhece (0+1)*0^ω como o estado final F. A aceita 0^ω. Então, A irá visitar algum estado F depois de ler alguns prefixos finitos de 0^ω, digamos após a i₀th letra. A também aceita a ω-cadeia 0^i₀10^ω. Portanto, para algum i₁, após o prefixo 0^i₀10^i₁ o autômato irá visitar algum estado em F. Continuando com esta construção da ω-palavra 0^i₀10^i₁10^i₂... é gerado, o que causa a visita de A em algum estado de F infinitas vezes e a cadeia não está em(0+1)*0^ω. Contradição.

A classe de linguagens reconhecíveis por autômatos de Büchi determinísticos é caracterizada pelo seguinte lema.

Lema: Uma ω-linguagem é reconhecível por um autômato de Büchi determinístico sse ela é limite de alguma linguagem regular.

Prova: Qualquer autômato de Büchi determinístico A pode ser visto como um autômato finito determinístico A' e vice-versa, uma vez que ambos os tipos de autômato são definidos como 5-tuplas de mesmos componentes, apenas a interpretação de condição de aceitação é diferente. Iremos mostrar que L(A) é o limite de L(A'). Uma ω-cadeia é aceita por A sse ela irá forçar A a visitar os estados finais infinitas vezes. Sse, um número infinito de prefixos desta ω-cadeia irá ser aceita por A'. Assim, G(A) é uma linguagem limite de L(A').

Algoritmos

Verificação de modelos de sistemas de estados finitos podem muitas vezes ser traduzidos em várias operações de Autômatos de Büchi. Além das operações de fecho apresentadas acima, a seguir estão algumas operações úteis para as aplicações do Autômato de Büchi.

Determinização

Desde que os autômatos de Büchi determinísticos são estritamente menos expressivos do que os autômatos não-determinísticos, não pode haver um algoritmo para determinização do Autômato de Büchi. Mas o teorema de McNaughton e a construção de Safra fornecem algoritmos que podem traduzir um autômato de Büchi em um autômato de Muller determinístico ou um autômato de Rabin determinístico.

Verificação de vacuidade

A linguagem reconhecida por um autômato de Büchi não é vazia sse existe um estado final que acessível a partir do estado inicial, e encontra-se em um ciclo.

Um algoritmo eficiente que pode verificar o vazio de um autômato de Büchi:

1. Considere o autômato como um grafo direcionado e decompô-lo em componentes fortemente conectados .
2. Executar uma pesquisa (por exemplo,a busca em profundidade) para encontrar os componentes que são acessíveis a partir do estado inicial.
3. Verificar se existe um componente fortemente ligado não trivial que seja acessível e contém um estado final.

Cada um dos passos deste algoritmo pode ser feito em tempo linear no tamanho autômato, portanto, o algoritmo é claramente ótimo.

Redução ao mínimo

O algoritmo para minimizar o autômato finito não-determinístico também minimiza corretamente um autômato de Büchi. O algoritmo não garante o mínimo autômato de Büchi. Note que algoritmos para minimizar o autômato finito determinístico não funciona mpara o autômato de Büchi determinístico.

Ver também

• Aritmética de Büchi