Autómata del árbol infinito

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

Michael Rabin ^[1] utilizó por primera vez un autómata finito que corre sobre un árbol infinito para demostrar la decidibilidad de la lógica monádica de segundo orden . Además, se ha observado que los árboles autómatas 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 los autómatas.

Los autómatas de árbol infinito funcionan 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. ${\ Displaystyle \ Sigma}$ ${\ Displaystyle A = (\ Sigma, D, Q, q_ {0}, \ delta, F)}$

Un autómata infinita de árboles es determinista si para todo , y , la relación de transición tiene exactamente una tupla. ${\ Displaystyle q \ in Q}$ ${\ Displaystyle \ sigma \ in \ Sigma}$ ${\ Displaystyle d \ in D}$ ${\ Displaystyle \ delta (q, \ sigma, d)}$ ${\ Displaystyle 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 del autómata. Un poco más formalmente, una corrida de un autómata de árbol sobre un árbol etiquetado es un árbol etiquetado como sigue. Suponga que el autómata alcanzó un nodo de un árbol de entrada y está actualmente en estado . Deje que el nodo esté etiquetado con y sea su grado de ramificación. Luego, el autómata procede a seleccionar una tupla del conjunto y clonarse a sí mismo en copias. Para cada uno, una copia del autómata pasa al nodo y cambia su estado a ${\ Displaystyle A}$ ${\ Displaystyle \ Sigma}$ ${\ Displaystyle (T, V)}$ ${\ displaystyle Q}$ ${\ Displaystyle (T_ {r}, r)}$ ${\ Displaystyle t}$ ${\ Displaystyle q}$ ${\ Displaystyle t}$ ${\ Displaystyle \ sigma \ in \ Sigma}$ ${\ Displaystyle d (t)}$ ${\ Displaystyle (q_ {1}, ..., q_ {d (t)})}$ ${\ Displaystyle \ delta (q, \ sigma, d (t))}$ ${\ Displaystyle d (t)}$ ${\ Displaystyle 0 <i \ leq d (t)}$ ${\ displaystyle ti}$ ${\ Displaystyle q_ {i}}$ . Esto produce una corrida que es un árbol etiquetado. Formalmente, una ejecución en el árbol de entrada satisface las dos condiciones siguientes. ${\ displaystyle Q}$ ${\ Displaystyle (T_ {r}, r)}$