Bisimulation

Lezione del 2018-11-30.

A view of the design process

Come abbiamo affermato al termine di R.E. by operational semantics, analizzando i sistemi reattivi [1] l’equivalenza tra il prodotto dell’analisi tramite la operational semantics e quello della denotational semantics non ci è sufficiente, in quanto la struttura dell’automa a stati che lo rappresenta è significativa.

Più in generale, per i sistemi reattivi la language equivalence [2] non è adeguata perché gli stati intermedi e la relativa struttura dell’automa sono significativi.

Quindi abbiamo una situazione in cui descriviamo il sistema con un linguaggio di specifica, e lo modelliamo in un labeled transition system tramite la operational semantics:

\[P_d \, \overset{operational \, semantics}{\rightsquigarrow} \, Model\]

Il modello viene usato per vari tipi di verifiche riguardo le proprietà \(\varphi\) del sistema, espresse con un lingaggio di specifiche delle proprietà:

\[P_{specification} \, \overset{op.sem.}{\rightsquigarrow} \, Model \, \overset{model \, checking}{\models} \, \varphi\]

I linguaggi di specifiche delle proprietà, usualmente sono formule logiche scritte con estensioni della propositional logic. In tal modo, data la proprietà, è possibile utilizzare il modello per verificare se la proprietà è soddisfatta dal modello stesso.

L’implementazione del codice comincia dopo le verifiche del modello.

Esistono anche tool che permettono la scrittura automatica del codice a partire dal modello, ma l’ottimizzazione del codice lascia a desiderare. Tipicamente sono usati per la prototipazione.

Scoprire un problema di architettura riguardo le proprietà del sistema, o un deadlock, durante la fase di coding, può essere disastroso. Per questo le fasi di modellazione e di model checking sono estremamente importanti, consentono di variare rapidamente l’architettura del sistema prima di avere cominciato il coding.

Effettuata con soddisfazione la fase [3] di model checking, è possibile proseguire con una serie di attività di refinement del sistema, volte ad una formalizzazione sempre più dettagliata del sistema, sino ad arrivare ad una specifica d’implementazione (nel seguito: \(P_{impl}\)). Questa non va confusa con il coding, è una specifica su come fare il coding:

\[P_{spec} \, \overset{\sqsubset}{\sim} \, P_{spec1} \, \overset{\sqsubset}{\sim} \, \cdots \, \overset{\subset}{\sim} \, P_{impl}\]

Ad esempio, potremmo avere la seguente specifica generica: \(P_{spec} \equiv (ab+ba)\), ed arrivare ad una specifica d’implementazione del tipo: \(P_{impl} \equiv (a \parallel b)\). Questo è un sistema che tratta la sequenza di azioni ab o il suo opposto: ba. La relativa specifica d’implementazione recita: «usa due componenti in parallelo, uno in grado di eseguire a e l’altro di eseguire b».

Durante le attività di refinement i vari passaggi devono dare luogo a sistemi equivalenti: \(P_{spec} \sim P_{impl}\).

Per verificare ciò avremo due tipi di controlli:

• model checking, ovvero data una proprietà del sistema, deve essere verificata con entrambi i modelli \(P \models \varphi\);
• equivalence checking, ovvero si verifica l’equivalenza delle due specifiche da confrontare: \(P_1 \sim P_2\);

Da cui il seguente (importante) teorema. «Per ogni sistema \(P_1\) e \(P_2\), per ogni attributo \(\varphi\) nel linguaggio della formula, i due sistemi sono equivalenti iff per ogni attributo \(P_1\) soddisfa l’attributo iff \(P_2\) soddisfa lo stesso attributo». Formalmente:

\[P_1 \sim P_2 \; \text{iff} \; \forall \varphi \in L_f \; (P_1 \models \varphi \; \text{iff} \; P_2 \models \varphi)\]

Questo teorema afferma che due sistemi sono equivalenti se e solo se soddisfano la stessa classe di formule [4].

Bisimulation relation

