Algèbre de processus

Les algèbres comprennent une notion de processus inactif ou terminé, qui caractérise un processus ne pouvant interagir avec le reste de l'environnement. Le plus souvent, ce processus est noté ${\displaystyle 0}$ ou ${\displaystyle NIL}$.

La composition séquentielle permet de composer des actions ordonnées. Par exemple, dans CCS, la composition séquentielle est notée ${\displaystyle a.b.0}$, qui désigne un processus qui peut effectuer l'action ${\displaystyle a}$, puis l'action ${\displaystyle b}$.

La seconde forme de composition est la composition parallèle, qui indique des actions qui peuvent s'effectuer sans indication d'ordre. Toujours dans CCS, la composition parallèle est notée ${\displaystyle a|b}$, qui désigne un processus qui peut effectuer ${\displaystyle a}$ et ${\displaystyle b}$, dans n'importe quel ordre.

Bien que toutes les algèbres de processus intègrent une notion de communication entre processus, il y a une grande variabilité dans la manière dont les communications sont gérées.

Ainsi, par exemple, dans CCS, la communication consiste simplement en la synchronisation entre deux processus sur une action: si on a un processus ${\displaystyle a.0}$ et un processus ${\displaystyle {\overline {a}}.0}$ en parallèle, où ${\displaystyle {\overline {a}}}$ est l'action duale de ${\displaystyle a}$ (noté ${\displaystyle a.0\ |\ {\overline {a}}.0}$ comme vu dans la section précdente); alors les deux processus peuvent, atomiquement, effectuer l'action ${\displaystyle a}$ (resp. ${\displaystyle {\overline {a}}}$): ${\displaystyle a.0\ |\ {\overline {a}}.0}$ devient ${\displaystyle 0\ |\ 0}$.

Par ailleurs, il est possible d'avoir des formes plus complexes de communication. Par exemple, le ${\displaystyle \pi }$-calcul d'ordre superieur permet l'échange de messages dont le contenu est lui-même un processus: ${\displaystyle a\langle P\rangle .0}$ désigne un processus qui envoie le processus ${\displaystyle P}$ sur le canal ${\displaystyle a}$; par ailleurs, un processus ${\displaystyle a(x).x}$ peut recevoir ce processus (lié à la variable ${\displaystyle x}$) et l'instancier: ${\displaystyle a\langle P\rangle .0\ |\ a(x).x}$ devient ${\displaystyle 0\ |\ P}$.