Autómata Büchi

Un autómata Büchi con dos estados, y , el primero de los cuales es el estado inicial y el segundo es el de aceptación. Sus entradas son palabras infinitas sobre los símbolos . Como ejemplo, acepta la palabra infinita , donde denota la repetición infinita de una cadena. Rechaza la palabra infinita . ${\displaystyle q_{0}}$ ${\displaystyle q_{1}}$ ${\displaystyle \{a,b\}}$ ${\displaystyle (ab)^{\omega }}$ ${\displaystyle x^{\omega }}$ ${\displaystyle aaab^{\omega }}$

En informática y teoría de autómatas , un autómata Büchi determinista es una máquina teórica que acepta o rechaza infinitas entradas. Este tipo de máquina tiene un conjunto de estados y una función de transición que determina a qué estado debe pasar la máquina desde su estado actual cuando lee el siguiente carácter de entrada. Algunos estados son estados de aceptación y uno de ellos es el estado de inicio. La máquina acepta una entrada si y solo si pasará por un estado de aceptación infinitas veces a medida que lee la entrada.

Un autómata Büchi no determinista , más tarde denominado simplemente autómata Büchi , tiene una función de transición que puede tener múltiples salidas, lo que lleva a muchos caminos posibles para la misma entrada; acepta una entrada infinita si y solo si algún camino posible la acepta. Los autómatas Büchi deterministas y no deterministas generalizan los autómatas finitos deterministas y los autómatas finitos no deterministas a entradas infinitas. Cada uno es un tipo de ω-autómata . Los autómatas Büchi reconocen los lenguajes ω-regulares , la versión de palabras infinitas de los lenguajes regulares . Reciben su nombre del matemático suizo Julius Richard Büchi , quien los inventó en 1962. ^[1]

Los autómatas de Büchi se utilizan a menudo en la comprobación de modelos como una versión teórica de autómatas de una fórmula en lógica temporal lineal .

Definición formal

Formalmente, un autómata Büchi determinista es una tupla A  = ( Q ,Σ,δ, q ₀ , F ) que consta de los siguientes componentes:

• Q es un conjunto finito . Los elementos de Q se denominan estados de A.
• Σ es un conjunto finito llamado alfabeto de A.
• δ:  Q  × Σ →  Q es una función, llamada función de transición de A .
• q ₀ es un elemento de Q , llamado estado inicial de A .
• F ⊆ Q es la condición de aceptación . A acepta exactamente aquellas ejecuciones en las que al menos uno de los estados que ocurren infinitamente a menudo está  en F.

En un autómata Büchi ( no determinista ) , la función de transición δ se reemplaza por una relación de transición Δ que devuelve un conjunto de estados, y el estado inicial único q ₀ se reemplaza por un conjunto I de estados iniciales. En general, el término autómata Büchi sin calificador se refiere a autómatas Büchi no deterministas.

Para un formalismo más completo, véase también ω-autómata .

Propiedades del cierre

El conjunto de autómatas Büchi se cierra bajo las siguientes operaciones.

Sean y autómatas de Büchi y un autómata finito . ${\displaystyle \scriptstyle A=(Q_{A},\Sigma ,\Delta _{A},I_{A},{F}_{A})}$ ${\displaystyle \scriptstyle B=(Q_{B},\Sigma ,\Delta _{B},I_{B},{F}_{B})}$ ${\displaystyle \scriptstyle C=(Q_{C},\Sigma ,\Delta _{C},I_{C},{F}_{C})}$

• Unión : Hay un autómata Büchi que reconoce el lenguaje. ${\displaystyle \scriptstyle L(A)\cup L(B).}$

Prueba: Si suponemos que wlog está vacío , entonces es reconocido por el autómata Büchi ${\displaystyle \scriptstyle Q_{A}\cap Q_{B}}$ ${\displaystyle \scriptstyle L(A)\cup L(B)}$ ${\displaystyle \scriptstyle (Q_{A}\cup Q_{B},\Sigma ,\Delta _{A}\cup \Delta _{B},I_{A}\cup I_{B},{F}_{A}\cup {F}_{B}).}$

• Intersección : Hay un autómata Büchi que reconoce el lenguaje. ${\displaystyle \scriptstyle L(A)\cap L(B).}$

