# References on model checking and pi calculi

I'm a mathematician and it looks like I need to learn about these topics. What would be good references that go into the technical details of the following topics?

(s)pi calculus

model checking

I'm not really interested in applying these tools, but in their actual mathematical constructions, since it looks like they might contain ideas that I'm looking for.

-

For the $\pi$-calculus, the following texts should be of interest. [1] is a relatively gentle introduction while [2] summarises the state of the art about 10 years ago. A lot of progress has been made since, but that's not yet written up in a textbook. The original papers [3] are also quite readable but contain much detail that may overwhelm a novice (or may be instructive, since it's usually omitted in later accounts). Milner has written a little tutorial [4]. Finally, if you have not encountered process theory, the original CCS book [5] might be a good place to do so. It deals with CCS, a predecessor to the $\pi$ calculus, and key technical ideas in the theory of $\pi$-calculus like bisimulation are explained in a simpler setting.

Regarding the spi-calculus, I suggest to look at the original paper [6], but note that the spi-calculus has largely been superseded by the applied pi-calculus [7]. The applied pi-calculus is widely used in modelling cryptographic protocols. [8] is a tutorial of applied pi.

1. Communicating and Mobile Systems: The $\pi$ Calculus, by R. Milner.

2. The $\pi$-Calculus: A Theory of Mobile Processes, by D. Sangiorgi and D. Walker.

3. A Calculus of Mobile Processes, Part 1 and Part 2, by R. Milner, J. Parrow and D. Walker.

4. The Polyadic pi-Calculus: A Tutorial, by R. Milner.

5. Communication and Concurrency, by R. Milner.

6. A Calculus for Cryptographic Protocols The Spi Calculus, by M. Abadi and A. Gordon.

7. Mobile values, new names, and secure communication, by M. Abadi and C. Fournet.

8. Applied pi calculus, by M. Ryan and B. Smyth.

If you spell out the ideas you are looking for, maybe we can give you more focussed reading recommendations.

-

Principles of Modelchecking is in my opinion "the book" on modelchecking.

It is very comprehensive, understandable and beautifully written.

-
I'm not sure what "the" means here. If that is your opinion, it would be good to emphasise this. I do not believe there is common consensus on what the definitive reference on model checking is. – Vijay D Dec 24 '12 at 8:44
maybe I'm a bit biased since I study under one of the authors. As a beginner this book is perfect. – Ronny Brendel Dec 24 '12 at 9:13
I think having personal preferences is perfectly fine, as long as you make it explicit, especially if you have connections to the authors. – Vijay D Dec 24 '12 at 9:32

Depending on the depth you want to understand the topic, I can also recommend the (nicely written) article "an automata theoretic approach to branching time model checking" by Kupferman, Vardi, and Wolper. It presents a unified approach for model checking LTL, CTL, CTL*, and mu-calculus. I see this approach as a versatile set of tools to handle proof obligations on finite state systems. The article also contains many useful pointers to earlier approaches.

(In my oppinion, the book "principles of model checking", though perfectly fine for teaching, is a little too wordy to enter the material as a researcher. It also does not contain the approach of the article above, but relies on older approaches building solely on nondeterministic Büchi automata on words instead of alternating Büchi automata on trees.)

Merry Christmas.

-