Autômato de árvore infinita

Em ciência da computação e lógica matemática, um autômato de árvore infinita é uma máquina de estados que lida com estruturas de árvores infinitas. Pode ser visto como uma extensão de um autômato de árvore finita, que aceita apenas estruturas de árvores finitas. Também pode ser visto como uma extensão de alguns autômatos de palavras infinitas, como o autômato de Büchi e o autômato de Muller.

Um autômato finito que roda em uma árvore infinita foi usado pela primeira vez por Rabin para provar a decidibilidade da lógica de segunda ordem monádica. Foi também observado que autômato de árvore e teorias lógicas estão intimamente ligados e permitem que problemas de decisão em lógica sejam reduzidos a problemas de decisão para autômato.

Definição

Um autômato de árvore infinita roda sobre uma árvore rotulada $\Sigma$. Há muitas formulações ligeiramente diferentes de autômato de árvore. Aqui uma das formulações é descrita. Um autômato de árvore infinita é uma tupla $A=(\Sigma ,D,Q,\delta ,q_{0},F)$ onde,

• $\Sigma$ é um alfabeto.
• $D\subset \mathbb {N}$ é um conjunto finito. Cada elemento de $D$ é um grau permitido na árvore de entrada.
• $Q$ é um conjunto finito de estados.
• $\delta :Q\times \Sigma \times D\rightarrow 2^{Q^{*}}$ é uma função de transição que mapeia um estado de um autômato $q\in Q$, um caracter de entrada $\sigma \in \Sigma$, e um grau $d\in D$ para um conjunto de d-tuplas de estados.
• $q_{0}\in Q$ é o estado inicial do autômato.
• $F\subseteq \Sigma ^{\omega }$ é uma condição de aceitação.

Execução

Uma execução do autômato de árvore $A$ sobre uma árvore $(T,V)$ $\Sigma$-rotulada é uma árvore $(T_{r},r)$ $Q$-rotulada. Suponhamos que o autômato de árvore está no estado $q$ e chegou a um nó $t$ marcado com $\sigma \in \Sigma$ da árvore de entrada. $d(t)$ é o grau do nó $t$. Em seguida, o autômato continua selecionando uma tupla $(q_{1},...,q_{d(t)})$ do conjunto $\delta (q,\sigma ,d(t))$ e dividindo-se em $d(t)$ cópias de si mesmo. Para cada $0<i\leq d(t)$, uma cópia entra no estado $q_{i}$ e prossegue para o nó $t.i$. Este processo produz uma execução sobre uma árvore.

Formalmente, executando $(T_{r},r)$ na árvore de entrada satisfaz as seguintes duas condições:

1. $r(\epsilon )=q_{0}$
2. Para todo $t\in T_{r}$ com $r(t)=q$, existe um $(q_{1},...,q_{d(t)})\in \delta (q,V(t),d(t))$ tal que, para todo $0<i\leq d(t)$, temos $t.i\in T_{r}$ e $r(t.i)=q_{i}$

Condição de aceitação

Em uma execução $(T_{r},r)$, um caminho infinito é marcado por uma sequência de estados. Esta sequência de estados forma uma palavra infinita sobre os estados. Se todas essas palavras infinitas pertencem a condição de aceitação $F$, então, a execução é de aceitação. As condições de aceitação interessantes são Büchi, Rabin, Streett e Muller. Se para uma árvore de entrada $(T,V)$  $\Sigma$-rotulada existe uma execução de aceitação, então, a árvore de entrada é aceita pelo autômato. O conjunto de todas as árvores aceitas $\Sigma$-rotuladas é chamado de linguagem da árvore ${\mathcal {L}}(A)$ que é reconhecida pelo autômato de árvore $A$.

Observações

O conjunto $D$ pode parecer estranho para algumas pessoas. Algumas vezes $D$ é omitido da definição, quando é um conjunto singleton que significa que uma árvore de entrada tem ramificação fixa em cada nó. Por exemplo, se $D={2}$, então a árvore de entrada tem que ser uma árvore binária completa.

Autômato de árvore infinita é determinístico se, para algum $q\in Q$, $\sigma \in \Sigma$ e $d\in D$ a função de transição $\delta (q,\sigma ,d)$ tem exatamente um elemento. Caso contrário, o autômato é não-determinístico.

Aceitando linguagens de árvores

As condições de aceitação de Muller, de paridade, de Rabin e de Streett em um autômato de árvore infinita reconhecem as mesmas linguagens de árvores.

Mas, a condição de aceitação de Büchi é estritamente mais fraca que outras condições de aceitação, por exemplo, existe uma linguagem de árvore, que pode ser reconhecida pela condição de aceitação de Muller em autômato de árvore infinita, mas que não pode ser reconhecida por nenhuma condição de aceitação de Büchi para algum autômato de árvore infinita.

Linguagens de árvores, as quais são reconhecidas pelas condições de aceitação de Muller são fechadas sob união, interseção, projeção e complemento.