Algebra of communicating processes

ACP uses instantaneous, atomic actions (${\displaystyle {\mathit {a,b,c,...}}}$) as its primitives. Some actions have special meaning, such as the action ${\displaystyle \delta }$, which represents deadlock or stagnation, and the action ${\displaystyle \tau }$, which represents a silent action (abstracted actions that have no specific identity).

Actions can be combined to form processes using a variety of operators. These operators can be roughly categorized as providing a basic process algebra, concurrency, and communication.

• Choice and sequencing – the most fundamental of algebraic operators are the alternative operator (${\displaystyle +}$), which provides a choice between actions, and the sequencing operator (${\displaystyle \cdot }$), which specifies an ordering on actions. So, for example, the process

${\displaystyle (a+b)\cdot c}$

first chooses to perform either ${\displaystyle {\mathit {a}}}$ or ${\displaystyle {\mathit {b}}}$, and then performs action ${\displaystyle {\mathit {c}}}$. How the choice between ${\displaystyle {\mathit {a}}}$ and ${\displaystyle {\mathit {b}}}$ is made does not matter and is left unspecified. Note that alternative composition is commutative but sequential composition is not (because time flows forward).

• Concurrency – to allow the description of concurrency, ACP provides the merge and left-merge operators. The merge operator, ${\displaystyle \vert \vert }$, represents the parallel composition of two processes, the individual actions of which are interleaved. The left-merge operator, ${\displaystyle \vert \lfloor }$, is an auxiliary operator with similar semantics to the merge, but a commitment to always choose its initial step from the left-hand process. As an example, the process

${\displaystyle (a\cdot b)\vert \vert (c\cdot d)}$

may perform the actions ${\displaystyle a,b,c,d}$ in any of the sequences ${\displaystyle abcd,acbd,acdb,cabd,cadb,cdab}$. On the other hand, the process

${\displaystyle (a\cdot b)\vert \lfloor (c\cdot d)}$

may only perform the sequences ${\displaystyle abcd,acbd,acdb}$ since the left-merge operators ensure that the action ${\displaystyle {\mathit {a}}}$ occurs first.

• Communication — interaction (or communication) between processes is represented using the binary communications operator, ${\displaystyle \vert }$. For example, the actions ${\displaystyle r(d)}$ and ${\displaystyle w(d)}$ might be interpreted as the reading and writing of a data item ${\displaystyle d\in D=\{1,2,3,\ldots \}}$, respectively. Then the process

${\displaystyle \left(\sum _{d\in D}r(d)\cdot y\right)\vert (w(1)\cdot z)}$

will communicate the value ${\displaystyle 1}$ from the right component process to the left component process (i.e. the identifier ${\displaystyle {\mathit {d}}}$ is bound to the value ${\displaystyle 1}$, and free instances of ${\displaystyle {\mathit {d}}}$ in the process ${\displaystyle {\mathit {y}}}$ take on that value), and then behave as the merge of ${\displaystyle {\mathit {y}}}$ and ${\displaystyle {\mathit {z}}}$.

• Abstraction — the abstraction operator, ${\displaystyle \tau _{I}}$, is a way to "hide" certain actions, and treat them as events that are internal to the systems being modelled. Abstracted actions are converted to the silent step action ${\displaystyle \tau }$. In some cases, these silent steps can also be removed from the process expression as part of the abstraction process. For example,

${\displaystyle \tau _{\{c\}}((a+b)\cdot c)=(a+b)\cdot \tau }$

which, in this case, can be reduced to

${\displaystyle a+b}$

since the event ${\displaystyle {\mathit {c}}}$ is no longer observable and has no observable effects.

Using the alternative and sequential composition operators, ACP defines a basic process algebra which satisfies the axioms[3]

${\displaystyle {\begin{matrix}x+y&=&y+x\\(x+y)+z&=&x+(y+z)\\x+x&=&x\\(x+y)\cdot z&=&(x\cdot z)+(y\cdot z)\\(x\cdot y)\cdot z&=&x\cdot (y\cdot z)\end{matrix}}}$

Beyond the basic algebra, two additional axioms define the relationships between the alternative and sequencing operators, and the deadlock action, ${\displaystyle \delta }$

${\displaystyle {\begin{matrix}\delta +x&=&x\\\delta \cdot x&=&\delta \end{matrix}}}$

The axioms associated with the merge, left-merge, and communication operators are[3]

${\displaystyle {\begin{matrix}x\vert \vert y&=&x\vert \lfloor y+y\vert \lfloor x+x\vert y\\a\cdot x\vert \lfloor y&=&a\cdot (x\vert \vert y)\\a\vert \lfloor y&=&a\cdot y\\(x+y)\vert \lfloor z&=&(x\vert \lfloor z)+(y\vert \lfloor z)\\a\cdot x\vert b&=&(a\vert b)\cdot x\\a\vert b\cdot x&=&(a\vert b)\cdot x\\a\cdot x\vert b\cdot y&=&(a\vert b)\cdot (x\vert \vert y)\\(x+y)\vert z&=&x\vert z+y\vert z\\x\vert (y+z)&=&x\vert y+x\vert z\end{matrix}}}$

When the communications operator is applied to actions alone, rather than processes, it is interpreted as a binary function from actions to actions, ${\displaystyle \vert :A\times A\rightarrow A}$. The definition of this function defines the possible interactions between processes — those pairs of actions that do not constitute interactions are mapped to the deadlock action, ${\displaystyle \delta }$, while permitted interaction pairs are mapped to corresponding single actions representing the occurrence of an interaction. For example, the communications function might specify that

${\displaystyle a\vert a\rightarrow c}$

which indicates that a successful interaction ${\displaystyle a\vert a}$ will be reduced to the action ${\displaystyle c}$. ACP also includes an encapsulation operator, ${\displaystyle \partial _{H}}$ for some ${\displaystyle H\subseteq A}$, which is used to convert unsuccessful communication attempts (i.e. elements of ${\displaystyle H}$ that have not been reduced via the communication function) to the deadlock action. The axioms associated with the communications function and encapsulation operator are[3]

${\displaystyle {\begin{matrix}a\vert b&=&b\vert a\\(a\vert b)\vert c&=&a\vert (b\vert c)\\a\vert \delta &=&\delta \\\partial _{H}(a)&=&a{\mbox{ if }}a\notin H\\\partial _{H}(a)&=&\delta {\mbox{ if }}a\in H\\\partial _{H}(x+y)&=&\partial _{H}(x)+\partial _{H}(y)\\\partial _{H}(x\cdot y)&=&\partial _{H}(x)\cdot \partial _{H}(y)\\\end{matrix}}}$

The axioms associated with the abstraction operator are[3]

${\displaystyle {\begin{matrix}\tau _{I}(\tau )&=&\tau \\\tau _{I}(a)&=&a{\mbox{ if }}a\notin I\\\tau _{I}(a)&=&\tau {\mbox{ if }}a\in I\\\tau _{I}(x+y)&=&\tau _{I}(x)+\tau _{I}(y)\\\tau _{I}(x\cdot y)&=&\tau _{I}(x)\cdot \tau _{I}(y)\\\partial _{H}(\tau )&=&\tau \\x\cdot \tau &=&x\\\tau \cdot x&=&\tau \cdot x+x\\a\cdot (\tau \cdot x+y)&=&a\cdot (\tau \cdot x+y)+a\cdot x\\\tau \cdot x\vert \lfloor y&=&\tau \cdot (x\vert \vert y)\\\tau \vert \lfloor x&=&\tau \cdot x\\\tau \vert x&=&\delta \\x\vert \tau &=&\delta \\\tau \cdot x\vert y&=&x\vert y\\x\vert \tau \cdot y&=&x\vert y\end{matrix}}}$

Note that the action a in the above list may take the value δ (but of course, δ cannot belong to the abstraction set I).