Struttura Sintattica di CCS

L'insieme delle azioni del CCS è definito da $\:A_{ccs} = Act \:\cup\: \{\tau\}\:$ dove $Act$ comprende tutte le azioni esterne (input e output) che possono essere svolte dal sistema, mentre $\tau$ rappresenta l'azione interna.

Gli operatori di base del CCS sono i seguenti (indichiamo con E, F, G etc. espressioni formate da processi, azioni ed operatori):

Sequenzializzazione

$\:\:\alpha.E \:;\; \overline{\alpha}.E \:;\: \tau.E$

Somma

$\:\:E + F \:;\: \sum_{i\in I} \: E_i \quad$ (I è un insieme indicizzato)

Composizione parallela

$\:\:E \:\vert\: F$

Restrizione

$\:\: E \:\backslash L \quad (L \subseteq A_{ccs}-\{\tau\})$

Relabelling

$\:\:E[f] \quad (f:A_{ccs} \: \rightarrow \: A_{ccs})$

Equazione di Definizione

$\:\:NAME \stackrel{{def}}{{=}}E$

Schematizzando, i termini di questo calcolo sono generati dalla seguente Grammatica espressa in Backus Normal Form:

$$P\:\: ::= \:\: nil \:\: \raisebox{-0.22cm}{ \rule{0.2mm}{0.6cm} }... ... \: \backslash \:L \:\: \raisebox{-0.22cm}{ \rule{0.2mm}{0.6cm} } \:\:P[f] \:\:$$

dove P e Q sono processi generici mentre $nil$ è il processo inattivo che non esegue alcun comportamento.

Con CCS si possono "simulare" molti operatori presenti in altre algebre di processi. Vediamo due semplici esempi:

Hiding

$\:\: P \: / \: L \:\stackrel{{def}}{{=}}(P \: \vert \: Ever(\overline{l_1})\: \vert \:\cdots \:\vert \: Ever(\overline{l_n})) \: \backslash \:L\quad$ dove $L = \{l_1,...,l_n\} \:$ ed $\: Ever(l_i) \: = \: l_i.Ever(l_i)$. Con Ever si ripetono continuamente le azioni $\overline{l_i}$ e quindi appena il processo P svolge un certo $l_j$ si ha la sincronizzazione che dà come risultato $\tau$ ($l_j$ non è più visibile e questo è l'obiettivo dell'Hiding).

Link

$\:\:P^\smallfrown Q \:\stackrel{{def}}{{=}}\: (P[m/out] \:\vert\: Q[m/in])\:\backslash m \quad$ dove i due processi interagiscono tramite le porte $in$ ed $\overline{out}$, perciò si ha la sincronizzazione sostituendo le etichette con $m$ ed $\overline{m}$.

Abbiamo visto che alcuni operatori preservano il determinismo al contrario di altri. Supponendo che i processi $P$, $Q$ e $P_i$ siano deterministici, riassumiamo il comportamento dei combinatori presenti in CCS:

• 0, $\alpha.\:P$ e $P \backslash L$ sono sempre deterministici.
• $\sum_i \:\alpha_i.\:P_i \:$ lo è solo se gli $\alpha_i$ sono tutti distinti.
• $P\:\vert\:Q\:$ se i due processi non hanno azioni in comune o complementari tra loro.
• $P[f]\:$ se la funzione di relabelling è iniettiva sulle azioni di $P$.

Esempio Bill-Ben 9: Utilizzando l'algebra CCS, il sistema concorrente Bill_Ben può essere definito nel seguente modo:

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