Assiomatizzazione di testing equivalence

Seguendo sempre la linea applicata per la bisimulazione, cerchiamo ora un'insieme di assiomi corretto e completo rispetto alla nozione di testing equivalence. Prima di fare questo, vediamo le relazione tra questa nuova equivalenza e proprio la bisimulazione debole:

Teorema 7..1   Dati due processi $p$ e $q$ tali che $p\:\approx\: q$, questo implica $p \: \sqsubseteq_{may} \: q$.

Dimostrazione. Dimostriamo l'implicazione inversa delle negazioni, e cioè: $p \: \not\sqsubseteq_{may} \: q \: \Rightarrow \: p \: \not\approx \: q$.

Secondo la definizione alternativa di $\sqsubseteq_{may}$ si ha:

$$P \not \sqsubseteq_{may} Q$$    implica che $$\exists s : \: P \stackrel{s}{\Longrightarrow} \land \: Q \stackrel{s}{\not \Rightarrow}$$

Procediamo dunque per induzione sulla struttura di $s$:

Caso base: s=a
Sostituiamo questa ipotesi nella relazione scritta sopra e si ottiene $P \stackrel{a}{\Longrightarrow} \land \: Q \stackrel{a}{\not \Rightarrow}$. Si possono allora distinguere due casi per $P \stackrel{a}{\Rightarrow}$ :

1. $P \stackrel{a}{\rightarrow} \land \: Q \stackrel{a}{\not \Rightarrow}$.
   Ma dalla definizione di $\approx$ si ottiene che $P \not \approx Q$.

2. $P \stackrel{\tau}{\longrightarrow} P' \stackrel{a}{\Longrightarrow} \land \: Q \stackrel{a}{\not \Rightarrow}$.
   Dimostriamo dunque la tesi per induzione sulla somma delle profondità di P e Q. Ci troviamo difronte a tre casi per $Q \stackrel{a}{\not \Rightarrow}$:

   a)

   $Q \stackrel{b}{\rightarrow}$ con $b \neq a$.
   Essendo $b \neq a$ per definizione di bisimulazione si ha direttamente $P \not \approx Q$.

   b)

   $Q \stackrel{\tau}{\not \rightarrow}$.
   Quindi si ha che $P \stackrel{\tau}{\rightarrow}P'$ e $Q \stackrel{\epsilon}{\Rightarrow}Q$. Assumiamo per assurdo $P' \approx Q$, allora per definizione si avrebbe $P \approx Q$. Ma per induzione interna, la somma delle profondità di $P'$ e Q è minore di 1 rispetto a quella di P e Q, per cui si otterrebbe l'assurdo $P' \not \approx Q$.
   Anche in questo caso si ottiene che $P \not \approx Q$.

   c)

   $Q \stackrel{\tau}{\longrightarrow} Q' \stackrel{a}{\not \Rightarrow}$.
   Avremmo quindi $P \stackrel{\tau}{\rightarrow} P' \stackrel{a}{\Rightarrow}$. La somma delle profondità di $P'$ e $Q'$ è inferiore di 2 rispetto a quella di P e Q, perciò applicando l'ipotesi induttiva interna otteniamo che $P' \not \approx Q'$, da cui, nuovamente, che $P \not \approx Q$.

Passo induttivo: $s=as' \land \: P \stackrel{s}{\Rightarrow} \land \: Q \stackrel{s}{\not \Rightarrow}$.
Quindi, si ha $P \stackrel{a}{\Longrightarrow} P' \stackrel{s'}{\Rightarrow}$. Si devono prendere in considerazione due casi:

1. $Q \stackrel{a}{\not \Rightarrow}$.
   Si può riapplicare il caso base.

2. $Q \stackrel{a}{\Longrightarrow} Q' \stackrel{s'}{\not \Rightarrow}$.
   Applicando l'ipotesi induttiva per $P'$ e $Q'$ e si ha $P' \not \approx Q'$, da cui si ottiene $P \not \approx Q$.

$\qedsymbol$

Dimostriamo un teorema simile anche per il preordine di must:

Teorema 7..2   Dati due processi $p$ e $q$ tali che $p\:\approx\: q$, questo implica $p \: \sqsubseteq_{must} \: q$.

Dimostrazione. La dimostrazione segue il metodo visto in precedenza: vedremo cioè che $P \not \sqsubseteq_{must} Q \Rightarrow P \not \approx Q.$

Secondo la definizione alternativa di $\sqsubseteq_{must}$ si ha:

$$P \not\sqsubseteq_{must} Q$$    implica che $$\forall L \subseteq Act, \exists s :$$

$$\forall P' : \: P \stackrel{s}{\Longrightarrow} P' \land \: Init(P') \cap L \neq \emptyset$$

$$\exists Q' : \: Q \stackrel{s}{\Longrightarrow} Q' \land \: Init(Q') \cap L = \emptyset ,$$

dove con $Init(P)$ intendiamo l'insieme delle azioni iniziali che il processo $P$ può compiere.

Quanto scritto sopra significa che esiste un processo $Q'$ che non può fare nessuna azione di L, mentre P ne può fare almeno una: sia questa azione $a \in L$. Quindi $P \stackrel{s}{\Longrightarrow} P' \stackrel{a}{\Rightarrow}$ e $Q \stackrel{s}{\Longrightarrow} Q' \stackrel{a}{\not \Rightarrow}$. Da cui si ricava $P' \not \approx Q'$ e di conseguenza $P \not \approx Q$.

$\qedsymbol$

Possiamo facilmente mostrare che:

Teorema 7..3   Dati due processi $p$ e $q$ tali che $p\:\approx\: q$, questo implica $p \: \sqsubseteq_{test} \: q$.

Dimostrazione. La prova è immediata: dalla definizione di $\sqsubseteq_{test}$ e dai due precedenti teoremi la tesi è banalmente verificata. $\qedsymbol$

I tre risultati precedenti sono molto importanti per la correttezza dell'assiomatizzazione che andiamo cercando, in quanto provano che gli assiomi per la bisimulazione debole sono validi anche per i preordini della testing equivalence.