The algebra of communicating processes (ACP) is an algebraic approach to reasoning about concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras or process calculi. ACP was initially developed by Jan Bergstra and Jan Willem Klop in 1982,[1] as part of an effort to investigate the solutions of unguarded recursive equations. More so than the other seminal process calculi (CCS and CSP), the development of ACP focused on the algebra of processes, and sought to create an abstract, generalized axiomatic system for processes,[2] and in fact the term process algebra was coined during the research that led to ACP.
ACP is fundamentally an algebra, in the sense of universal algebra. This algebra is a way to describe systems in terms of algebraic process expressions that define compositions of other processes, or of certain primitive elements.
ACP uses instantaneous, atomic actions (
a,b,c,...
\delta
\tau
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.
+
⋅
(a+b) ⋅ c
first chooses to perform either
a
b
c
a
b
\vert\vert
\vert\lfloor
(a ⋅ b)\vert\vert(c ⋅ d)
may perform the actions
a,b,c,d
abcd,acbd,acdb,cabd,cadb,cdab
(a ⋅ b)\vert\lfloor(c ⋅ d)
may only perform the sequences
abcd,acbd,acdb
a
\vert
r(d)
w(d)
d\inD=\{1,2,3,\ldots\}
\left(\sumdr(d) ⋅ y\right)\vert(w(1) ⋅ z)
will communicate the value
1
d
1
d
y
y
z
\tauI
\tau
\tau\{c\
which, in this case, can be reduced to
a+b
since the event
c
ACP fundamentally adopts an axiomatic, algebraic approach to the formal definition of its various operators. The axioms presented below comprise the full axiomatic system for ACP
\tau
Using the alternative and sequential composition operators, ACP defines a basic process algebra which satisfies the axioms[3]
\begin{matrix} x+y&=&y+x\\ (x+y)+z&=&x+(y+z)\\ x+x&=&x\\ (x+y) ⋅ z&=&(x ⋅ z)+(y ⋅ z)\\ (x ⋅ y) ⋅ z&=&x ⋅ (y ⋅ z) \end{matrix}
Beyond the basic algebra, two additional axioms define the relationships between the alternative and sequencing operators, and the deadlock action,
\delta
\begin{matrix} \delta+x&=&x\\ \delta ⋅ x&=&\delta \end{matrix}
The axioms associated with the merge, left-merge, and communication operators are[3]
\begin{matrix} x\vert\verty&=&x\vert\lfloory+y\vert\lfloorx+x\verty\\ a ⋅ x\vert\lfloory&=&a ⋅ (x\vert\verty)\\ a\vert\lfloory&=&a ⋅ y\\ (x+y)\vert\lfloorz&=&(x\vert\lfloorz)+(y\vert\lfloorz)\\ a ⋅ x\vertb&=&(a\vertb) ⋅ x\\ a\vertb ⋅ x&=&(a\vertb) ⋅ x\\ a ⋅ x\vertb ⋅ y&=&(a\vertb) ⋅ (x\vert\verty)\\ (x+y)\vertz&=&x\vertz+y\vertz\\ x\vert(y+z)&=&x\verty+x\vertz \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,
\vert:A x A → A
\delta
a\verta → c
a\verta
c
\partialH
H\subseteqA
H
\begin{matrix} a\vertb&=&b\verta\\ (a\vertb)\vertc&=&a\vert(b\vertc)\\ a\vert\delta&=&\delta\\ \partialH(a)&=&aifa\notinH\\ \partialH(a)&=&\deltaifa\inH\\ \partialH(x+y)&=&\partialH(x)+\partialH(y)\\ \partialH(x ⋅ y)&=&\partialH(x) ⋅ \partialH(y)\\ \end{matrix}
The axioms associated with the abstraction operator are[3]
\begin{matrix} \tauI(\tau)&=&\tau\\ \tauI(a)&=&aifa\notinI\\ \tauI(a)&=&\tauifa\inI\\ \tauI(x+y)&=&\tauI(x)+\tauI(y)\\ \tauI(x ⋅ y)&=&\tauI(x) ⋅ \tauI(y)\\ \partialH(\tau)&=&\tau\ x ⋅ \tau&=&x\\ \tau ⋅ x&=&\tau ⋅ x+x\\ a ⋅ (\tau ⋅ x+y)&=&a ⋅ (\tau ⋅ x+y)+a ⋅ x\\ \tau ⋅ x\vert\lfloory&=&\tau ⋅ (x\vert\verty)\\ \tau\vert\lfloorx&=&\tau ⋅ x\\ \tau\vertx&=&\delta\\ x\vert\tau&=&\delta\\ \tau ⋅ x\verty&=&x\verty\\ x\vert\tau ⋅ y&=&x\verty \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).
ACP has served as the basis or inspiration for several other formalisms that can be used to describe and analyze concurrent systems, including: