Autómata de árbol infinito

En informática y lógica matemática , un autómata de árbol infinito es una máquina de estados que trabaja con estructuras de árbol infinito . Puede considerarse 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 palabras infinitas a árboles infinitos.

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

Los autómatas de árbol infinito funcionan en árboles etiquetados como . Existen muchas definiciones ligeramente diferentes; aquí hay una. 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)}$

• ${\estilo de visualización \Sigma}$es un alfabeto. Este alfabeto se utiliza para etiquetar nodos de un árbol de entrada.
• ${\displaystyle D\subconjunto \mathbb {N} }$es un conjunto finito de grados de ramificación permitidos en un árbol de entrada. Por ejemplo, si , un árbol de entrada debe ser un árbol binario, o si , entonces cada nodo tiene 1, 2 o 3 hijos.${\displaystyle D=\{2\}}$${\displaystyle D=\{1,2,3\}}$
• ${\estilo de visualización Q}$es un conjunto finito de estados; es inicial.${\displaystyle q_{0}}$
• ${\displaystyle \delta :Q\veces \Sigma \veces D\rightarrow 2^{Q^{*}}}$es una relación de transición que asigna un estado de autómata , una letra de entrada y un grado a un conjunto de -tuplas de estados.${\displaystyle q\en Q}$${\displaystyle \sigma \en \Sigma }$${\displaystyle d\en D}$${\estilo de visualización d}$
• ${\displaystyle F\subseteq Q^{\omega }}$es una condición de aceptación.

Un autómata de árbol infinito es determinista si para cada , , y , la relación de transición tiene exactamente una -tupla. ${\displaystyle q\en Q}$${\displaystyle \sigma \en \Sigma }$${\displaystyle d\en D}$${\displaystyle \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 etiquetado es un árbol etiquetado de la siguiente manera. Supongamos que el autómata llegó a un nodo de un árbol de entrada y actualmente está en el estado . Sea el nodo etiquetado con y su grado de ramificación. Luego, el autómata procede seleccionando una tupla del conjunto y clonándose a sí mismo en copias. Para cada , una copia del autómata procede al nodo y cambia su estado a . 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 A}$${\estilo de visualización \Sigma}$${\estilo de visualización (T,V)}$${\estilo de visualización Q}$${\displaystyle (T_{r},r)}$${\estilo de visualización t}$${\estilo de visualización q}$${\estilo de visualización t}$${\displaystyle \sigma \en \Sigma }$${\estilo de visualización d(t)}$${\displaystyle (q_{1},...,q_{d(t)})}$${\displaystyle \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}}$${\estilo de visualización Q}$${\displaystyle (T_{r},r)}$

• ${\displaystyle r(\epsilon )=q_{0}}$.
• Para cada con , existe un tal que para cada , tenemos y .${\displaystyle t\en T_{r}}$${\displaystyle r(t)=q}$${\displaystyle (q_{1},...,q_{d(t)})\in \delta (q,V(t),d(t))}$${\displaystyle 0<i\leq d(t)}$${\displaystyle ti\in T_{r}}$${\displaystyle r(ti)=q_{i}}$

Si el autómata no es determinista, puede haber varias ejecuciones diferentes en el mismo árbol de entrada; para los autómatas deterministas, la ejecución es única.

En una serie , una ruta infinita está etiquetada por una secuencia de estados. Esta secuencia de estados forma una palabra infinita sobre estados. Si todas estas palabras infinitas pertenecen a la condición de aceptación , entonces la serie es de aceptación . Las condiciones de aceptación interesantes son Büchi , Rabin , Streett , Muller y paridad . Si para un árbol con etiqueta de entrada existe una serie de aceptación, entonces el autómata acepta el árbol de entrada. El conjunto de todos los árboles con etiqueta de aceptación se denomina lenguaje de árbol , que es reconocido por el autómata de árbol . ${\displaystyle (T_{r},r)}$${\estilo de visualización F}$${\estilo de visualización \Sigma}$${\estilo de visualización (T,V)}$${\estilo de visualización \Sigma}$${\displaystyle {\mathcal {L}}(A)}$${\estilo de visualización A}$

Los autómatas de árboles no deterministas de Muller, Rabin, Streett y de paridad reconocen el mismo conjunto de lenguajes de árboles y, por lo tanto, tienen el mismo poder expresivo. Pero los autómatas de árboles de Büchi no deterministas son estrictamente más débiles, es decir, existe un lenguaje de árboles que puede ser reconocido por un autómata de árboles de Rabin pero no puede ser reconocido por ningún autómata de árboles de Büchi. ^[2] (Por ejemplo, no existe ningún autómata de árboles de Büchi que reconozca el conjunto de árboles etiquetados con - cuyo cada camino tiene solo un número finito de s, véase, por ejemplo, ^[3] ). Además, los autómatas de árboles deterministas (Muller, Rabin, Streett, paridad, Büchi, bucle) son estrictamente menos expresivos que sus variantes no deterministas. Por ejemplo, no existe ningún autómata de árboles determinista que reconozca el lenguaje de árboles binarios cuya raíz tiene su hijo izquierdo o derecho marcado con . Esto está en marcado contraste con los autómatas en palabras infinitas , donde los ω-autómatas de Büchi no deterministas tienen el mismo poder expresivo que los demás. ${\estilo de visualización \{a,b\}}$${\estilo de visualización a}$${\estilo de visualización a}$

Los lenguajes de los autómatas no deterministas de Muller/Rabin/Streett/árbol de paridad están cerrados bajo unión, intersección, proyección y complementación.

• Wolfgang Thomas (1990). "Autómatas en objetos infinitos". En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. págs. 133–191.En particular: Parte II Autómatas en árboles infinitos , págs. 165-185.
• A. Saoudi y P. Bonizzoni (1992). "Autómatas en árboles infinitos y control racional". En Maurice Nivat y Andreas Podelski (ed.). Autómatas de árboles y lenguajes . Estudios en informática e inteligencia artificial. Vol. 10. Ámsterdam: Holanda Septentrional. págs. 189-200.