Prueba: El autómata Büchi reconoce dónde ${\displaystyle \scriptstyle A'=(Q',\Sigma ,\Delta ',I',F')}$ ${\displaystyle \scriptstyle L(A)\cap L(B),}$

• ${\displaystyle \scriptstyle Q'=Q_{A}\times Q_{B}\times \{1,2\}}$
• ${\displaystyle \scriptstyle \Delta '=\Delta _{1}\cup \Delta _{2}}$
  • ${\displaystyle \scriptstyle \Delta _{1}=\{((q_{A},q_{B},1),a,(q'_{A},q'_{B},i))|(q_{A},a,q'_{A})\in \Delta _{A}{\text{ and }}(q_{B},a,q'_{B})\in \Delta _{B}{\text{ and if }}q_{A}\in F_{A}{\text{ then }}i=2{\text{ else }}i=1\}}$
  • ${\displaystyle \scriptstyle \Delta _{2}=\{((q_{A},q_{B},2),a,(q'_{A},q'_{B},i))|(q_{A},a,q'_{A})\in \Delta _{A}{\text{ and }}(q_{B},a,q'_{B})\in \Delta _{B}{\text{ and if }}q_{B}\in F_{B}{\text{ then }}i=1{\text{ else }}i=2\}}$
• ${\displaystyle \scriptstyle I'=I_{A}\times I_{B}\times \{1\}}$
• ${\displaystyle \scriptstyle F'=\{(q_{A},q_{B},2)|q_{B}\in F_{B}\}}$

Por construcción, es una ejecución del autómata A' en la palabra de entrada w si es ejecución de A en w y es ejecución de B en w . es aceptante y es aceptante si r' es concatenación de una serie infinita de segmentos finitos de 1-estados (estados con tercer componente 1) y 2-estados (estados con tercer componente 2) alternativamente. Existe tal serie de segmentos de r' si r' es aceptado por A'. ${\displaystyle \scriptstyle r'=(q_{A}^{0},q_{B}^{0},i^{0}),(q_{A}^{1},q_{B}^{1},i^{1}),\dots }$ ${\displaystyle \scriptstyle r_{A}=q_{A}^{0},q_{A}^{1},\dots }$ ${\displaystyle \scriptstyle r_{B}=q_{B}^{0},q_{B}^{1},\dots }$ ${\displaystyle \scriptstyle r_{A}}$ ${\displaystyle \scriptstyle r_{B}}$

• Concatenación : Hay un autómata Büchi que reconoce el lenguaje ${\displaystyle \scriptstyle L(C)\cdot L(A).}$

Prueba: Si suponemos que wlog está vacío , entonces el autómata Büchi reconoce , donde ${\displaystyle \scriptstyle Q_{C}\cap Q_{A}}$ ${\displaystyle \scriptstyle A'=(Q_{C}\cup Q_{A},\Sigma ,\Delta ',I',F_{A})}$ ${\displaystyle \scriptstyle L(C)\cdot L(A)}$

• ${\displaystyle \scriptstyle \Delta '=\Delta _{A}\cup \Delta _{C}\cup \{(q,a,q')|q'\in I_{A}{\text{ and }}\exists f\in F_{C}.(q,a,f)\in \Delta _{C}\}}$
• ${\displaystyle \scriptstyle {\text{ if }}I_{C}\cap F_{C}{\text{ is empty then }}I'=I_{C}{\text{ otherwise }}I'=I_{C}\cup I_{A}}$

• ω-closure : Si no contiene la palabra vacía entonces hay un autómata Büchi que reconoce el lenguaje ${\displaystyle \scriptstyle L(C)}$ ${\displaystyle \scriptstyle L(C)^{\omega }.}$

Demostración: El autómata Büchi que reconoce se construye en dos etapas. Primero, construimos un autómata finito A' tal que A' también reconoce pero no hay transiciones entrantes a estados iniciales de A'. Por lo tanto, donde Nótese que porque no contiene la cadena vacía. En segundo lugar, construiremos el autómata Büchi A" que reconoce agregando un bucle de regreso al estado inicial de A'. Por lo tanto, , donde ${\displaystyle \scriptstyle L(C)^{\omega }}$ ${\displaystyle \scriptstyle L(C)}$ ${\displaystyle \scriptstyle A'=(Q_{C}\cup \{q_{\text{new}}\},\Sigma ,\Delta ',\{q_{\text{new}}\},F_{C}),}$ ${\displaystyle \scriptstyle \Delta '=\Delta _{C}\cup \{(q_{\text{new}},a,q')|\exists q\in I_{C}.(q,a,q')\in \Delta _{C}\}.}$ ${\displaystyle \scriptstyle L(C)=L(A')}$ ${\displaystyle \scriptstyle L(C)}$ ${\displaystyle \scriptstyle L(C)^{\omega }}$ ${\displaystyle \scriptstyle A''=(Q_{C}\cup \{q_{\text{new}}\},\Sigma ,\Delta '',\{q_{\text{new}}\},\{q_{\text{new}}\})}$ ${\displaystyle \scriptstyle \Delta ''=\Delta '\cup \{(q,a,q_{\text{new}})|\exists q'\in F_{C}.(q,a,q')\in \Delta '\}.}$

• Complementación : Hay un autómata Büchi que reconoce el lenguaje ${\displaystyle \scriptstyle \Sigma ^{\omega }/L(A).}$

Prueba: La prueba se presenta aquí .

Idiomas reconocibles

Los autómatas de Büchi reconocen los lenguajes ω-regulares . Utilizando la definición de lenguaje ω-regular y las propiedades de cierre de los autómatas de Büchi mencionadas anteriormente, se puede demostrar fácilmente que se puede construir un autómata de Büchi de modo que reconozca cualquier lenguaje ω-regular. Para la inversa, véase construcción de un lenguaje ω-regular para un autómata de Büchi.

Autómatas Büchi deterministas y no deterministas

Un autómata Büchi no determinista que reconoce ⁠ ⁠ ${\displaystyle (0\cup 1)^{*}0^{\omega }}$

La clase de autómatas Büchi deterministas no es suficiente para abarcar todos los lenguajes omega-regulares. En particular, no existe ningún autómata Büchi determinista que reconozca el lenguaje ⁠ ⁠ ${\displaystyle (0\cup 1)^{*}0^{\omega }}$ , que contiene exactamente palabras en las que 1 aparece solo un número finito de veces. Podemos demostrar por contradicción que no existe tal autómata Büchi determinista. Supongamos que A es un autómata Büchi determinista que reconoce ⁠ ⁠ ${\displaystyle (0\cup 1)^{*}0^{\omega }}$ con el estado final F . A acepta ⁠ ⁠ ${\displaystyle 0^{\omega }}$ . Entonces, A visitará algún estado en F después de leer algún prefijo finito de ⁠ ⁠ ${\displaystyle 0^{\omega }}$ , digamos después de la ⁠ ⁠ ${\displaystyle i_{0}}$ letra. A también acepta la ω-palabra Por lo tanto, para algún ⁠ ⁠ , después del prefijo el autómata visitará algún estado en F . Continuando con esta construcción se genera la palabra ω que hace que A visite algún estado en F infinitas veces y la palabra no está en ⁠ ⁠ Contradicción. ${\displaystyle 0^{i_{0}}10^{\omega }.}$ ${\displaystyle i_{1}}$ ${\displaystyle 0^{i_{0}}10^{i_{1}}}$ ${\displaystyle 0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots }$ ${\displaystyle (0\cup 1)^{*}0^{\omega }.}$

La clase de lenguajes reconocibles por los autómatas Büchi deterministas se caracteriza por el siguiente lema.

Lema: Un lenguaje ω es reconocible por un autómata Büchi determinista si es el lenguaje límite de algún lenguaje regular .

Demostración: Cualquier autómata determinista de Büchi A puede ser visto como un autómata finito determinista A' y viceversa, ya que ambos tipos de autómata se definen como 5-tuplas de los mismos componentes, solo la interpretación de la condición de aceptación es diferente. Mostraremos que ⁠ ⁠ ${\displaystyle L(A)}$ es el lenguaje límite de ⁠ ⁠ ${\displaystyle L(A')}$ . Una ω-palabra es aceptada por A si obligará a A a visitar estados finales infinitamente a menudo. Por lo tanto, infinitos prefijos finitos de esta ω-palabra serán aceptados por A' . Por lo tanto, ⁠ ⁠ ${\displaystyle L(A)}$ es un lenguaje límite de ⁠ ⁠ ${\displaystyle L(A')}$ .

