Given that Springer already has two books on the subject of finite model theory and descriptive complexity [1,2], one would think the market was saturated, but clearly there is room for more. That Libkin has managed to produce an interesting treatment, in spite of the competition, is impressive.
The book begins with introductory and background chapters with sections highlighting the connections to other areas in logic and computer science. Then we have the mandatory chapter on Ehrenfeucht-Fraïssé games, but with more emphasis on explaining why they work. Instead of Hintikka formulas (more common in classical logic), types are used (as is more common in finite model theory). This is also evident later, when the Abiteboul-Vianu theorem is proven using ordering of types.
I particularly liked the chapter on locality of first-order (FO) logic (an area Libkin has done a lot of work). Both in this and the previous chapter, on games, there is a conscious effort to be formal but to retain intuition as one wades through the formalism.
After a brief treatment of order-invariant FO logic, there is an excellent chapter on FO model checking. I liked the careful distinction between data, expression, combined and fixed-parameter complexity. Perhaps the complexity of satisfiability (which comes three chapters later) could have been brought into this discussion, to clarify how this yields another notion of the complexity of a logic.
Monadic second-order logic (MSO) and counting quantifiers are treated next, before Fagin's theorem is proven. A chapter on fixed point logics follows. Since this is technically the hardest part, going through FO and existential second-order logics earlier is a good warm up strategy for teaching.
A couple of chapters on finite variable logics and zero-one laws follow. There is also a nice chapter on embedded model theory, which applies to databases which use integers or reals as data (such as those which store maps). I personally was unaware of this line of work and enjoyed reading about it. There is a final chapter discussing other applications, notably temporal logic and constraints.
Libkin concentrates on making his book a text; the other two mentioned earlier in this review were monographs, more suitable for a seminar course than a regular graduate course. The latter is what Libkin targets.
Immerman's book [1] concentrates on making results accessible. For example, it has a proof that parity is not in AC0, a result that is used without proof by Libkin.
Ebbinghaus and Flum's book [2] is more oriented towards presenting techniques, which is what Libkin also concentrates on. But while the students reading Ebbinghaus and Flum are expected to have a thorough grounding in logic, those reading Libkin's book are expected to be more familiar with databases (as in the connection of, for example, SQL to FO logic).
In summary, I welcome Libkin's book as an interesting text from the database point of view. Perhaps in a few years' time, we will understand finite model theory well enough to start with the SQL-FO connection and provide a treatment that undergraduates can tackle.
References
[2] N. Immerman. Descriptive complexity, Springer, 1998.
[1] H.-D. Ebbinghaus and J. Flum. Finite model theory, Springer, 1995.