In informatica teorica, un automa di Büchi è un ω-automa o automa finito che opera su parole di lunghezza infinita, con una particolare condizione di accettazione: una traccia ha successo se e solo se passa un numero infinito di volte per almeno uno stato accettante. Questo tipo di automa viene comunemente utilizzato per il model checking.

Questo tipo di automa è stato definito dal matematico Julius Richard Büchi^[1].

Un automa di Büchi su un alfabeto ${\displaystyle \Sigma }$ è un ω-automa ${\displaystyle {\mathcal {A}}=(Q,{\mathcal {F}},I,T)}$, dove

• ${\displaystyle Q}$ è un insieme finito di stati;
• ${\displaystyle {\mathcal {F}}\subset Q\times \Sigma \times Q}$ è l'insieme delle transizioni;
• ${\displaystyle I\subseteq Q}$ è l'insieme degli stati iniziali;
• ${\displaystyle T\subseteq Q}$ è un insieme di stati finali o terminali o accettanti.

Spesso si assume che l'insieme degli stati iniziali sia composto da un singolo elemento. Una transizione ${\displaystyle f=(p,a,q)\in {\mathcal {F}}}$ è composta da uno stato di partenza ${\displaystyle p}$, un'etichetta ${\displaystyle a}$ e uno stato di arrivo ${\displaystyle q}$. Un calcolo ${\displaystyle c}$ (detto anche un percorso o una traccia) è una serie infinita di transizioni consecutive:

${\displaystyle c=(p_{0},a_{1},p_{1})(p_{1},a_{2},p_{2})\cdots }$

