The authors of this monograph basically address one problem: generating an algorithm that model checks a formula in linear temporal logic against a product transition system. The authors reduce the question to three basic problems, and present ways of solving the problems. Throughout, the emphasis is on the basic difficulty that model checking encounters, namely the state explosion that takes place when dealing with concurrent systems.

This could have been a research paper instead of a book. The authors smartly realized, however, that quite a bit of concurrency and verification theory comes into play, including unfoldings, Mazurkiewicz traces, livelocks, and Büchi automata (which they call testers). The presentation is detailed without being overly pedantic. I also liked the fact that complexity aspects are always kept in mind, and lower bounds and upper bounds are provided whenever available. References are also provided, as well as pointers to software. This book can be used as a reading course in this area for graduate students; I intend to use it in this way.

I think this is a refreshing way of looking at concurrency and verification, particularly at this time, when the early work of Clarke, Emerson, and Sifakis has attained the status of a Turing award.