Autómata de árbol infinito

Estructura matemática

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 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 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 árboles y las teorías lógicas están estrechamente relacionados y esto permite que los problemas de decisión en lógica se reduzcan a problemas de decisión para autómatas.

Definición

Los autómatas de árboles infinitos funcionan en árboles etiquetados . Hay muchas definiciones ligeramente diferentes; Aqui 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)}$

• ${\displaystyle \Sigma }$es un alfabeto. Este alfabeto se utiliza para etiquetar 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 , un árbol de entrada tiene que ser un árbol binario, o si , entonces cada nodo tiene 1, 2 o 3 hijos. ${\displaystyle D=\{2\}}$ ${\displaystyle D=\{1,2,3\}}$
• ${\displaystyle Q}$es un conjunto finito de estados; es inicial. ${\displaystyle q_{0}}$
• ${\displaystyle \delta :Q\times \Sigma \times 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\in Q}$ ${\displaystyle \sigma \in \Sigma }$ ${\displaystyle d\in D}$ ${\displaystyle 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\in Q}$ ${\displaystyle \sigma \in \Sigma }$ ${\displaystyle d\in D}$ ${\displaystyle \delta (q,\sigma ,d)}$ ${\displaystyle d}$

Correr

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 árbol autómata 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 se encuentra en el estado . Sea el nodo etiquetado con y su grado de ramificación. Luego, el autómata procede a seleccionar una tupla del conjunto y clonarse en copias. Para cada uno , una copia del autómata ingresa 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 dos condiciones siguientes. ${\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 t.i}$ ${\displaystyle q_{i}}$ ${\displaystyle Q}$ ${\displaystyle (T_{r},r)}$

• ${\displaystyle r(\epsilon )=q_{0}}$.
• Para cada con , existe tal que para cada , tenemos y . ${\displaystyle t\in 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 t.i\in T_{r}}$ ${\displaystyle r(t.i)=q_{i}}$

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

Condición de aceptación

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

Poder expresivo de las condiciones de aceptación.

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

Referencias

1. Rabin, MO: Decidibilidad de teorías de segundo orden y autómatas en árboles infinitos , Transactions of the American Mathematical Society , vol. 141, págs. 1 a 35, 1969.
2. Rabin, MO: Relaciones débilmente definibles y autómatas especiales , Lógica matemática y fundamento de la teoría de conjuntos , págs. 1-23, 1970.
3. Ong, Luke, Autómatas, lógica y juegos (PDF) , p. 92 (Teorema 6.1)

Literatura

• 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 sobre árboles infinitos , págs. 165-185.
• A. Saoudi y P. Bonizzoni (1992). "Autómatas sobre árboles infinitos y control racional". En Maurice Nivat y Andreas Podelski (ed.). Autómatas y lenguajes de árboles . Estudios en Informática e Inteligencia Artificial. vol. 10. Ámsterdam: Holanda Septentrional. págs. 189-200.