Autómatas que operan sobre entradas en forma de árbol en lugar de palabras, reconociendo conjuntos de árboles finitos o infinitos (rankeados o no) según condiciones de aceptación; se utilizan para caracterizar lenguajes regulares de árboles y decidir propiedades de modelos de términos, lógicas sobre árboles y problemas de verificación con estructura ramificada.

Principio

Definir una ejecución que asigne estados a los nodos según reglas de transición locales (bottom-up, top-down o alternante) y aceptar un árbol si la ejecución satisface criterios de aceptación designados (por ejemplo, estados finales en la raíz, condiciones de paridad en ramas infinitas).

Demostración

Un autómata de árboles finito bottom-up reconoce el conjunto de árboles sintácticos tipados de expresiones bien formadas; en análisis de programas, un autómata de árboles puede caracterizar los formatos de heap alcanzables y así reducir el análisis de formas a la comprobación de vaciedad.

Aplicación incorrecta

Tratar a los autómatas de árboles exactamente como autómatas de palabras: emplear dispositivos deterministas top-down cuando son estrictamente menos expresivos que los bottom-up nondeterministas, o ignorar las distinciones rankeado/no-rankeado y sus costes de traducción.

Consecuencia

Proporciona cierres bajo unión, intersección y a menudo complementación (según la variante), problemas de vaciedad y pertenencia decidibles, y una correspondencia con MSO sobre árboles que da lugar a caracterizaciones lógicas y procedimientos decidibles.

Inversión

En vez de usar autómatas para reconocer lenguajes de árboles, se pueden expresar propiedades de árboles en lógicas (MSO, cálculo μ modal) y emplear herramientas lógicas para razonar sobre árboles; esta inversión enfatiza la expresividad lógica y la manipulación sintáctica frente a las construcciones automáticas.

Límite

Se aplica a árboles con etiquetado de nodos y estructura de ramificación definida; las variantes (bottom-up, top-down, determinista, no determinista, alternante, de paridad, Rabin) difieren en potencia expresiva y propiedades de cierre; no todas manejan árboles no ordenados o con datos sin extensiones.

Tensión semántica

Tensión entre determinismo y expresividad (los modelos deterministas pueden ser más débiles o caros de construir) y entre técnicas para árboles finitos e infinitos, donde la aceptación en ramas infinitas requiere condiciones de aceptación más ricas y métodos decisionales distintos.

Síntesis

Los Autómatas de Árboles generalizan los autómatas de palabras a estructuras ramificadas: al estructurar ejecuciones a lo largo de nodos y explotar condiciones de aceptación, ofrecen una explicación automata-teórica de las propiedades de árboles que fundamenta resultados de decidibilidad y caracterización lógica para modelos en forma de árbol.