Forme normali per testing

In modo analogo a quanto fatto con bisimulazione definiamo ora delle forme normali che ci aiuteranno per verificare la completezza degli assiomi.

Definizione 7..8 (di insieme saturato)   Sia $\mathcal{L}$ un insieme non vuoto di insiemi finiti, cioè $\mathcal{L} \subseteq \mathbb{P}(Act)$. Sia $Act(\mathcal{L})=\{ a\vert a \in L, L \in \mathcal{L} \}$ l'insieme di tutte le azioni di $\mathcal{L}$. Si dice che $\mathcal{L}$ è saturato se $\forall K \subseteq Act$

$$L \in \mathcal{L} \land \: L \subseteq K \subseteq Act(\mathcal{L})$$    implica $$K \in \mathcal{L}$$

Cerchiamo di spiegare intuitivamente cosa si intende con la definizione precedente: sia $\mathcal{L}$ un insieme di insiemi di azioni; estraiamo da questo tutte le azioni elementari e mettiamole in un insieme chiamato $Act(\mathcal{L})$. Prendiamo ora un sottoinsieme di azioni $K$: se possiamo trovare sempre un elemento L appartenente a $\mathcal{L}$ che sia sottoinsieme di $K$, e se questo $K$ contiene azioni presenti anche in $Act(\mathcal{L})$ allora possiamo dire che $\mathcal{L}$ è saturato.

Definizione 7..9 (Forma normale)   Un processo è in forma normale se è in una delle due forme:

a)

$\sum \{ \tau . \sum \{ a.P_{a}\vert a \in L\}\vert L \in \mathcal{L} \}$ con $P_{a}$ in forma normale

b)

$\sum \{ a.P_{a}\vert a \in L\}$ con $P_{a}$ in forma normale

dove $\mathcal{L}$ è un insieme saturato

Questa forma normale ci consente di stratificare un processo in fasi do si fanno solo azioni invisibili o solo azioni visibili.

Definizione 7..10 (Weak normal form)   Un processo è in weak normal form (w.n.f.) se è del tipo:

$$\sum \{ a.P_{a}\vert a \in L\}$$    con $$P_{a}$$    in weak normal form$$$$

Tramite questa nozione, i processi sono visti come alberi deterministici di azioni visibili. Questa è la forma normale utilizzata per l'assiomatizzazione della may, che è una congruenza in quanto coincide con l'equivalenza a tracce. Inoltre abbiamo questo risultato:

Teorema 7..5   Ogni processo in forma normale può essere portato in weak normal form.

Dimostrazione. La dimostrazione viene fatta per induzione sulla profondità del processo.

Caso base: nil, il quale è già in w.n.f.

Passo induttivo: sia P il nostro processo ed $\alpha \in Init(P)$, allora si hanno due casi possibili:

1. $\alpha = \tau$

   Si può eliminare il $\tau$ tramite gli assiomi (N4) e (F1) e sul resto del processo si applica l'ipotesi induttiva.

2. $\alpha \neq \tau$

   Se $\alpha$ è distinto da tutti i $\beta \in Init(P)$ allora, tramite l'ipotesi induttiva, si ottiene la tesi.

   Se, invece, $\alpha = \beta$ allora tramite l'assioma (N1) e l'ipotesi induttiva si ottiene nuovamente la tesi.

$\qedsymbol$