Autómato de árvore

Um autómato de árvore é um tipo de máquina de estados que lida com estruturas em árvore (de topologia em árvore), ao invés de strings como as máquinas de estado mais convencionais.

Tal como acontece com os autómatos clássicos, um autómato de árvores finito (FTA) pode ser um autómato determinístico ou não. De acordo com a maneira que o autómato processa a árvore de entrada, o autómato de árvores finito pode ser de dois tipos: (a) bottom-up, (b) top-down. Essa é uma questão importante, pois apesar de os autómatos finitos de árvore não-determinísticos bottom-up e top-down serem equivalentes em poder expressivo, os autómatos determinísticos top-down são estritamente menos poderosos do que seus homólogos em bottom-up, por que as propriedades especificadas pelo autómato de árvores determinístico dependem apenas das propriedades do caminho. (Autómatos de árvore determinísticos bottom-up são tão poderosos quanto os autómatos em árvore não-determinísticos)

Definições

Um alfabeto classificado é um par com um alfabeto ${\mathcal {F}}$ e uma função $Arity:{\mathcal {F}}\rightarrow \mathbb {N}$. Cada letra tem a sua aridade para que ela possa ser usada para construir termos. Elementos nulos (com aridade zero) são também chamados constantes. Termos construídos com símbolos unários e constantes podem ser considerados como [string (ciência da computação)|strings]]. Maiores aridades formam árvores.

Um autómato de árvores finito bottom-up sobre $F$ é definida por: $(Q,F,Q_{f},\Delta )$

Onde $Q$ é um conjunto de letras unárias (estados), $F$ é um alfabeto classificado, $Q_{f}\subseteq Q$ é um conjunto de estados finais, e $\Delta$ é um conjunto de regras de transição, ou seja, rescreve as regras dos nós cujas raízes dos filhos são estados, para nós cujas raízes são estados. Assim o estado de um nó é deduzido do estado de seus filhos.

Não há estado inicial como tal, mas as regras de transição para símbolos constantes (folhas) podem ser consideradas como estados iniciais. A árvore é aceita se o estado rotulado na raiz é um estado de aceitação.

Um autómato de árvore finito sobre $F$ é definido por: $(Q,F,I,\Delta )$

Existem duas diferenças no autómato de árvore bottom-up: primeiro, $I\subseteq Q$, o conjunto de seus estados iniciais, substitui $Q_{F}$; segundo, suas regras de transição são o inverso, ou seja, rescreve as regras dos nós cujas raízes são estados para nós cujas raízes dos filhos são estados. A árvore é aceite se todo ramo pode passar por esse caminho.

Rescrever as regras fazem os símbolos de $Q$ 'viajarem' ao longo dos ramos da árvore.

Pode-se facilmente imaginar que os autómatos de árvore não-determinísticos top-down são equivalentes aos não-deterministas bottom-up; as regras de transição são simplesmente invertidas, e os estados finais se tornam os estados iniciais.

A razão pela qual os deterministas top-down (FTA) são menos poderosos do que os seus homólogos bottom-up relaciona-se com o facto de um FTA determinista ser, por definição, aquele em que não há duas regras de transição contendo o mesmo lado esquerdo. Para autómatos de árvore, regras de transição são regras de reescrita; e para top-down, o lado esquerdo serão os nós pai. Consequentemente, um autómato de árvore determinístico top-down só será capaz de testar as árvore cujas propriedades são verdadeiras em todos os ramos, porque a escolha do estado para escrever em cada ramo do filho é determinado no nó pai, sem saber o conteúdo dos ramos filhos.

Propriedades

Determinismo

Como dito anteriormente, um autómato de árvore é determinístico quando não há duas regras de transição com o mesmo lado esquerdo. Esta definição corresponde à ideia intuitiva de que para um autómato ser determinístico, uma e apenas uma transição deve ser possível para um determinado nó.

Reconhecibilidade

Para um autómato bottom-up, um termo-chão t (isto é, uma árvore) é aceito se existe uma redução que começa a partir de t e termina com q(t), onde q é um estado final. Para um autómato de top-down, um termo-chão t é aceite se existe uma redução que começa a partir de q(t) e termina com t, onde q(t) é um estado inicial.

A linguagem de árvore $L(A)$ reconhecida por um autómato de árvore $A$ é o conjunto de todos os termos-chão aceitos por $A$. Um conjunto de termos-chão é reconhecível se existe um autómato de árvore que o reconhece.

Uma propriedade importante é que homomorfismos lineares (isto é, que preservam a aridade) preservam a reconhecibilidade.

Completude e Redução

Um autômato de árvore finito não-determinístico é completo se houver pelo menos uma regra de transição disponível para cada possível combinação de símbolo estados. Um estado $q$ é acessível se existe um termo $t$ chão, que tem uma redução de t para q (t). Um FTA é reduzido se todos os seus estados são acessíveis.

Lema do Bombeamento

Seja $L$ um conjunto de termos chão reconhecíveis. Então, existe uma constante $k>0$ satisfazendo: para cada termo chão $t$ em $L$ que tenha $Altura(t)>k$, existe um contexto $C\in C(F)$, um contexto não-trivial $C'\in C(F)$ e um termo chão $u$ tal que $t=C[C'[u]]$ and, for all $n\geq 0$ $C[C'^{n}[u]]\in L$.

Fechamento ou Clausura

A classe de linguagens árvore reconhecível é fechada sob união, sob complementação, e sob cruzamento.

Teorema de Myhill-Nerode

Uma congruência nas linguagens-árvore é uma relação como se segue:

$u_{1}\equiv v_{1}\wedge \ldots \wedge u_{n}\equiv v_{n}\Rightarrow f(u_{1},\ldots ,u_{n})\equiv f(v_{1},\ldots ,v_{n})$

Será de índice finito se o número de classes de equivalência é finito.

Para uma dada linguagem árvore $L$, defina $u\equiv _{L}v$ se para todos os contextos $C\in C(F)$, $C[u]\in L\Leftrightarrow C[v]\in L$.

O teorema de Myhill-Nerode para autómatos de árvore afirma que as 3 seguintes afirmações são equivalentes:

1. L é uma linguagem árvore reconhecível
2. L é a união de algumas classes de equivalência de congruência de índice finito
3. a relação $\equiv _{L}$ é uma congruência de índice finito

Ligações externas

Todas as informações nessa página foram tiradas do Capítulo 1 de http://tata.gforge.inria.fr

Implementations

• (OCaml) Grappa - Ranked and Unranked Tree Automata Libraries (http://www.grappa.univ-lille3.fr/~filiot/tata/)
• (OCaml) Timbuk - Tools for Reachability Analysis and Tree Automata Calculations (http://www.irisa.fr/celtique/genet/timbuk/)
• (Java) LETHAL - Library for working with finite tree and hedge automata (http://lethal.sf.net/)
• (Isabelle [OCaml, SML, Haskell]) - Machine-Checked Tree Automata Library (http://afp.sourceforge.net/entries/Tree-Automata.shtml)
• (C++) VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata - (http://www.fit.vutbr.cz/research/groups/verifit/tools/libvata/)