Home

Federica EU

1/12

Adriano Peron » 13.Comportamenti infiniti: Automi di Büchi

Temi della lezione

Introduzione agli Automi di Büchi:

Definizione
Condizioni di accettazione alla Büchi
Proprietà di chiusura e decidibilità.

Automi di Büchi

Gli automi a stati finiti (automi regolari) rappresentano macchine che interagiscono con l’ambiente per un tempo finito (numero illimitato ma finito di interazioni).

Il comportamento corretto prevede la terminazione in uno stato di accettazione.

Non in tutti i sistemi o programmi la terminazione rappresenta un fatto positivo e necessario.

Si pensi a sistemi che non devono elaborare un risultato (sistemi trasformazionali) ma che devono mantenere in maniera continuativa l’interazione con un ambiente (sistemi reattivi).

Gli automi di Büchi descrivono macchine a stati finiti dove l’interazione tra ambiente e macchina non termina ma prosegue all’infinito.

Omega-parole

Gli automi a stati finiti (automi regolari) possono essere visti come accettori di linguaggi finitari:

il numero di parole di un linguaggio può essere infinito ma la lunghezza di ciascuna parola, seppure illimitata, è finita;

Se $\Sigma$ è l’alfabeto, la parola appartiene a $\Sigma^{\star}$ .

Gli automi di Büchi possono essere visti come accettori di $\omega-\mbox{linguaggi}$ :

Se $\Sigma$ è l’alfabeto, la parola appartiene a $\Sigma^{\omega}$ ;

Le $\omega-\mbox{parole}$ , sono sequenze di simboli indicizzate sull’intero insieme dei numeri naturali.

$\omega-\mbox{parola}\ \alpha$ :

$\alpha : N\ \longrightarrow\ \Sigma$

Automi di Büchi: sintassi

Sintatticamente non c’è alcuna differenza tra gli automi di Büchi e gli Automi Regolari.

Un Automa di Büchi è una tupla
$B = \langle\Sigma ,Q, q_{0}, \Delta ,F \rangle$ , dove

$\Sigma$ è l’alfabeto di input;
Q è l’insieme finito degli stati;
$q_{0}$ è lo stato iniziale;
$\Delta \subseteq Q \times \Sigma \times Q$ è la
relazione di transizione;
$F \subseteq Q$ è l’insieme degli stati finali.

Un automa B è deterministico sse
$\langle q,a,q'\rangle,\langle q,a,q''\rangle \in Q \mbox{ implica } q' =q''$

Automi di Büchi: semantica

Come nel caso degli Automi Regolari l’LTS coincide con l’automa stesso. Cambia invece la nozione di comportamento (infinito e non più finito) e soprattutto quella di accettazione.

Un comportamento di B su una $\omega\mbox{-parola}\ \alpha \in \Sigma^{\omega}$ è un cammino infinito dell’LTS di B a partire dallo stato iniziale i cui archi siano etichettati (nell’ordine) da $\alpha$ .

Un comportamento è di successo se vi è almeno uno stato finale in F che occorre un numero infinito di volte nel cammino (accettazione alla Büchi).

In mancanza di terminazione il criterio di accettazione si basa sulla possibilità di circolare indefinitamente in cicli dell’automa che contengano almeno uno stato finale.

(Essendo finito il numero di stati i soli cammini infiniti sono quelli che attraversano un ciclo un numero infinito di volte)

Una $\omega\mbox{-parola}\ \alpha \in \Sigma^{\omega}$ è accettata da B se esiste un comportamento di successo di B su $\alpha$ .

Esempio

Due esempi di automi di Büchi sull’alfabeto {a,b}.

$B_1$ riconosce il linguaggio $L_1$ con parole in $\{a,b\}^{\omega}$ con un numero finito di occorrenze di b.

$B_2$ riconosce il linguaggio $L_2$ con parole in $\{a,b\}^{\omega}$ con un numero infinito di occorrenze di b.

Si osservi che
$B_1$ non è deterministico; $B_2$ è deterministico;
$L_1 \mbox{ e }L_2$ sono complementari.

Fig.1 Esempi di automi.

Determinizzazione per gli Automi di Büchi

I linguaggi $L_1 \mbox{ e }L_2$ possono esemplificare una proprietà degli Automi di Büchi.

Gli Automi di Büchi non sono determinizzabili (diversamente dagli automi regolari), ossia

