Principles of Model Checking

An example transition system used to model a process

The introduction and first chapter outline the field of model checking: a model of a machine or process can be analysed to see if desirable properties hold. For instance, a vending machine might satisfy the property "the balance can never fall below €0,00". A video game might enforce the rule "if the player has 0 lives then the game ends in a loss". Both the vending machine and video game can be modelled as transition systems. Model checking is the process of describing such requirements in mathematical language, and automating proofs that the model satisfies the requirements, or discovery of counterexamples if the model is faulty.

The second chapter focuses on creating an appropriate model for concurrent systems, where multiple parts of an algorithm (set of instructions) can be carried out simultaneously by different machines or parts of a machine.

Chapters 3 explores types of rules that a transition system may satisfy: linear time properties. A safety property, such as "no deadlock states are possible", is of the form "an undesirable outcome can never occur". A liveness property, such as "a shared resource will always eventually be made available to a component that requests it", is of the form "a desirable outcome will eventually happen". Fairness properties such as "a traffic light never stops changing colour" can be used as preconditions i.e. assumptions from which other properties can be deduced.

The fourth chapter is about regular and ω-regular language properties, and theoretical machines such as Büchi automata that model the languages. It gives model-checking algorithms to verify properties or find counterexamples.

The fifth and sixth chapters explore linear temporal logic (LTL) and computation tree logic (CTL), two classes of formula that express properties. LTL encodes requirements about paths through a system, such as "every Monopoly player passes 'Go' infinitely often"; CTL encodes requirements about states in a system, such as "from any position, all players can eventually land on 'Go'". CTL* formulae, which combine the two grammars, are also defined. Algorithms for model-checking formulae in these logics are given.

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. The ninth and tenth chapters are about extensions to the logics and automata previously considered, including through addition of a clock speed (timed automata) or probabilities (probabilistic automata, based on Markov chains).

François Laroussinie, writing in The Computer Journal, recommended the book to researchers, lecturers, students and engineers, calling the book "impressive". Laroussinie found the textbook comprehensive and accessibly written, with a good number of examples, exercises and motivating ideas for key concepts. With a "unified framework", the first seven chapters cover classical theory and the last three chapters cover extensions of model checking.[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".[2]

In 2014, the book was one of the five most-cited academic texts monitored by the Book Citation Index (BKCI).[3]

• Lange, Martin (2010), MathSciNet, MR 2493187{{citation}}: CS1 maint: untitled periodical (link)

• Official website