Communicating and mobile systems: The pi-calculus by Robin Milner
This was a really fantastic book, which develops a mathematical treatment of concurrency using some really beautiful mathematics.
The book starts with a chapter on Automata, covering regular languages and Arden’s rule which can be used to express the accepted languages of an automaton as a regular expression. The text then covers how we can study the interaction of such automata, by way of complementary transitions – one automata transitions using ‘a’ and the other transitions using ‘a bar’ at the same time. The text then moves on to labelled transition systems. Within this framework, we study the notion of strong simulation, where two such systems are equivalent if a series of external observations on one can be simulated by the other. This leads to a notion of bisimulation, when the two system simulate each other, making them equivalent when observed by an outside party which carries out experiments on them. Strong simulation, for example, allows the two machines a.(b|c) and a.b | a.c to be differentiated.
A language of process expressions is then defined, and a set of rules is given for determining the internal reactions of the system. This is studied and then a labelled transition system is defined for the system of process expressions. At this point we can apply strong bisimulation to allow us to determine when two process expressions are equivalent. At this point in the text, the use of induction over the height of the reduction tree together with case analysis of the last step of the reduction, allows us to almost magically derive a whole series of interesting results.
It turns out however, that we really want the internal transitions of the system to be ignored when we are considering if two processes are equivalent. Hence the text moves onto a notion of weak bisimulation. In this notion, any transition can be surrounded before and after by an arbitary number of internal reactions. The book then has a large number of examples of system for which the equivalence is proved.
Part two of the book moves onto the pi-calculus. This extends the process expressions from simply having two processes interact by having them both doing complementary transitions at the same time, to allowing a value to pass across a channel between the two processes. This monadic pi-calculus is extended to a polyadic pi-calculus using syntactic sugaring, allowing a vector of values to be passed by first passing new channel and then passing values across this new local channel. We then go on to look at strong and weak bisimulation using this new system. Along the way, there are many examples, including the translation of the lambda calculus into this computational model and the use of sorts which allows the checking of the validity of the channel interactions and also allows more proofs to be derived for certain types of interactions where the sorts constrain the interactions. Examples also show how an object oriented language can be embedded into the framework.
In summary, a thought provoking book with some beautiful theory.