This is the second volume of Jensen's work on colored Petri nets (CP-nets). The first volume introduces the model, while this volume concentrates on analysis methods. This volume requires familiarity with CP-nets. I strongly recommend a careful study of volume 1 before reading this volume, because the material would be of little or no interest to readers not familiar with the concepts introduced there.
Jensen addresses three main topics here: occurrence graphs, invariants, and timed CP-nets. Occurrence graphs are addressed well in the first three chapters. Chapter 1 presents full occurrence graphs, which generalize reachability graphs of Petri nets. Chapter 2 introduces a reduction technique for occurrence graphs based on equivalence classes, while chapter 3 shows how to reduce the size of the occurrence graph using symmetries. Invariants and timed CP-nets are discussed in chapters 4 and 5, respectively.
The examination of the topics is proportional to their order. Occurrence graphs are discussed and illustrated in depth; invariants are clearly introduced and demonstrated on examples; and the discussion of timed CP-nets is limited. The compact presentation of place and transition invariants for CP-nets is justified by the limited set of concepts that constitute the theory of invariance. The discussion of timed CP-nets is surprisingly short, however. Despite the huge amount of literature that presents many different ways to introduce time in Petri nets and discusses several analysis techniques, the book dedicates only a few pages to timed CP-nets. The book only considers a temporal extension where tokens are "forced" to stay in their place once created, to simulate the duration of actions. Analysis techniques for timed and stochastic Petri nets receive less emphasis than I would have expected.
Most of the material presented in this book has previously been addressed in scientific papers, summarized in the excellent bibliographical remarks at the end of each chapter. Part of the book presents interesting original results. In particular, occurrence graphs with equivalence classes, discussed in chapter 2, are an original scientific contribution of this book.
Each topic is discussed at three levels: it is informally introduced through examples; then formal definitions are given; and finally performance and automation issues are discussed. This interesting and efficacious style may not fully satisfy pure theoreticians, who might be annoyed by the numerous practicalities, while practitioners could find the theory excessive and hard to cope with. However, I encourage both theoreticians and practitioners who are familiar with CP-nets and would like to study analysis techniques for CP-nets not to give up.
The presentation is hampered by the many inessential references to volume 1. While frequent references to tools stress the importance of automation for practical uses of analysis techniques, they can also frustrate readers who do not have access to those tools, and thus cannot solve some of the exercises.
The style, exercises, and bibliographical remarks make this book useful as a textbook for an advanced course on CP-nets, which should follow a course based on the first volume.
Unlike most books on Petri nets, which try to illustrate all aspects of the formalism, this book focuses on a specific subject: the analysis of CP nets. No other book I am aware of discusses this subject at a comparable level of detail. The typography, indexes, and references are good.
- M. Pezzé, Milan, Italy
GENERAL TERMS: LANGUAGES, THEORY, VERIFICATION
This volume contains a detailed presentation of the analysis methods for CP-nets. The analysis methods allow the modeller to investigate dynamic properties of CP-nets, e.g., the properties defined in Chap. 4 of Vol. 1. We describe the main ideas behind the analysis methods and the mathematics on which they are based. We also describe how the methods are used in practice and how they are supported by computer tools.
Some parts of this volume are rather theoretical while other parts are application oriented. The purpose of the volume is to teach the reader how to use the formal analysis methods. This does not require a deep understanding of the underlying mathematical theory (although such knowledge will, of course, be a help). Chapters 13 deal with occurrence graphs, Chap. 4 deals with invariants, and Chap. 5 defines the behaviour of timed CP-nets.
In Chap. 5 of Vol. 1 we introduced the basic ideas behind occurrence graphs and place invariants. The descriptions there were intuitive, imprecise and without proofs. In this volume we give the precise unambiguous definitions, prove the correctness of the various techniques, and explain how to use the methods in practice. To make the description complete we repeat the informal introductions provided in Vol. 1.
ISBN: 3-540-58276-2
