Interleaving

Gli operatori di parallelismo che abbiamo appena visto hanno la proprietà che i processi possono sincronizzare su certe porte. Invece con l'operatore di interleaving si gestiscono processi completamente indipendenti l'un l'altro.

Indichiamo l'interleaving di due espressioni con $\: E \:\mid\:\!\parallel\: F \:$; in questo caso il sistema eseguirà in sequenza le azioni dei due processi senza mai effettuare comunicazioni. Se sia E che F possono effettuare la stessa azione $\alpha$, allora si ha una scelta non deterministica su quale delle due espressioni prosegue. Questo operatore ha le proprietà simmetrica, associativa e distributiva.

Esempio Bill-Ben 5: Nel nostro solito sistema, facendo l'interleaving tra Bill e Ben, si avrà la seguente sommatoria di processi:

Bill $\:\mid\:\:\!\!\!\parallel\:$ Ben	$\stackrel{{def}}{{=}}$	$\overline{work}.\: \overline{play}. \:meet. \:\overline{meet}$ + $\overline{play}.\: \overline{work}. \:meet. \:\overline{meet}$ +
		$\overline{work}.\: \overline{play}. \:\overline{meet}. \:meet$ + $\overline{play}.\: \overline{work}. \:\overline{meet}. \:meet$