Interest in the application of formal methods in distributed systems has grown considerably in the last decade. Distributed algorithms--algorithms that operate on physically or logically distributed processors--are now undergoing an examination to see whether what works in practice will work in theory; this book forms a part of this examination.

Reisig attacks two general problems. The first is to describe an algorithm precisely in a fashion suitable for analysis. The second is to perform the analysis and prove formally that the algorithm produces the desired result. This work relies heavily on Petri nets in both phases, a widely used approach that reflects the author’s background.

The approach is solidly theoretical. Accordingly, issues that plague the computational scientist, such as the effect of architecture on the choice of algorithm, and the choice of language, are not considered. The work is thus European in flavor. Indeed, the author notes that the book’s view cannot be retained for large systems.

The first part introduces the concepts required to model the algorithms. Because of its emphasis on locality, a simple producer-consumer single-buffer system is effectively used to introduce the Petri net notation and formalization and its suitability for distributed algorithms. A very useful section describes the book’s relation with other textbooks and in particular that of Lynch [1].

The concepts of interleaved runs and concurrent runs are introduced, with the previous example being used to underpin the essential differences. This leads to good discussions of the concepts of progress and fairness in a distributed algorithm. A well-illustrated set of case studies, including Dijkstra’s dining philosophers, the crosstalk problem, and a number of mutex algorithms, completes the introduction. At the end of this part, the reader will have acquired the chosen formalism for coping with concurrency.

The second section extends the formal model from elementary to generalized systems nets. The same examples are used and expanded, and new ones added. There is a good mixture of formalism, example, and illustration, with the examples becoming increasingly standard and relevant, including consensus and phase synchronization. This leads to a third section that analyzes elementary systems--systems essentially involving only control structures. The final section analyzes advanced systems, that is, those permitting data structures. In both cases, most of the examples chosen are normal and relevant.

The presentation throughout is in the Euclidean style, with formal definitions, lemmas, theorems, and mathematical-style proofs. The layout is relatively dense, but the appropriate use of italics and boldface, together with the wealth of illustrations and the use of white space, make the material easy to follow. The style is equally normal, and the text is thus very reminiscent of undergraduate mathematical texts.

The proofs are well constructed, relatively easy to follow, and accurate. The book will give researchers and graduate students who have the appropriate background a good introduction to this growing area. It could be used as the basis of a course, and the reference list is useful, but care must be taken, first because of the speed of development, and second because a commitment to the book’s underlying philosophy must be made. Given the nature of the material, the typography is excellent and relatively error-free. An index would have been useful for those dipping into the material. This is a good book to have on the shelf.