Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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

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

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 contatore


Implementazione del contatore

LTS dell’implementazione del contatore.

LTS dell'implementazione del contatore.


Implementazione del contatore

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

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.

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.

Esempio bisimulazione debole

Esempio di due LTS non fortemente bisimili ma debolmente bisimili.

Esempio di due LTS non fortemente bisimili ma debolmente bisimili.


Esempio bisimulazione debole (segue)

Gli LTS della specifica e della implementazione del contatore sono debolmente bisimili.

Gli LTS della specifica e della implementazione del contatore sono debolmente bisimili.


  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion