This is a book on modal logic as it was in the 1980s, when this reviewer wrote his dissertation (and probably when the authors did as well). In the '90s, I worked on modal logics to describe behaviour of computational structures. While reviewing this book, I wondered what it would have been like to have it around at that time.
The authors express their annoyance with the view that modal logic amounts to rather simple-minded uses of two operators Diamond and Box. Instead they concentrate on more general results, and to the connection of modal logic to first-order logic, algebra and computational complexity. Although the blurb says prior acquaintance with first-order logic and its semantics is assumed, I would go further and demand prior acquaintance with the model theory of first-order logic. Ultrafilters, ultraproducts and ultrapowers pop up everywhere and if you don't know how they work, the book might seem a bit intimidating.
Assuming such a background, some of the results proved in an accessible way here are the Jónsson-Tarski theorem ('52), Bull's theorem ('66), the Goldblatt-Thomason theorem ('74), Sahlqvist's theorems on correspondence and completeness ('75), Ladner's theorem ('77) and van Benthem's characterization of modal logic in classical logic ('83).
The core chapters are ``Models'', ``Frames'' and ``Completeness'', supplemented by chapters on ``Algebras'' and ``Computation''. In a final chapter, the authors sketch more recent ``Extensions'', such as the Sahlqvist theorem for the difference operator ('93) and a modal Lindström theorem ('95). These show once again the authors' interest in explaining general results.
I think the book has a definite audience among logicians, but I want to focus upon the utility for computer scientists. I liked the treatment of bisimulation in the Models chapter, but was baulked by the constant reference to first-order logic.
In their recommendation on a course for computer scientists, the authors put in the canonical results from the Completeness chapter, but not the sections on transforming the canonical model, on the step-by-step method and on rules for the undefinable. Axiomatizations for semantically driven models require these techniques, and they are mentioned only briefly in treatments like Hughes and Creswell [HC96]. In [LRT92], [LPRT95], we had to work our way through these techniques, inspired by Krister Segerberg and John Burgess (in [HPL84]). Having these sections at hand in a book would have been invaluable. I wondered why Since and Until were banished to the chapter on Extensions, they could have been dealt with here. On the other hand, the last section on Bull's theorem seems to fit in more with the Frames chapter.
The Algebras chapter seems a bit unmotivated. General frames are introduced as models and algebras rolled into one, whereas the intuition of [HC96] that general frames are between models and frames, in that they preserve substitution, seems more insightful.
The Computation chapter is excellent. I liked the sections on quasi-models and mosaics and on undecidability (again, work carried out by us ab initio in [LRT93], [LPRT95] where a book would have been welcome) and especially the three sections on NP, PSPACE and EXPTIME. From the last chapter, I enjoyed the treatment of the guarded and packed fragments of first-order logic.
To sum up, the book is good on what it promises to deliver, and useful to have as a reference. There are four appendices on necessary background, an excellent annotated and classified bibliography and a decent index. The historical notes at the end of every chapter are also useful, although they tend to be a bit Amsterdam-centred. For instance, for all the authors' lament over the neglect of algebra in modal logic, only a single mention is made of the work of Helena Rasiowa, Roman Sikorski and their Polish school. The topological connections that they made from modal logic, extending the work of Marshall Stone, are not touched upon.
Fitting in with the book's style, I would have liked to see the characterization of modal mu-calculus within monadic second-order logic by David Janin and Igor Walukiewicz [JW96], and as a convincing algebraic application, the completeness proof of modal mu-calculus via modal mu-algebras by Simon Ambler, Marta Kwiatkowska and Nicholas Measor [AKM95].
For computer scientists, a book more oriented to their needs is necessary. For instance, those intending to learn about how to use modal logic to model their particular system need not bother with this book.
The authors wish to acknowledge and incorporate ideas from computer science, but this is mainly limited to propositional dynamic logic. Perhaps the main lesson to be learnt from computer science is that fragments of second-order logic are more important for its purposes than first-order logic. In particular, dealing with ``second-order'' behaviours generated from finite transition structures and the connection to automata theory is not addressed here. Where I felt the book was definitely dated from our viewpoint is in the total absence of model checking: this has been a significant contribution of computer science to modal logic.
The book by Michael Huth and Mark Ryan [HR00] is good on these aspects, although perhaps not general enough to suit the authors' tastes.
There are remarkably few typos and a list is put up at the book's webpage. The few I could find outside this are:
In Exercise 3.7.1, the transitivity formula is wrongly written.
In the Notes to Chapter 3, last paragraph, fourth line from the bottom,
``model version'' should be ``modal version''.