Review from reviews.com

The plethora of textbooks giving a computing viewpoint on logic is evidence that logic is central to the study of computer science, but is there room for yet another? If this text covered the familiar ground, the answer would probably be “no,” but Huth and Ryan have chosen to illustrate their text with up-to-date, relevant, and challenging case studies of how logic is being used in practice, rather than the more pedestrian and predictable examples given in many texts. In particular, they cover model checking--which is arguably the great success story of the application of logic in computing over the last decade--as well as modal logics for reasoning about belief and the more traditional application of logic to imperative program verification.

The first two chapters cover propositional and predicate logic, with an emphasis on proof in a natural deduction system. The most difficult aspect of natural deduction systems is the way in which assumptions are introduced and discharged; the authors use a box notation to delimit the scope of assumptions. Natural deduction systems are the best for the construction of proofs by the learner, and while no notation can make the discharge of assumptions into a routine operation, the authors’ choice makes good sense for the beginner. These chapters, and indeed the whole book, are well supplied with exercises that range from the routine to the more challenging.

The third chapter is where the book departs from the well-trodden path by introducing model checking for the temporal logic computation tree logic (CTL), a branching time logic whose model checking problem is tractable. The model checking problem is to ascertain whether a particular structure--a finite structure of “possible worlds,” or a transition system--satisfies (“is a model for”) a formula of CTL. Model checking is attractive for a number of reasons. It can be performed automatically, it can be implemented efficiently (see remarks on chapter 6 below), and when a structure fails to satisfy a formula, the algorithm can produce a counterexample in the form of a trace of the system that does not exhibit the required behavior. The authors first introduce CTL and illustrate its use in practical specification problems. They then present a naive model checking algorithm and discuss its implementation in the SMV system.

Chapter 6 contains an excellent exposition of binary decision diagrams (BDDs), a novel representation of Boolean functions. Given an ordering on the variables of a function, a reduced, ordered BDD gives a canonical representation of the Boolean function; more traditional representations such as conjunctive and disjunctive normal forms fail to have this property. Having canonical representations of Boolean functions has a number of consequences: testing for satisfiability and validity becomes a matter of checking equality with trivially true or false BDDs, and equality between functions can be checked by checking the equality of BDDs, which in turn can be performed simply by checking equality of pointers. The authors show how BDD representations can be built for arbitrary functions, and then extend this to representations of models, transition systems, and state sets. Thus, the naive model checking algorithm can be replaced by a symbolic algorithm, and on this basis, models with state sets of the order of 10100 can be efficiently checked.

Chapters 4 and 5 cover Hoare logics for imperative program verification and modal logics for multi-agent systems. Both chapters give a clear view of the application and contain a comprehensive collection of exercises.

The authors write well and convey their enthusiasm for the subject and its application. The text can be used for a higher-level undergraduate module, or as material in an introductory graduate course. Its style also lends it to self-study; supplementary materials, such as solutions to some of the exercises, are available on the Web. In summary, I recommend it highly.
Reviewer: Simon Thompson Review #: CR122851 (0002-0071)
                
          
Specifying And Verifying And Reasoning About Programs (F.3.1 )
         
          
Modal Logic (F.4.1 ... )