Algoritmos

La comprobación de modelos de sistemas de estados finitos se puede traducir a menudo en diversas operaciones con autómatas de Büchi. Además de las operaciones de cierre presentadas anteriormente, las siguientes son algunas operaciones útiles para las aplicaciones de los autómatas de Büchi.

Determinación

Dado que los autómatas de Büchi deterministas son estrictamente menos expresivos que los autómatas no deterministas, no puede haber un algoritmo para la determinización de los autómatas de Büchi. Pero el teorema de McNaughton y la construcción de Safra proporcionan algoritmos que pueden traducir un autómata de Büchi en un autómata de Müller determinista o en un autómata de Rabin determinista . ^[2]

Comprobación de vacío

El lenguaje reconocido por un autómata Büchi no es vacío si y solo si hay un estado final que es alcanzable desde el estado inicial y se encuentra en un ciclo.

Un algoritmo eficaz que puede comprobar el vacío de un autómata Büchi:

1. Considere el autómata como un gráfico dirigido y descompóngalo en componentes fuertemente conectados (SCC).
2. Ejecute una búsqueda (por ejemplo, una búsqueda en profundidad ) para encontrar qué SCC son accesibles desde el estado inicial.
3. Verifique si hay un SCC no trivial al que se pueda acceder y que contenga un estado final.

