Calculus of communicating systems: Difference between revisions
Gareth Jones (talk | contribs) m increasing spacing in BNF grammar definition |
Gareth Jones (talk | contribs) m adding comment about livelock/deadlock diagnosis (with reference) |
||
| Line 1: | Line 1: | ||
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. |
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]].<ref>{{cite book |editor1-first=Ulrich |editor1-last=Herzog |title=Formal Methods for Performance Evaluation |accessdate=2009-04-21 |series=Lecture Notes in Computer Science |volume=4486 |year=2007 |month=May |publisher=Springer |doi=10.1007/978-3-540-72522-0 |pages=318–370 |chapter=Tackling Large State Spaces in Performance Modelling |chapterurl=http://aesop.doc.ic.ac.uk/pubs/large-state-spaces/ }}</ref> |
||
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". |
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". |
||
| Line 36: | Line 36: | ||
* Robin Milner: ''A Calculus of Communicating Systems'', Springer Verlag, ISBN 0-387-10235-3. 1980. |
* 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-131-15007-3. 1989 |
* Robin Milner, ''Communication and Concurrency'', Prentice Hall, International Series in Computer Science, ISBN 0-131-15007-3. 1989 |
||
{{Reflist}} |
|||
[[Category:Process calculi]] |
[[Category:Process calculi]] |
||
Revision as of 13:17, 21 April 2009
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.[1]
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:
![{\displaystyle P::=0\,\,\,|\,\,\,a.P\,\,\,|\,\,\,A\,\,\,|\,\,\,P+Q\,\,\,|\,\,\,P|Q\,\,\,|\,\,\,P[b/a]\,\,\,|\,\,\,P\backslash a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e5d90e96e43af30d453f0f40257fd48cf83fe05b)
The parts of the syntax are, in the order given above
- empty process
- the empty process 0 is a valid CCS process
- action
- the process a.P can perform an action a and continue as the process P
- process identifier
- write to use the identifier A to refer to the process P
- choice
- the process P+Q can proceed either as the process P or the process Q
- parallel composition
- processes P and Q exist simultaneously
- renaming
- P[b/a] is the process P with all actions named a renamed as b
- restriction
- P\a is the process P without action a
Related calculi and models
- 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.
Some other languages based on CCS:
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-131-15007-3. 1989
- ^ Herzog, Ulrich, ed. (2007). "Tackling Large State Spaces in Performance Modelling". Formal Methods for Performance Evaluation. Lecture Notes in Computer Science. Vol. 4486. Springer. pp. 318–370. doi:10.1007/978-3-540-72522-0.
{{cite book}}:|access-date=requires|url=(help); External link in|chapterurl=|chapterurl=ignored (|chapter-url=suggested) (help); Unknown parameter|month=ignored (help)
 | This computer science article is a stub. You can help Wikipedia by expanding it. |