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''' &mdash; 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''' &mdash; 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''' &mdash; 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''' &mdash; 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 &mdash; 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 &mdash; 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]]