Calculus of Communicating Systems
Encyclopedia
The Calculus of Communicating Systems (CCS) 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 composition, choice between actions and scope restriction. CCS is useful for evaluating the qualitative correctness of properties of a system such as deadlock
or livelock.
According to Milner, "There is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework".
The expressions of the language are interpreted as a labelled transition system
. Between these models, bisimilarity is used as a semantic equivalence.
The parts of the syntax are, in the order given above
empty process : the empty process
is a valid CCS process
action : the process
can perform an action 
and continue as the process 
process identifier : write
to use the identifier 
to refer to the process 
(which may contain the identifier 
itself, i.e., recursive definitions are allowed)
choice : the process
can proceed either as the process 
or the process 
parallel composition :
tells that processes 
and 
exist simultaneously
renaming :
is the process 
with all actions named 
renamed as 
restriction :
is the process 
without action 
Some other languages based on CCS:
Models that have been used in the study of CCS-like systems:
Process calculus
In computer science, the process calculi 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...
introduced by Robin Milner
Robin Milner
Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
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 composition, choice between actions and scope restriction. CCS is useful for evaluating the qualitative correctness of properties of a system such as deadlock
Deadlock
A deadlock is a situation where in two or more competing actions are each waiting for the other to finish, and thus neither ever does. It is often seen in a paradox like the "chicken or the egg"...
or livelock.
According to Milner, "There is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework".
The expressions of the language are interpreted as a labelled transition system
State transition system
In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
. Between these models, bisimilarity is used as a semantic equivalence.
Syntax
Given a set of action names, the set of CCS processes is defined by the following BNF grammar:The parts of the syntax are, in the order given above
empty process : the empty process
is a valid CCS processaction : the process
can perform an action and continue as the process process identifier : write
to use the identifier to refer to the process (which may contain the identifier itself, i.e., recursive definitions are allowed)choice : the process
can proceed either as the process or the process parallel composition :
tells that processes and exist simultaneouslyrenaming :
is the process with all actions named renamed as restriction :
is the process without action Related calculi and models
- Communicating Sequential ProcessesCommunicating sequential processesIn 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), developed by Tony Hoare, is a language that arose at a similar time to CCS. - The pi-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...
, developed by Milner in the late 80's, provides mobility of communication links by allowing processes to communicate the names of communication channels themselves. - PEPAPEPAPerformance Evaluation Process Algebra is a stochastic process algebra designed for modelling computer and communication systems introduced by Jane Hillston in the 1990s...
, developed by Jane HillstonJane HillstonJane Hillston is Professor of Quantitative Modelling and an EPSRC Advanced Research Fellow in the School of Informatics, University of Edinburgh, Scotland....
introduces activity timing and probabilistic choice, allowing performance metrics to be evaluated.
Some other languages based on CCS:
- Calculus of Broadcasting SystemsCalculus of Broadcasting SystemsCalculus of Broadcasting Systems is a CCS-like calculus where processes speak one at a time and each is heard instantaneously by all others. Speech is autonomous, contention between speakers being resolved nondeterministically, but hearing only happens when someone else speaks. Observationally...
- Language Of Temporal Ordering SpecificationLanguage Of Temporal Ordering SpecificationLanguage Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....
(LOTOS)
Models that have been used in the study of CCS-like systems:
- History monoidHistory monoidIn 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...
- Actor modelActor modelIn 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...