Process Calculus

A formal language used to specify the actions of processes and their sequential and concurrent composition. A process calculus has a formal semantics which is useful in attempts to prove certain properties about a software design, such as freedom from DeadLock or LiveLock, or that resources are fairly shared between concurrent processes. See ProofOfCorrectness.

Examples include:

• CSP, CommunicatingSequentialProcesses (http://archive.comlab.ox.ac.uk/csp.html). Also see FiniteStateProcesses.
• CCS (CalculusOfCommunicatingSystems?, RobinMilner, TuringAward 1991)
• the PiCalculus (http://www.cs.auc.dk/mobility/)
• the JoinCalculus

What is the relation between this and the ActionCalculi?

See http://www.cl.cam.ac.uk/users/rm135/ac9.ps . Essentially, ActionCalculi are descriptions of process calculi (and various other foundational models) using a common mathematical framework.

---

Any reason ActorsModel isn't listed here? It seems to be sufficiently formal to merit the label "calculus".

ActorsModel technically isn't a calculus because it (intentionally) is not specified as a notation or language, but rather as a collection of laws that may apply to a given language. So a ProcessCalculus can be an instantiation of the ActorsModel (such as the JoinCalculus, for example).

---

CategoryConcurrency