Abbiamo detto che la trace equivalence non è sufficiente perchè abbiamo necessità di tenere in considerazione gli stati intermedi presenti nell’automa tra lo stato iniziale e quelli finali, considerando ogni possibile comportamento, ovvero la relativa struttura di ramificazione.

Un altro tipo di equivalenza è l'isomorfismo: due processi sono equivalenti se generano esattamente lo stesso labeled transition system. Questo è un criterio accettabile, ma molto forte. Ad esempio si consideri il seguente semplice esempio:

Questi due processi hanno lo stesso comportamento: entrambi gestiscono l’azione a per poi terminare con successo. Da un punto di vista di un osservatore esterno non vi è differenza. Ma non hanno la stessa struttura, quindi non sono isomorficamente equivalenti.

Quindi, se la trace equivalence è troppo debole per comparare sistemi reattivi, l’isomorfismo è troppo forte.

La relazione di bisimulazione è un modo per comparare sistemi reattivi considerando il comportamento degli stati intermedi, ma senza bloccare la struttura di branching.

Non si confonda la bisimulazione con la simulazione, è un concetto diverso ed originale. Per rendercene conto consideriamo il concetto di simulazione.

Simulation relation

Nel caso di simulazione, dati due sistemi \(P_1\) e \(P_2\), diciamo che uno simula l’altro quando per ogni attività di \(P_1\) anche \(P_2\) riesce ad eseguirla, raggiungendo uno stato in cui questo processo può avere luogo nuovamente.

Formalmente «Q simula P» si scrive: \(P \overset{\sqsubset}{\sim} Q\) [5].

Si ricordi che una relazione di equivalenza soddisfa le proprietà riflessiva, simmetrica, e transitiva.

Questa non è una relazione di equivalenza, perché non esiste la proprietà simmetrica; è una relazione di preordine [6]. Valgono le proprietà

• riflessiva («P simula P»: \(P \overset{\sqsubset}{\sim} P\));
• e transitiva («se P simula Q e Q simula R, allora P simula R»: \((P \overset{\sqsupset}{\sim} Q \wedge Q \overset{\sqsupset}{\sim} R) \Rightarrow P \overset{\sqsupset}{\sim} R\))

Se si aggiunge la proprietà simmetrica, allora otteniamo il concetto di equivalenza basata su simulazione [7]:

\[P \sim_s Q \; \text{if} \; (P \overset{\sqsubset}{\sim} Q \wedge Q \overset{\sqsubset}{\sim} P)\]

Riprendendo il concetto di simulazione, formalizziamolo meglio. Diciamo che «Q simula P quando per qualunque \(a \in Act\) allora \(P \xrightarrow{a} P'\) implica \(Q \xrightarrow{a} Q'\) tale che \(Q'\) simula \(P'\)»:

\[P \overset{\sqsubset}{\sim} Q \; \text{whenever} \; \forall a \in Act, \; P \xrightarrow{a} P' \; \text{implies} \; Q \xrightarrow{a} Q' \; \text{such that} \; P' \overset{\sqsubset}{\sim} Q'\]

Si nota che la simulazione deve continuare finché il sistema P continua a funzionare, raggiungendo una terminazione con successo o un deadlock.

(esempio3) Vediamo un esempio interessante. Consideriamo i seguenti sistemi:

chiedendoci prima se il sistema a destra (stati \(q_n\)) può simulare il sistema a sinistra (stati \(s_n\)) applicando le azioni \(a \cdot b\). E, successivamente, l’inverso: se il sistema a sinistra può simulare quello a destra.

Prima tesi: \(s_1 \overset{\sqsubset}{\sim} q_1\):

1. usiamo le definizioni quando applichiamo l’azione a ai due sistemi; abbiamo: \(s_1 \xrightarrow{a} s_2\), mentre a sua volta: \(q_1 \xrightarrow{a} q_2\) (seguendo il ramo sx di \(q_1\));
2. ora ci chiediamo \(s_2 \overset{\sqsubset}{\sim} q_2\)?
3. come sopra applichiamo l’azione b ai due sistemi, abbiamo: \(s_2 \xrightarrow{b} s_3\), mentre a sua volta: \(q_2 \xrightarrow{b} q_3\).
4. ora, \(s_3 \overset{\sqsubset}{\sim} q_3\)? risposta: sì, per mancanza di ulteriori azioni.

