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 entradas infinitas. Dicha máquina tiene un conjunto de estados y una función de transición, que determina a qué estado debe moverse 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 de inicio. La máquina acepta una entrada si y solo 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 muchos caminos posibles para la misma entrada; acepta una entrada infinita si y solo si se acepta alguna ruta posible. 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 son tipos de ω-autómatas . Los autómatas Büchi reconocen los idiomas regulares ω , la versión de palabras infinitas de los idiomas regulares . Llevan el nombre del matemático suizo Julius Richard Büchi , quien los inventó en 1962. [1]
Los autómatas 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 0 , F ) que consta de los siguientes componentes:
- Q es un conjunto finito . Los elementos de Q se llaman los estados de A .
- Σ es un conjunto finito llamado el alfabeto de la A .
- δ: Q × Σ → Q es una función, llamada función de transición de A .
- q 0 es un elemento de Q , llamado el estado inicial de A .
- F ⊆ Q es la condición de aceptación . A acepta exactamente esas carreras en el que al menos uno de los estados infinitamente a menudo ocurren está en F .
En un autómata de 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 0 se reemplaza por un conjunto I de estados iniciales. Generalmente, el término autómata Büchi sin calificador se refiere a los 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.
Dejar y ser autómatas Büchi y ser un autómata finito .
- Unión : Existe un autómata Büchi que reconoce el idioma
- Prueba: si asumimos, wlog , está vacío entonces es reconocido por el autómata Büchi
- Intersección : hay un autómata Büchi que reconoce el idioma
- Prueba: el autómata Büchi reconoce dónde
- Por construcción, es una ejecución del autómata A 'en la palabra de entrada w si se ejecuta de A en w y se ejecuta de B en w . está aceptando y acepta si r 'es la concatenación de una serie infinita de segmentos finitos de estados 1 (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 '.
- Concatenación : existe un autómata Büchi que reconoce el idioma
- Prueba: si asumimos, wlog , está vacío, entonces el autómata Büchi reconoce , dónde
- ω-cierre : Si no contiene la palabra vacía, entonces hay un autómata Büchi que reconoce el idioma
- 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, dónde 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, , dónde
- Complementación : Existe un autómata Büchi que reconoce el idioma
- Prueba: la prueba se presenta aquí .
Idiomas reconocibles
Los autómatas Büchi reconocen los lenguajes regulares ω . Usando la definición de lenguaje regular ω y las propiedades de cierre anteriores de los autómatas Büchi, se puede mostrar fácilmente que un autómata Büchi puede construirse de manera que reconozca cualquier lenguaje regular ω dado. Para el caso contrario, consulte la construcción de un lenguaje regular for para un autómata Büchi.
Autómatas Büchi deterministas versus no deterministas
La clase de autómatas deterministas de Büchi no es suficiente para abarcar todos los lenguajes omega-regulares. En particular, no existe un autómata Büchi determinista que reconozca el lenguaje, que contiene exactamente palabras en las que 1 aparece solo un número finito de veces. Podemos demostrarlo por contradicción que no existe tal autómata Büchi determinista. Supongamos que A es un autómata Büchi determinista que reconocecon el conjunto de estado final F . A acepta. Entonces, A visitará algún estado en F después de leer algún prefijo finito de, di después de la a 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 la palabra ωse genera lo que hace que A visite algún estado en F infinitamente a menudo y la palabra no está en Contradicción.
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ómatas se definen como 5-tuplas de los mismos componentes, solo la interpretación de la condición de aceptación es diferente. Te mostraremos que es el lenguaje límite de . A acepta una palabra ω si obliga a A a visitar estados finales infinitamente a menudo. si, A ' aceptará un número infinito de prefijos finitos de esta palabra ω . Por eso, es un lenguaje límite de .
Algoritmos
La verificación de modelos de sistemas de estados finitos a menudo se puede traducir en varias operaciones en autómatas 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 deterministas de Büchi son estrictamente menos expresivos que los 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 solo si hay un estado final que sea alcanzable desde el estado inicial y que se encuentre en un ciclo.
Un algoritmo eficaz que puede comprobar el vacío de un autómata Büchi:
- Considere el autómata como un gráfico dirigido y descompóngalo en componentes fuertemente conectados (SCC).
- Ejecute una búsqueda (por ejemplo, la búsqueda en profundidad ) para encontrar qué SCC son accesibles desde el estado inicial.
- Compruebe si hay un SCC no trivial que sea accesible y 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, por lo que el algoritmo es claramente óptimo.
- Minimización
El algoritmo para minimizar el autómata finito no determinista también minimiza correctamente un autómata Büchi. El algoritmo no garantiza un autómata Büchi mínimo [ aclaración necesaria ] . Sin embargo, los algoritmos para minimizar el autómata finito determinista no funcionan para el autómata Büchi determinista.
Variantes
Transformación de otros modelos de descripción a autómatas Büchi no deterministas
De los autómatas Büchi generalizados (GBA)
- Múltiples conjuntos de estados en condición de aceptación pueden traducirse en un conjunto de estados mediante una construcción de autómatas , que se conoce como "construcción de conteo". Digamos que A = (Q, Σ, ∆, q 0 , {F 1 , ..., F n }) es un GBA, donde F 1 , ..., F n son conjuntos de estados de aceptación, entonces el autómata Büchi equivalente es A ' = (Q', Σ, ∆ ', q' 0 , F '), donde
- Q '= Q × {1, ..., n}
- q ' 0 = (q 0 , 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 × {1}
De la fórmula lógica temporal lineal
- Aquí se ofrece una traducción de una fórmula lógica temporal lineal a un autómata Büchi generalizado . Y, una traducción de un autómata Büchi generalizado a un autómata Büchi se presenta arriba.
De los autómatas Muller
- Un autómata Muller dado se puede transformar en un autómata Büchi equivalente con la siguiente construcción de autómatas . Supongamos que A = (Q, Σ, ∆, Q 0 , {F 0 , ..., F n }) es un autómata de Muller, donde F 0 , ..., F n son conjuntos de estados de aceptación. Un autómata Büchi equivalente es A ' = (Q', Σ, ∆ ', Q 0 , F'), donde
- Q'= Q ∪ ∪ n i = 0 {i} x F i × 2 F i
- ∆ '= ∆ ∪ ∆ 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} x F i × {F i }
- 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 a través de una transición en ∆ 1 . A continuación, las transiciones en Δ 2 tratar de 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 ∆ 2 intenta visitar todos los estados de F i una y otra vez. Así pues, si los estados R = F i son visitados infinitamente a menudo entonces A' acepta la entrada correspondiente y lo mismo ocurre A . Esta construcción sigue de cerca la primera parte de la demostración del teorema de McNaughton .
De estructuras Kripke
- Que la propuesta estructura Kripke ser definido por M = ⟨ Q , I , R , L , AP ⟩ donde Q es el conjunto de estados, que es el conjunto de estados iniciales, R es una relación entre dos estados también interpretado como un borde, L es la etiqueta para el Estado y AP son el conjunto de las proposiciones atómicas que forma L .
- El autómata Büchi tendrá las siguientes características:
- si ( q , p ) pertenece a R y L ( p ) = a
- y init q si q pertenece a I y L ( q ) = a .
- Sin embargo, tenga en cuenta que existe una diferencia en la interpretación entre las estructuras de Kripke y los autómatas Büchi. Mientras que el primero nombra explícitamente la polaridad de cada variable de estado para cada estado, el segundo simplemente declara el conjunto actual de variables que se mantienen o no son verdaderas. No dice absolutamente nada sobre las otras variables que podrían estar presentes en el modelo.
Referencias
- ↑ Büchi, JR (1962). "Sobre un método de decisión en aritmética restringida de segundo orden". Proc. Congreso Internacional de Lógica, Método y Filosofía de la Ciencia. 1960 . Stanford: Stanford University Press: 425–435. doi : 10.1007 / 978-1-4613-8928-6_23 . ISBN 978-1-4613-8930-9.
- ^ Safra, S. (1988), "Sobre la complejidad de los ω-autómatas", Actas del 29º Simposio Anual sobre Fundamentos de la Ciencia de la Computación (FOCS '88) , Washington DC, EE. UU .: IEEE Computer Society, págs. 319–327, doi : 10.1109 / SFCS.1988.21948 , S2CID 206559211.
- Bakhadyr Khoussainov; Anil Nerode (6 de diciembre de 2012). Teoría de los autómatas y sus aplicaciones . Springer Science & Business Media. ISBN 978-1-4612-0171-7.
- Thomas, Wolfgang (1990). "Autómatas sobre objetos infinitos". En Van Leeuwen (ed.). Manual de Informática Teórica . Elsevier. págs. 133-164.
enlaces externos
- "Autómatas de estado finito en entradas infinitas" (PDF) . Cite journal requiere
|journal=
( ayuda ) - Vardi, Moshe Y. "Un enfoque teórico de los autómatas para la lógica temporal lineal". CiteSeerX 10.1.1.125.8126 . Cite journal requiere
|journal=
( ayuda )