Gli automi di Büchi non-deterministici sono più espressivi di quelli deterministici

La classe dei linguaggi accettati da automi di Büchi non-deterministici include strettamente quella dei linguaggi accettati da automi deterministici.

Ad esempio, $L_2$ è accettato da un automa deterministico ma per il suo complemento $L_1$ non c’è nessun automa deterministico che lo possa accettare.

Dall’esempio si desume anche che la classe dei linguaggi di Büchi deterministici non è chiusa per operazione di complementazione.

Proprietà di chiusura per gli Automi di Büchi

I risultati principali sulla classe dei linguaggi accettati da Automi di Büchi (detti anche $\omega$ -linguaggi regolari) sono riportati di seguito:

La classe degli $\omega$ -linguaggi regolari è chiusa per:

Unione
Intersezione
Complemento

Il problema del linguaggio vuoto per gli automi di Büchi è decidibile in tempo lineare nella taglia dell’automa.

Una caratterizzazione degli $\omega$ -linguaggi regolari è la seguente:

L è un $\omega$ -linguaggio regolare sse L è l’unione finita di insiemi di $\omega$ -parole aventi la forma

$U.V^{\omega}$

dove $U,V \subseteq \Sigma^{*}$ sono insiemi regolari.

Costruzione dell’automa per l’intersezione

Si ricordi la costruzione dell’automa per l’intersezione di due linguaggi accettati da automi regolari.

L’automa intersezione è ottenuto mettendo in parallelo i due automi e sincronizzando la loro evoluzione:

Lo stato è dato accoppiando lo stato di entrambi (stato delle due componenti parallele);
Una transizione sincronizza una coppia di transizioni sullo stesso simbolo;
Uno stato finale indica il simultaneo raggiungimento di uno stato finale nelle due componenti.

Nel caso degli Automi di Büchi la verifica della condizione di accettazione è più laboriosa.

Non è corretto richiedere che uno stato finale delle due componenti sia raggiunto simultaneamente (sincronamente) un numero infinito di volte.

Le due componenti possono attraversare infinitamente spesso uno stato finale in modo scorrelato l’una dall’altra.

Idea: usare il passaggio del testimone. Quando una componente ha il testimone e parte da uno stato finale può cedere il testimone all’altra componente perché osservi anch’essa uno stato finale. Un numero infinito di passaggi del testimone garantisce il soddisfacimento della condizione di accettazione.

Esempio di costruzione dell’automa intersezione

L’intersezione di $\langle\Sigma ,Q_1, q_{0,1}, \Delta_1 ,F_1 \rangle \mbox{ e } \langle\Sigma ,Q_2, q_{0,2}, \Delta_2 ,F_2 \rangle$
è l’automa

$\langle\Sigma ,Q_1 \times Q_2\times \{1,2\}, (q_{0,1},q_{0,2},0), \Delta ,F_1 \times Q_2\times \{1\}\rangle$ con

$\begin{array}{ll}\Delta = \{ \langle (q_1,q_2,i), a, (q'_1,q'_2,j)\rangle : \\ & \langle q_1,a,q'_1\rangle \in \Delta_1 \mbox{ e }\\ & \langle q_2,a,q'_2\rangle \in \Delta_2\} \mbox{ e }\\ & i=1, q_1\in F_1, j=2 \mbox{ oppure }\\ & i=1, q_1\not \in F_1, j=1 \mbox{ oppure }\\ & i=2, q_2\in F_2, j=1 \mbox{ oppure }\\ & i=2, q_2\not\in F_2, j=2\} \end{array}$

Intersezione di automi

Fig. 2. Esempio di intersezione di automi di Büchi.

Decidibiltà del problema del vuoto

Negli automi regolari per risolvere il problema del vuoto si verifica l’esistenza di un cammino dallo stato iniziale ad uno stato finale nell’LTS (finito) dell’automa.

Banale problema di raggiungibilità in un grafo con numero di nodi ed archi finito.

Negli automi di Büchi basta verificare l’esistenza di un cammino nell’LTS (finito) dell’automa dallo stato iniziale ad un ciclo che contenga uno stato finale.

E’ ancora un problema di raggiungibilità in un grafo con numero di nodi ed archi finito per il quale esistono algoritmi efficienti di complessità lineare.

In Fig. 3 l’automa ammette linguaggio non vuoto perché lo stato finale si trova in un ciclo raggiungibile.