Assiomi

Quando si definisce un'assiomatizzazione si utilizza molto la regola di sostituzione per le dimostrazioni, quindi è necessario che la relazione considerata sia una congruenza: purtroppo per la testing equivalence questa proprietà non è vera:

Teorema 7..4   La testing equivalence non è una congruenza.

Dimostrazione. La dimostrazione è molto semplice, in quanto basta mostrare un contesto che non preserva la sostitutività. Prendiamo l'equazione $a \simeq_{test} \tau .a$ vera poiché

• $a \simeq_{may} \tau .a$ in quanto i due processi hanno le stesse tracce deboli $\stackrel{a}{\Rightarrow}$

• $a \simeq_{must} \tau .a$ in quanto gli unici osservatori interessanti sono $w$ e $\bar{a}.w$.

Consideriamo il contesto b+[$\:$] e si ottiene $b+a \not \simeq_{test} b+\tau .a$: prendiamo infatti l'osservatore $O=\bar{b}.w$ ed otteniamo:

• $b+a$ must satisfy $O$

• $b+\tau .a$ not must satisfy $O$
  in quanto la computazione $b+\tau .a\vert\bar{b}.w \stackrel{\tau}{\rightarrow}a\vert\bar{b}.w$ non è soddisfacente.

$\qedsymbol$

In maniera simile a quanto fatto per la weak bisimulation, daremo ora una definizione leggermente differente della testing equivalence in modo che la proprietà di essere una congruenza sia rispettata:

Definizione 7..7 (di testing congruence)   $P \sqsubseteq_{test}^{C} Q$ sse $P \sqsubseteq_{test}Q \land \: (P \stackrel{\tau}{\rightarrow} \: \Rightarrow \: Q \stackrel{\tau}{\rightarrow})$.

La differenza è minima ma fondmentale: si richiede infatti che se la prima azione di P è un $\tau$, allora anche Q fa come prima azione proprio $\tau$.

Mostriamo ora quali sono gli assiomi di questa teoria: