Principles of Model Checking

Chapters 3 explores types of rules that a transition system may satisfy: linear time properties.

The seventh chapter explores formal ways to compare transition systems, such as bisimulation; the eighth is about partial order reductions that aim to reduce the computation required to verify properties of a model.

Laroussinie found the textbook comprehensive and accessibly written, with a good number of examples, exercises and motivating ideas for key concepts.

[1] In ACM Computing Reviews, Gabriel Ciobanu believed the textbook could be used in advanced undergraduate or graduate courses, and would be useful to researchers.

Ciobanu praised the "clear and intuitive" presentation and said it "should be appreciated for its pedagogical approach to covering basic concepts, deep theoretical results, and advanced topics in model checking research".

Buchi automaton
An example transition system used to model a process