Algebra of Communicating Processes

Algebra of Communicating Processes

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,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] 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,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] 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" (mathit{a,b,c,...}) as its primitives. Some actions have special meaning, such as the action delta, which represents deadlock or stagnation, and the action au, 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 (+), which provides a choice between actions, and the "sequencing operator" (cdot), which specifies an ordering on actions. So, for example, the process

: (a+b)cdot c

: first chooses to perform either mathit{a} or mathit{b}, and then performs action mathit{c}. How the choice between mathit{a} and 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, vert vert, represents the parallel composition of two processes, the individual actions of which are interleaved. The left-merge operator, vertlfloor, 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

:(a cdot b) vert vert (c cdot d)

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

:(a cdot b) vert lfloor (c cdot d)

: may only perform the sequences abcd, acbd, acdb since the left-merge operators ensures that the action mathit{a} occurs first.

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

:(sum_{d in D} r(d) cdot y) vert (w(1) cdot z)

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

* Abstraction — the abstraction operator, au_I, 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 au. In some cases, these silent steps can also be removed from the process expression as part of the abstraction process. For example,

: au_{{c((a+b)cdot c) = (a + b) cdot au

:which, in this case, can be reduced to

: a + b

:since the event mathit{c} 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τ (ACP with abstraction).

Basic process algebra

Using the alternative and sequential composition operators, ACP defines a "basic process algebra" which satisfies the axiomsJ.A. Bergstra and J.W. Klop, [http://www.cs.vu.nl/~jwk/ACPL-TAU.PDF "ACPτ: A Universal Axiom System for Process Specification"] , CWI Quarterly 15, pp. 3-23, 1987]

:egin{matrix}x + y &=& y + x\(x+y)+z&=& x+(y+z)\x+x&=&x\(x+y)cdot z &=& (xcdot z) + (ycdot z)\(x cdot y)cdot z &=& x cdot (y cdot z)end{matrix}

Deadlock

Beyond the basic algebra, two additional axioms define the relationships between the alternative and sequencing operators, and the "deadlock" action, delta

:egin{matrix}delta + x &=& x\delta cdot x &=& deltaend{matrix}

Concurrency and interaction

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

:egin{matrix}x vertvert y &=& x vertlfloor y + y vertlfloor x + x vert y\a cdot x vertlfloor y &=& acdot ( x vertvert y)\a vertlfloor y &=& a cdot y \(x+y) vertlfloor z &=& (x vertlfloor z) + (y vertlfloor 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 &=& (avert b)cdot (x vert vert y)\(x + y)vert z &=& xvert z + yvert z\x vert (y + z) &=& xvert y + xvert zend{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 imes A ightarrow 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, 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:a vert a ightarrow cwhich indicates that a successful interaction a vert a will be reduced to the action c. ACP also includes an encapsulation operator, partial_H for some H subseteq A, which is used to convert unsuccessful communication attempts (i.e. elements of 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

:egin{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 otin 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}

Abstraction

The axioms associated with the abstraction operator are

:egin{matrix} au_I( au) &=& au\ au_I(a) &=& a mbox{ if } a otin I\ au_I(a) &=& au mbox{ if } a in I\ au_I(x + y) &=& au_I(x) + au_I(y)\ au_I(x cdot y) &=& au_I(x) cdot au_I(y)\partial_H( au) &=& au\ x cdot au &=& x\ au cdot x &=& au cdot x + x\acdot( aucdot x + y) &=& acdot( aucdot x + y) + acdot x \ au cdot x vertlfloor y &=& aucdot ( x vertvert y)\ au vertlfloor x &=& au cdot x \ au vert x &=& delta\x vert au &=& delta\ aucdot x vert y &=& x vert y\x vert aucdot y &=& x vert y\(x + y)vert z &=& xvert z + yvert z\x vert (y + z) &=& xvert y + xvert zend{matrix}

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 [P.J.L. Cuijpers and M.A. Reniers, "Hybrid process algebra", Technical Report, Department of Mathematics and Computer Science, Technical University Eindhoven, 2003]

References


Wikimedia Foundation. 2010.

Игры ⚽ Нужен реферат?

Look at other dictionaries:

  • Communicating Sequential Processes — (CSP) ist eine von Tony Hoare an der Universität Oxford entwickelte Prozessalgebra zur Beschreibung von Interaktion zwischen kommunizierenden Prozessen. Die Idee wurde als imperative Sprache 1978 von Tony Hoare erstmals vorgestellt, dann von ihm… …   Deutsch Wikipedia

  • Communicating sequential processes — In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.[1] It is a member of the family of mathematical theories of concurrency known as process algebras, or …   Wikipedia

  • Construction and Analysis of Distributed Processes — Developer(s) the INRIA VASY team Initial release 1986, 24–25 years ago Stable release …   Wikipedia

  • ACP — • Algebra of Communicating Processes • Ancillary Control Programm/Process • Advanced Computational Processor • Aerospace Computer Program Weltraumfahrt • Airline Control Program Luftfahrt • Aerosol Collector and Pyrolyscience investigation… …   Acronyms

  • Actor model and process calculi history — The Actor model and process calculi share an interesting history and co evolution.Early workThe Actor model, first published in 1973, [Carl Hewitt, Peter Bishop and Richard Steiger. A Universal Modular Actor Formalism for Artificial Intelligence… …   Wikipedia

  • Process calculus — In computer science, the process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. Process calculi provide a tool for the high level description of interactions, communications, and …   Wikipedia

  • Actor model and process calculi — In computer science, the Actor model and process calculi are two closely related approaches to the modelling of concurrent digital computation. See Actor model and process calculi history.There are many similarities between the two approaches,… …   Wikipedia

  • Denotational semantics — In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach to formalizing the meanings of programming languages by constructing mathematical objects (called denotations)… …   Wikipedia

  • Формальные методы — Пример формальной спецификации с использованием Z нотации В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для …   Википедия

  • MCRL2 — is a specification language for describing concurrent discrete event systems. It is accompanied with a toolset, that facilitates tools, techniques and methods for simulation, analysis and visualization of behaviour. The behavioural part of the… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”