Process calculi are algebraic frameworks for modeling and reasoning about concurrent and communicating systems. CCS (Calculus of Communicating Systems), created by Robin Milner, models processes that synchronize via named channels, with an algebraic syntax for parallel composition, choice, restriction, and recursion. The pi-calculus extends CCS with name passing — channels can transmit channel names, enabling dynamic reconfiguration of communication topology. Process equivalences, particularly bisimulation, provide rigorous criteria for when two processes exhibit the same observable behavior. Process calculi serve as the theoretical foundation for session types, concurrent programming models, and formal analysis of communication protocols.
Process calculi provide algebraic languages for describing concurrent systems — collections of processes that compute independently and interact through communication. Unlike lambda calculus (which models sequential computation via function application) or Turing machines (which model computation via tape manipulation), process calculi take interaction as the primitive concept. The fundamental operation is not evaluation or state transition but communication between processes.
CCS (Calculus of Communicating Systems), introduced by Robin Milner in 1980, builds processes from a small set of operators. Prefix (a.P: do action a then behave as P) sequences actions. Choice (P + Q: behave as either P or Q, nondeterministically) models branching. Parallel composition (P | Q: P and Q run concurrently) models concurrency. Restriction ((new a)P: make channel a private to P) models scope. Recursion (rec X.P: recursive process) models repetition. Communication occurs when parallel processes perform complementary actions on the same channel: a.P | a-bar.Q can synchronize, producing a silent (tau) transition and evolving to P | Q. This synchronous handshake is CCS's model of interaction.
The pi-calculus, introduced by Milner, Parrow, and Walker in 1992, adds a crucial capability: name passing. In CCS, communication transmits no data — it is pure synchronization. In the pi-calculus, communication transmits channel names: a<b>.P sends the name b on channel a, and a(x).Q receives a name on channel a, binding it to x. Since the received name can be used for further communication, the communication topology evolves dynamically. A process can receive a fresh channel name and use it to talk to a previously unknown partner. This makes the pi-calculus expressive enough to model mobile systems, object-oriented programming (where objects are processes and method calls are channel communications), and protocols that establish private sessions.
Bisimulation is the key equivalence notion. Two processes are bisimilar if they can match each other's actions step for step, at every point maintaining the ability to continue matching. Formally, a bisimulation is a relation R such that whenever (P, Q) is in R and P transitions via action a to P', then Q can also transition via a to some Q' where (P', Q') is in R — and symmetrically. Bisimulation is strictly finer than trace equivalence (which only compares the sets of possible action sequences): two processes can have identical traces but differ in their branching structure, and bisimulation detects this difference. This sensitivity to branching makes bisimulation the right equivalence for reasoning about interactive systems, where the environment can observe and influence choices.
Process calculi are the theoretical foundation for several practical developments. Session types (discussed separately) use pi-calculus channels as the substrate for typed communication protocols. The actor model (used in Erlang and Akka) is closely related to asynchronous pi-calculus. Formal verification of communication protocols often models the protocol in a process calculus and checks properties like deadlock freedom, livelock freedom, and secrecy using bisimulation or model checking. Tools like mCRL2 and the Mobility Workbench implement process-algebraic verification. The pi-calculus's encoding of the lambda calculus establishes it as a Turing-complete model of computation, demonstrating that interaction is as fundamental as computation itself.