LEGGE DI ESPANSIONE

Spesso un sistema concorrente viene definito tramite Composizione parallela di molti processi sui quali viene effettuato un Relabelling in modo che possano sincronizzarsi tra loro, per poi applicare una Restrizione sull'insieme delle azioni di sincronizzazione. L'espansione permette di elaborare le azioni di questi $P_i$ e trasformare la descrizione del sistema in una sommatoria di termini del tipo $\:\alpha.\:P \:$ (Standard Concurrent Form).

Le azioni manipolare sono di due tipi: quelle delle singole componenti e quelle che diventano azioni interne perché derivano da una comunicazione tra due processi.

Sia $\quad P \equiv (P_1[f_1] \:\vert\: \cdots \:\vert\: P_n[f_n])\:\backslash L\quad$ allora:

$$P = \sum \: \{\:f_i(\alpha).\:(P_1[f_1] \:\vert\: \cdots \:\vert\: P_i'[f_i] \:\vert\: \cdots \:\vert\: P_n[f_n]) \:\backslash L \: :$$

$$\qquad P_i \stackrel{\alpha}{\longrightarrow} P_i' \:,\: f_i(\alpha) \not\in (L \cup \overline{L})\:\}$$

$$+ \sum \: \{\:\tau.\:(P_1[f_1] \:\vert\: \cdots \:\vert\: P_i'[f_i]... ...ts \:\vert\: P_j'[f_j] \:\vert\: \cdots \:\vert\: P_n[f_n]) \:\backslash L \: :$$

$$\qquad P_i \stackrel{\alpha}{\longrightarrow} P_i' \:,\: P_j \stackrel{\beta}{\longrightarrow} P_j' \:,\: f_i(\alpha) = \overline{f_j(\beta)} \:\}$$

Diamo adesso la versione senza l'operazione di relabelling:

$\quad P \equiv (P_1\:\vert\: \cdots \:\vert\: P_n)\:\backslash L\quad$ allora:

$$P = \sum \: \{\:\alpha.\:(P_1 \:\vert\: \cdots \:\vert\: P_i' \:\vert\: \cdots \:\vert\: P_n) \:\backslash L \: :$$

$$\qquad P_i \stackrel{\alpha}{\longrightarrow} P_i' \:,\: \alpha \not\in (L \cup \overline{L})\:\}$$

$$+ \sum \: \{\:\tau.\:(P_1 \:\vert\: \cdots \:\vert\: P_i' \:\vert\: \cdots \:\vert\: P_j' \:\vert\: \cdots \:\vert\: P_n) \:\backslash L \: :$$

$$\qquad P_i \stackrel{\alpha}{\longrightarrow} P_i' \:,\: P_j \stackrel{\overline{\alpha}}{\longrightarrow} P_j' \:,\: i<j \:\}$$

Vediamo un semplice esempio in cui può essere molto utile la legge di espansione:

Esempio 3..2  

$$P \:\stackrel{{def}}{{=}}\: \alpha.\:P' + \beta.\:P'' \qquad \qqu... ...'' \qquad \qquad R \:\stackrel{{def}}{{=}}\: (P \:\vert\: Q)\backslash \alpha$$

Nella composizione ristretta $R$ ci sono due azioni del primo tipo ($\beta$ e $\gamma$) ed una comunicazione sull'azione $\alpha$. Quindi si ottiene:

$$R \:\stackrel{{def}}{{=}}\: \beta.\:(P'' \:\vert\: Q)\:\backslash... ...: Q'') \:\backslash \alpha \:+\: \tau.\:(P' \:\vert\: Q')\:\backslash \alpha$$

Se conosciamo i processi $P',\:P'',\:Q',\:Q''$ si può iterare il procedimento fino ad avere una forma concorrente standard con solo prefissi e somme.

Esempio Bill-Ben 10: Nel solito esempio, si arriva alla forma concorrente standard con i seguenti passaggi:

BILL_BEN	$\stackrel{{def}}{{=}}$	$\overline{play}.\:(meet.nil\:\vert\:\textsc{Ben})\:\backslash \{meet\} +\over... ...{work}.\:(\textsc{Bill} \:\vert\: \overline{meet}.\:nil)\:\backslash \{meet\}$
BILL_BEN	$\stackrel{{def}}{{=}}$	$\overline{play}.\:\overline{work}.\:(meet.nil\:\vert\: \overline{meet}.\: nil) \:\backslash \{meet\} \:+$
		$\overline{work}.\:\overline{play}.\:(meet.nil\:\vert\:\overline{meet}.\:nil)\:\backslash \{meet\}$
BILL_BEN	$\stackrel{{def}}{{=}}$	$\overline{play}.\:\overline{work}.\:\tau.\:nil\: + \:\overline{work}.\:\overline{play}.\:\tau.\:nil$

Nell'ultimo passaggio si è immediatamente trasformato $(nil\:\vert\:nil)\:\backslash \{meet\}$ nel semplice processo inattivo $nil$.