Petri Nets: Fundamental Models, Verification and Applications

Petri Nets: Fundamental Models, Verification and Applications......Page 5
Table of Contents......Page 7
Preface......Page 17
Introduction......Page 19
Part 1. Fundamental Models......Page 29
1.1.1. Automata and state machine models......Page 31
1.1.2. Tasks and processes......Page 33
1.1.3. Some models......Page 34
1.2.1. Composing state machines......Page 36
1.2.2. Composition and synchronization......Page 38
1.3. Concepts and definitions......Page 39
1.3.2. Definition of the semantics of parallelism......Page 40
1.3.3. Firing transitions......Page 41
1.4. Accessibility graph or marking graph......Page 43
1.5.2. Synchronization by a signal......Page 46
1.5.3. Mutual exclusion......Page 47
1.5.4. The reader and writer mechanisms......Page 49
1.5.5. Bounded buffers......Page 51
1.6. Conclusion......Page 52
1.7. Bibliography......Page 53
2.1. Basic models......Page 55
2.2.1. Different global semantics......Page 57
2.2.2. Conclusion......Page 58
2.3. The alternating bit protocol (ABP): model and verification......Page 60
2.3.1. Loss of messages......Page 61
2.3.2. Modeling losses......Page 62
2.4. Communicating state machines and PNs......Page 64
2.5. Conclusion......Page 65
2.6. Bibliography......Page 66
3.1. Introduction......Page 69
3.2.1. Semantics of a net......Page 72
3.2.2. Usual properties......Page 73
3.3.1. Definitions and first applications......Page 80
3.3.2. Flow computations......Page 86
3.3.3. Semiflow computation......Page 88
3.3.4. Application of invariants to the analysis of a net......Page 90
3.4. Net reductions......Page 93
3.4.1. Pre-agglomeration of transitions......Page 94
3.4.2. Post-agglomeration of transitions......Page 96
3.4.3. Deletion of redundant places......Page 97
3.5.1. General results......Page 98
3.5.2. State machines......Page 102
3.5.3. Event graph......Page 103
3.5.4. Free choice net......Page 105
3.6. Bibliography......Page 113
4.1. Introduction......Page 115
4.2. Decidability and complexity notions......Page 117
4.3. Theoretical results about the reachability graph......Page 120
4.4.1. Construction of the covering graph......Page 123
4.4.2. Shortest sequences......Page 129
4.4.3. Backward analysis......Page 131
4.5. The reachability problem......Page 133
4.5.2. A sufficient condition for reachability......Page 134
4.6.1. Netswith inhibitor arcs......Page 137
4.6.2. Self-modifying nets......Page 139
4.6.3. Recursive nets......Page 141
4.7. Languages of Petri nets......Page 144
4.8. Bibliography......Page 148
5.1. Introduction......Page 151
5.2.1. Time nets......Page 154
5.2.2. States and firing rule......Page 155
5.2.3. Set of states, schedules......Page 156
5.2.4. Firing domains......Page 157
5.3.1. State classes......Page 158
5.3.2. Transitions between state classes......Page 159
5.3.3. State class equality......Page 162
5.3.4. Class graph......Page 164
5.3.5. Marking graph and class graph......Page 165
5.4.1. Analyzing behavior of time-dependent systems......Page 166
5.4.3. Boundedness......Page 167
5.4.5. Time-dependent analyses, existence of schedules......Page 171
5.5. Application example......Page 172
5.6.1. Interpreting multi-enabled transitions......Page 177
5.6.2. Other time extensions......Page 182
5.7.2. Application example......Page 184
5.8. Conclusion......Page 186
5.9. Bibliography......Page 187
6.1. Time, synchronization and autonomous behaviors......Page 191
6.3. Temporal composition......Page 192
6.4.1. The semantics of “waiting”......Page 193
6.4.2. Pragmatics and time assumptions......Page 195
6.5.1. Definition of the model......Page 196
6.5.2. The different firing semantics......Page 197
6.5.3. Relating times behavior......Page 204
6.6.2. Intra- and inter-stream drifts......Page 205
6.6.3. Modeling stream composition......Page 207
6.6.5. Modeling multimedia scenarios......Page 208
6.6.6. TSPN for designing hypermedia architectures......Page 209
6.8. Bibliography......Page 210
7.1. Introduction......Page 213
7.2.1. A client-server model......Page 214
7.2.2. Client distinction......Page 216
7.2.3. Server distinction......Page 218
7.2.4. Equivalent unfolded net......Page 220
7.2.5. Colored model for the alternate bit protocol......Page 222
7.3.1. Notation......Page 224
7.3.2. The formalismof colored nets......Page 225
7.3.3. Unfolding of a colored net......Page 227
7.4. Well-formed net definition......Page 228
7.4.1. Color domains......Page 229
7.4.2. Color functions......Page 231
7.4.3. Guards......Page 233
7.4.4. The formalismofwell-formed nets......Page 235
7.4.5. Regular nets and ordered nets......Page 238
7.5.1. Interpreted nets......Page 240
7.5.2. Algebraic nets......Page 242
7.7. Bibliography......Page 247
8.1. Introduction......Page 249
8.2. The symbolic reachability graph......Page 250
8.2.1. Symbolic markings......Page 251
8.2.2. Symbolic marking representation......Page 253
8.2.3. Symbolic firing rule......Page 258
8.2.4. Example of a symbolic reachability graph......Page 262
8.3. Colored invariants......Page 266
8.3.1. Definition of invariants of high level Petri nets......Page 267
8.3.2. Computing flows of a high level net: principles and difficulties......Page 270
8.3.3. Computing a non-parametrized generative flow family......Page 271
8.3.4. Parametrized generative family of flows for regular nets......Page 278
8.3.5. Computation of positive flows......Page 280
8.4. Structural reductions......Page 281
8.4.1. Principles of extension to high level nets......Page 282
8.4.2. Pre-agglomeration and post-agglomeration of transitions......Page 283
8.4.4. Application examples......Page 289
8.5. Conclusion......Page 293
8.6. Bibliography......Page 294
9.1. Introduction......Page 297
9.2.1. The stochastic model......Page 299
9.2.2. Analysis with renewing theory......Page 301
9.2.3. Discrete time Markov chains......Page 302
9.2.4. Continuous time Markov chains......Page 304
9.2.5. Semi-Markovian processes......Page 306
9.2.6. Regenerative Markovian processes......Page 307
9.3.1. Stochastic Petri nets with general distributions......Page 308
9.3.2. Stochastic Petri nets with exponential distributions......Page 310
9.3.3. Generalized stochastic Petri nets......Page 311
9.3.4. Deterministic stochastic Petri nets......Page 312
9.3.5. Phase-type stochastic Petri nets......Page 314
9.4.1. Research of a product form......Page 315
9.4.2. Bound computations......Page 318
9.4.3. Approximation methods......Page 321
9.4.4. Unbounded Petri nets......Page 325
9.5. Conclusion......Page 326
9.6. Bibliography......Page 327
10.1. Introduction......Page 331
10.2. Markovian aggregation......Page 333
10.3. Presentation of stochastic well-formed Petri nets......Page 335
10.3.1. The stochastic process of a well-formed Petri net......Page 336
10.3.2. Definition of stochastic well-formed Petri nets......Page 337
10.3.3. Modeling a multiprocessor system......Page 338
10.4. From the symbolic graph to Markovian aggregation......Page 341
10.4.1. Verification of the aggregation condition......Page 342
10.4.2. Computation of the parameters of the aggregated chain......Page 344
10.4.3. Performance indices of the multiprocessor system......Page 345
10.5. Conclusion......Page 346
10.6. Bibliography......Page 347
11.1. Introduction......Page 349
11.2. Synchronized Markov chains......Page 350
11.2.1. Tensor products......Page 352
11.2.2. Tensor sum and continuous time Markov chains......Page 354
11.3.1. Synchronous decomposition of generalized stochastic     Petri nets......Page 357
11.3.2. Asynchronous decomposition of generalized stochastic Petri nets......Page 360
11.3.3. Tensor analysis of phase-type Petri nets......Page 361
11.4. Tensor decomposition of stochastic well-formed Petri nets......Page 362
11.4.2. The specification problem......Page 363
11.4.3.The resolution problem......Page 364
11.4.4. A tensor decomposition method for SWN......Page 366
11.4.5. Application in the asynchronous case......Page 368
11.6. Bibliography......Page 372
Part 2. Verification and Application of Petri Nets......Page 375
12.1. Introduction......Page 377
12.2. Kripke structures and transitions systems......Page 380
12.3.1. Syntax and semantics......Page 382
12.3.2. Methods evaluation......Page 385
12.3.3. Temporal logic and Petri nets......Page 397
12.4. Behavioral approach......Page 399
12.4.1. Bisimulation relations......Page 403
12.4.2. Weak equivalences......Page 413
12.4.3. Modal characterizations of behavioral equivalences......Page 423
12.5.1. Undecidability results......Page 429
12.5.2. Decidability results......Page 435
12.6. Bibliography......Page 439
13.1. Introduction......Page 443
13.2.1. Preliminary information......Page 444
13.2.2. Net homomorphisms......Page 445
13.2.3. Occurrence nets......Page 446
13.3.1. Branching processes......Page 449
13.3.2. Unfoldings......Page 451
13.4.1. Definition......Page 452
13.4.2. Adequate orders and complete finite prefixes......Page 453
13.4.3. Verification of safety properties......Page 455
13.4.4. Detection of infinite behaviors......Page 456
13.6. Bibliography......Page 460
14.1. Introduction......Page 463
14.2.1.Verification of Kripke structures......Page 465
14.2.2. Symmetric Kripke structures......Page 467
14.2.3.Verification of symmetric Kripke structures......Page 469
14.3.1. Presentation of the model......Page 472
14.3.2. Specification of the property to be verified......Page 480
14.3.3. Building of the symbolic synchronized product......Page 482
14.4. Efficient implementations and further work......Page 485
14.5. Conclusion......Page 486
14.6. Bibliography......Page 487
15.1. Introduction......Page 489
15.2.1. Motivations......Page 490
15.2.2. From composition to abstraction......Page 491
15.2.3. Verification of temporal coherence......Page 494
15.3.2. Hierarchical time stream Petri nets......Page 496
15.3.3. Interrupts as a combination of abstraction and temporal composition......Page 499
15.3.4. HTSPN state......Page 500
15.4.1. Modeling hypermedia systems......Page 502
15.4.2. A solution to “lip-synchronization” using HTSPNs......Page 503
15.5. Conclusion......Page 505
15.6. Bibliography......Page 506
16.1. Introduction......Page 509
16.2.2. Connectors and their interpretation......Page 511
16.2.3. Sequent calculus......Page 512
16.3.1. Various approaches......Page 513
16.3.2. Approach with marking......Page 514
16.3.3. Equivalence between reachability in a Petri net and provability of one sequent in linear logic......Page 516
16.4.1. Labeling......Page 518
16.4.2. Graph of precedence relations......Page 519
16.4.3. Conflicts of transitions and tokens......Page 520
16.5.1. Introduction......Page 521
16.5.2. Simple temporal networks......Page 522
16.5.3. Temporal labeling......Page 524
16.6. Conclusion......Page 527
16.7. Bibliography......Page 528
17.1. Introduction......Page 529
17.2.1. Multimedia information: characteristics and requirements......Page 530
17.2.2. Asynchronous distributed systems......Page 533
17.3.1. Modeling requirements......Page 535
17.3.2. Modeling example for a videoconference application......Page 538
17.4.2. Modeling of a videoconference application......Page 540
17.4.3. Using a partial order transport......Page 544
17.5. Conclusion......Page 550
17.6. Bibliography......Page 551
18.1. Introduction......Page 555
18.2. Modeling of manufacturing systems......Page 556
18.2.1. Discrete event systems aspects......Page 557
18.2.2. Cyclic aspects......Page 561
18.2.3. High throughput aspects......Page 566
18.2.4. Weighted marked graphs......Page 571
18.3.1. Performance evaluation methods......Page 572
18.3.2. Deterministic and stochastic discrete marked graphs......Page 577
18.3.3. Discrete weighted marked graphs......Page 579
18.3.4. Continuous weighted marked graphs......Page 580
18.4. Optimization of manufacturing systems......Page 587
18.4.1. Deterministic marked graphs......Page 588
18.4.2 Stochastic marked graphs......Page 589
18.4.3. Extension to deterministic weighted marked graphs......Page 591
18.4.4. Applications......Page 595
18.5. Conclusions......Page 599
18.6. Bibliography......Page 600
Conclusion......Page 605
List of Authors......Page 607
Index......Page 609