Autómatas de Árboles

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.