Cada uno de los pasos de este algoritmo se puede realizar en el tiempo lineal en el tamaño del autómata, por lo que el algoritmo es claramente óptimo.

Minimización

Minimizar autómatas Büchi deterministas (es decir, dado un autómata Büchi determinista, encontrar un autómata Büchi determinista que reconozca el mismo lenguaje con un número mínimo de estados) es un problema NP-completo. ^[3] Esto contrasta con la minimización de DFA , que se puede realizar en tiempo polinomial.

Variantes

• Autómata Co-Büchi
• Autómata Büchi débil
• Autómata Büchi semideterminista
• Autómata Büchi generalizado

Transformación de otros modelos de descripción a autómatas Büchi no deterministas

DeAutómatas Büchi generalizados(GBA)

Múltiples conjuntos de estados en condición de aceptación pueden ser traducidos a un conjunto de estados mediante una construcción de autómatas, que se conoce como "construcción de conteo". Digamos que A  = (Q,Σ,∆,q ₀ ,{F ₁ ,...,F _n }) es un GBA, donde F ₁ ,...,F _n son conjuntos de estados de aceptación, entonces el autómata Büchi equivalente es A'  = (Q', Σ, ∆',q' ₀ ,F'), donde

• Q' = Q × {1,...,n}
• q'0 ₌ ( _q0,1 )
• ∆' = { ( (q,i), a, (q',j) ) | (q,a,q') ∈ ∆ y si q ∈ F _i entonces j=((i+1) mod n) de lo contrario j=i }
• F'=F1 _× {1}

DeLógica temporal linealfórmula

Aquí se presenta una traducción de una fórmula de lógica temporal lineal a un autómata Büchi generalizado . Y arriba se presenta una traducción de un autómata Büchi generalizado a un autómata Büchi.

DeAutómatas de Muller

Un autómata de Muller dado puede transformarse en un autómata de Büchi equivalente con la siguiente construcción de autómatas. Supongamos que A  = (Q,Σ,∆,Q ₀ ,{F ₀ ,...,F _n }) es un autómata de Muller, donde F ₀ ,...,F _n son conjuntos de estados de aceptación. Un autómata de Büchi equivalente es A'  = (Q', Σ, ∆',Q ₀ ,F'), donde

