A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://en.wikipedia.org/wiki/Calculus_of_communicating_systems below:

Calculus of communicating systems - Wikipedia

From Wikipedia, the free 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, summation 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.

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 ∖ a {\displaystyle 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 {\displaystyle 0} is a valid CCS process
action
the process a . P 1 {\displaystyle a.P_{1}} can perform an action a {\displaystyle a} and continue as the process P 1 {\displaystyle P_{1}}
process identifier
write A = d e f P 1 {\displaystyle A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}} to use the identifier A {\displaystyle A} to refer to the process P 1 {\displaystyle P_{1}} (which may contain the identifier A {\displaystyle A} itself, i.e., recursive definitions are allowed)
summation
the process P 1 + P 2 {\displaystyle P_{1}+P_{2}} can proceed either as the process P 1 {\displaystyle P_{1}} or the process P 2 {\displaystyle P_{2}}
parallel composition
P 1 | P 2 {\displaystyle P_{1}|P_{2}} tells that processes P 1 {\displaystyle P_{1}} and P 2 {\displaystyle P_{2}} exist simultaneously
renaming
P 1 [ b / a ] {\displaystyle P_{1}[b/a]} is the process P 1 {\displaystyle P_{1}} with all actions named a {\displaystyle a} renamed as b {\displaystyle b}
restriction
P 1 ∖ a {\displaystyle P_{1}{\backslash }a} is the process P 1 {\displaystyle P_{1}} without action a {\displaystyle a}

Some other languages based on CCS:

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


RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4