Per ${\displaystyle c}$, lo stato iniziale è ${\displaystyle p_{0}}$, la sua etichetta è la parola infinita ${\displaystyle a_{1}a_{2}\cdots a_{n}\cdots }$. Il calcolo ha esito positivo e la parola viene accettata (o riconosciuta dall'automa) se passa infinitamente spesso attraverso uno stato terminale.

Un automa è detto deterministico se soddisfa le due condizioni seguenti:

• possiede un solo stato iniziale;
• per ogni stato ${\displaystyle q}$ e per ogni lettera ${\displaystyle a}$, c'è al massimo una transizione che parte da ${\displaystyle q}$ e recante l'etichetta ${\displaystyle a}$.

L'automa di Büchi ${\displaystyle {\mathcal {A}}=(\{q_{0},q_{1}\},{\mathcal {F}},q_{0},q_{1})}$ su un alfabeto ${\displaystyle \{a,b\}}$ il cui insieme di transizioni ${\displaystyle {\mathcal {F}}}$ è visualizzato nella figura a sinistra.

La parola infinita ${\displaystyle bbbb\cdots }$ non è accettata perché l'unica traccia corrispondente è ${\displaystyle q_{0}q_{0}q_{0}\cdots }$ e l'unico stato che appare un numero infinito di volte è ${\displaystyle q_{0}}$, il quale non è accettante. D'altra parte, la parola ${\displaystyle aaaa\cdots }$ è accettata perché vi corrisponde la traccia ${\displaystyle q_{0}q_{1}q_{1}\cdots }$, e ${\displaystyle q_{1}}$ vi appare un numero infinito di volte ed è uno stato accettante. Più in generale, l'automa accetta le parole infinite sull'alfabeto di due lettere ${\displaystyle a}$ e ${\displaystyle b}$, che contengono solo un numero finito di lettere ${\displaystyle a}$, vale a dire l'espressione regolare ${\displaystyle b^{*}a(a^{*}b^{+}a)^{\omega }}$.

Un altro esempio è l'automa di Büchi deterministico nella figura a destra; l'automa ha tre stati: ${\displaystyle q_{0}}$, ${\displaystyle q_{1}}$ e ${\displaystyle q_{2}}$. Questo automa riconosce le parole infinite in cui ogni occorrenza di ${\displaystyle b}$ è preceduta da un numero pari non nullo di occorrenze di ${\displaystyle a}$. Il calcolo su una parola del linguaggio accettato si avvia nello stato iniziale ${\displaystyle q_{0}}$ e legge un numero pari di ${\displaystyle a}$ (diverso da zero perché la prima ${\displaystyle a}$ determina la transizione in ${\displaystyle q_{1}}$). Se viene letto un numero dispari di ${\displaystyle a}$, l'automa si trova nello stato ${\displaystyle q_{1}}$, altrimenti nello stato ${\displaystyle q_{2}}$ (che è accettante e quindi deve riproporsi un numero infinito di volte nella traccia). La transizione in ${\displaystyle b}$ porta dallo ${\displaystyle q_{2}}$ allo stato ${\displaystyle q_{0}}$ e la sequenza ricomincia.

Gli automi di Büchi deterministici sono strettamente meno espressivi degli automi di Büchi non deterministici^[2][3]. In altri termini, vi sono dei linguaggi riconosciuti da automi di Büchi non deterministici che non possono essere riconosciuti dagli automi di Büchi deterministici.

Gli insiemi di parole infinite riconosciute dagli automi di Büchi corrispondono ai linguaggi ω-regolari, cioè gli insiemi della forma

${\displaystyle \bigcup _{1}^{m}U_{i}V_{i}^{\omega }}$

dove gli ${\displaystyle U_{i}}$ e ${\displaystyle V_{i}}$ sono linguaggi regolari e i ${\displaystyle V_{i}}$ non contengono la parola vuota. Questi linguaggi sono anche chiamati la ω-chiusura di Kleene dei linguaggi regolari^[4].

Per ottenere la formula generica per le espressioni regolari riconosciute da un automa di Büchi, si procede come segue. Dato un automa di Büchi, sia ${\displaystyle W(p,q)}$ l'insieme delle parole finite riconosciute avente ${\displaystyle p}$ come stato iniziale e ${\displaystyle q}$ come stato finale, ossia tutte le parole rappresentate dalle etichette su una traccia da ${\displaystyle p}$ a ${\displaystyle q}$. Questi linguaggi finiti sono regolari. Una parola infinita ${\displaystyle x}$ è accettata se esiste un calcolo che passa un numero infinito di volte da uno stato terminale. Sia ${\displaystyle q}$ questo stato terminale attraverso il quale la traccia passa un numero infinito di volte. Questo equivale a dire

${\displaystyle x\in W(q_{0},q)W(q,q)^{\omega }}$

per uno stato iniziale ${\displaystyle q_{0}}$. Prendendo gli insiemi su tutti gli stati iniziali e terminali, si ottiene la formula data^[4]. Per dimostrare che, reciprocamente, tutti i linguaggi ω-regolari sono riconosciuti dagli automi di Büchi, si usano le operazioni di chiusura^[5].

La descrizione dei linguaggi ω-regolari riconosciuti mostra che il problema della parola è decidibile per gli automi di Büchi, poiché è sufficiente verificare se almeno uno dei linguaggi regolari dati da ${\displaystyle W(q_{0},q)W(q,q)}$ non è vuoto.

I linguaggi riconosciuti dagli automi di Büchi sono chiusi per una serie di operazioni.

• Unione: Siano ${\displaystyle {\mathcal {A}}=(Q_{A},{\mathcal {F}}_{A},I_{A},T_{A})}$ e ${\displaystyle {\mathcal {B}}=(Q_{B},{\mathcal {F}}_{B},I_{B},T_{B})}$ due automi che rispettivamente riconoscono i linguaggi ${\displaystyle L_{A}}$ e ${\displaystyle L_{B}}$. Un automa che riconosce l'unione ${\displaystyle L_{A}\cup L_{B}}$ si ottiene unendo i due automi. Assumendo che gli insiemi di stati ${\displaystyle Q_{A}}$ e ${\displaystyle Q_{B}}$ siano disgiunti: l'automa ${\displaystyle {\mathcal {C}}=(Q_{A}\cup Q_{B},{\mathcal {F}}_{A}\cup {\mathcal {F}}_{B},I_{A}\cup I_{B},T_{A}\cup T_{B})}$ riconosce l'unione ${\displaystyle L_{A}\cup L_{B}}$.

• ω-chiusura: Per ogni linguaggio regolare ${\displaystyle L}$ che non contiene la stringa vuota, l'ω-linguaggio ${\displaystyle L^{\omega }}$ viene riconosciuto da un automa di Büchi. Sia ${\displaystyle {\mathcal {A}}=(Q,{\mathcal {F}},i,T)}$ un automa a stati finiti che riconosce ${\displaystyle L}$. Se ha un solo stato iniziale ${\displaystyle i}$ e nessuna transizione (ossia, l'automa più semplice che è possibile costruire). Si possono aggiungere ad ${\displaystyle {\mathcal {A}}}$ le transizioni ${\displaystyle (q,a,i)}$ per ogni transizione ${\displaystyle (q,a,t)}$ di ${\displaystyle {\mathcal {F}}}$ con ${\displaystyle t\in T}$. L'automa di Büchi così costruito, con un solo stato iniziale che è anche terminale, riconosce ${\displaystyle L^{\omega }}$.

