The π-calculus is a process algebra for modelling concurrency. The π-calculus allows dynamic topologies of processes to be modelled, whereas the earlier CCS (calculus of communicating systems) and CSP (communicating sequential processes) process algrebras could only model static (unchanging) topologies. The best introductory work that I've found so far is An Introduction to the pi-Calculus
It is far more approachable than the tutorial by Robin Milner (The Polyadic π-Calculus: A Tutorial
). An interesting recent work is
Algebraic Process Calculi:
The First Twenty Five Years and Beyond
, which are the proceedings from a workshop held in 2005. It appears that in the last 25 years there has been an explosion in the number of process algebras, and that there is quite a lot of research being performed in this area. So understanding the π-calculus is really just a beginning!
I've started trying to model the Minix-3 system using the π-calculus. It is mainly a pedagogical exercise - my immediate aim is to become more familiar with the π-calculus, but it would be nice to start using the process algebra to start proving behaviours about Minix-3.