En la teoría de los autómatas , una rama de la informática teórica , un ω -autómata (o autómata de flujo ) es una variación de un autómata finito que se ejecuta con cadenas infinitas, en lugar de finitas, como entrada. Dado que los ω-autómatas no se detienen, tienen una variedad de condiciones de aceptación en lugar de simplemente un conjunto de estados de aceptación.
Los ω-autómatas son útiles para especificar el comportamiento de sistemas que no se espera que terminen, como hardware, sistemas operativos y sistemas de control . Para tales sistemas, es posible que desee especificar una propiedad como "para cada solicitud, eventualmente sigue un reconocimiento", o su negación "hay una solicitud que no va seguida de un reconocimiento". La primera es una propiedad de infinitas palabras: no se puede decir de una secuencia finita que satisfaga esta propiedad.
Las clases de ω-autómatas incluyen los autómatas de Büchi , los autómatas de Rabin, los autómatas de Streett, los autómatas de paridad y los autómatas de Muller , cada uno de ellos determinista o no determinista. Estas clases de ω-autómatas difieren sólo en términos de condiciones de aceptación. Todos reconocen precisamente los lenguajes ω regulares excepto el autómata determinista Büchi, que es estrictamente más débil que todos los demás. Aunque todos estos tipos de autómatas reconocen el mismo conjunto de lenguajes ω , difieren en la concisión de la representación de un lenguaje ω determinado.
Formalmente, un autómata ω determinista es una tupla A = ( Q ,Σ,δ, Q 0 , Acc ) que consta de los siguientes componentes:
Una entrada para A es una cadena infinita sobre el alfabeto Σ, es decir, es una secuencia infinita α = ( a 1 , a 2 , a 3 ,...). La ejecución de A en dicha entrada es una secuencia infinita ρ = ( r 0 , r 1 , r 2 ,...) de estados, definida de la siguiente manera:
El objetivo principal de un autómata ω es definir un subconjunto del conjunto de todas las entradas: el conjunto de entradas aceptadas . Mientras que en el caso de un autómata finito ordinario cada ejecución termina con un estado r n y la entrada se acepta si y sólo si r n es un estado de aceptación, la definición del conjunto de entradas aceptadas es más complicada para los ω-autómatas. Aquí debemos mirar todo el recorrido ρ. La entrada se acepta si la ejecución correspondiente está en Acc . El autómata denomina lenguaje ω reconocido al conjunto de palabras ω de entrada aceptadas, que se denota como L(A).
La definición de Acc como un subconjunto de Q ω es puramente formal y no adecuada para la práctica porque normalmente dichos conjuntos son infinitos. La diferencia entre varios tipos de ω-autómatas (Büchi, Rabin, etc.) consiste en cómo codifican ciertos subconjuntos Acc de Q ω como conjuntos finitos y, por tanto, en qué subconjuntos pueden codificar.
Formalmente, un autómata ω no determinista es una tupla A = ( Q ,Σ,Δ, Q 0 , Acc ) que consta de los siguientes componentes:
A diferencia de un autómata ω determinista, que tiene una función de transición δ, la versión no determinista tiene una relación de transición Δ. Tenga en cuenta que Δ puede considerarse como una función: Q × Σ → P ( Q ) de Q × Σ al conjunto de potencias P ( Q ). Por lo tanto, dado un estado q n y un símbolo a n , el siguiente estado q n +1 no está necesariamente determinado de forma única, sino que hay un conjunto de posibles siguientes estados.
Una ejecución de A en la entrada α = ( a 1 , a 2 , a 3 ,...) es cualquier secuencia infinita ρ = ( r 0 , r 1 , r 2 ,...) de estados que satisface las siguientes condiciones :
Un autómata ω no determinista puede admitir muchas ejecuciones diferentes en cualquier entrada determinada, o ninguna en absoluto. La entrada se acepta si al menos una de las ejecuciones posibles es aceptada. La aceptación de una ejecución depende solo de Acc , como ocurre con los autómatas ω deterministas. Todo ω-autómata determinista puede considerarse como un ω-autómata no determinista tomando Δ como la gráfica de δ. Las definiciones de ejecuciones y aceptación de ω-autómatas deterministas son entonces casos especiales de los casos no deterministas.
Las condiciones de aceptación pueden ser conjuntos infinitos de palabras ω. Sin embargo, la gente estudia principalmente condiciones de aceptación que son finitamente representables. A continuación se enumeran una variedad de condiciones de aceptación populares.
Antes de discutir la lista, hagamos la siguiente observación. En el caso de sistemas que se ejecutan infinitamente, a menudo nos interesa saber si cierto comportamiento se repite infinitamente. Por ejemplo, si una tarjeta de red recibe infinitas solicitudes de ping, es posible que no responda a algunas de las solicitudes, pero debería responder a un subconjunto infinito de solicitudes de ping recibidas. Esto motiva la siguiente definición: Para cualquier ejecución ρ, sea Inf(ρ) el conjunto de estados que ocurren infinitamente con frecuencia en ρ. Esta noción de que ciertos estados sean visitados con infinita frecuencia será útil para definir las siguientes condiciones de aceptación.
Todo autómata Büchi puede considerarse un autómata Müller. Basta con sustituir F por F ' que consta de todos los subconjuntos de Q que contienen al menos un elemento de F. De manera similar, cada autómata Rabin, Streett o de paridad también puede considerarse un autómata de Muller.
El siguiente lenguaje ω L sobre el alfabeto Σ = {0,1}, que puede ser reconocido por un autómata Büchi no determinista: L consta de todas las palabras ω en Σ ω en las que 1 aparece sólo un número finito de veces. Un autómata Büchi no determinista que reconoce L necesita sólo dos estados q 0 (el estado inicial) y q 1 . Δ consta de los triples ( q 0 ,0, q 0 ), ( q 0 ,1, q 0 ), ( q 0 ,0, q 1 ) y ( q 1 ,0, q 1 ). F = { q 1 }. Para cualquier entrada α en la que 1 ocurre solo un número finito de veces, hay una ejecución que permanece en el estado q 0 mientras haya 1 para leer, y luego pasa al estado q 1 . Esta ejecución es exitosa. Si hay infinitos unos, entonces sólo hay una ejecución posible: la que siempre permanece en el estado q 0 . (Una vez que la máquina salió de q 0 y alcanzó q 1 , no puede regresar. Si se lee otro 1, no hay un estado sucesor).
Tenga en cuenta que el lenguaje anterior no puede ser reconocido por un autómata Büchi determinista , que es estrictamente menos expresivo que su contraparte no determinista.
Un lenguaje ω sobre un alfabeto finito Σ es un conjunto de palabras ω sobre Σ, es decir, es un subconjunto de Σ ω . Se dice que un lenguaje ω sobre Σ es reconocido por un autómata ω A (con el mismo alfabeto) si es el conjunto de todas las palabras ω aceptadas por A. El poder expresivo de una clase de ω-autómatas se mide por la clase de todos los lenguajes ω que pueden ser reconocidos por algún autómata de la clase.
Los autómatas no deterministas de Büchi, paridad, Rabin, Streett y Muller, respectivamente, reconocen exactamente la misma clase de lenguajes ω. [1] Estos se conocen como cierre ω-Kleene de los lenguajes regulares o como lenguajes ω regulares . Utilizando diferentes pruebas, también se puede demostrar que los autómatas de paridad determinista, Rabin, Streett y Muller reconocen los lenguajes ω regulares. De esto se deduce que la clase de lenguas ω regulares está cerrada bajo complementación. Sin embargo, el ejemplo anterior muestra que la clase de autómatas Büchi deterministas es estrictamente más débil.
Debido a que los autómatas no deterministas de Muller, Rabin, Streett, paridad y Büchi son igualmente expresivos, se pueden traducir entre sí. Usemos la siguiente abreviatura : por ejemplo, NB significa ω-autómata de Büchi no determinista, mientras que DP significa ω-autómata de paridad determinista. Entonces se cumple lo siguiente.
Puede encontrar una descripción general completa de las traducciones en la fuente web a la que se hace referencia. [3]
Los ω-autómatas se pueden utilizar para demostrar la decidibilidad de S1S, la teoría monádica de segundo orden (MSO) de números naturales bajo su sucesor. Los autómatas de árbol infinito extienden los autómatas ω a árboles infinitos y pueden usarse para demostrar la decidibilidad de S2S , la teoría MSO con dos sucesores, y esto puede extenderse a la teoría MSO de gráficos con ancho de árbol acotado (dado un límite fijo) .
