<p>For the $\pi$-calculus, the following texts should be of interest. [<a href="http://www.cambridge.org/us/knowledge/isbn/item1161297/?site_locale=en_US" rel="nofollow">1</a>] is a relatively gentle introduction while [<a href="http://www.cambridge.org/gb/knowledge/isbn/item1151382/The%20Pi-Calculus/?site_locale=en_GB" rel="nofollow">2</a>] 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 [<a href="http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/ECS-LFCS-89-85.ps" rel="nofollow">3</a>] 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 [<a href="http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-86/ECS-LFCS-89-86.ps" rel="nofollow">4</a>]. Finally, if you have not encountered process theory, the original CCS book [<a href="http://books.google.com.ar/books/about/Communication_and_Concurrency.html?id=QPyyQgAACAAJ&amp;redir_esc=y" rel="nofollow">5</a>] 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.</p>

<p>Regarding the spi-calculus, I suggest to look at the original paper [<a href="http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps" rel="nofollow">6</a>], but note that the spi-calculus has largely been superseded by the applied pi-calculus [<a href="ftp://apotheca.hpl.hp.com/pub/DEC/SRC/publications/ma/spi-dist2.pdf" rel="nofollow">7</a>]. The applied pi-calculus is widely used in modelling cryptographic protocols. [<a href="http://seclab.stanford.edu/pcl/cs259/WWW06/papers/p104-abadi.pdf" rel="nofollow">8</a>] is a tutorial of applied pi.</p>

<ol>
<li><p><a href="http://www.cambridge.org/us/knowledge/isbn/item1161297/?site_locale=en_US" rel="nofollow">Communicating and Mobile Systems: The $\pi$ Calculus</a>, by R. Milner.</p></li>
<li><p><a href="http://www.cambridge.org/gb/knowledge/isbn/item1151382/The%20Pi-Calculus/?site_locale=en_GB" rel="nofollow">The $\pi$-Calculus: A Theory of Mobile Processes</a>, by D. Sangiorgi and D. Walker.</p></li>
<li><p>A Calculus of Mobile Processes, <a href="http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/ECS-LFCS-89-85.ps" rel="nofollow">Part 1</a> and <a href="http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-86/ECS-LFCS-89-86.ps" rel="nofollow">Part 2</a>, by R. Milner, J. Parrow and D. Walker.</p></li>
<li><p><a href="http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps" rel="nofollow">The Polyadic pi-Calculus: A Tutorial</a>, by R. Milner.</p></li>
<li><p><a href="http://books.google.com.ar/books/about/Communication_and_Concurrency.html?id=QPyyQgAACAAJ&amp;redir_esc=y" rel="nofollow">Communication and Concurrency</a>, by R. Milner.</p></li>
<li><p><a href="ftp://apotheca.hpl.hp.com/pub/DEC/SRC/publications/ma/spi-dist2.pdf" rel="nofollow">A Calculus for Cryptographic Protocols The Spi Calculus</a>, by M. Abadi and A. Gordon.</p></li>
<li><p><a href="http://seclab.stanford.edu/pcl/cs259/WWW06/papers/p104-abadi.pdf" rel="nofollow">Mobile values, new names, and secure communication</a>, by M. Abadi and C. Fournet.</p></li>
<li><p><a href="http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/11-applied-pi.extended.pdf" rel="nofollow">Applied pi calculus</a>, by M. Ryan and B. Smyth.</p></li>
</ol>

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

CC BY-SA 3.0
2012-12-23T10:36:30.687Z
2012-12-23T18:43:26.017Z
2012-12-23T18:43:26.017Z
Martin Berger
<p><a href="http://is.ifmo.ru/books/_principles_of_model_checking.pdf" rel="nofollow">Principles of Modelchecking</a> is in my opinion "the book" on modelchecking.</p>

<p>It is very comprehensive, understandable and beautifully written.</p>