Quindi la prima tesi è dimostrata.

Controllare la seconda tesi: \(q_1 \overset{\sqsubset}{\sim} s_1\) è una attività più articolata.

Sequendo il ramo sinistro di \(q_1\) abbiamo un comportamento analogo al precedente:

1. applicando a: \(q_1 \xrightarrow{a} q_2\) e \(s_1 \xrightarrow{a} s_2\);
2. ora ci chiediamo \(q_2 \overset{\sqsubset}{\sim} s_2\)?
3. applicando b: \(q_2 \xrightarrow{b} q_3\). \(s_2 \xrightarrow{b} s_3\);
4. \(q_3 \overset{\sqsubset}{\sim} s_3\) per mancanza di ulteriori azioni.

Ma \(q_1\) ha anche un ramo destro, che dobbiamo essere in grado di simulare:

1. applicando a, seguendo il ramo destro di \(q_1\): \(q_1 \xrightarrow{a} q_4\) e \(s_1 \xrightarrow{a} s_2\);
2. ora ci chiediamo \(q_4 \overset{\sqsubset}{\sim} s_2\)? La risposta è sì per mancanza di ulteriori azioni!

Si arriva alla interessante conclusione che gli stati in deadlock sono simulati da un qualunque altro stato perché non richiedono alcuna azione.

Infatti dovrebbe essere:

\[\forall a \in Act \; q_4 \xrightarrow{a} q' \Rightarrow s_2 \xrightarrow{a} s'\]