• Q' = Q ∪  ∪ n i =0 {i} × Fi ×  2 Fi
• ∆'= ∆ ∪ ∆ 1  ∪ ∆ 2 , donde
  • ∆ 1  ={ ( q, a, (i, q', ∅) ) | (q, a, q') ∈ ∆ y q' ∈ F i }
  • ∆ 2 ={ ( (i,q,R), a, (i,q',R') ) | (q,a,q')∈∆ y q,q' ∈ F i y si R=F i entonces R'= ∅ de lo contrario R'=R∪{q} }
• F'= ∪ n i=0 {i} × Fi ×  { Fi }

A' conserva el conjunto original de estados de A y les añade estados adicionales. El autómata Büchi A' simula el autómata Muller A de la siguiente manera: al comienzo de la palabra de entrada, la ejecución de A' sigue a la ejecución de A , ya que los estados iniciales son los mismos y ∆' contiene a ∆. En alguna posición elegida de forma no determinista en la palabra de entrada, A' decide saltar a los estados recién añadidos mediante una transición en ∆ ₁ . Entonces, las transiciones en ∆ ₂ intentan visitar todos los estados de F _i y siguen haciendo crecer R . Una vez que R se vuelve igual a F _i , se restablece al conjunto vacío y ∆ ₂ intenta visitar todos los estados de F _i una y otra vez. Por tanto, si los estados R = F _i se visitan infinitamente a menudo, A' acepta la entrada correspondiente y también lo hace A . Esta construcción sigue de cerca la primera parte de la prueba del teorema de McNaughton .

De las estructuras de Kripke

Sea la estructura de Kripke dada definida por M = ⟨ Q , I , R , L , AP ⟩ donde Q es el conjunto de estados, I es el conjunto de estados iniciales, R es una relación entre dos estados también interpretada como una arista, L es la etiqueta para el estado y AP son el conjunto de proposiciones atómicas que forman  L .

El autómata Büchi tendrá las siguientes características:

${\displaystyle Q_{\text{final}}=Q\cup \{{\text{init}}\}}$

${\displaystyle \Sigma =2^{AP}}$

${\displaystyle I=\{{\text{init}}\}}$

${\displaystyle F=Q\cup \{{\text{init}}\}}$

${\displaystyle \delta =q{\overrightarrow {a}}p}$si ( q , p ) pertenece a R y L ( p ) = a

y init q si q pertenece a I y L ( q ) = a . ${\displaystyle {\overrightarrow {a}}}$

Sin embargo, cabe señalar que existe una diferencia en la interpretación entre las estructuras de Kripke y los autómatas de Büchi. Mientras que las primeras nombran explícitamente la polaridad de cada variable de estado para cada estado, los segundos simplemente declaran que el conjunto actual de variables se cumple o no. No dice absolutamente nada sobre las otras variables que podrían estar presentes en el modelo.

Complementación

En teoría de autómatas , la complementación de un autómata Büchi es la tarea de complementar un autómata Büchi, es decir, construir otro autómata que reconozca el complemento del lenguaje ω-regular reconocido por el autómata Büchi dado. La existencia de algoritmos para esta construcción demuestra que el conjunto de lenguajes ω-regulares está cerrado bajo complementación.

Esta construcción es particularmente difícil en relación con las construcciones para las otras propiedades de cierre de los autómatas de Büchi. La primera construcción fue presentada por Büchi en 1962. ^[4] Más tarde, se desarrollaron otras construcciones que permitieron una complementación eficiente y óptima. ^{[5] [6] [7] [8] [9]}

La construcción de Büchi

Büchi presentó ^[4] una construcción de complemento doblemente exponencial en forma lógica. Aquí, tenemos su construcción en la notación moderna usada en la teoría de autómatas. Sea A  = ( Q ,Σ,Δ, Q ₀ , F ) un autómata de Büchi. Sea ~ _A una relación de equivalencia sobre elementos de Σ ⁺ tal que para cada v,w ∈ Σ ⁺ , v  ~ _A  w si y solo si para todo p,q ∈ Q , A tiene un recorrido de p a q sobre v si y solo si esto es posible sobre w y además A tiene un recorrido vía F de p a q sobre v si y solo si esto es posible sobre w . Cada clase de ~ _A define una función f : Q → 2 ^Q × 2 ^Q de la siguiente manera: para cada estado p ∈ Q , tenemos ( Q ₁ , Q ₂ )= f ( p ), donde Q ₁ = { q ∈ Q | w puede mover el autómata A de p a q } y Q ₂ = { q ∈ Q | w puede mover el autómata A de p a q a través de un estado en F }. Nótese que Q ₂ ⊆ Q ₁ . Si f es una función definible de esta manera, denotamos la clase (única) que define f por L _f .

Los siguientes tres teoremas proporcionan una construcción del complemento de A utilizando las clases de equivalencia de ~ _A .

Teorema 1: ~ _A tiene un número finito de clases equivalentes y cada clase es un lenguaje regular .
Demostración: Puesto que hay un número finito de f : Q → 2 ^Q × 2 ^Q , la relación ~ _A tiene un número finito de clases de equivalencia. Ahora demostramos que L _f es un lenguaje regular. Para p , q ∈ Q e i ∈ {0,1}, sea A _{i , p , q} = ( {0,1}× Q , Σ, Δ ₁ ∪Δ ₂ , {(0, p )}, {( i , q )} ) un autómata finito no determinista , donde Δ ₁ = { ((0, q ₁ ),(0, q ₂ )) | ( q ₁ , q ₂ ) ∈ Δ} ∪ { ((1, q ₁ ),(1, q ₂ )) | ( q ₁ , q ₂ ) ∈ Δ}, y Δ ₂ = { ((0, q ₁ ),(1, q ₂ )) | q ₁ ∈ F ∧ ( q ₁ , q ₂ ) ∈ Δ }. Sea Q' ⊆ Q . Sea α _{p ,Q'} = ∩{ L ( A _{1, p , q} ) | q ∈ Q'}, que es el conjunto de palabras que pueden mover A desde p a todos los estados en Q' a través de algún estado en F . Sea β _{p ,Q'} = ∩{ L ( A _{0, p , q} )- L ( A _{1, p , q} )-{ε} | q ∈ Q'}, que es el conjunto de palabras no vacías que pueden mover A desde p a todos los estados en Q' y no tiene una carrera que pase por ningún estado en F . Sea γ _{p ,Q'} = ∩{ Σ ⁺ - L ( A _{0, p , q} ) | q ∈ Q'}, que es el conjunto de palabras no vacías que no pueden mover Ade p a cualquiera de los estados en Q'. Dado que los lenguajes regulares son cerrados bajo intersecciones finitas y bajo complementos relativos, cada α _{p ,Q'} , β _{p ,Q'} y γ _{p ,Q'} es regular. Por definiciones, L _f = ∩{ α _{p , Q 2} ∩ β _{p , Q 1 - Q 2} ∩ γ _{p , Q - Q 1} | ( Q ₁ , Q ₂ )= f ( p ) ∧ p ∈ Q }.

Teorema 2: Para cada w ∈ Σ ^ω , existen ~ _A clases L _f y L _g tales que w ∈ L _f ( L _g ) ^ω .
Demostración: Utilizaremos el teorema de Ramsey infinito para demostrar este teorema. Sea w = a ₀ a ₁ ... y w ( i , j ) = a _i ... a _{j -1} . Considérese el conjunto de números naturales N . Sean las clases de equivalencia de ~ _A los colores de los subconjuntos de N de tamaño 2. Asignamos los colores de la siguiente manera. Para cada i < j , sea el color de { i , j } la clase de equivalencia en la que aparece w ( i , j ). Por el teorema de Ramsey infinito, podemos encontrar un conjunto infinito X ⊆ N tal que cada subconjunto de X de tamaño 2 tenga el mismo color. Sea 0 < i ₀ < i ₁ < i ₂ .... ∈ X . Sea f una función definitoria de una clase de equivalencia tal que w (0, i ₀ ) ∈ L _f . Sea g una función definitoria de una clase de equivalencia tal que para cada j >0, w ( i _{j -1} , i _j ) ∈ L _g . Entonces w ∈ L _f ( L _g ) ^ω .

Teorema 3: Sean L _f y L _g clases de equivalencia de ~ _A . Entonces L _f ( L _g ) ^ω es un subconjunto de L ( A ) o disjunto de L ( A ).
Demostración: Supóngase que hay una palabra w ∈ L ( A ) ∩ L _f ( L _g ) ^ω , de lo contrario el teorema se cumple trivialmente. Sea r una sucesión aceptante de A sobre la entrada w . Necesitamos demostrar que cada palabra w' ∈ L _f ( L _g ) ^ω también está en L ( A ), es decir, existe una sucesión r' de A sobre la entrada w' tal que un estado en F ocurre en r' infinitamente a menudo. Como w ∈ L _f ( L _g ) ^ω , sea w ₀ w ₁ w ₂ ... = w tal que w ₀ ∈ L _f y para cada i > 0, w _i ∈ L _g . Sea s _i el estado en r después de consumir w ₀ ... w _i . Sea I un conjunto de índices tales que i ∈ I si y solo si el segmento de recorrido en r desde s _i hasta s _{i +1} contiene un estado de F . I debe ser un conjunto infinito. De manera similar, podemos descomponer la palabra w'. Sea w' ₀ w' ₁ w' ₂ ... = w' tal que w' ₀ ∈ L _f y para cada i > 0, w' _i ∈ L _g . Construimos r' inductivamente de la siguiente manera. Sea el primer estado de r' igual a r . Por definición de L _f , podemos elegir un segmento de recorrido en la palabra w' ₀ para llegar a s ₀. Por hipótesis de inducción, tenemos una serie en w' ₀ ...w' _i que llega a s _i . Por definición de L _g , podemos extender la serie a lo largo del segmento de palabra w' _{i +1} de modo que la extensión llegue a s _i+1 y visite un estado en F si i ∈ I . El r' obtenido a partir de este proceso tendrá infinitos segmentos de serie que contienen estados de F , ya que I es infinito. Por lo tanto, r' es una serie aceptante y w' ∈ L ( A ).

Por los teoremas anteriores, podemos representar Σ ^ω - L ( A ) como unión finita de lenguajes ω-regulares de la forma L _f ( L _g ) ^ω , donde L _f y L _g son clases de equivalencia de ~ _A . Por lo tanto, Σ ^ω - L ( A ) es un lenguaje ω-regular. Podemos traducir el lenguaje a un autómata Büchi. Esta construcción es doblemente exponencial en términos del tamaño de A .

Referencias

1. Büchi, JR (1962). "Sobre un método de decisión en aritmética restringida de segundo orden". Obras completas de J. Richard Büchi . Stanford: Stanford University Press. págs. 425–435. doi :10.1007/978-1-4613-8928-6_23. ISBN . 978-1-4613-8930-9. {{cite book}}: |journal=ignorado ( ayuda )
2. Safra, S. (1988), "Sobre la complejidad de los ω-autómatas", Actas del 29.º Simposio anual sobre fundamentos de la informática (FOCS '88) , Washington DC, EE. UU.: IEEE Computer Society, págs. 319-327, doi : 10.1109/SFCS.1988.21948, ISBN 0-8186-0877-3, Número de identificación del sujeto  206559211.
3. Schewe, Sven (2010). "Minimización de la paridad determinista y de los autómatas de Büchi y minimización relativa de los autómatas finitos deterministas". arXiv : 1007.1333 [cs.FL].
4. Büchi, JR (1962), "Sobre un método de decisión en aritmética restringida de segundo orden", Proc. Congreso Internacional sobre Lógica, Método y Filosofía de la Ciencia, Stanford, 1960 , Stanford: Stanford University Press, págs. 1–12.
5. McNaughton, R. (1966), "Prueba y generación de secuencias infinitas mediante un autómata finito", Información y Control , 9 (5): 521–530, doi : 10.1016/s0019-9958(66)80013-x.
6. Sistla, AP; Vardi, MY ; Wolper, P. (1987), "El problema de complementación para autómatas de Büchi con aplicaciones a la lógica temporal", Theoretical Computer Science , 49 (2–3): 217–237, doi : 10.1016/0304-3975(87)90008-9.
7. Safra, S. (octubre de 1988), "Sobre la complejidad de los ω-autómatas", Proc. 29.° Simposio IEEE sobre fundamentos de la informática , White Plains, Nueva York , págs. 319-327.
8. Kupferman, O. ; Vardi, MY (julio de 2001), "Los autómatas alternos débiles no son tan débiles", ACM Transactions on Computational Logic , 2 (3): 408–429, doi :10.1145/377978.377993.
9. Schewe, Sven (2009). Complementación de Büchi hecha estricta. STACS.

• Bakhadyr Khoussainov; Anil Nerode (6 de diciembre de 2012). Teoría de autómatas y sus aplicaciones. Springer Science & Business Media. ISBN 978-1-4612-0171-7.
• Thomas, Wolfgang (1990). "Autómatas en objetos infinitos". En Van Leeuwen (ed.). Handbook of Theoretical Computer Science . Elsevier. págs. 133–164.

Enlaces externos

• "Autómatas de estados finitos en entradas infinitas" (PDF) .
• Vardi, Moshe Y. "Un enfoque teórico de autómatas para la lógica temporal lineal". CiteSeerX  10.1.1.125.8126 .