Automa di Büchi

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].

Definizione modifica

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

$Q$ è un insieme finito di stati;
${\mathcal {F}}\subset Q\times \Sigma \times Q$ è l'insieme delle transizioni;
$I\subseteq Q$ è l'insieme degli stati iniziali;
$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 $f=(p,a,q)\in {\mathcal {F}}$ è composta da uno stato di partenza $p$ , un'etichetta $a$ e uno stato di arrivo $q$ . Un calcolo $c$ (detto anche un percorso o una traccia) è una serie infinita di transizioni consecutive:

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

Per $c$ , lo stato iniziale è $p_{0}$ , la sua etichetta è la parola infinita $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 $q$ e per ogni lettera $a$ , c'è al massimo una transizione che parte da $q$ e recante l'etichetta $a$ .

Esempi modifica

Esempio 1 modifica

Automa di Büchi che riconosce le parole infinite che includono infinite sequenze di

a

.

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

La parola infinita $bbbb\cdots$ non è accettata perché l'unica traccia corrispondente è $q_{0}q_{0}q_{0}\cdots$ e l'unico stato che appare un numero infinito di volte è $q_{0}$ , il quale non è accettante. D'altra parte, la parola $aaaa\cdots$ è accettata perché vi corrisponde la traccia $q_{0}q_{1}q_{1}\cdots$ , e $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 $a$ e $b$ , che contengono solo un numero finito di lettere $a$ , vale a dire l'espressione regolare $b^{*}a(a^{*}b^{+}a)^{\omega }$ .

Automa di Büchi che riconosce le parole infinite in cui ogni occorrenza

b

è preceduta da un numero pari diverso da zero di

a

.

Esempio 2 modifica

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

Linguaggi riconosciuti modifica

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

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

dove gli $U_{i}$ e $V_{i}$ sono linguaggi regolari e i $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 $W(p,q)$ l'insieme delle parole finite riconosciute avente $p$ come stato iniziale e $q$ come stato finale, ossia tutte le parole rappresentate dalle etichette su una traccia da $p$ a $q$ . Questi linguaggi finiti sono regolari. Una parola infinita $x$ è accettata se esiste un calcolo che passa un numero infinito di volte da uno stato terminale. Sia $q$ questo stato terminale attraverso il quale la traccia passa un numero infinito di volte. Questo equivale a dire

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

per uno stato iniziale $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 $W(q_{0},q)W(q,q)$ non è vuoto.

Proprietà di chiusura modifica

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

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

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

Concatenazione: Per ogni linguaggio regolare $L$ ed ogni ω-linguaggio $M$ riconosciuto da un automa di Büchi, il prodotto dei due linguaggi $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 ${\mathcal {A}}=(Q_{A},{\mathcal {F}}_{A},I_{A},T_{A})$ e ${\mathcal {B}}=(Q_{B},{\mathcal {F}}_{B},I_{B},T_{B})$ due automi che rispettivamente riconoscono i linguaggi $L_{A}$ e $L_{B}$ . Un automa che riconosce l'intersezione $L_{A}\cap L_{B}$ è costruito come segue:

{\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 ${\mathcal {F}}$ copiano quelle in ${\mathcal {F_{A}}}$ e ${\mathcal {F_{B}}}$ per i primi due componenti e cambiano il terzo componente da 0 a 1 quando uno stato di $T_{A}$ compare nel primo componente, da 1 a 2 quando uno stato di $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 $T_{A}$ e uno stato di $T_{B}$ appaiono infinitamente spesso nella prima e nella seconda componente. Quindi, scegliendo come stati terminali quelli in ${\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].

Collegamento con altri automi modifica

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 $(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.

Automi co-Büchi modifica

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].

Algoritmica modifica

Logica temporale lineare e model checking modifica

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.

Trasformazione di un automa di Büchi generalizzato in un automa di Büchi classico.

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 $T\subseteq Q$ è sostituito da un insieme finito $\{T_{1},\dots ,T_{k}\}$ con $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 $T_{i}$ .

L'esempio verifica sulle parole dell'alfabeto { $\top$ , cr1, cr2} la proprietà $\varphi$ che occorre "infinitamente spesso nella sezione critica 1, e infinitamente spesso nella sezione critica 2". La lettera $\top$ corrisponde ad una sezione non critica, cr1 corrisponde alla sezione critica 1 e cr2 alla sezione critica 2. $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à $\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à $\varphi$ scritta in LTL con $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 $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].

S1S e WS1S modifica

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].

Note modifica

