NationMaster - Encyclopedia: 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 (Baeten 2004), as part of an effort to investigate the solutions of unguarded recursive equations. Moreso 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 (Luttik 2005), and in fact the term process algebra was coined during the research that led to ACP. Universal algebra is the field of mathematics that studies the ideas common to all algebraic structures. ... Concurrent systems are an area of study in computer science, where concurrency or parallelism is important. ... The process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. ... The Calculus of Communicating Systems (or CCS) (one of the first process calculi) was developed by Robin Milner. ... In computer science, Communicating Sequential Processes (CSP) is a language for describing patterns of interaction. ... Universal algebra is the field of mathematics that studies the ideas common to all algebraic structures. ...

1 Informal description
- 1.1 Primitives
- 1.2 Algebraic operators
2 Formal definition
3 Related formalisms
4 References

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. Universal algebra is the field of mathematics that studies the ideas common to all algebraic structures. ...

Primitives

ACP uses instantaneous, atomic actions ( $a, b, c,...$ ) as its primitives. Some actions have special meaning, such as the action $δ$ , which represents deadlock or stagnation, and the action $τ$ , which represents a silent action (abstracted actions that have no specific identity). A deadlock is a situation wherein two or more competing actions are waiting for the other to finish, so neither ever does. ...

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

a

b

, and then performs action

c

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

a b c d, a c b d, a c d b, c a b d, c a d b, c d a b

. On the other hand, the process

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

may only perform the sequences

a b c d, a c b d, a c d b

since the left-merge operators ensures that the action

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

d

is bound to the value

1

, and free instances of

d

in the process

y

take on that value), and then behave as the merge of

y

and

z

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

$tau_{{c}}((a+b)cdot c) = (a + b) cdot tau$

which, in this case, can be reduced to

a + b

since the event

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 satisifies the axioms (Bergstra and Klop 1987)

$begin{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, $δ$

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

Concurrency and interaction

The axioms associated with the merge, left-merge, and communication operators are (Bergstra and Klop 1987)

$begin{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 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, $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, $δ$ , while permitted interaction pairs are mapped to corresponding single actions representing the occurence of an interaction. For example, the communications function might specify that

$a vert a rightarrow c$

which 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 (Bergstra and Klop 1987)

$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}$

Abstraction

The axioms associated with the abstraction operator are (Bergstra and Klop 1987)

$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 acdot(taucdot x + y) &=& acdot(taucdot x + y) + acdot x tau cdot x vertlfloor y &=& taucdot ( x vertvert y) tau vertlfloor x &=& tau cdot x tau vert x &=& delta x vert tau &=& delta taucdot x vert y &=& x vert y x vert taucdot y &=& x vert y (x + y)vert z &=& xvert z + yvert z x vert (y + z) &=& xvert y + xvert z end{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:

μCRL

HyPA — a process algebra for hybrid systems (Cuijpers and Reniers 2003)

References

^- J.C.M. Baeten: A brief history of process algebra, Rapport CSR 04-02, Vakgroep Informatica, Technische Universiteit Eindhoven, 2004

^- J.A. Bergstra and J.W. Klop: ACP_τ: A Universal Axiom System for Process Specification, CWI Quarterly 15, pp. 3-23, 1987

^- P.J.L. Cuijpers and M.A. Reniers: Hybrid process algebra, Technical Report, Department of Mathematics and Computer Science, Technical University Eindhoven, 2003

^- Bas Luttik: What is algebraic in process theory, Algebraic Process Calculi: The First Twenty Five Years and Beyond, Bertinoro, Italy, August 1, 2005

Category: Process calculi 2004 (MMIV) was a leap year starting on Thursday of the Gregorian calendar. ... 1987 (MCMLXXXVII) was a common year starting on Thursday of the Gregorian calendar. ... 2003 (MMIII) was a common year starting on Wednesday of the Gregorian calendar. ... August 1 is the 213th day of the year in the Gregorian Calendar (214th in leap years), with 152 days remaining. ... 2005 (MMV) was a common year starting on Saturday of the Gregorian calendar. ...

COMMENTARY

Share your thoughts, questions and commentary here

Want to know more?
Search encyclopedia, statistics and forums:

Feeds | Contact
The Wikipedia article included on this page is licensed under the GFDL.
Images may be subject to relevant owners' copyright.
All other elements are (c) copyright NationMaster.com 2003-5. All Rights Reserved.
Usage implies agreement with terms.

Contents

Informal description GA_googleFillSlot("encyclopedia_square");