Los lenguajes ω regulares son una clase de lenguajes ω que generalizan la definición de lenguajes regulares a infinitas palabras. Büchi demostró en 1962 que los lenguajes ω-regulares son precisamente los que se pueden definir en una lógica monádica de segundo orden particular llamada S1S.
Los elementos de A ω se obtienen concatenando palabras de A infinitas veces. Tenga en cuenta que si A es regular, A ω no es necesariamente ω-regular, ya que A podría ser {ε}, el conjunto que contiene solo la cadena vacía , en cuyo caso A ω = A , que no es un lenguaje ω y por lo tanto no un idioma ω-regular.
Teorema : Un autómata Büchi reconoce una lengua ω si y solo si es una lengua regular ω.
Prueba : cada lenguaje ω-regular es reconocido por un autómata Büchi no determinista; la traducción es constructiva. Usando las propiedades de cierre de los autómatas Büchi y la inducción estructural sobre la definición de lenguaje regular ω, se puede demostrar fácilmente que un autómata Büchi puede construirse para cualquier lenguaje regular ω dado.
A la inversa, para un determinado Büchi autómata A = ( Q , Σ, δ, I , F ) , se construye un lenguaje ω-regular y luego vamos a demostrar que este lenguaje es reconocida por A . Para una palabra ω w = a 1 a 2 ... sea w ( i , j ) el segmento finito a i +1 ... a j -1 a j de w . Para cada q , q ' ∈ Q , definimos un lenguaje regular L q, q ' que es aceptado por el autómata finito ( Q , Σ, δ , q , { q' }) .