Process calculus
Encyclopedia
In computer science
, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebra
ic laws that allow process descriptions to be manipulated and analyzed, and permit formal reasoning about equivalences between processes (e.g., using bisimulation
). Leading examples of process calculi include CSP
, CCS
, ACP
, and LOTOS
. More recent additions to the family include the
-calculus
, the ambient calculus
, PEPA
and the fusion calculus.
behaviour, timing information, and specializations for studying molecular interactions), there are several features that all process calculi have in common:
and 
, usually written 
, is the key primitive distinguishing the process calculi from sequential models of computation. Parallel composition allows computation in 
and 
to proceed simultaneously and independently. But it also allows interaction, that is synchronisation and flow of information from 
to 
(or vice versa) on a channel shared by both. Crucially, an agent or process can be connected to more than one channel at a time.
Channels may be synchronous or asynchronous. In the case of a synchronous channel, the agent sending a message waits until another agent has received the message. Asynchronous channels do not require any such synchronization. In some process calculi (notably the
-calculus
) channels themselves can be sent in messages through (other) channels, allowing the topology of process interconnections to change. Some process calculi also allow channels to be created during the execution of a computation.
) and an output operator (e.g. 
), both of which name an interaction point (here 
) that is used to synchronise with a dual interaction primitive.
Should information be exchanged, it will flow from the outputting to the inputting process. The output primitive will specify the data to be sent. In
, this data is 
. Similarly, if an input expects to receive data, one or more bound variables will act as place-holders to be substituted by data, when it arrives. In 
, 
plays that role. The choice of the kind of data that can be exchanged in an interaction is one of the key features that distinguishes different process calculi.
and then send that data on 
. Sequential composition can be used for such purposes. It is well known from other models of computation. In process calculi, the sequentialisation operator is usually integrated with input or output, or both. For example, the process 
will wait for an input on 
. Only when this input has occurred will the process 
be activated, with the received data through 
substituted for identifier 
.
The interpretation of this reduction rule is:
The class of processes that
is allowed to range over as the continuation of the output operation substantially influences the properties of the calculus.
synthesis of compact, minimal and compositional systems, the ability to restrict interference is crucial. Hiding operations allow control of the connections made between interaction points when composing
agents in parallel. Hiding can be denoted in a variety of ways. For example, in the
-calculus
the hiding of a name
in 
can be expressed as 
, while in CSP
it might be written as
.
can be understood as abbreviating the parallel composition of a countably infinite number of 
processes:
, 
, 
, 
, or some other appropriate symbol) which has no interaction points. It is utterly inactive and its sole purpose is to act as the inductive anchor on top of which more interesting processes can be generated.
s and the lambda calculus
possibly being the best-known examples today. The surprising fact that they are essentially equivalent, in the sense that they are all encodable into each other, supports the Church-Turing thesis. Another shared feature is more rarely commented on: they all are most readily understood as models of sequential computation. The subsequent consolidation of computer science required a more subtle formulation of the notion of computation, in particular explicit representations of concurrency and communication. Models of concurrency such as the process calculi, Petri-Nets in 1962, and the Actor model
in 1973 emerged from this line of enquiry.
Research on process calculi began in earnest with Robin Milner
's seminal work on the Calculus of Communicating Systems
(CCS) during the period from 1973 to 1980. C.A.R. Hoare's Communicating Sequential Processes
(CSP) first appeared in 1978, and was subsequently developed into a fully-fledged process calculus during the early 1980s. There was much cross-fertilization of ideas between CCS and CSP as they developed. In 1982 Jan Bergstra
and Jan Willem Klop
began work on what came to be known as the Algebra of Communicating Processes
(ACP), and introduced the term process algebra to describe their work. CCS, CSP, and ACP constitute the three major branches of the process calculi family: the majority of the other process calculi can trace their roots to one of these three calculi.
. This is to be expected as process calculi are an active field of study. Currently research on process calculi focuses on the following problems.
is the free object
that is generically able to represent the histories of individual communicating processes. A process calculus is then a formal language
imposed on a history monoid in a consistent fashion. That is, a history monoid can only record a sequence of events, with synchronization, but does not specify the allowed state transitions. Thus, a process calculus is to a history monoid what a formal language is to a free monoid (a formal language is a subset of the set of all possible finite-length strings of an alphabet generated by the Kleene star
).
The use of channels for communication is one of the features distinguishing the process calculi from other models of concurrency
, such as Petri net
s and the Actor model
(see Actor model and process calculi
). One of the fundamental motivations for including channels in the process calculi was to enable certain algebraic techniques, thereby making it easier to reason about processes algebraically.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebra
Algebra
Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...
ic laws that allow process descriptions to be manipulated and analyzed, and permit formal reasoning about equivalences between processes (e.g., using bisimulation
Bisimulation
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
). Leading examples of process calculi include CSP
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
, CCS
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
, ACP
Algebra of Communicating Processes
The Algebra of Communicating Processes 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, as part...
, and LOTOS
Language Of Temporal Ordering Specification
Language Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....
. More recent additions to the family include the
-calculusPi-calculus
In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
, the ambient calculus
Ambient calculus
In computer science, the ambient calculus is a process calculus devised by Luca Cardelli and Andrew D. Gordon in 1998, and used to describe and theorise about concurrent systems that include mobility...
, PEPA
PEPA
Performance Evaluation Process Algebra is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s...
and the fusion calculus.
Essential features
While the variety of existing process calculi is very large (including variants that incorporate stochasticStochastic
Stochastic refers to systems whose behaviour is intrinsically non-deterministic. A stochastic process is one whose behavior is non-deterministic, in that a system's subsequent state is determined both by the process's predictable actions and by a random element. However, according to M. Kac and E...
behaviour, timing information, and specializations for studying molecular interactions), there are several features that all process calculi have in common:
- Representing interactions between independent processes as communication (message-passing), rather than as the modification of shared variables
- Describing processes and systems using a small collection of primitives, and operators for combining those primitives
- Defining algebraic laws for the process operators, which allow process expressions to be manipulated using equational reasoning
Mathematics of processes
To define a process calculus, one starts with a set of names (or channels) whose purpose is to provide means of communication. In many implementations, channels have rich internal structure to improve efficiency, but this is abstracted away in most theoretic models. In addition to names, one needs a means to form new processes from old. The basic operators, always present in some form or other, allow:- parallel composition of processes
- specification of which channels to use for sending and receiving data
- sequentialization of interactions
- hiding of interaction points
- recursion or process replication
Parallel composition
Parallel composition of two processes and , usually written , is the key primitive distinguishing the process calculi from sequential models of computation. Parallel composition allows computation in and to proceed simultaneously and independently. But it also allows interaction, that is synchronisation and flow of information from to (or vice versa) on a channel shared by both. Crucially, an agent or process can be connected to more than one channel at a time.Channels may be synchronous or asynchronous. In the case of a synchronous channel, the agent sending a message waits until another agent has received the message. Asynchronous channels do not require any such synchronization. In some process calculi (notably the
-calculusPi-calculus
In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
) channels themselves can be sent in messages through (other) channels, allowing the topology of process interconnections to change. Some process calculi also allow channels to be created during the execution of a computation.
Communication
Interaction can be (but isn't always) a directed flow of information. That is, input and output can be distinguished as dual interaction primitives. Process calculi that make such distinctions typically define an input operator (e.g.) and an output operator (e.g. ), both of which name an interaction point (here ) that is used to synchronise with a dual interaction primitive.Should information be exchanged, it will flow from the outputting to the inputting process. The output primitive will specify the data to be sent. In
, this data is . Similarly, if an input expects to receive data, one or more bound variables will act as place-holders to be substituted by data, when it arrives. In , plays that role. The choice of the kind of data that can be exchanged in an interaction is one of the key features that distinguishes different process calculi.Sequential composition
Sometimes interactions must be temporally ordered. For example, it might be desirable to specify algorithms such as: first receive some data on and then send that data on . Sequential composition can be used for such purposes. It is well known from other models of computation. In process calculi, the sequentialisation operator is usually integrated with input or output, or both. For example, the process will wait for an input on . Only when this input has occurred will the process be activated, with the received data through substituted for identifier .Reduction semantics
The key operational reduction rule, containing the computational essence of process calculi, can be given solely in terms of parallel composition, sequentialization, input, and output. The details of this reduction vary among the calculi, but the essence remains roughly the same. The reduction rule is:The interpretation of this reduction rule is:
- The process
sends a message, here 
, along the channel 
. Dually, the process 
receives that message on channel 
. - Once the message has been sent,
becomes the process 
, while 
becomes the process 
, which is 
with the place-holder 
substituted by 
, the data received on 
.
The class of processes that
is allowed to range over as the continuation of the output operation substantially influences the properties of the calculus.Hiding
Processes do not limit the number of connections that can be made at a given interaction point. But interaction points allow interference (i.e. interaction). For thesynthesis of compact, minimal and compositional systems, the ability to restrict interference is crucial. Hiding operations allow control of the connections made between interaction points when composing
agents in parallel. Hiding can be denoted in a variety of ways. For example, in the
-calculusPi-calculus
In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
the hiding of a name
in can be expressed as , while in CSPCommunicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
it might be written as
.Recursion and replication
The operations presented so far describe only finite interaction and are consequently insufficient for full computability, which includes non-terminating behaviour. Recursion and replication are operations that allow finite descriptions of infinite behaviour. Recursion is well known from the sequential world. Replication can be understood as abbreviating the parallel composition of a countably infinite number of processes:Null process
Process calculi generally also include a null process (variously denoted as, , , , or some other appropriate symbol) which has no interaction points. It is utterly inactive and its sole purpose is to act as the inductive anchor on top of which more interesting processes can be generated.Discrete and continuous process algebra
Process algebra has been studied for discrete time and continuous time (real time or dense time)History
In the first half of the 20th century, various formalisms were proposed to capture the informal concept of a computable function, with μ-recursive functions, Turing MachineTuring machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
s and the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
possibly being the best-known examples today. The surprising fact that they are essentially equivalent, in the sense that they are all encodable into each other, supports the Church-Turing thesis. Another shared feature is more rarely commented on: they all are most readily understood as models of sequential computation. The subsequent consolidation of computer science required a more subtle formulation of the notion of computation, in particular explicit representations of concurrency and communication. Models of concurrency such as the process calculi, Petri-Nets in 1962, and the Actor model
Actor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
in 1973 emerged from this line of enquiry.
Research on process calculi began in earnest with Robin Milner
Robin Milner
Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
's seminal work on the Calculus of Communicating Systems
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
(CCS) during the period from 1973 to 1980. C.A.R. Hoare's Communicating Sequential Processes
Communicating sequential processes
In computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
(CSP) first appeared in 1978, and was subsequently developed into a fully-fledged process calculus during the early 1980s. There was much cross-fertilization of ideas between CCS and CSP as they developed. In 1982 Jan Bergstra
Jan Bergstra
Jan A. Bergstra is a Dutch computer scientist. His work has focussed on logic and the theoretical foundations of software engineering, especially on formal methods for system design...
and Jan Willem Klop
Jan Willem Klop
Jan Willem Klop is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of TeReSe and his fixed point combinatorwhere- External links :*...
began work on what came to be known as the Algebra of Communicating Processes
Algebra of Communicating Processes
The Algebra of Communicating Processes 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, as part...
(ACP), and introduced the term process algebra to describe their work. CCS, CSP, and ACP constitute the three major branches of the process calculi family: the majority of the other process calculi can trace their roots to one of these three calculi.
Current research
Various process calculi have been studied and not all of them fit the paradigm sketched here. The most prominent example may be the ambient calculusAmbient calculus
In computer science, the ambient calculus is a process calculus devised by Luca Cardelli and Andrew D. Gordon in 1998, and used to describe and theorise about concurrent systems that include mobility...
. This is to be expected as process calculi are an active field of study. Currently research on process calculi focuses on the following problems.
- Developing new process calculi for better modeling of computational phenomena.
- Finding well-behaved subcalculi of a given process calculus. This is valuable because (1) most calculi are fairly wild in the sense that they are rather general and not much can be said about arbitrary processes; and (2) computational applications rarely exhaust the whole of a calculus. Rather they use only processes that are very constrained in form. Constraining the shape of processes is mostly studied by way of type systemType systemA type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
s.
- Logics for processes that allow one to reason about (essentially) arbitrary properties of processes, following the ideas of Hoare logicHoare logicHoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
.
- Behavioural theory: what does it mean for two processes to be the same? How can we decide whether two processes are different or not? Can we find representatives for equivalence classes of processes? Generally, processes are considered to be the same if no context, that is other processes running in parallel, can detect a difference. Unfortunately, making this intuition precise is subtle and mostly yields unwieldy characterisations of equality (which in most cases must also be undecidable, as a consequence of the halting problemHalting problemIn computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
). BisimulationBisimulationIn theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
s are a technical tool that aids reasoning about process equivalences.
- Expressivity of calculi. Programming experience shows that certain problems are easier to solve in some languages than in others. This phenomenon calls for a more precise characterisation of the expressivity of calculi modeling computation than that afforded by the Church-Turing thesis. One way of doing this is to consider encodings between two formalisms and see what properties encodings can potentially preserve. The more properties can be preserved, the more expressive the target of the encoding is said to be. For process calculi, the celebrated results are that the synchronous
-calculusPi-calculusIn theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
is more expressive than its asynchronous variant, has the same expressive power as the higher-order
-calculusPi-calculusIn theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
, but is less than the ambient calculusAmbient calculusIn computer science, the ambient calculus is a process calculus devised by Luca Cardelli and Andrew D. Gordon in 1998, and used to describe and theorise about concurrent systems that include mobility...
.
- Using process calculus to model biological systems (stochastic
-calculus, BioAmbients, Beta Binders, BioPEPA, Brane calculus). It is thought by some that the compositionality offered by process-theoretic tools can help biologists to organise their knowledge more formally.
Software implementations
The ideas behind process algebra have given rise to several tools including:Relationship to other models of concurrency
The history monoidHistory monoid
In mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process...
is the free object
Free object
In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. It is a part of universal algebra, in the sense that it relates to all types of algebraic structure . It also has a formulation in terms of category theory, although this is in yet more abstract terms....
that is generically able to represent the histories of individual communicating processes. A process calculus is then a formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
imposed on a history monoid in a consistent fashion. That is, a history monoid can only record a sequence of events, with synchronization, but does not specify the allowed state transitions. Thus, a process calculus is to a history monoid what a formal language is to a free monoid (a formal language is a subset of the set of all possible finite-length strings of an alphabet generated by the Kleene star
Kleene star
In mathematical logic and computer science, the Kleene star is a unary operation, either on sets of strings or on sets of symbols or characters. The application of the Kleene star to a set V is written as V*...
).
The use of channels for communication is one of the features distinguishing the process calculi from other models of concurrency
Concurrent computing
Concurrent computing is a form of computing in which programs are designed as collections of interacting computational processes that may be executed in parallel...
, such as Petri net
Petri net
A Petri net is one of several mathematical modeling languages for the description of distributed systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions and places...
s and the Actor model
Actor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
(see Actor model and process calculi
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...
). One of the fundamental motivations for including channels in the process calculi was to enable certain algebraic techniques, thereby making it easier to reason about processes algebraically.
Further reading
- Matthew HennessyMatthew HennessyMatthew Hennessy is an Irish computer scientist who has contributed especially to concurrency , process calculi and programming language semantics....
: Algebraic Theory of Processes, The MIT Press, ISBN 0-262-08171-7.
- C. A. R. HoareC. A. R. HoareSir Charles Antony Richard Hoare , commonly known as Tony Hoare or C. A. R. Hoare, is a British computer scientist best known for the development of Quicksort, one of the world's most widely used sorting algorithms...
: Communicating Sequential Processes, Prentice HallPrentice HallPrentice Hall is a major educational publisher. It is an imprint of Pearson Education, Inc., based in Upper Saddle River, New Jersey, USA. Prentice Hall publishes print and digital content for the 6-12 and higher-education market. Prentice Hall distributes its technical titles through the Safari...
, ISBN 0-13-153289-8.- This book has been updated by Jim Davies at the Oxford University Computing LaboratoryOxford University Computing LaboratoryThe Department of Computer Science, until 2011 named the Computing Laboratory , is a department of Oxford University in England...
and the new edition is available for download as a PDFPortable Document FormatPortable Document Format is an open standard for document exchange. This file format, created by Adobe Systems in 1993, is used for representing documents in a manner independent of application software, hardware, and operating systems....
file at the Using CSP website.
- This book has been updated by Jim Davies at the Oxford University Computing Laboratory
- Robin MilnerRobin MilnerArthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
: A Calculus of Communicating Systems, Springer Verlag, ISBN 0-387-10235-3.
- Robin MilnerRobin MilnerArthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
: Communicating and Mobile Systems: the Pi-Calculus, Springer Verlag, ISBN 0-521-65869-1.