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.
Definición
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.
- es un alfabeto. Este alfabeto se utiliza para etiquetar los nodos de un árbol de entrada.
- 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.
- es un conjunto finito de estados; es inicial.
- es una relación de transición que mapea un estado de autómata , una letra de entrada y un grado a un conjunto de -tuplas de estados.
- 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 uno -tupla.
Correr
Intuitivamente, una ejecución de un árbol autómata 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, un plazo de un autómata árbol sobre un -árbol etiquetado es un -árbol etiquetado como sigue. Supongamos que el autómata llega a un nodo de un árbol de entrada y está actualmente en estado . Deja que el nodo ser etiquetado con y sea su grado de ramificación. Luego, el autómata procede seleccionando una tupla del set y clonarse en copias. Para cada, una copia del autómata pasa al nodo y cambia su estado a . Esto produce una corrida que es una-árbol etiquetado. Formalmente, una carrera en el árbol de entrada cumple las dos condiciones siguientes.
- .
- Para cada con , existe un tal que por cada , tenemos y .
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.
Condición de aceptación
En una carrera , 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, entonces la carrera está aceptando . Las condiciones de aceptación interesantes son Büchi , Rabin , Streett , Muller y parity . Si por una entrada-árbol etiquetado , existe una ejecución de aceptación, entonces el autómata acepta el árbol de entrada . El conjunto de todos aceptados-los árboles etiquetados se llama lenguaje de árbol que es reconocido por el autómata del árbol.
Poder expresivo de las condiciones de aceptación
Los autómatas no deterministas de Muller, Rabin, Streett y de árbol de paridad reconocen el mismo conjunto de lenguajes de árbol y, por lo 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 un autómata de árbol Büchi que reconozca el conjunto de-arboles etiquetados cuyos caminos tienen solo un número finito s, ver eg [3] ) Además, los autómatas de árbol deterministas (Muller, Rabin, Streett, parity, Büchi, looping) son estrictamente menos expresivos que sus variantes no deterministas. Por ejemplo, no existe un autómata de árbol determinista que reconozca el lenguaje de árboles binarios cuya raíz tiene su hijo izquierdo o derecho marcado con. Esto contrasta fuertemente con los autómatas de palabras infinitas , donde los autómatas ω no deterministas de Büchi tienen el mismo poder expresivo que los demás.
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
- ^ Rabin, MO: Decidibilidad de las teorías y autómatas de segundo orden en árboles infinitos , Transactions of the American Mathematical Society , vol. 141, págs. 1-35, 1969.
- ^ 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.
- ^ Ong, Luke, Autómatas, lógica y juegos (PDF) , págs.92 (Teorema 6.1)
- Wolfgang Thomas (1990). "Autómatas en objetos infinitos". En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de Informática Teórica. B . Elsevier. págs. 133-191.En particular: Part II Automata on Infinite Trees , pp.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 e idiomas de árboles . Estudios en Informática e Inteligencia Artificial. 10 . Amsterdam: Holanda Septentrional. págs. 189-200.