Operatore di Restrizione

Può essere assegnato ad un processo P ed ha la definizione $\:\backslash L\:$ dove $L \subseteq Act$. Se L contiene una sola azione si scrive $\:\backslash \alpha\:$. La restrizione ha quindi come parametro un insieme di etichette che vengono internalizzate, cioè diventano locali all'interno del sistema e non sono più visibili da un osservatore esterno. Ovviamente l'azione $\tau$ non può essere ristretta perché è già interna al sistema. E' importante sottolineare che oltre alle azioni $\alpha \in L$, sono internalizzate anche tutte le eventuali azioni complementari $\overline{\alpha}$.

In conclusione, nel processo P ristretto da L le azioni presenti in L sono proibite a meno che non facciano parte di una sincronizzazione. Per questo motivo utilizzando questo operatore l'insieme di comportamenti osservabili diminuisce. Dalla regola di transizione si vede che oltre ad essere deterministico è anche un operatore statico:

$$\renewcommand {\arraystretch}{1.2} \begin{array}{c}E \stackrel{\... ...kslash L \end{array} \quad (\alpha \:,\: \overline{\alpha} \: \not\in \: L)$$

Nel seguente esempio si vede un sistema formato dal solo processo non deterministico Coin definito ricorsivamente. Con la restrizione sulla porta $heads$, il sistema può fare l'azione $toss$ e proseguire con $tails$; se invece la scelta ricade sul sommando di destra, dopo $toss$ non ci sono più comportamenti attuabili.

$$\textsc{Coin}\: \stackrel{{def}}{{=}}\: (toss.tails.\textsc{Coin} + toss.heads.\textsc{Coin}) \: \backslash heads$$

Le derivazioni potranno essere le seguenti:

• $\textsc{Coin} \: \stackrel{toss}{\longrightarrow} \: (heads.\textsc{Coin}) \: \backslash heads \not\ longrightarrow$
• $\textsc{Coin} \: \stackrel{toss}{\longrightarrow} \: (tails.\textsc{Coin}) \: \backslash heads \: \stackrel{tails}{\longrightarrow} \: \textsc{Coin}$
• $(heads.\textsc{Coin}) \: \backslash heads \: \not\ longrightarrow$
• $(tails.\textsc{Coin}) \: \backslash heads \: \stackrel{tails}{\longrightarrow} \: \textsc{Coin}$

La restrizione assume grande importanza soprattutto se applicata ad un'azione che sincronizza due processi. Si parla perciò di composizione ristretta che talvolta viene indicata con

$$P\:\vert _L\: Q \:\stackrel{{def}}{{=}}\: (P\:\vert\:Q)\:\backslash L$$

Se abbiamo $\: (P\vert Q) \: \backslash \alpha\:$ e se i due processi hanno uno $\alpha$ e l'altro $\overline{\alpha}$ tra i loro comportamenti, sicuramente queste azioni non possono essere eseguite isolatamente, ma solo tramite la sincronizzazione sulla porta specificata ottenendo come risultato $\tau$.

Esempio Bill-Ben 6: Nel sistema Bill_Ben, le regole di transizione della composizione parallela non vietano di fare $\: (meet.nil\vert\textsc{Ben})\: \stackrel{meet}{\longrightarrow} \: (nil\vert\textsc{Ben})\:$ evitando perciò la sincronizzazione. Restringendo l'azione $meet$ su Bill_Ben sicuramente il cammino del sistema è:

$$(\textsc{Bill} \:\vert\: \textsc{Ben})\backslash meet \: \stackr... ...\longrightarrow} \: (meet.nil \:\vert\: \overline{meet}.nil) \backslash meet$$

$$(meet.nil \:\vert\: \overline{meet}.nil) \backslash meet \: \stackrel{\tau}{\longrightarrow} \: (nil \:\vert\: nil) \backslash meet$$

Ovviamente le prime due derivazioni singole posso essere scambiate di ordine e la composizione parallela finale equivale a $nil$. Si conclude che la comunicazione tra i due processi Bill e Ben avviene internamente al sistema sulla porta etichettata con $meet$ e sempre dopo che i due hanno effettuato i propri output iniziali.