• Concatenazione: Per ogni linguaggio regolare ${\displaystyle L}$ ed ogni ω-linguaggio ${\displaystyle M}$ riconosciuto da un automa di Büchi, il prodotto dei due linguaggi ${\displaystyle L\circ M}$ è un ω-linguaggio riconosciuto da un automa di Büchi.

Le tre proprietà precedenti dimostrano che ogni ω-linguaggio regolare è riconoscibile da un automa di Büchi.

• Intersezione: Siano ${\displaystyle {\mathcal {A}}=(Q_{A},{\mathcal {F}}_{A},I_{A},T_{A})}$ e ${\displaystyle {\mathcal {B}}=(Q_{B},{\mathcal {F}}_{B},I_{B},T_{B})}$ due automi che rispettivamente riconoscono i linguaggi ${\displaystyle L_{A}}$ e ${\displaystyle L_{B}}$. Un automa che riconosce l'intersezione ${\displaystyle L_{A}\cap L_{B}}$ è costruito come segue:

${\displaystyle {\mathcal {C}}=\{Q_{A}\times Q_{B}\times \{0,1,2\},Q_{A}\times Q_{b}\times \{0\},{\mathcal {F}},T\}}$

dove le transizioni di ${\displaystyle {\mathcal {F}}}$ copiano quelle in ${\displaystyle {\mathcal {F_{A}}}}$ e ${\displaystyle {\mathcal {F_{B}}}}$ per i primi due componenti e cambiano il terzo componente da 0 a 1 quando uno stato di ${\displaystyle T_{A}}$ compare nel primo componente, da 1 a 2 quando uno stato di ${\displaystyle T_{B}}$ appare nel secondo componente e torna a 0 immediatamente dopo. In un calcolo, un 2 appare infinitamente spesso come terza componente se e solo se uno stato di ${\displaystyle T_{A}}$ e uno stato di ${\displaystyle T_{B}}$ appaiono infinitamente spesso nella prima e nella seconda componente. Quindi, scegliendo come stati terminali quelli in ${\displaystyle {\mathcal {T}}=Q_{A}\times Q_{b}\times \{2\}}$ otteniamo un automa di Büchi con il comportamento desiderato.

I linguaggi riconosciuti dagli automi di Büchi sono chiusi rispetto alla complementazione. Richard Büchi ne ha dato una dimostrazione nel 1962^[1]. In seguito, sono state date altre costruzioni dell'automa riconoscente il linguaggio complementare di un ω-linguaggio^[6][7][8][9].

Gli automi di Büchi sono equivalenti agli automi di Muller, agli automi di Rabin, agli automi di Streett o automi di parità. Tuttavia, differiscono nella loro concisione. Ad esempio, gli automi di Büchi sono esponenzialmente più concisi degli automi di Rabin nel senso seguente: esiste una famiglia di linguaggi ${\displaystyle (L_{n})_{n=2\ldots }}$ sull'alfabeto {0, 1, #}, riconoscibile da automi di Büchi non deterministici di dimensione O(n), ma ogni automa di Rabin non deterministico che riconosca lo stesso linguaggio deve essere di dimensione almeno n!^[10].

Gli automi di Büchi non deterministici rappresentano esattamente le proprietà della logica monadica del secondo ordine con un successore (S1S), chiamate anche "proprietà ω-regolari". La logica S1S è strettamente più espressiva della logica temporale lineare.

Esiste una condizione duale per l'accettazione degli automi di Büchi: questi sono gli automi co-Büchi. La condizione di accettazione diventa: una traccia (o calcolo o percorso infinito) ha successo se e solo se uno stato che appare un numero finto di volte è uno stato accettante^[11].

Gli automi di Buchi vengono utilizzati nel model checking in cui sorgono quesiti sulle proprietà degli algoritmi. Ad esempio, sapere se il linguaggio accettato da un automa di Büchi non deterministico è vuoto è una proprietà che viene decisa in tempo lineare^[12]. Una formula di logica temporale lineare (LTL) può essere riconosciuta da un automa di Büchi, ma la sua dimensione sarà esponenziale nella dimensione della formula LTL^[13]. Questa trasformazione può essere usata per:

• Decidere il problema di soddisfacibilità di LTL. Questo problema è PSPACE-completo.
• Fare verifiche con il model checking. Per questo si costruisce l'automa di Büchi equivalente alla formula LTL e si fa il prodotto con il sistema da verificare. Il prodotto è un automa di Büchi e la verifica consiste nel testare se il linguaggio accettato è vuoto.

