Model Checking Reading Club/Baier, Katoen: Principles of Model Checking

These pages contain remarks and comments – many typos and errata, some proposals for change – that we have found during reading the book:

Principles of model checking / Christel Baier; Joost-Pieter Katoen. – Cambridge, Mass.: MIT Press, 2008.

ISBN 978-0-262-02649-9.

We are a reading group consisting of staff members at the Computer Science Department of the Radboud Universiteit in Nijmegen, the Netherlands. Additionally, Tim Leonard has contributed some remarks.

The information is mainly addressed to the authors (Christel Baier and Joost-Pieter Katoen); however, we have seen that also others may profit from reading it. As we haven't read all chapters completely, you will find that the number of comments differs considerably between chapters.

General Comments

• I think, to make proofs more understandable, it would be nice to present the proof idea by an example or at least to combine the proofs with examples. Faranak Heidarian

Comments to Single Chapters

• Frontmatter, Preface
• Chapter 1: System Verification
• Chapter 2: Modeling Concurrent Systems
• Chapter 3: Linear-Time Properties
• Chapter 4: Regular Properties
• Chapter 5: Linear Temporal Logic
• Chapter 6: Computation Tree Logic
• Chapter 7: Equivalences and Abstraction
• Chapter 8: Partial Order Reduction
• Chapter 9: Timed Automata
• Chapter 10: Probabilistic Systems
• Appendix A: Appendix: Preliminaries