Autómata de árbol infinito

---

En informática y lógica matemática , un autómata de árbol infinito es una máquina de estado que se ocupa de estructuras de árbol infinito . Puede verse como una extensión de los autómatas de árbol finito de arriba hacia abajo a árboles infinitos o como una extensión de los autómatas de palabra infinita a árboles infinitos.

Michael Rabin ^[1] utilizó por primera vez un autómata finito que se ejecuta en un árbol infinito para probar la decidibilidad de la lógica monádica de segundo orden . Se ha observado además que los autómatas de árbol y las teorías lógicas están estrechamente conectados y permite que los problemas de decisión en lógica se reduzcan a problemas de decisión para autómatas.

Los autómatas de árbol infinito trabajan en árboles etiquetados . Hay muchas definiciones ligeramente diferentes; acá hay uno. Un autómata de árbol infinito (no determinista) es una tupla con los siguientes componentes.${\ estilo de visualización \ Sigma}$${\displaystyle A=(\Sigma,D,Q,q_{0},\delta,F)}$

Un autómata de árbol infinito es determinista si para cada , y , la relación de transición tiene exactamente una -tupla.${\ estilo de visualización q \ en Q}$${\ estilo de visualización \ sigma \ en \ Sigma}$${\ estilo de visualización d \ en D}$${\ estilo de visualización \ delta (q, \ sigma, d)}$${\ estilo de visualización d}$

Intuitivamente, una ejecución de un autómata de árbol en un árbol de entrada asigna estados de autómata a los nodos del árbol de una manera que satisface la relación de transición de autómata. Un poco más formalmente, una ejecución de un autómata de árbol sobre un árbol con etiqueta es un árbol con etiqueta de la siguiente manera. Suponga que el autómata llegó a un nodo de un árbol de entrada y actualmente se encuentra en el estado . Deje que el nodo sea ​​etiquetado con y sea ​​su grado de ramificación. Luego, el autómata procede seleccionando una tupla del conjunto y clonándose en copias. Para cada uno, una copia del autómata procede al nodo y cambia su estado a${\ estilo de visualización A}$${\ estilo de visualización \ Sigma}$${\ estilo de visualización (T, V)}$${\ estilo de visualización Q}$${\ estilo de visualización (T_ {r}, r)}$${\ estilo de visualización t}$${\ estilo de visualización q}$${\ estilo de visualización t}$${\ estilo de visualización \ sigma \ en \ Sigma}$${\ estilo de visualización d (t)}$${\ estilo de visualización (q_{1},...,q_{d(t)})}$${\ estilo de visualización \ delta (q, \ sigma, d (t))}$${\ estilo de visualización d (t)}$${\displaystyle 0<i\leq d(t)}$${\displaystyle ti}$${\ estilo de visualización q_ {i}}$. Esto produce una ejecución que es un árbol etiquetado. Formalmente, una ejecución en el árbol de entrada satisface las siguientes dos condiciones.${\ estilo de visualización Q}$${\ estilo de visualización (T_ {r}, r)}$

---