Semantica Operazionale di CCS

Con semantica operazionale di un'algebra di processi si intendono i passi di esecuzione che possono essere fatti da un processo. Questi comportamenti sono descritti dagli assiomi e dalle regole di transizione per gli operatori che nel CCS sono le seguenti:

Sequenzializzazione

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

Somma

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

Composizione parallela

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

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

Restrizione

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

Relabelling

$\qquad\renewcommand {\arraystretch}{1.2} \begin{array}{c}E \stackrel{\alpha}{... ... \hline E[f] \: \stackrel{f(\alpha)}{\longrightarrow} \: E'[f] \end{array}$

Equazione di definizione

$\qquad\renewcommand {\arraystretch}{1.2} \begin{array}{c}E \stackrel{\alpha}{... ...rel{\alpha}{\longrightarrow} E' \end{array} \quad (N \stackrel{{def}}{{=}}E)$

Possiamo associare l'algebra CCS ad un LTS in cui l'insieme di stati è formato dai processi del sistema, l'insieme di azioni visibili $Act$ è composto dalle azioni esterne $A_{ccs}$ (a cui si aggiunge quella interna $\tau$) ed R comprende tutte le possibili derivazioni nel sistema (date dalle regole di transizione per gli operatori).

Più precisamente, la semantica transizionale di CCS può essere definita con il seguente labelled transition system:

$$\mathcal{L} \:=\: (\mathcal{P} \:,\: P_0 \:,\: A_{ccs} \:,\: \{\stackrel{\alpha}{\longrightarrow} : \alpha \in A_{ccs}\})$$

dove $\mathcal{P}$ è la classe delle espressioni di processi che costituiscono la sintassi dei termini CCS e $P_0$ è il processo iniziale del sistema.

Inoltre, per organizzare meglio un modello in CCS, esistono delle leggi equazionali che possono semplificare la struttura di un sistema. Queste leggi si applicano agli operatori e si dividono in:
- Statiche: si riferiscono ai combinatori statici di Composizione parallela, Restrizione e Relabelling.
- Dinamiche: coinvolgono gli operatori dinamici di Sequenzializzazione, Somma e Ricorsione.
- di Espansione: è una legge molto utile che coinvolge entrambi i gruppi.