Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical UseThis three-volume work presents a coherent description of the theoretical and practical aspects of coloured Petri nets (CP-nets). The second volume contains a detailed presentation of the analysis methods for CP-nets. They allow the modeller to investigate dynamic properties of CP-nets. The main ideas behind the analysis methods are described as well as the mathematics on which they are based and also how the methods are supported by computer tools. Some parts of the volume are theoretical while others are application oriented. The purpose of the volume is to teach the reader how to use the formal analysis methods, which does not require a deep understanding of the underlying mathematical theory. |
Contents
Full Occurrence Graphs | 1 |
11 Introduction to Ographs | 2 |
12 Formal Definition of Ographs | 4 |
13 Directed Paths and Strongly Connected Components | 6 |
14 Proof Rules for Ographs | 11 |
Distributed Data Base | 17 |
Dining Philosophers | 20 |
17 Computer Tools for Ographs | 22 |
35 Computer Tools for OSgraphs | 92 |
Bibliographical Remarks | 97 |
Exercises | 98 |
Invariants | 101 |
41 Introduction to Place Invariants | 102 |
42 Formal Definition of Place Invariants | 107 |
43 Automatic Calculation of Place Invariants | 113 |
44 Interactive Calculation of Place Invariants | 119 |
Bibliographical Remarks | 33 |
Exercises | 34 |
Occurrence Graphs with Equivalence Classes | 39 |
21 Introduction to OEgraphs | 40 |
22 Formal Definition of OEgraphs | 42 |
23 Proof Rules for OEgraphs | 46 |
Distributed Data Base | 52 |
ProducerConsumer System | 54 |
26 Labelled OEgraphs | 60 |
27 Computer Tools for OEgraphs | 62 |
Bibliographical Remarks | 64 |
Exercises | 65 |
Occurrence Graphs with Symmetries | 69 |
31 Symmetry Specifications | 70 |
32 Proof Rules for OSgraphs | 75 |
33 Permutation Symmetries | 79 |
34 Labelled OSgraphs | 86 |
45 Transition Invariants | 131 |
46 Uniform CPnets | 138 |
Bibliographical Remarks | 142 |
Exercises | 143 |
Timed CPnets | 145 |
51 Introduction to Timed CPnets | 146 |
52 Timed Multisets | 150 |
53 Formal Definition of Timed CPnets | 153 |
54 Relationships Between Timed and Untimed CPnets | 156 |
Protocol | 159 |
56 Analysis of Timed CPnets | 162 |
Bibliographical Remarks | 164 |
Exercises | 166 |
| 169 | |
| 173 | |
Common terms and phrases
algorithm Analogously arc expressions b₁ BE(c bi-implications bijective binding elements bounds calculate colour set column compatible equivalence specification consider construct contains corresponding CPN tools data base managers data base system defined directed cycle directed graph dynamic properties end of Sect equivalence class equivalence relation fairness properties finite occurrence formal definition Hence Id Id identical incidence matrix initial marking integer investigate labelled OS-graph linear liveness properties M₁ M₁(p maps means Mn+1 multi-set number of nodes O-graph occurrence graph tool occurrence sequence output arc packet permutation symmetry Petri Nets philosopher system place flows place instance place invariants place weights process control system proof rules properties in Def prove PT-net reachable marking reduced matrix resource allocation system ring network rules in Prop SCC-graph SCCT self-symmetries strongly connected component symmetry specification tokens transition flows transition invariant untimed CP-net verify weighted-set
Popular passages
Page 169 - International Conference on Application and Theory of Petri Nets, Paris, France, June 1990. Reprinted in High-Level Petri Nets. Theory and Application, K. Jensen and G. Rozenberg (editors), Springer Verlag, 1991.
Page 169 - AV Aho, JE Hopcroft, JD Oilman. The design and analysis of computer algorithms, Addison-Wesley, Reading, Mass., 1974.