Testing equivalence

Un'elegante caratterizzazione alternativa della failure equivalence è chiamata testing equivalence, secondo la quale due processi sono equivalenti quando passano gli stessi test.

Consideriamo dunque un processo P definito su $Act_{\tau}$ ed un osservatore O definito su $Act_{\tau} \cup \{w\}$ dove $w \not\in Act$ è l'azione che indica il soddisfacimento dell'osservatore. Un'osservatore può essere visto come un agente che svolge dei test specifici sui processi. Il risultato del test di O su P viene indicato con una computazione $c \in Comp(O,P)$, l'insieme non vuoto di tutte le computazioni possibili. Naturalmente ora dobbiamo definire cos'è una computazione:

Definizione 5..8 (Computazione)   Dato un processo P ed un osservatore O con stati iniziali rispettivamente $p$ e $o$, si definisce una computazione da $<p,o>$ come una sequenza finita di coppie di stati $<p_n,o_n>$ dove:

1. $<p_0,o_0>$ corrisponde a $<p,o>$;

2. i) $<p_n,o_n> \stackrel{\tau}{\longrightarrow} <p_{n+1},o_{n+1}>$ se $p_n \stackrel{\tau}{\longrightarrow} p_{n+1}$ e $o_n = o_{n+1}$ oppure $o_n \stackrel{\tau}{\longrightarrow} o_{n+1}$ e $p_n = p_{n+1}$

   ii) $<p_n,o_n> \stackrel{\alpha}{\longrightarrow} <p_{n+1},o_{n+1}>$ se $p_n \stackrel{\alpha}{\longrightarrow} p_{n+1}$ e $o_n \stackrel{\alpha}{\longrightarrow} o_{n+1}$

3. Se la sequenza è finita allora l'ultimo elemento $<p_k,o_k> \stackrel{\mu}{\not\rightarrow}$ per ogni $\mu \in Act_{\tau}$.

Si ha quindi:

i) P may satisfy O se esiste una sequenza $s \in {Act}^*$ tale che $p_0 \stackrel{s}{\Rightarrow}$, $o_0 \stackrel{s}{\Longrightarrow}o_n$ e $o_n\stackrel{w}{\rightarrow}$;

ii) P must satisfy O se per ogni computazione $<p_0,o_0> \stackrel{\mu_1}{\longrightarrow} <p_1,o_1> \stackrel{\mu_2}{\longrightarrow} \dots$ $\exists n \geq 0$ tale che $o_n\stackrel{w}{\rightarrow}$

Il significato di quanto scritto sopra è che nel caso may deve esistere almeno una computazione in cui due processi eseguono la stessa sequenza di azioni ed alla fine il processo osservatore è soddisfatto; nel caso must, qualsiasi computazione deve portare al soddisfacimento dell'osservatore.

Con le definizioni appena riportate si possono introdurre i preordini (indichiamo con $\mathcal{O}$ l'insieme degli osservatori):

$$P \: {\sqsubseteq}_{may} \: Q \quad \Longleftrightarrow \quad \forall O \in \mathcal{O} \quad P \: may \: O \Rightarrow Q \: may \: O$$

$$P \: {\sqsubseteq}_{must} \: Q \quad \Longleftrightarrow \quad \forall O \in \mathcal{O} \quad P \: must \: O \Rightarrow Q \: must \: O$$

Come detto, prendendo in considerazione i kernel di questi due preordini possiamo definire la may-equivalence e la must-equivalence rispettivamente in questo modo:

$$P \: {\simeq}_{may} \: Q \quad \Longleftrightarrow \quad P \: {\sqsubseteq}_{may} \: Q \quad \wedge \quad Q \: {\sqsubseteq}_{may} \: P$$

$$P \: {\simeq}_{must} \: Q \quad \Longleftrightarrow \quad P \: {\sqsubseteq}_{must} \: Q \quad \wedge \quad Q \: {\sqsubseteq}_{must} \: P$$

Infine possiamo definire il preordine di testing e l'equivalenza di testing (o testing equivalence) tra due processi come:

$$P \: {\sqsubseteq}_{test} \: Q \quad \Longleftrightarrow \quad P \: {\sqsubseteq}_{may} \: Q \quad \wedge \quad P \: {\sqsubseteq}_{must} \: Q$$

$$P \: {\simeq}_{test} \: Q \quad \Longleftrightarrow \quad P \: {\simeq}_{may} \: Q \quad \wedge \quad P \: {\simeq}_{must} \: Q$$

La testing equivalence uguaglia tutti i processi che possono superare gli stessi test, ovvero soddisfare gli stessi osservatori, mentre nell'equivalenza per fallimenti avevamo che i processi venivano uguagliati in base ai test che non venivano superati. Come già detto all'inizio, queste due equivalenze sono identiche in CCS.