Equivalenza di traccia

Un modo naturale di considerare due sistemi equivalenti consiste nel vedere se possono eseguire le stesse sequenze di azioni visibili, astraendo in questo modo dalle azioni interne (invisibili) di un sistema: cioè, due processi sono equivalenti se consentono lo stesso insieme di sequenze di azioni.

Definizione 5..1 (Traccia)   La traccia $s \in {Act}^*$ di un processo P è una sequenza di azioni ${\alpha}_1, \dots, {\alpha}_n$ tale che esiste un certo Q raggiungibile da P eseguendo le azioni di $s$. Si parla di traccia forte se $P \stackrel{s}{\longrightarrow} Q$ e di traccia debole se $P \stackrel{s}{\Longrightarrow} Q$.

Possiamo ora introdurre il concetto di equivalenza di traccia:

Definizione 5..2 (Equivalenza di traccia)   Due sistemi P e Q si dicono fortemente equivalenti di traccia, $P \: {\sim}_t \: Q$ se

$$\forall s \in {Act_{\tau}}^* \qquad P \stackrel{s}{\rightarrow} \quad \Longleftrightarrow \quad Q \stackrel{s}{\rightarrow}$$

Analogamente, P e Q si dicono debolmente equivalenti di traccia, $P \: {\approx}_t \: Q$ se

$$\forall s \in {Act}^* \qquad P \stackrel{s}{\Rightarrow} \quad \Longleftrightarrow \quad Q \stackrel{s}{\Rightarrow}$$

La differenza tra queste due equivalenze risiede nel modo di interpretare le azioni invisibili $\tau$: nel caso dell'equivalenza forte le azioni $\tau$ sono viste al pari delle altre azioni visibili, mentre nell'equivalenza debole vengono usate, al posto delle derivazioni, le discendenze: una discendenza è una derivazione debole in cui si possono eseguire zero o più azioni $\tau$ all'interno della traccia di azioni visibili $s$.

L'equivalenza ${\sim}_t$ è quella che viene ormai utilizzata da tempo nella teoria degli automi e dei linguaggi: infatti, vengono identificati come equivalenti processi che possono generare lo stesso linguaggio (insieme di stringhe sull'alfabeto dato); considerando però sistemi che interagiscono con l'ambiente esterno, diventa importante sapere se certe comunicazioni avranno sempre luogo oppure se esiste la possibilità di deadlock: la trace equivalence non consente di differenziare sistemi con comportamenti diversi in questo senso. Cerchiamo di chiarire quanto detto con un esempio: si vede che $\alpha.nil \: {\approx}_t \: \alpha.nil+\tau.nil$ però, mentre nel primo processo si esegue sempre l'azione visibile $\alpha$, nel secondo caso con un'azione interna (e quindi una sequenza visibile $\varepsilon$) si raggiunge proprio uno stato di deadlock, in quanto tutte le azioni esterne sono proibite.

Un'altro fatto è di notevole importanza: si vede facilmente che $\alpha.(\beta.nil+\gamma.nil) {\sim}_t \alpha.\beta.nil + \alpha.\gamma.nil$. É infatti intuitivo vedere che non ci sono modo per distinguere questi due processi considerando solo le azioni che possono eseguire: i due processi hanno le medesime traccie ( $\alpha \beta$ e $\alpha \gamma$) ma nel processo di destra, una volta eseguita l'azione iniziale $\alpha$ si può fare solo una delle due transazioni, mentre nel caso di sinistra si ha ancora la possibilità di scegliere. Questo significa che l'equivalenza vale negli stati iniziali, ma non più negli stati raggiunti successivamente.

Una nota a suo favore va comunque fatta: l'equivalenza di traccia è preservata da tutti gli operatori di base ed è perciò una congruenza: questa affermazione vedremo non sarà sempre vero ed alcune equivalenze "più importanti", non preservate dalla somma, dovranno essere ridefinite perchè questa proprietà sia verificata.