^ ^a ^b ^c (EN) Julius R. Büchi, On a decision method in restricted second order arithmetic, Proc. International Congress on Logic, Method, and Philosophy of Science (1960), Stanford University Press, 3 gennaio 1962, pp. 1-12.
^ Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Pressª ed., 31 maggio 2008, p. 191 e p. 975, ISBN 978-0-262-02649-9.
^ Farwer
^ ^a ^b Farwer, p. 6.
^ Thomas, pp. 138-139.
^ (EN) Robert McNaughton, Testing and generating infinite sequences by a finite automaton, in Information and Control, vol. 9, 1966, pp. 521-530, DOI:10.1016/s0019-9958(66)80013-x.
^ (EN) A. P. Sistla, M. Y. Vardi e P. Wolper, The complementation problem for Büchi automata with applications to temporal logic, in Theoretical Computer Science, vol. 49, 1987, pp. 217-237, DOI:10.1016/0304-3975(87)90008-9.
^ (EN) Shmuel Safra, On the complexity of ω-automata, in Proc. 29th IEEE Symposium on Foundations of Computer Science, White Plains, New York, ottobre 1988, pp. 319-327.
^ (EN) O. Kupferman e M. Y. Vardi, Weak alternating automata are not that weak, in ACM Transactions on Computational Logic, vol. 2, n. 2, luglio 2001, pp. 408-429.
^ Farwer, p. 18, Teorema 1.30.
^ (EN) Guillaume Sadegh, Complementing Büchi Automata (PDF), in Technical Report, t. 0903, révision 2073, Le Kremlin-Bicêtre, Laboratoire de Recherche et Développement de l’Epita, maggio 2009.
^ Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Pressª ed., 31 maggio 2008, p. 185, Th. 4.42 e p. 975, ISBN 978-0-262-02649-9.
^ Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Pressª ed., 31 maggio 2008, p. 975, ISBN 978-0-262-02649-9.
^ (EN) Paul Gastin e Denis Oddoux, Fast LTL to Büchi Automata Translation, in Computer Aided Verification, Lecture Notes in Computer Science, Berlino, Heidelberg, Springer, 18 luglio 2001, pp. 53-65, DOI:10.1007/3-540-44585-4_6, ISBN 3-540-44585-4. URL consultato il 7 febbraio 2018.
^ (EN) Luke Ong - Automata, Logic and Games: Theory and Application 1. Büchi Automata and S1S (PDF), su cs.ox.ac.uk.

Bibliografia modifica

(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.

Altri progetti modifica

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

Portale Informatica

Portale Matematica

[:0-1] (EN) Julius R. Büchi, On a decision method in restricted second order arithmetic, Proc. International Congress on Logic, Method, and Philosophy of Science (1960), Stanford University Press, 3 gennaio 1962, pp. 1-12.

[2] Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Pressª ed., 31 maggio 2008, p. 191 e p. 975, ISBN 978-0-262-02649-9.

[3] Farwer

[Farwer6-4] Farwer, p. 6.

[5] Thomas, pp. 138-139.

[6] (EN) Robert McNaughton, Testing and generating infinite sequences by a finite automaton, in Information and Control, vol. 9, 1966, pp. 521-530, DOI:10.1016/s0019-9958(66)80013-x.

[7] (EN) A. P. Sistla, M. Y. Vardi e P. Wolper, The complementation problem for Büchi automata with applications to temporal logic, in Theoretical Computer Science, vol. 49, 1987, pp. 217-237, DOI:10.1016/0304-3975(87)90008-9.

[8] (EN) Shmuel Safra, On the complexity of ω-automata, in Proc. 29th IEEE Symposium on Foundations of Computer Science, White Plains, New York, ottobre 1988, pp. 319-327.

[9] (EN) O. Kupferman e M. Y. Vardi, Weak alternating automata are not that weak, in ACM Transactions on Computational Logic, vol. 2, n. 2, luglio 2001, pp. 408-429.

[10] Farwer, p. 18, Teorema 1.30.

[11] (EN) Guillaume Sadegh, Complementing Büchi Automata (PDF), in Technical Report, t. 0903, révision 2073, Le Kremlin-Bicêtre, Laboratoire de Recherche et Développement de l’Epita, maggio 2009.

[12] Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Pressª ed., 31 maggio 2008, p. 185, Th. 4.42 e p. 975, ISBN 978-0-262-02649-9.

[13] Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Pressª ed., 31 maggio 2008, p. 975, ISBN 978-0-262-02649-9.

[14] (EN) Paul Gastin e Denis Oddoux, Fast LTL to Büchi Automata Translation, in Computer Aided Verification, Lecture Notes in Computer Science, Berlino, Heidelberg, Springer, 18 luglio 2001, pp. 53-65, DOI:10.1007/3-540-44585-4_6, ISBN 3-540-44585-4. URL consultato il 7 febbraio 2018.

[15] (EN) Luke Ong - Automata, Logic and Games: Theory and Application 1. Büchi Automata and S1S (PDF), su cs.ox.ac.uk.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]