CC BY-SA 3.0
2012-12-24T08:44:36.113Z
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
CC BY-SA 3.0
2012-12-24T09:13:52.097Z
maybe I'm a bit biased since I study under one of the authors. As a beginner this book is perfect.
Ronny Brendel
CC BY-SA 3.0
2012-12-24T09:32:35.860Z
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
CC BY-SA 3.0
2012-12-23T22:45:38.267Z
2012-12-24T09:11:44.763Z
2012-12-24T09:11:44.763Z
Ronny Brendel
<p>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. </p>

<p>(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.) </p>

<p>Merry Christmas. </p>

CC BY-SA 3.0
2012-12-24T12:11:51.570Z
2012-12-24T12:18:54.407Z
2012-12-24T12:18:54.407Z
Markus
<p>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?</p>

<p>(s)pi calculus</p>

<p>model checking</p>

<p>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.</p>

<reference-request><pl.programming-languages><big-list>
References on model checking and pi calculi
dts
# References on model checking and pi calculi

(Asked by: username_0 on 2012-12-20)

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.

**Tags:** reference-request, pl.programming-languages, big-list


---

## 3 answers

### Answer by username_1 on 2012-12-23. Score: 5

For the $\pi$-calculus, the following texts should be of interest. [[1](http://www.cambridge.org/us/knowledge/isbn/item1161297/?site_locale=en_US)] is a relatively gentle introduction while [[2](http://www.cambridge.org/gb/knowledge/isbn/item1151382/The%20Pi-Calculus/?site_locale=en_GB)] 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](http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/ECS-LFCS-89-85.ps)] 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](http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-86/ECS-LFCS-89-86.ps)]. Finally, if you have not encountered process theory, the original CCS book [[5](http://books.google.com.ar/books/about/Communication_and_Concurrency.html?id=QPyyQgAACAAJ&redir_esc=y)] 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](http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps)], but note that the spi-calculus has largely been superseded by the applied pi-calculus [[7](ftp://apotheca.hpl.hp.com/pub/DEC/SRC/publications/ma/spi-dist2.pdf)]. The applied pi-calculus is widely used in modelling cryptographic protocols. [[8](http://seclab.stanford.edu/pcl/cs259/WWW06/papers/p104-abadi.pdf)] is a tutorial of applied pi.

1. [Communicating and Mobile Systems: The $\pi$ Calculus](http://www.cambridge.org/us/knowledge/isbn/item1161297/?site_locale=en_US), by R. Milner.
2. [The $\pi$-Calculus: A Theory of Mobile Processes](http://www.cambridge.org/gb/knowledge/isbn/item1151382/The%20Pi-Calculus/?site_locale=en_GB), by D. Sangiorgi and D. Walker.
3. A Calculus of Mobile Processes, [Part 1](http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/ECS-LFCS-89-85.ps) and [Part 2](http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-86/ECS-LFCS-89-86.ps), by R. Milner, J. Parrow and D. Walker.
4. [The Polyadic pi-Calculus: A Tutorial](http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps), by R. Milner.
5. [Communication and Concurrency](http://books.google.com.ar/books/about/Communication_and_Concurrency.html?id=QPyyQgAACAAJ&redir_esc=y), by R. Milner.
6. [A Calculus for Cryptographic Protocols The Spi Calculus](ftp://apotheca.hpl.hp.com/pub/DEC/SRC/publications/ma/spi-dist2.pdf), by M. Abadi and A. Gordon.
7. [Mobile values, new names, and secure communication](http://seclab.stanford.edu/pcl/cs259/WWW06/papers/p104-abadi.pdf), by M. Abadi and C. Fournet.
8. [Applied pi calculus](http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/11-applied-pi.extended.pdf), 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.


---

### Answer by username_2 on 2012-12-23. Score: 1

[Principles of Modelchecking](http://is.ifmo.ru/books/_principles_of_model_checking.pdf) is in my opinion "the book" on modelchecking.

It is very comprehensive, understandable and beautifully written.

> **Comments:**
> **username_3**: 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.  
> **username_2**: maybe I'm a bit biased since I study under one of the authors. As a beginner this book is perfect.  
> **username_3**: I think having personal preferences is perfectly fine, as long as you make it explicit, especially if you have connections to the authors.  

---

### Answer by username_4 on 2012-12-24. Score: 0

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.


---

