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	Meaning
.	—	action prefix
+	—	choice
\|	—	parallel
~	—	bisimulation

Metatheory. Strong bisimulation is a congruence in CCS: bisimilar processes remain bisimilar in any context. Weak bisimulation abstracts from internal actions. Trace equivalence is coarser than bisimulation. CCS is Turing-complete. The π-calculus extends CCS with name-passing (channels can be sent as data), enabling mobility. Equational axiomatizations exist for finite processes.

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. Choice of equivalence matters: trace equivalence may equate processes that behave differently under parallel composition; bisimulation is finer but harder to check. State explosion: even finite CCS processes can generate exponentially large state spaces. Real-time and probability require extensions (timed CSP, probabilistic process algebra). The algebraic laws are elegant but proofs can be intricate. No single "right" process algebra: CCS, CSP, ACP differ in technical details and intended applications.