Equivalenze di bisimulazione

Introduciamo ora alcune delle più usate equivalenze per lo studio del comportamento di sistemi concorrenti: le equivalenze di bisimulazione. Questa nozione di equivalenza tra processi si basa, come le altre, sull'idea che vogliamo poter distinguere due processi solo se questa differenza può essere identificata da un processo esterno che interagisce con loro.

In questa parte daremo sono una prima introduzione al significato di questa relazione cercando di coglierne il senso: i concetti verranno poi ripresi in seguito in un discorso più ampio e completo.

Introdurremo prima una nozione in cui le azioni $ \tau$, quelle azioni che sono interne ai processi, vengono considerate esattamente come le altre azioni e questo ci porterà a definire una equivalenza abbastanza stretta che chiameremo equivalenza forte o bisimulazione forte. Noteremo poi che, dal momento che le azioni interne non possono essere osservate od individuate da un processo esterno, queste potranno non essere considerate; ciò ci porterà ad una nozione di equivalenza più debole che chiameremo equivalenza osservazionale

Il motivo per cui mostreremo prima l'equivalenza forte è dato dalla sua semplicità e dal fatto che possiede interessanti proprietà algebriche: infatti risulta essere una congruenza, cioè viene preservata da tutti gli operatori della nostra algebra.

Il nostro punto di partenza rimane sempre quello di ottenere un'equivalenza più forte di quella a traccie che, come ci ricordiamo, non è sufficiente a caratterizzare l'equivalenza fra processi in modo soddisfacente.

Inoltre, quello che la bisimulazione introduce e che la rende così importante è la valutazione dell'equivalenza fatta sia prima che dopo aver eseguito azioni comuni.



Subsections
Morpheus 2004-02-10