Composizione Parallela

Questo operatore statico permette la concorrenza tra due processi che eseguono azioni complementari, quindi è presente nelle algebre di processi in cui si ha distinzione tra input e output su una porta.

Si denota con il simbolo $\vert$ che mette in relazione due processi. Il sistema $P \:\vert\: Q$ esegue l'interleaving dei due processi oppure la sincronizzazione. Nel primo caso le due espressioni proseguono facendo le proprie azioni in sequenza (non necessariamente alternandosi), mentre si sincronizzano quando vengono eseguite due azioni complementari $\alpha$ e $\overline{\alpha}$. In questo caso il comportamento risultante è l'azione silente $\tau$. In questo caso si può parlare di comunicazione tra due processi sulla porta $\alpha$.

Stavolta le regole di transizione sono tre:

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

$$\renewcommand {\arraystretch}{1.2} \begin{array}{c}E \stackrel{\... ...\ \hline E\vert F \stackrel{\tau}{\longrightarrow} E'\vert F' \end{array}$$

Esempio Bill-Ben 4 Supponiamo che il sistema Bill-Ben (finora trattato come un unico processo) sia invece formato da due processi che agiscono in parallelo; inoltre le azioni $play$ e $work$ sono degli output, mentre l'azione interna $\tau$ viene eseguita su una porta etichettata con $meet$.

I due processi svolgono la loro prima azione separatamente (emettendo i segnali di uscita dalle porte $play$ e $work$) e dopo possono sincronizzarsi sulla porta $meet$:

$$\textsc{Bill}\: \stackrel{{def}}{{=}}\: \overline{play}.meet.nil$$

$$\textsc{Ben} \: \stackrel{{def}}{{=}}\: \overline{work}.\overline{meet}.nil$$

$$\textsc{Bill}\_\textsc{Ben}\: \stackrel{{def}}{{=}}\: (\textsc{Bill}\:\vert\: \textsc{Ben})$$

Le derivazioni che risultano dalle regole di transizione viste sono:

• $\overline{play}.meet.nil \: \stackrel{\overline{play}}{\longrightarrow} \: meet.nil \qquad$ che implica $\qquad \textsc{Bill}\:\stackrel{\overline{play}}{\longrightarrow}\: meet.nil \:$ (dalla regola per $\stackrel{{def}}{{=}}$)
• $(\textsc{Bill}\vert \textsc{Ben})\: \stackrel{\overline{play}}{\longrightarrow} \: (meet.nil\vert\textsc{Ben})$
• $(meet.nil\vert\textsc{Ben})\: \stackrel{\overline{work}}{\longrightarrow} \: (meet.nil\vert\overline{meet}.nil)$
• $(meet.nil\vert\overline{meet}.nil) \: \stackrel{\tau}{\longrightarrow} \: (nil\vert nil) \qquad$ (non ci sono più transizioni possibili)

Le ultime tre derivazioni coinvolgono l'operatore di composizione parallela per l'interleaving e per la sincronizzazione.