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 infinitas . Puede considerarse una extensión de los autómatas de árbol finito descendentes a árboles infinitos, o una extensión de los autómatas de palabra infinita a árboles infinitos.

Un autómata finito que opera sobre un árbol infinito fue utilizado por primera vez por Michael Rabin ^{[ 1 ]} 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 relacionados, lo que permite 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${\displaystyle \Sigma }$-árboles etiquetados . Hay muchas definiciones ligeramente diferentes; aquí hay una. Un autómata de árbol infinito (no determinista) es una tupla${\displaystyle A=(\Sigma ,D,Q,q_{0},\delta ,F)}$con los siguientes componentes.

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

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

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 ejecución de un autómata de árbol${\displaystyle A}$más de un${\displaystyle \Sigma }$-árbol etiquetado${\displaystyle (T,V)}$es un${\displaystyle Q}$-árbol etiquetado${\displaystyle (T_{r},r)}$como sigue. Supongamos que el autómata llegó a un nodo${\displaystyle t}$de un árbol de entrada y actualmente se encuentra en estado${\displaystyle q}$. Deja que el nodo${\displaystyle t}$estar etiquetado con${\displaystyle \sigma \in \Sigma }$y${\displaystyle d(t)}$sea ​​su grado de ramificación. Luego, el autómata procede seleccionando una tupla.${\displaystyle (q_{1},...,q_{d(t)})}$del conjunto${\displaystyle \delta (q,\sigma ,d(t))}$y clonándose a sí mismo en${\displaystyle d(t)}$copias. Por cada${\displaystyle 0<i\leq d(t)}$, una copia del autómata pasa al nodo${\displaystyle ti}$y cambia su estado a${\displaystyle q_{i}}$. Esto produce una carrera que es una${\displaystyle Q}$-árbol etiquetado. Formalmente, una carrera${\displaystyle (T_{r},r)}$en el árbol de entrada satisface las dos condiciones siguientes.

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

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

En una carrera${\displaystyle (T_{r},r)}$, un camino infinito está etiquetado 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${\displaystyle F}$, entonces la ejecución es aceptable . Las condiciones de aceptación interesantes son Büchi , Rabin , Streett , Muller y paridad . Si para una entrada${\displaystyle \Sigma }$-árbol etiquetado ${\displaystyle (T,V)}$Si existe una ejecución de aceptación, entonces el árbol de entrada es aceptado por el autómata. El conjunto de todos los árboles aceptados${\displaystyle \Sigma }$Los árboles etiquetados se denominan lenguaje de árboles.${\displaystyle {\mathcal {L}}(A)}$que es reconocido por el autómata de árbol${\displaystyle A}$.

Los autómatas de árboles de Muller, Rabin, Streett y paridad no deterministas 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${\displaystyle \{a,b\}}$-árboles etiquetados cuyo camino tiene solo un número finito de${\displaystyle a}$s, véase, por ejemplo ^{, [ 3 ]} ). Además, los autómatas de árboles deterministas (Muller, Rabin, Streett, paridad, Büchi, bucles) 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 los árboles binarios cuya raíz tiene su hijo izquierdo o derecho marcado con${\displaystyle a}$Esto contrasta marcadamente 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.

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

• Wolfgang Thomas (1990). "Autómatas sobre 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 (eds.). Autómatas de árboles y lenguajes . Estudios en informática e inteligencia artificial. Vol.  10. Ámsterdam: North-Holland. pp. 189–200 .