Caratterizzazione alternativa di must

La definizione alternativa del preordine di must non è così diretta come la precedente: abbiamo bisogno di alcune premesse per poter proseguire:

Definizione 7..5   $\:$

• (P after s) = $\{ P'\: \vert \: P\stackrel{s}{\Longrightarrow}P' \}$ è l'insieme dei processi che P può raggiungere dopo aver fatto $s \: \in \: Act^{*}$.

• (P must a) sse $P \stackrel{\tau}{\Longrightarrow}P'$ implica $P'\stackrel{a}{\Longrightarrow}$, cioè P può evolvere con $\tau$ e raggiungere stati in cui può fare a.

• (P must L) sse $\exists a \in L$ t.c. P must a.

• ( $\mathbb{P}$ must L) sse $\forall P \: \in \: \mathbb{P} \quad$ P must L.

Tramite queste premesse, possiamo introdurre la caratterizzazione alternativa di must:

Definizione 7..6  

$P \sqsubseteq_{must}Q$ se $\forall s \in Act^{*}, \: \forall L \subseteq Act$, con $L$ finito, $P \stackrel{s}{\Rightarrow}$ implica:

• $Q \stackrel{s}{\Rightarrow}$

• ((P after s) must L) implica ((Q after s) must L)
  cioè per ciascun dei processi raggiunti da P dopo aver fatto $\stackrel{s}{\Rightarrow}$ esiste un'azione di L che possono fare dopo zero o più $\tau$.

Il vantaggio di questa diversa caratterizzazione è che la sequenza di azioni interessanti sono un numero finito e quindi la prova si riduce drasticamente in quanto per ogni sequenza $x$ non interessante si ha che (P after x)= $\emptyset$, come mostra il seguente

Lemma 7..1 (P after s)   must $\emptyset$ sse $s \: \not\in$ Traces(P).

Dimostrazione. ( $\Leftarrow$) E' banale, in quanto se $s \: \not\in$ Traces(P) questo implica che (P after s) = $\emptyset$.

( $\Rightarrow$) Supponiamo che $s \: \in$ Traces(P). Allora sappiamo che esiste un $P'$ tale che $P \stackrel{s}{\Longrightarrow} P'$ e per nessun $a \: \in \: \emptyset$ si ha che $P' \stackrel{a}{\longrightarrow}$ e quindi si ha che (P after s) not must$\: \emptyset$. $\qedsymbol$