Calculus of communicating systems
This article needs additional citations for verification. (November 2011) (Learn how and when to remove this template message)
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.
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".
Given a set of action names, the set of CCS processes is defined by the following BNF grammar:
The parts of the syntax are, in the order given above
- empty process
- the empty process is a valid CCS process
- the process can perform an action and continue as the process
- process identifier
- write to use the identifier to refer to the process (which may contain the identifier itself, i.e., recursive definitions are allowed)
- the process can proceed either as the process or the process
- parallel composition
- tells that processes and exist simultaneously
- is the process with all actions named renamed as
- is the process without action
Related calculi, models, and languages
- 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.
- 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:
- 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
- Herzog, Ulrich, ed. (May 2007). "Tackling Large State Spaces in Performance Modelling". Formal Methods for Performance Evaluation. Lecture Notes in Computer Science. 4486. Springer. pp. 318–370. doi:10.1007/978-3-540-72522-0. Retrieved 2009-04-21.
- 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
- Montesi, Fabrizio; Guidi, Claudio; Lucchi, Roberto; Zavattaro, Gianluigi (2007-06-27). "JOLIE: a Java Orchestration Language Interpreter Engine". Electronic Notes in Theoretical Computer Science. 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). 181: 19–33. doi:10.1016/j.entcs.2007.01.051. ISSN 1571-0661.