Girish Mahajan (Editor)

Calculus of communicating systems

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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.

Contents

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.

Syntax

Given a set of action names, the set of CCS processes is defined by the following BNF grammar:

P ::= | a . P 1 | A | P 1 + P 2 | P 1 | P 2 | P 1 [ b / a ] | P 1 a

The parts of the syntax are, in the order given above

empty process 
the empty process is a valid CCS process
action 
the process a . P 1 can perform an action a and continue as the process P 1
process identifier 
write A = d e f P 1 to use the identifier A to refer to the process P 1 (which may contain the identifier A itself, i.e., recursive definitions are allowed)
choice 
the process P 1 + P 2 can proceed either as the process P 1 or the process P 2
parallel composition 
P 1 | P 2 tells that processes P 1 and P 2 exist simultaneously
renaming 
P 1 [ b / a ] is the process P 1 with all actions named a renamed as b
restriction 
P 1 a is the process P 1 without action a
  • Communicating sequential processes (CSP), developed by Tony Hoare, is a language that arose at a similar time to CCS.
  • The pi-calculus, developed by Milner in the late 80's, provides mobility of communication links by allowing processes to communicate the names of communication channels themselves.
  • PEPA, developed by Jane Hillston introduces activity timing in terms of exponentially distributed rates and probabilistic choice, allowing performance metrics to be evaluated.
  • Some other languages based on CCS:

  • Calculus of broadcasting systems
  • Language Of Temporal Ordering Specification (LOTOS)
  • Models that have been used in the study of CCS-like systems:

  • History monoid
  • Actor model
  • References

    Calculus of communicating systems Wikipedia