Verification of Reactive Systems by Klaus Schneider Springer Verlag, 2003, 600pp, ISBN 3-540-00296-0

Abstract

This book discusses four approaches typically used for the verification of reactive systems.However, the book is not merely a description of these four formalisms, since the existing connections between these techniques are also established.In addition, complexity results associated with each method are presented, together with discussions about good features and difficulties that must be faced when dealing with each particular technique.It cannot be said that this is a practical book.On the contrary, this book presents fundamental theory that every researcher on formal methods should be familiar with.Therefore, the audience for this book is mainly theoreticians with some background in automata theory and logics.They will enjoy discovering the underlying interrelations among the different approaches presented along the book.Almost all the results presented encompass useful descriptions and explanations, which makes the reading more fluent, especially when the reader doesn't want to go into the details of a specific proof or result.It must be said that the notation used by the authors does not always follow the established notation, as used in the original research papers, for instance.This fact increases the difficulty of reading the text since some extra time must be invested in getting accustomed to the new notation.Independently from the contents, the readability of the book is sometimes degraded due to the presence of some typographical errors, but they do not prevent the reader from understanding the topics of the text.Looking into the contents, the book starts with a marvelous introduction where, first of all, a classification of formal methods and systems can be found.The ancient (maybe not so ancient) history of logic theories and verification techniques is narrated.This part of the book, in addition to being a very nice introductory description of the formalisms that will be described in the rest of the book, is also an advertisement to the reader of the theoretical point of view that will be used through the book, which continuously will frame the equivalences and relations among the four formalisms.The book includes a remarkable bibliography section.This is not only notable for its contents, but also for how they are cited.Bibliographic references are perfectly integrated into the book itself, and can be especially useful in the introduction and in the appendixes, where the topics are not completely developed and the reader is referred to related and perhaps more detailed works.Before considering the main contents of the book, the second chapter presents a unified specification language which combines µ-calculus, ω-automata, temporal logics and predicate logics.This unified language provides the author with an unified notation for defining each formalism in the rest of the book and for showing the formal links between the different approaches.Notions such as Kripke structures, fairness, simulations, bisimulations and products of structures are introduced and will be used in several sections of the book.The organization of the main chapters of the book is as follows: Chapter 3 is devoted to the first formalism, the µ-calculus; then, Chapter 4 deals with ω-automata, the following chapter describes temporal logics (in particular, variants of CTL) and finally, in Chapter 6, predicate logics are used for the verification of reactive systems.Note that although these four chapters