Process Algebra
Origin. Robin Milner developed CCS (Calculus of Communicating Systems, 1980) and later the π-calculus (1992). Tony Hoare developed CSP (Communicating Sequential Processes, 1978, 1985). Jan Bergstra and Jan Willem Klop developed ACP (Algebra of Communicating Processes, 1984). These provide algebraic frameworks for concurrent and distributed systems.
Models. Concurrent processes and their interactions. How do independent agents communicate, synchronize, and compose? Process algebras model systems where multiple things happen simultaneously, potentially interacting. Core question: when are two concurrent systems behaviorally equivalent?
Formalism.
CCS (Milner): Processes: P, Q, ... Actions: a, b, ... (input), ā, b̄, ... (output), τ (internal/silent)
Syntax:
- 0 (nil process, does nothing)
- a.P (prefix: do action a, then behave as P)
- P + Q (choice: behave as P or Q)
- P | Q (parallel composition: P and Q run concurrently)
- P \ L (restriction: hide actions in set L)
- P[f] (relabeling: rename actions via f)
Synchronization: a.P | ā.Q → τ.(P | Q) — complementary actions synchronize into τ.
CSP (Hoare): Events: a, b, ... (no input/output distinction in basic CSP)
- STOP (deadlock)
- a → P (prefix)
- P □ Q (external choice: environment chooses)
- P ⊓ Q (internal choice: process chooses)
- P ∥ Q (parallel with synchronization on common events)
- P ||| Q (interleaving, no synchronization)
- P \ A (hiding events in A)
Behavioral equivalences:
- Trace equivalence: same sequences of visible actions
- Bisimulation: processes simulate each other step-by-step
- Testing equivalence: same observable behavior under all tests
- Failures equivalence: same traces and deadlock conditions
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| . | — | Action prefix | Perform an action, then continue |
| + | — | Choice | CCS nondeterministic choice |
| | | — | Parallel | CCS concurrent composition |
| ~ | — | Bisimilarity | Step-by-step mutual simulation |
| τ | U+03C4 | Tau | Internal, unobservable action |
| ā | U+0101 | Latin small a with macron | Co-action complementary to a |
| \ | — | Restriction | Hide a set of actions (CCS) |
| □ | U+25A1 | White square | CSP external choice: the environment decides |
| ⊓ | U+2293 | Square cap | CSP internal choice: the process decides |
| ∥ | U+2225 | Parallel to | CSP parallel, synchronizing on shared events |
| ||| | — | Interleaving | CSP parallel with no synchronization |
| → | U+2192 | Prefix / transition | CSP prefix a → P; also a labelled step |
| STOP | — | Deadlock | CSP process that refuses every event |
| 0 | — | Nil | CCS process that does nothing |
Metatheory. Strong bisimilarity is a congruence for every CCS operator, so bisimilar processes may be substituted in any context; weak bisimilarity is not, since it fails to be preserved by +, and the largest congruence contained in it is observational congruence. The Hennessy–Milner theorem (1985) characterizes the equivalence logically: for image-finite processes, two states are bisimilar exactly when they satisfy the same formulas of Hennessy–Milner logic. Hennessy and Milner also gave a finite equational axiomatization, sound and complete for strong bisimilarity on finite CCS terms, using the expansion law to eliminate parallel composition. Moller (1990) proved that this detour is unavoidable: bisimilarity over CCS with parallel composition admits no finite equational axiomatization without an auxiliary operator such as left merge, which is why ACP includes one. Van Glabbeek's linear-time/branching-time spectrum orders the equivalences between trace and bisimulation, each with its own modal characterization. Bisimilarity is P-complete for finite-state processes, decidable by Paige–Tarjan partition refinement, and Christensen, Hüttel and Stirling (1992) proved it decidable for BPA, where language equivalence is not.
Applies to. Concurrent system specification. Protocol verification. Distributed systems. Model checking (CCS, CSP tools like FDR). Security protocol analysis. Biological systems modeling. Web service composition.
Limitations. There is no canonical equivalence. Van Glabbeek's spectrum is a lattice, not a point, and the choice among trace, failures, testing and bisimulation is a modelling decision the algebra does not settle, so a result proved for one need not transfer to another. Abstraction from internal actions loses the congruence property: weak bisimilarity is not preserved by +, and must be repaired by passing to observational congruence. Moller's theorem says the algebra cannot be purely behavioural — a finite axiomatization of parallel composition requires an auxiliary operator, left merge, with no independent operational reading. Composing n finite processes yields a state space exponential in n, and trace refinement between finite-state processes is PSPACE-complete, so the worst case is intractable independently of the tool. Beyond the well-behaved fragments bisimilarity is undecidable outright, as it is for Petri nets.
© 2026 Lingenic LLC