Calculus of communicating systems
- 2 min read
- 2 chapters
Explore on Lably
ToursExplore Lably’s 3D toursAccording 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:
- ref
The parts of the syntax are, in the order given above
- inactive process
- the inactive process is a valid CCS process
- action
- the process can perform an action and continue as the process
- process identifier
- define , and then use the identifier to refer to the process (which may contain the identifier itself, i.e., recursive definitions are allowed)
- summation
- 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
Sign in to keep reading
One more chapter is free with a Lably account.
Related calculi, models, and languages
- Communicating sequential processes (CSP), developed by Tony Hoare, is a formal language that arose at a similar time to CCS.
- The Algebra of Communicating Processes (ACP) was developed by Jan Bergstra and Jan Willem Klop in 1982, and uses an axiomatic approach (in the style of Universal algebra) to reason about a similar class of processes as CCS.
- The pi-calculus, developed by Robin Milner, Joachim Parrow, and David Walker in the late 80's extends CCS with 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.
- Reversible Communicating Concurrent Systems (RCCS) introduced by Vincent Danos, Jean Krivine, and others, introduces (partial) reversibility in the execution of CCS processes.
Some other languages based on CCS:
- Calculus of broadcasting systems
- Language Of Temporal Ordering Specification (LOTOS)
- Process Calculus for Spatially-Explicit Ecological Models (PALPS) is an extension of CCS with probabilistic choice, locations and attributes for locations
- Java Orchestration Language Interpreter Engine (Jolie)
Models that have been used in the study of CCS-like systems:
- History monoid
- Actor model