La trasformazione di una formula LTL in un automa di Büchi viene solitamente presentata con un passo intermedio, chiamato automa di Büchi generalizzato, per il quale la condizione di accettazione è più generale. Un automa di Büchi generalizzato è come un automa di Büchi, tranne per il fatto che l'insieme degli stati terminali ${\displaystyle T\subseteq Q}$ è sostituito da un insieme finito ${\displaystyle \{T_{1},\dots ,T_{k}\}}$ con ${\displaystyle T_{i}\subseteq Q}$. La condizione di accettazione diventa la seguente: una traccia ha successo se e solo se per ogni i essa passa un numero infinito di volte per almeno uno stato accettante di ${\displaystyle T_{i}}$.

L'esempio verifica sulle parole dell'alfabeto { ${\displaystyle \top }$, cr1, cr2} la proprietà ${\displaystyle \varphi }$ che occorre "infinitamente spesso nella sezione critica 1, e infinitamente spesso nella sezione critica 2". La lettera ${\displaystyle \top }$ corrisponde ad una sezione non critica, cr1 corrisponde alla sezione critica 1 e cr2 alla sezione critica 2. ${\displaystyle T\subseteq Q}$ è uguale a {{q ₁ }, {q ₂ }}: un'esecuzione accettante deve passare infinitamente spesso per q1 e infinitamente spesso per q2. Questo corrisponde a quanto descritto dalla proprietà ${\displaystyle \varphi }$.

Come primo passo, la formula LTL viene trasformata in un automa di Büchi generalizzato (l'idea è che gli stati dell'automa siano i sottoinsiemi massimi di sotto-formule della formula LTL). Ad esempio, per la proprietà ${\displaystyle \varphi }$ scritta in LTL con ${\displaystyle GFcr_{1}\land GFcr_{2}}$ (sempre in futuro cr1 e sempre in futuro cr2), l'automa generalizzato è dato dall'automa in alto nella figura. Questo automa si trasforma in un normale automa di Büchi facendo una copia dell'automa generalizzato per ogni sottoinsieme ${\displaystyle T_{i}}$. Nell'esempio a lato, viene copiato due volte: la prima copia corrisponde a {q ₁ } e la seconda a {q ₂ }. Una volta che si incontra q ₁, si passa alla seconda copia. Una volta che q ₂ è soddisfatto, si torna alla prima copia. L'automa ottenuto è un classico automa di Büchi e la condizione di accettazione è di passare un'infinità di volte per q ₁ o per q ₂'. Per costruzione, questa condizione equivale a passare un'infinità di volte in q ₁ e un'infinità di volte in q ₂ nell'automa generalizzato.

Esistono algoritmi efficaci per costruire un automa di Büchi equivalente da una formula LTL^[14].

Richard Büchi^[1] ha mostrato che c'è equivalenza, per ogni linguaggio infinito L, tra:

• L è definibile da una proprietà S1S (logica monadica del secondo ordine con un successore);
• L è definibile da una proprietà WS1S (logica monadica di secondo ordine con un successore, detta "debole" (weak), ovvero che la quantificazione del secondo ordine porta su insiemi finiti);
• L è riconoscibile da un automa di Büchi.

Le equivalenze sono effettive: una formula S1S si trasforma in un automa di Büchi. Pertanto, la logica S1S (e WS1S) è decidibile. La logica S1S è di complessità non elementare^[15].

• (EN) Wolfgang Thomas, Automata on infinite objects, in Jan Van Leeuwen (a cura di), Handbook of Theoretical Computer Science: Formal Models and Semantics, t. B, MIT Press, 1990, pp. 133-192, ISBN 0-262-72015-9.
• (EN) Berndt Farwer, ω-Automata, in Erich Grädel, Wolfgang Thomas e Thomas Wilke (a cura di), Automata logics, and infinite games: A guide to current research,, collana Lecture Notes in Computer Science, n. 2500, Springer-Verlag New York, Inc., 1º gennaio 2002, pp. 3-22, ISBN 978-3-540-00388-5.
• (EN) Samuel Eilenberg, Chap. XIV. Infinite Behavior of Finite Automata, in Automata, Languages and Machines, collana Pure and Applied Mathematics, Vol. A, Academic Press, 1974, pp. 379-393, ISBN 978-0-12-234001-7.

• Wikimedia Commons contiene immagini o altri file su automa di Büchi

Portale Informatica

Portale Matematica