Equivalenza per fallimenti

Come detto poco sopra, il fatto che l'equivalenza a traccie eguagli un processo che termina in deadlock con uno che non lo fa, la rende in generale troppo debole; un'altra interessante equivalenza è la testing equivalence che sembra essere la più piccola equivalenza in grado di differenziare processi che terminano in uno stato di deadlock da processi che invece non terminano in quello stato.

Definizione 5..5 (Fallimento)   Un fallimento è una coppia $(s,L)$, dove $s$ è una traccia ed $L$ è un insieme di etichette di azioni.

Definizione 5..6   Un fallimento $(s,L)$ appartiene ad un processo P (per il caso strong) se esiste un processo P' tale che

• $P \stackrel{s}{\longrightarrow} P'$

• $P' \stackrel{\tau}{\not\rightarrow}$

• $\forall l\in L, P' \stackrel{l}{\not\rightarrow}$

Per il caso weak, invece, si ha

• $P \stackrel{s}{\Longrightarrow} P'$

• $P' \stackrel{\tau}{\not\rightarrow}$

• $\forall l\in L, P' \stackrel{l}{\not\rightarrow}$

La definizione precedente dice che il processo P può derivare (o discendere, se ci troviamo nel caso weak) la sequenza $s$ ed arrivare in uno stato in cui non è possibile fare nessuna ulteriore azione (neanche $\tau$) se l'ambiente consente solo le azioni in $L$.

Definizione 5..7 (Equivalenza per fallimenti)   Due processi $P$ e $Q$ si dicono equivalenti per fallimenti se possiedono esattamente gli stessi fallimenti; nel caso l'equivalenza sia forte si indica con $P \: {\sim}_f \: Q$, mentre se è debole con $P \: {\approx}_f \: Q$.

É facile vedere che l'equivalenza per fallimenti implica l'equivalenza a traccie, in quanto una traccia è parte di un fallimento.