alt=A Büchi automaton|miniatura|Un autòmat Büchi amb dos estats, i , el primer dels quals és l'estat inicial i el segon és l'acceptació. Les seves entrades són infinites paraules sobre els símbols . Com a exemple, accepta la paraula infinita , on denota la repetició infinita d'una cadena. Rebutja la paraula infinita . En informàtica i teoria d'autòmats, un autòmat de Büchi determinista és una màquina teòrica que accepta o rebutja entrades infinites. Aquesta màquina té un conjunt d'estats i una funció de transició, que determina a quin estat s'ha de moure la màquina des del seu estat actual quan llegeix el següent caràcter d'entrada. Alguns estats accepten estats i un estat és l'estat inicial. La màquina accepta una entrada si i només si passarà per un estat d'acceptació infinites vegades mentre llegeix l'entrada.
Un autòmat Büchi no determinista, més tard anomenat autòmat Büchi, té una funció de transició que pot tenir múltiples sortides, donant lloc a molts camins possibles per a la mateixa entrada; accepta una entrada infinita si i només si accepta algun camí possible. Els autòmats de Büchi deterministes i no deterministes generalitzen els autòmats finits deterministes i els autòmats finits no deterministes a entrades infinites. Cadascun són tipus de ω-autòmats. Els autòmats de Büchi reconeixen els llenguatges ω-regulars, la versió infinita de les llengües regulars. Reben el nom del matemàtic suís Julius Richard Büchi, que els va inventar el 1962.
Els autòmats de Büchi s'utilitzen sovint en la verificació de models com a versió teòrica d'autòmats d'una fórmula en lògica temporal lineal.
Definició formal Formalment, un autòmat de Büchi determinista és una tupla A = ( Q ,Σ,δ, q 0, F) que consta dels components següents:
Q és un conjunt finit. Els elements de Q s'anomenen estats de A. Σ és un conjunt finit anomenat alfabet de A. δ: Q × Σ → Q és una funció, anomenada funció de transició de A. q 0 és un element de Q, anomenat estat inicial de A. F ⊆ Q és la condició d'acceptació. A accepta exactament aquelles execucions en què es troba almenys un dels estats que es produeixen amb freqüència infinita F.
En un autòmat de Büchi (no determinista), la funció de transició δ es substitueix per una relació de transició Δ que retorna un conjunt d'estats, i l'estat inicial únic q 0 es substitueix per un conjunt I d'estats inicials. Generalment, el terme autòmat Büchi sense qualificador fa referència a autòmats Büchi no deterministes.
Per a un formalisme més complet, vegeu també ω-automaton.
Propietats de tancament El conjunt d'autòmats Büchi està tancat sota les operacions següents.
Sigui i uns autòmats de Büchi i un autòmat finit.
Unió : Hi ha un autòmat Büchi que reconeix el llenguatge
Prova: si suposem, wlog, aleshores està buit és reconegut per l'autòmat Büchi
Intersecció : Hi ha un autòmat Büchi que reconeix el llenguatge
Prova: L'autòmat Büchi reconeix o
Per construcció, és una execució de l'autòmat A' a la paraula d'entrada w si s'executa de A sobre w i s'executa de B sobre w. està acceptant i s'accepta si r' és la concatenació d'una sèrie infinita de segments finits d'1-estats (estats amb tercer component 1) i 2-estats (estats amb tercer component 2) alternativament. Hi ha aquesta sèrie de segments de r' si r' és acceptat per A'.
Concatenació : Hi ha un autòmat Büchi que reconeix el llenguatge
Prova: si suposem, wlog, està buit llavors l'autòmat Büchi reconeix , on
ω -tancament : Si no conté la paraula buida llavors hi ha un autòmat Büchi que reconeix la llengua *
Prova: L'autòmat Büchi que reconeix es construeix en dues etapes. Primer, construïm un autòmat finit A' tal que A' també reconegui però no hi ha transicions entrants als estats inicials de A'. Així, on Tingueu en compte que perquè no conté la cadena buida. En segon lloc, construirem l'autòmat Büchi A" que reconeix afegint un bucle de tornada a l'estat inicial de A'. Així, , on
Complementació : Hi ha un autòmat Büchi que reconeix el llenguatge
Prova: la prova es presenta aquí.
Algorismes La comprovació de models de sistemes d'estats finits sovint es pot traduir en diverses operacions en autòmats Büchi. A més de les operacions de tancament presentades anteriorment, a continuació es mostren algunes operacions útils per a les aplicacions dels autòmats Büchi.
Referències
Categoria:Informàtica Categoria:Computabilitat