Home

Federica EU

1/9

Adriano Peron » 3.Astrazione e Bisimulazione debole

Specifica-raffinamento

Il criterio di bisimulazione forte non è adeguato allo sviluppo top-down di una specifica.

Si richiede un criterio di equivalenza in grado di astrarre dai dettagli introdotti nell’implementazione e non presenti nella specifica.

Manca la possibilità di esprimere una forma di astrazione.

Sviluppo top-down delle specifiche

Esempio specifica

Esempio di un contatore.

Specifica di un banale contatore che permette incrementi e decrementi unitari.

Alfabeto: incremento unitario (inc) e decremento unitario (dec).

Stati: in relazione al valore del contatore.

LTS contatore

Implementazione della specifica

Esempio di un contatore: implementazione.

Il contatore viene implementato mediante un registro di scorrimento con max locazioni.

Incrementi nella prima locazione a destra.

Decrementi nell’ultima locazione a sinistra.

Gli incrementi scorrono da destra a sinistra.

Stato: una tupla che indica per ogni posizione lo stato di riempimeto degli elementi del registro (0 vuoto, 1 pieno).

Alfabeto: incremento unitario (inc), decremento unitario (dec), shift $\tau$ .

Implementazione contatore

Implementazione del contatore

LTS dell'implementazione del contatore.

Implementazione del contatore

LTS del raffinamento non fortemente bisimilare a quello della specifica (con max=3).

Bisimulazione debole

Serve distinguere tra:

Eventi osservabili (alfabeto $\Sigma$ )

Eventi interni non osservabili rappresentati dal simbolo $\tau$ .

La bisimulazione debole verifica la bisimilarità a meno di eventi interni non osservabili.

Definizioni:

Sia un LTS $\langle S,S_0,\Delta \rangle \mbox{ sull'alfabeto } \Sigma \cup \{\tau\}$ .

$\begin{array}{l}\mbox{Per }q \in S \mbox{ si scrive } q \stackrel {t}{\Longrightarrow} q' \in \Delta \mbox{ se}\\\mbox{esiste cammino } q_1 \stackrel {\lambda_1}{\longrightarrow} q_2 \ldots q_n\stackrel{\lambda_n}{\longrightarrow}q_{n+1}\mbox{con}\\q_1=q \mbox{ e } q_{n+1}=q' \mbox{ e } t = \lambda_1 \ldots \lambda_n \mbox{ con } \lambda_i \in \Sigma \cup\{\tau \}, 1 \leq i \leq n.\\\\\mbox{Per } \lambda \in \Sigma \cup \{\tau \}, \mbox{ si scrive } q \stackrel {\hat{\lambda}}{\Longrightarrow} {q'} \in \Delta \mbox{ se }\\q \stackrel {t}{\Longrightarrow} q' \in \Delta\mbox{ con } t = \tau^n \cdot \lambda \cdot \tau^m \mbox{ per qualche } n,m \geq 0.\\\\\mbox{Se}\lambda = \tau \mbox{ si ha }q \stackrel {\hat{\tau}}{\Longrightarrow} {q} \in \Delta.\end{array}$

Astrazione da eventi non osservabili.

Bisimulazione debole: definizione

Definizione di bisimulazione debole.

Dati due LTS $\langle S_1,S_{0,1}\Delta_1\rangle\ \mbox{ e } \langle S_2,S_{0,2}\Delta_2 \rangle \mbox{ su } \Sigma\cup \{\tau\}$ ,

una bisimulazione debole è una relazione $R_w \subseteq S_1 \times S_2$ che soddisfa il seguente requisito:

se $s_1\ R_w\ s_2$ allora deve valere

(1) $\forall \lambda \in \Sigma\cup \{\tau\} \mbox{ tale che } s_1 \stackrel{\lambda}{\longrightarrow} s'_1 \in\Delta_1, \exists s'_2\in S_2 \mbox{ tale che } s_2 \stackrel{\hat{\lambda}}{\Longrightarrow} s'_2 \in \Delta_2 \mbox{ e } s'_1\ R_w\ s'_2$ .

(2) $\forall \lambda \in \Sigma\cup \{\tau\}\mbox{ tale che } s_2 \stackrel{\lambda}{\longrightarrow} s'_2 \in\Delta_2, \exists s'_1\in S_1 \mbox{ tale che } s_1 \stackrel{\hat{\lambda}}{\Longrightarrow} s'_1 \in \Delta_1 \mbox{ e } s'_1\ R_w\ s'_2$ .