-calculus, seem to have surpassed it
in popularity when it comes to actual applications, dynamic logic has
always been and still remains a widely used and studied formalism, with
many applications, also outside the originally intended domain.
Yde Venema
Dynamic Logic
David Harel, Dexter Kozen and Jerzy Tiuryn
The MIT Press, Cambridge, Massachusetts
Hardback: ISBN 0-262-08289-6, $50
xv + 459 pages
Dynamic logic is the name for a family of logical formalisms that were
designed for reasoning about programs.
Paraphrasing the authors, we can described it technically as a blend
of three complementary classical ingredients: classical logic, modal
logic, and the algebra of regular events.
This blend dates back to the seventies, and although other logics, such
as temporal logic or the modal -calculus, seem to have surpassed it
in popularity when it comes to actual applications, dynamic logic has
always been and still remains a widely used and studied formalism, with
many applications, also outside the originally intended domain.
Naturally then, dynamic logic has been discussed in a fair number of survey papers, monographs and text books (some of those written by the indivual authors of this book themselves), but it is rather surprising that no earlier book could have been presented as ``the first comprehensive introduction to Dynamic Logic''. Where this book deserves such a qualification is an issue I will address after discussing the content of the book in some detail.
The main text of the book is divided into three parts of more or less equal length, and followed by a list of References and two navigation tools in the form of a useful list of Notation and Abbreviations and a well-designed Index.
Part I of the book, Fundamental Concepts, provides a 160 page survey of the background knowledge needed to understand the content of the book proper. The reader can find some basic information on mathematical prerequisites and extensive introductions to the theory of computation and to logic, together with a brief, informal introduction to reasoning about programs. I had some problems with this first part; not because of the quality of its exposition (which is exemplary) but because of its size which I found both too short and too long. Too short because the appearance of selfcontainment that Part I gives to the book is deceptive since it applies to knowledge rather than skills. I cannot imagine that any student without extensive prior exposure to logic and/or complexity theory will be able, on the basis of Part I, to go through this book successfully. But then, if the book is suitable only for readers with a firm formal background, this first part is far too detailed and, since it rather dominates the book and takes away a lot of space from the book's proper topics, it is far too long. Apart from this point, I also found some of the author's selection criteria debatable; for instance, why give a detailed exposition of equational logic and not of automata theory?
The second part of the book, on Propositional Dynamic Logic, is the one I liked best. In particular, the first half of its 120 pages provide an excellent exposition of the core theory of PDL; the authors carefully introduce the syntax and semantics, and continue with an elegant, crystal clear treatment of classical issues such as completeness and complexity of the satisfiability problem.
In the two remaining chapters of Part II the authors describe some variants of the standard propositional formalism. The chapter on various extensions of PDL with nonregular expressions makes a less crystallized impression, partly because of the seeming randomness of the formalisms that are introduced, partly because the main proof method, which uses pushdown tree automata, is not explained very well. The authors conclude this part with a chapter on a number of interesting variants of PDL, such as deterministic and concurrent PDL. This chapter was far too short for my taste, both because I have an personal research interest in some of the systems under discussion, but also because some of the proofs have been reduced to almost deceptive sketches. (To give one example, the completeness proof for deterministic PDL is certainly more involved than the proof sketch of Theorem 10.1 suggest.)
The third and final part of the book, First-Order Dynamic Logic, roughly counts 140 pages, most of which indeed discuss various versions of first-order DL. This part has a quite distinct flavor which is largely due the enormous expressive power that the combination of first-order logic and modal program operators provides. The authors introduce the large variety of first-order versions of DL, by carefully explaining that particular formalisms are not only determined by the set of program constructors, but also by the kind of atomic programs and test formulas, and by the auxiliary data structures one admits. In the subsequent chapters they develop the metamathematical theory of many of these formalisms, treating questions concerning complexity, axiomatizations and expressiveness in various degrees of detail. This part of the book is hard to summarize in a few lines; let me just say that although much of the material is of a fairly specialized nature, most of it is presented in a clear and lucid way (one unfortunate exception being the overly complicated introduction of the notion of spectral complexity).
The final two chapters of Part III are not so much about first-order
formalisms, but rather discuss variant of, different perspectives on,
and alternatives to, dynamic logic.
Topics treated include algorithmic logic, algebraic approaches to dynamic
logic such as dynamic algebras and Kleene algebras, temporal logics and
the modal -calculus.
As in the final chapters of Part II, I had the feeling that the allotted
space was too small to do justice to all of these topics.
Concluding my comments on the book's contents, I should mention that, despite the claim on comprehensiveness, some topics stand out by their absence. To start with, some of Dynamic Logic's closest logical neighbors are not mentioned at all; I'm thinking of description logics (see http://dl.kr.org/) in particular. Then, although the authors may advocate Dynamic Logic as a formal system for reasoning about programs, there are very few actual programs in the book, and the reader will not really see the formal system at work. Apparently, the authors are more interested in theoretical issues concerning the logic; but then it is surprising that some standard logical questions are not addressed at all. Take interpolation as an example (one with applicative relevance as well); as far as I know, it is still an open question whether PDL has Craig's interpolation property. Obviously I did not expect to see this book solve the problem, but I do feel that by omitting reference to interpolation altogether, the authors missed a chance of challenging the reader with an interesting research question. A similar example concerns the notion of bisimulation, which is not even mentioned in the book, although it is of fundamental importance in both modal logic and process theory,
I do believe this book provides a very good survey of the field of Dynamic Logic, despite the above list of omissions and despite the fact that the overly long introduction takes away space for more interesting details elsewhere. Almost every part of the book is written in a very clear style, while its exposition of the core theory of (propositional) dynamic logic is excellent. In short, this is an interesting, well-written book which will surely be the definitive text on dynamic logic for years to come. I can strongly recommend it to any researcher who wants to know the ins and outs of the field.
Would I also recommend the book for use in class?
The authors have used it in graduate courses, and each of the chapters is
closed by a list of exercises, so it is partly intended as a textbook.
Nevertheless, I have some hesitations here.
It is obvious that the book can only be used for advanced courses; but
for such a course, Part I would be too introductory, whereas Part III
is very specialized.
This would leave the second part on propositional dynamic logic, which
would provide excellent class room material.
But then, PDL is well covered by other texts as well, such as
Goldblatt's Logics of Time and Computation.