ω-autómata
En la teoría de autómatas , una rama de la informática teórica , un autómata ω (o autómata de flujo ) es una variación de autómatas finitos que se ejecuta en 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 los sistemas que no se espera que terminen, como el hardware, los sistemas operativos y los sistemas de control . Para tales sistemas, uno puede querer especificar una propiedad como "para cada solicitud, eventualmente sigue un reconocimiento", o su negación "hay una solicitud que no es seguida por un reconocimiento". La primera es una propiedad de infinitas palabras: no se puede decir de una sucesión finita que satisface 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 determinista o no determinista. Estas clases de autómatas ω difieren solo en términos de condiciones de aceptación . Todos reconocen con precisión 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 para un lenguaje ω dado.
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 tal entrada es una secuencia infinita ρ = ( r 0 , r 1 , r 2 ,...) de estados, definida como sigue:
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 solo si r n es un estado de aceptación, la definición del conjunto de entradas aceptadas es más complicada para ω-autómatas. Aquí debemos mirar toda la corrida ρ. La entrada se acepta si la ejecución correspondiente está en Acc . El conjunto de palabras ω de entrada aceptadas se denomina lenguaje ω reconocido por el autómata, que se denota como L(A).
