Algebra of Communicating Processes
3502617
210915401
2008-05-07T23:25:53Z
Allan McInnes
647621
/* Related formalisms */ replace external link with wikilink
The '''Algebra of Communicating Processes''' (ACP) is an [[Universal algebra|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,<ref name="baeten2004">J.C.M. Baeten, [http://www.win.tue.nl/fm/0402history.pdf ''A brief history of process algebra''], Rapport CSR 04-02, Vakgroep Informatica, Technische Universiteit Eindhoven, [[2004]]</ref> as part of an effort to investigate the solutions of unguarded recursive equations. More so than the other seminal process calculi ([[Calculus of Communicating Systems|CCS]] and [[Communicating sequential processes|CSP]]), the development of ACP focused on the [[Universal algebra|algebra]] of processes, and sought to create an abstract, generalized axiomatic system for processes,<ref name="luttik2005">Bas Luttik, [http://www.win.tue.nl/~luttik/Papers/AlgProc_essay.pdf ''What is algebraic in process theory''], [http://www.cs.auc.dk/~luca/BICI/PA-05/ Algebraic Process Calculi: The First Twenty Five Years and Beyond], Bertinoro, Italy, [[August 1]], [[2005]]</ref> and in fact the term ''process algebra'' was coined during the research that led to ACP.
== Informal description ==
ACP is fundamentally an algebra, in the sense of [[universal algebra]]. This algebra provides a way to describe systems in terms of algebraic process expressions that define compositions of other processes, or of certain primitive elements.
===Primitives===
ACP uses instantaneous, ''[[atomic actions]]'' (<math>\mathit{a,b,c,...}</math>) as its primitives. Some actions have special meaning, such as the action <math>\delta</math>, which represents [[deadlock]] or stagnation, and the action <math>\tau</math>, which represents a ''silent action'' (abstracted actions that have no specific identity).
===Algebraic operators ===
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 (<math>+</math>), which provides a choice between actions, and the ''sequencing operator'' (<math>\cdot</math>), which specifies an ordering on actions. So, for example, the process
: <math>(a+b)\cdot c</math>
: first chooses to perform either <math>\mathit{a}</math> or <math>\mathit{b}</math>, and then performs action <math>\mathit{c}</math>.
* '''Concurrency''' — to allow the description of concurrency, ACP provides the ''merge'' and ''left-merge'' operators. The merge operator, <math>\vert \vert</math>, represents the parallel composition of two processes, the individual actions of which are interleaved. The left-merge operator, <math>\vert\lfloor</math>, 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
:<math>(a \cdot b) \vert \vert (c \cdot d)</math>
: may perform the actions <math>a, b, c, d</math> in any of the sequences <math>abcd, acbd, acdb, cabd, cadb, cdab</math>. On the other hand, the process
:<math>(a \cdot b) \vert \lfloor (c \cdot d)</math>
: may only perform the sequences <math>abcd, acbd, acdb</math> since the left-merge operators ensures that the action <math>\mathit{a}</math> occurs first.
* '''Communication''' — interaction (or communication) between processes is represented using the binary communications operator, <math>\vert</math>. For example, the actions <math>r(d)</math> and <math>w(d)</math> might be interpreted as the reading and writing of a data item <math>d \in D = \{1,2,3,\ldots\}</math>, respectively. Then the process
:<math>(\sum_{d \in D} r(d) \cdot y) \vert (w(1) \cdot z)</math>
:will communicate the value <math>1</math> from the right component process to the left component process (''i.e.'' the identifier <math>\mathit{d}</math> is bound to the value <math>1</math>, and free instances of <math>\mathit{d}</math> in the process <math>\mathit{y}</math> take on that value), and then behave as the merge of <math>\mathit{y}</math> and <math>\mathit{z}</math>.
* '''Abstraction''' — the abstraction operator, <math>\tau_I</math>, provides 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 <math>\tau</math>. In some cases, these silent steps can also be removed from the process expression as part of the abstraction process. For example,
: <math>\tau_{\{c\}}((a+b)\cdot c) = (a + b) \cdot \tau</math>
:which, in this case, can be reduced to
: <math>a + b</math>
:since the event <math>\mathit{c}</math> is no longer observable and has no observable effects.
== Formal definition ==
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<sub>τ</sub> (ACP with abstraction).
=== Basic process algebra ===
Using the alternative and sequential composition operators, ACP defines a ''basic process algebra'' which satisfies the axioms<ref name="bergstraklop1987">J.A. Bergstra and J.W. Klop, [http://www.cs.vu.nl/~jwk/ACPL-TAU.PDF ''ACP<sub>τ</sub>: A Universal Axiom System for Process Specification''], CWI Quarterly 15, pp. 3-23, [[1987]]</ref>
:<math>
\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}
</math>
=== Deadlock ===
Beyond the basic algebra, two additional axioms define the relationships between the alternative and sequencing operators, and the ''deadlock'' action, <math>\delta</math>
:<math>
\begin{matrix}
\delta + x &=& x\\
\delta \cdot x &=& \delta
\end{matrix}
</math>
=== Concurrency and interaction ===
The axioms associated with the merge, left-merge, and communication operators are<ref name="bergstraklop1987"/>
:<math>
\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}
</math>
When the communications operator is applied to actions alone, rather than processes, it is interpreted as a binary function from actions to actions, <math>\vert : A \times A \rightarrow A</math>. 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, <math>\delta</math>, while permitted interaction pairs are mapped to corresponding single actions representing the occurrence of an interaction. For example, the communications function might specify that
:<math>a \vert a \rightarrow c</math>
which indicates that a successful interaction <math>a \vert a</math> will be reduced to the action <math>c</math>. ACP also includes an encapsulation operator, <math>\partial_H</math> for some <math>H \subseteq A</math>, which is used to convert unsuccessful communication attempts (i.e. elements of <math>H</math> that have not been reduced via the communication function) to the deadlock action. The axioms associated with the communications function and encapsulation operator are<ref name="bergstraklop1987"/>
:<math>
\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}
</math>
=== Abstraction ===
The axioms associated with the abstraction operator are<ref name="bergstraklop1987"/>
:<math>
\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\\
(x + y)\vert z &=& x\vert z + y\vert z\\
x \vert (y + z) &=& x\vert y + x\vert z
\end{matrix}
</math>
== Related formalisms ==
ACP has served as the basis or inspiration for several other formalisms that can be used to describe and analyze concurrent systems, including:
* [http://homepages.cwi.nl/~mcrl/ μCRL]
* [[mCRL2]]
* HyPA — a process algebra for hybrid systems<ref>P.J.L. Cuijpers and M.A. Reniers, ''Hybrid process algebra'', Technical Report, Department of Mathematics and Computer Science, Technical University Eindhoven, [[2003]]</ref>
== References ==
{{reflist}}
[[Category:Process calculi]]