calculus of communicating systems

{{Refimprove|date=November 2011}}

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, summation between actions and scope restriction. CCS is useful for evaluating the qualitative correctness of properties of a system such as deadlock or livelock.{{cite book |editor1-first=Ulrich |editor1-last=Herzog |title=Formal Methods for Performance Evaluation |access-date=2009-04-21 |series=Lecture Notes in Computer Science |volume=4486 |date=May 2007 |publisher=Springer |doi=10.1007/978-3-540-72522-0 |pages=318–370 |chapter=Tackling Large State Spaces in Performance Modelling |chapter-url=http://aesop.doc.ic.ac.uk/pubs/large-state-spaces/ |isbn=978-3-540-72482-7 |archive-date=2008-04-12 |archive-url=https://web.archive.org/web/20080412014710/http://aesop.doc.ic.ac.uk/pubs/large-state-spaces/ |url-status=dead }}

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.

__TOC__

Syntax

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

:P ::= 0\,\,\, | \,\,\,a.P_1\,\,\, | \,\,\,A\,\,\, | \,\,\,P_1+P_2\,\,\, | \,\,\,P_1|P_2\,\,\, | \,\,\,P_1[b/a]\,\,\, | \,\,\,P_1{\backslash}a\,\,\,

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

; inactive process : the inactive process 0 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 \overset{\underset{\mathrm{def}}{}}{=} 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)

; summation : 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{\backslash}a is the process P_1 without action a

Related calculi, models, and languages

Some other languages based on CCS:

A Philippou, M Toro, M Antonaki. Simulation and Verification in a Process Calculus for Spatially-Explicit Ecological Models.

Scientific Annals of Computer Science 23 (1). 2014

  • Java Orchestration Language Interpreter Engine (Jolie){{Cite journal |last=Montesi |first=Fabrizio |last2=Guidi |first2=Claudio |last3=Lucchi |first3=Roberto |last4=Zavattaro |first4=Gianluigi|date=2007-06-27|title=JOLIE: a Java Orchestration Language Interpreter Engine|journal=Electronic Notes in Theoretical Computer Science |series=Combined Proceedings of the Second International Workshop on Coordination and Organization (CoOrg 2006) and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2006) |volume=181 |pages=19–33|doi=10.1016/j.entcs.2007.01.051 |issn=1571-0661|doi-access=free }}

Models that have been used in the study of CCS-like systems:

References

  • Robin Milner: A Calculus of Communicating Systems, Springer Verlag, {{ISBN|0-387-10235-3}}. 1980.
  • Robin Milner, Communication and Concurrency, Prentice Hall, International Series in Computer Science, {{ISBN|0-13-115007-3}}. 1989

{{Reflist}}

{{DEFAULTSORT:Calculus of communicating systems}}

{{Concurrent computing}}

Category:1980 in computing

Category:Process calculi