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 infinitas palabras 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. Una máquina de este tipo 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 aceptan estados y un estado es el estado inicial. La máquina acepta una entrada si y sólo si pasará por un estado de aceptación infinitas veces mientras 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 muchas rutas posibles para la misma entrada; acepta una entrada infinita si y solo si alguna ruta posible la acepta. Los autómatas de Büchi deterministas y no deterministas generalizan los autómatas finitos deterministas y los autómatas finitos no deterministas a entradas infinitas. Cada uno de ellos son tipos de ω-autómatas . Los autómatas Büchi reconocen los lenguajes ω-regulares , la versión de palabras infinitas de los lenguajes regulares . Llevan el 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 verificación de modelos como una versión teórica de autómatas de una fórmula en lógica temporal lineal .

Definicion 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 llaman 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 con frecuencia está en  F .

En un autómata Büchi ( no determinista ) , la función de transición δ se reemplaza con 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. Generalmente, el término autómata Büchi sin calificativo se refiere a autómatas Büchi no deterministas.

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

Propiedades de cierre

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

Sea y sea autómata de Büchi y sea 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 : Existe un autómata Büchi que reconoce el idioma. ${\displaystyle \scriptstyle L(A)\cup L(B).}$

Prueba: si asumimos 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 idioma. ${\displaystyle \scriptstyle L(A)\cap L(B).}$

La 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 se ejecuta A en w y se ejecuta B en w . se acepta y se acepta si r' es la 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 A' acepta r'. ${\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 idioma. ${\displaystyle \scriptstyle L(C)\cdot L(A).}$

Prueba: si asumimos que wlog está vacío , entonces el autómata Büchi reconoce dónde ${\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}}$

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

Prueba: 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 los estados iniciales de A'. Entonces, tenga en cuenta que porque no contiene la cadena vacía. En segundo lugar, construiremos el autómata Büchi A" que reconoce agregando un bucle al estado inicial de A'. Entonces , 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 : Existe un autómata Büchi que reconoce el idioma. ${\displaystyle \scriptstyle \Sigma ^{\omega }/L(A).}$

Prueba: La prueba se presenta aquí .

Idiomas reconocibles

Los autómatas Büchi reconocen los lenguajes ω-regulares . Utilizando la definición de lenguaje ω-regular y las propiedades de cierre anteriores de los autómatas Büchi, se puede demostrar fácilmente que se puede construir un autómata Büchi de manera que reconozca cualquier lenguaje ω-regular determinado. Para lo contrario, consulte construcción de un lenguaje ω-regular para un autómata Büchi.

Autómatas Büchi deterministas versus 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 , que contiene exactamente palabras en las que 1 aparece sólo 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 con el conjunto de estados finales F. A acepta . Entonces, A visitará algún estado en F después de leer algún prefijo finito de , digamos después de la enésima letra. A también acepta la palabra ω. Por lo tanto, para algunos , 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 infinitamente veces y la palabra no esté en contradicción. ${\displaystyle (0\cup 1)^{*}0^{\omega }}$ ${\displaystyle (0\cup 1)^{*}0^{\omega }}$ ${\displaystyle 0^{\omega }}$ ${\displaystyle 0^{\omega }}$ ${\displaystyle i_{0}}$ ${\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 deterministas de Büchi 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 .

Prueba: Cualquier autómata Büchi determinista A puede verse 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. Demostraremos que es el lenguaje límite de . A acepta una palabra ω si obliga a A a visitar estados finales con una frecuencia infinita. Por lo tanto, A' aceptará infinitos prefijos finitos de esta palabra ω . Por tanto, es un lenguaje límite de . ${\displaystyle L(A)}$ ${\displaystyle L(A')}$ ${\displaystyle L(A)}$ ${\displaystyle L(A')}$

Algoritmos

La verificación de modelos de sistemas de estados finitos a menudo se puede traducir en varias operaciones en 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 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 determinació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 determinista de Muller o un autómata determinista de Rabin . ^[2]

Comprobación de vacío

El lenguaje reconocido por un autómata Büchi no está vacío si y sólo 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, la búsqueda en profundidad ) para encontrar qué SCC son accesibles desde el estado inicial.
3. Compruebe si existe 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 tiempo lineal en el tamaño del autómata, de ahí que el algoritmo sea claramente óptimo.

Minimización

Minimizar los 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

De autómatas de Büchi generalizados (GBA)

Se pueden traducir múltiples conjuntos de estados en condiciones de aceptación en un conjunto de estados mediante una construcción de autómata, lo 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 aceptantes y luego el autómata Büchi equivalente. es A'  = (Q', Σ, ∆',q' ₀ ,F'), donde

• Q' = Q × {1,...,n}
• q' ₀ = ( q ₀ ,1 )
• ∆' = { ( (q,i), a, (q',j) ) | (q,a,q') ∈ ∆ y si q ∈ F _i entonces j=((i+1) mod n) else j=i }
• F'=F ₁ × {1}

De la fórmula de lógica temporal lineal

Aquí se proporciona 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.

De los autómatas de Müller

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

• Q' = Q ∪  ∪ ⁿ _i=0 {i} × F _yo  × 2 ^{F _yo}
• ∆'= ∆ ∪ ∆ ₁  ∪ ∆ ₂ , donde
  • ∆ ₁  ={ ( q, a, (i,q',∅) ) | (q, a, q') ∈ ∆ y q' ∈ F _i }
  • ∆ ₂ ={ ( (i,q,R), a, (i,q',R') ) | (q,a,q')∈∆ y q,q' ∈ F _i y si R=F _i entonces R'= ∅ en caso contrario R'=R∪{q} }
• F'= ∪ ^norte _yo=0 {i} × F _yo  × {F _yo }

A' mantiene el conjunto original de estados de A y les agrega 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 ∆. En alguna posición elegida de forma no determinista en la palabra de entrada, A' decide saltar a estados recién agregados mediante una transición en ∆ ₁ . Entonces, las transiciones en ∆ ₂ intentan visitar todos los estados de F _i y siguen creciendo 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. Entonces, si los estados R = F _i se visitan con una frecuencia infinita, entonces A' acepta la entrada correspondiente y A también . Esta construcción sigue de cerca la primera parte de la demostración del teorema de McNaughton .

De las estructuras Kripke

Dejemos que la estructura de Kripke dada se defina 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 del 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

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

Sin embargo, tenga en cuenta que existe una diferencia en la interpretación entre las estructuras de Kripke y los autómatas de Büchi. Mientras que el primero nombra explícitamente la polaridad de cada variable de estado para cada estado, el segundo simplemente declara 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.

Referencias

1. Büchi, JR (1962). "Sobre un método de decisión en aritmética de segundo orden restringido". Las obras completas de J. Richard Büchi . Stanford: Prensa de la Universidad de Stanford. 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. , doi :10.1109/SFCS.1988.21948, ISBN 0-8186-0877-3, S2CID  206559211.
3. Schewe, Sven (2010). "Minimización de la paridad determinista y autómatas Büchi y minimización relativa de autómatas finitos deterministas". arXiv : 1007.1333 [cs.FL].

• Bakhadyr Khoussainov; Anil Nerode (6 de diciembre de 2012). Teoría de los autómatas y sus aplicaciones. Medios de ciencia y negocios de Springer. ISBN 978-1-4612-0171-7.
• Thomas, Wolfgang (1990). "Autómatas sobre infinitos objetos". En Van Leeuwen (ed.). Manual de informática teórica . Elsevier. págs. 133-164.

enlaces externos

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