Operatore Parallelo

In alcuni casi per la concorrenza tra due processi si trova questo combinatore $\:\parallel\:$ (anche $Par$) che rappresenta l'esecuzione concorrente in modo diverso. Infatti il sistema $\:P \parallel Q\:$ può eseguire l'interleaving come prima, oppure sincronizza i due processi quando essi eseguono una stessa azione $\alpha$ (le co-azioni $\overline{\alpha}$ non esistono). Inoltre il risultato per il sistema non è un passo interno, ma sempre l'azione visibile $\alpha$. Le regole di transizione per l'interleaving sono le stesse, mentre quella per la sincronizzazione diventa:

$$\renewcommand {\arraystretch}{1.2} \begin{array}{c}E \stackrel{\... ...E \parallel F \stackrel{\alpha}{\longrightarrow} E' \parallel F' \end{array}$$

Quindi nell'esempio $\textsc{Bill}\_\textsc{Ben}$, dove ogni azione soprabarrata $\overline{\alpha}$ viene sostituita da quella solita $\alpha$, si hanno le derivazioni:

$$(\textsc{Bill} \parallel \textsc{Ben})\: \stackrel{play}{\longri... ... \parallel meet.nil) \stackrel{meet}{\longrightarrow} \: (nil \parallel nil)$$

Notiamo che in questo caso l'azione concorrente $meet$ è visibile e quindi dovrà essere internalizzata in un altro modo (operatori di astrazione).