ma non esiste \(q_4 \xrightarrow{a} q'\), di conseguenza è soddisfatta l’implicazione \(\Rightarrow\). Infatti si ricordi che l’implicazione ha la seguente tabella di verità:

\[\begin{split}\begin{matrix} P_1 & P_2 & P_1 \Rightarrow P_2 \\ 0 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 0 & 0 \\ 1 & 1 & 1 \end{matrix}\end{split}\]

quindi l’unico caso in cui vale False si realizza per \((1 \Rightarrow 0) = 0\).

Un modo diverso di considerare il concetto è ragionare per premessa e conseguenza. Se la premessa: «per qualunque \(a \in Act\), \(P \xrightarrow{a} P'\)» non si può avverare, non si andrà mai a controllare la conseguenza, da cui la verità dell’implicazione.

Ora riprendiamo il concetto di introdurre nella relazione la proprietà simmetrica, ovvero:

\[(P \overset{\sqsubset}{\sim} Q \wedge Q \overset{\sqsubset}{\sim} P)\]

come detto, la presenza di questa proprietà, oltre la riflessiva e la transitiva, ci porta ad affermare che i sistemi P e Q sono equivalenti: \(P \sim_s Q\).

Ricordiamo l’esempio precedente. Abbiamo visto che \(s_1 \overset{\sqsubset}{\sim} q_1 \wedge q_1 \overset{\sqsubset}{\sim} s1\), quindi i due sistemi sono equivalenti: \(s_1 \sim_s q_1\).

Considerando il fatto che stiamo considerando sistemi reattivi, siamo soddisfatti di questa conclusione riguardo \(s_1\) e \(q_1\)? [8]

In realtà la mancanza di analisi della struttura di branching per i sistemi reattivi è causa di pericolosi bug d’implementazione.

Analizziamo la situazione dell’esempio mettendo i due sistemi sotto test. Cioè affianchiamo al sistema da osservare un sistema di test che in modo sincrono invia il comando x e a sua volta esegue l’azione equivalente \(\bar{x}\) su se stesso.

Il test termina con successo se raggiunge lo stato \(\bar{t}_3 \omega\) [9].

(esempio3_test1) Iniziamo considerando il sistema a sinistra, avremo il seguente comportamento:

Ogni riquadro della figura rappresenta una fase. La numerazione dei riquadri indica la successione temporale e a seguire è indicata l’azione di sincronizzazione. Ad esempio: \((a, \bar{a})\) indica l’azione di sincronizzazione con a a sinistra e \(\bar{a}\) per il sistema di test a destra.

Leggendo l’evoluzione del test:

1. si parte dagli stati \(s_1\) per il sistema in osservazione e \(t_1\) per il sistema di test;
2. all’esecuzione di \((a, \bar{a})\) il sistema in osservazione va in \(s_2\), mentre il sistema di test va in \(t_2\);
3. all’esecuzione di \((b, \bar{b})\) il sistema in osservazione va in \(s_3\), mentre il sistema di test va in \(t_3\) indicando terminazione con successo.

(esempio3_test2) Ora proviamo con lo stesso sistema di test ad osservare il comportamento del ramo destro del sistema a destra nell’esempio. Abbiamo il seguente diagramma:

Leggendo questo test:

1. si parte dagli stati \(q_1\) per il sistema in osservazione e \(t_1\) per il sistema di test;
2. all’esecuzione di \((a, \bar{a})\) il sistema in osservazione va in \(q_4\), mentre il sistema di test va in \(t_2\);
3. a questo punto siamo in una situazione di stallo: \((b, \bar{b})\) non può essere eseguito perché \(q_4\) è un deadlock; e il test non è in grado di terminare con successo.

Da questo esempio deduciamo che i due sistemi in osservazione non si comportano nello stesso modo per il test erogato, di conseguenza non possono essere considerati equivalenti.

Da qui l’idea intuitiva: dato un ambiente, se in un sistema sostituiamo un suo componente con un altro componente, il sistema complessivo deve continuare a funzionare come se la sostituzione non fosse avvenuta.

Bisimulation equivalence

Visto che la relazione di simulazione, pur essendo utile [10], è troppo debole per assicurarci una relazione di equivalenza, la dobbiamo rafforzare, senza arrivare alla rigidità dell’isomorfismo.

Per fare ciò, intuitivamente, diciamo che due stati, quello del sistema in osservazione e quello del sistema equivalente, devono essere in grado di simularsi a vicenda; e che ciò deve avvenire per tutti i possibili stati del sistema in osservazione.

La equivalenza per bisimulazione deriva dalla teoria dei giochi. E per indicare che gli stati p e q sono bisimulation equivalent si usa: \(p\sim q\).

Questa equivalenza si definisce in due passi:

1. una relazione binaria \(\mathbb{R}\) su un set di espressioni regolari \(\mathcal{E}\) (ovvero: \(\mathbb{R} \subseteq \mathcal{E} \times \mathcal{E}\)) è una bisimulation relation tutte le volte che per qualunque coppia di processi \((P, Q)\) in \(\mathbb{R}\), per qualunque possibile azione a, valgono le proprietà:
   1. il passaggio di P a P' implica il passaggio da Q a Q' e la coppia \((P', Q')\) appartiene ad \(\mathbb{R}\) [11] [12];
   2. inoltre il passaggio di Q a Q' implica il passaggio da P a P' e la coppia \((P', Q')\) appartiene ad \(\mathbb{R}\);
   3. P può terminare immediatamente se e solo se lo può fare anche Q [13];
2. due sistemi P e Q appartenenti al set delle R.E. (ovvero: \(P, Q \in \mathcal{E}\)) sono bisimili (bisimular) se e solo se esiste una bisimulation relation \(\mathbb{R}\) tale che la coppia (P, Q) appartiene ad \(\mathbb{R}\).

Si osservi:

• che la definizione precedente l’abbiamo data per l’insieme delle R.E.; ma è possibile utilizzarla per qualunque linguaggio formale di specifica di sistemi distribuiti;
• questa è una relazione di equivalenza valida per sistemi distribuiti; ne esistono altre, ma questo corso si limita a questa.

(esempio4) Con in mente la definizione precedente, applichiamo il secondo punto all’esempio relativo alla stessa semantica, che riportiamo qui di seguito con gli stati nominati:

Quindi voglia costruite una \(\mathbb{R}\) in cui tutte le coppie \((s_x, q_x)\) siano in grado di simularsi reciprocamente. Tentiamo con:

1. \((s_1, q_1) \in \mathbb{R}\), dopo di che tentiamo:
2. \((s_2, q_2) \in \mathbb{R}\), ma questa non è possibile perché \(s_2\) è in grado di eseguire b e c, mentre \(q_2\) solo b; allora proviamo
3. \((s_2, q_4) \in \mathbb{R}\), ma anche questa non è possibile perché \(s_2\) è in grado di eseguire b e c, mentre \(q_4\) solo c.

Non potendo costruire la relazione \(\mathbb{R}\) per tutte le coppie \((s_x, q_x)\) i due sistemi non sono bisimili.

(esempio5) Vediamo ora l’esempio:

In questo caso:

1. \((s_1, q_1) \in \mathbb{R}\), dopo di che tentiamo:
2. \((s_2, q_2) \in \mathbb{R}\), va bene perché sono entrambi terminali; allora proviamo anche:
3. \((s_2, q_4) \in \mathbb{R}\), anche questa va bene per lo stesso motivo.

per cui i due sistemi sono equivalenti in quanto vale:

\[\mathbb{R} = \{ (s_1, q_1), (s_2, q_2), (s_2, q_4) \}\]

Questo vuol dire che potremmo semplificare il sistema a destra sostituendolo con quello a sinistra.

Se analizziamo con lo stesso metodo l’esempio3, arriviamo alla conclusione che i due sistemi non sono bisimili perché gli stati \(s_2\) e \(q_4\) non si possono simulare reciprocamente: \(s_2\) è in grado di eseguire l’azione b, mentre \(q_4\) è uno stato terminale.

Lezione del 2018-12-13.

La nozione di bisimulation equivalence è importante anche per verificare se le attività di refinement sono avvenute correttamente. In particolare deve essere: \(P_{spec} \sim P_{impl}\) per essere certi che il modello implementativo non si sia discostato dai requisiti del sistema.

Quindi, dati due sistemi da confrontare, sono importanti gli algoritmi per effettuare la verifica della loro equivalenza, o meno. A questo fine esistono vari algoritmi. Tra i più efficienti vi sono quelli introdotti da Kanellakis e Smolka (vedi [SANR2011] pag.105 e succ.), che partono da una partizione iniziale degli stati, procedendo per raffinamenti successivi ottenuti applicando le trasformazioni della definizione di bisimulation equivalence.

Questi algoritmi sono lineari rispetto il numero di transizioni. E sono in grado di indicare quali path di transizioni non possono essere simulati da un sistema rispetto l’altro. Analizzando questi path è possibile decidere come modificare i sistemi ed effettuare una nuova analisi di bisimulazione.

---

[1]	Così come i sistemi concorrenti o multiprocesso.

[2]	Detta anche trace equivalence.

[3]	Attenzione: in realtà si tratta di più attività di test, ogni attributo di sistema avrà la sua.

[4]	Questa è una analogia rispetto il fatto che due algoritmi sequenziali sono equivalenti se e solo se soddisfano la stessa classe di test.

[5]	Si può anche leggere P è simulato da Q.

[6]	In inglese: preorder.

[7]	\(\sim_s\) indica equivalenza tramite simulzione.

[8]	Come vedremo nell’esempio che segue, la risposta è no.

[9]	Qui \(\omega\) indica terminazione con successo.

[10]	Sopratutto in fase di test.

[11]	Questa è una definizione ricorsiva: data la coppia di partenza \((P, Q) \in \mathbb{R}\), si richiede che la coppia di destinazione \((P', Q')\) sia a sua volta in \(\mathbb{R}\). Ovvero se la coppia di partenza è una bisimulazione, lo deve essere anche la coppia di destinazione.

[12]	Attenzione a mantenere l’ordine della coppia (P, Q).

[13]	\(P \surd \; \text{iff} \; Q \surd\) deve valere perché noi stiamo considerando la sintassi delle R.E. Senza questa non possiamo distinguere tra gli stati terminali 0 e 1.