Carl Adam Petri (1926 โ 2010)
Foreword
Preface
Acknowledgments
Introduction
Contents
List of Examples and Case Studies
Part I Modeling Techniques
1 An Example
1.1 A Cookie Vending Machine
1.2 A Look Inside
1.3 The Interface
1.4 Hot and Cold Transitions
1.5 Runs
1.6 Alternatives
1.7 Fine Tuning
1.8 Diverse Components
Exercises
Further Reading
2 The Basic Concepts
2.1 A Variant of the Cookie Vending Machine
2.2 Components of a Net
2.3 The Data Structure for Petri Nets: Multisets
2.4 Markings as Multisets
2.5 Steps with Constant Arc Labelings
2.6 Steps with Variable Arc Labelings
2.7 System Nets
2.8 Marking Graph
2.9 Final Markings
Exercises
Further Reading
3 Common Special Case: Elementary System Nets
3.1 Elementary System Nets
3.2 An Abstract Model of the Cookie Vending Machine
3.3 Mutual Exclusion
3.4 The Crosstalk Algorithm
3.5 1-Bounded Elementary System Nets
Exercises
Further Reading
4 Sequential and Distributed Runs
4.1 Sequential Runs
4.2 Tokens as Labeled Places
4.3 Actions
4.4 Distributed Runs
4.5 Example: A Bell Clock
4.6 The Kindergarten Game
4.7 Causal Order
4.8 The Composition of Distributed Runs
Exercises
Further Reading
5 Scenarios
5.1 Defining Scenarios
5.2 The Scenarios of the Crosstalk Algorithm
5.3 The Scenarios of the Cookie Vending Machine
Exercises
Further Reading
6 Further Notations for Elementary System Nets
6.1 Place Capacities
6.2 Arc Weights
6.3 Real Extensions
Exercises
Further Reading
7 The Synthesis Problem
7.1 Example: The Light/Fan System
7.2 The General Question of the Synthesis Problem
7.3 Regions of State Automata
7.4 The System Net of a State Automaton
7.5 The Solution to the Synthesis Problem
7.6 The Synthesis Problem of the Light/Fan State Automaton
Exercises
Further Reading
8 Composition of Nets
8.1 Nets with Interfaces
8.2 Communicating Nets
8.3 Unambiguous Decomposition into Open Nets
Exercises
Further Reading
Part II Analysis Methods
9 State Properties
9.1 Equations and Inequalities of the Cookie Vending Machine
9.2 Valid Equations
9.3 Example: Dining Philosophers
9.4 Valid Inequalities
9.5 Equations and Inequalities of Elementary System Nets
9.6 Modulo Equations
9.7 Propositional State Properties
Exercises
Further Reading
10 Traps and Cotraps of Elementary System Nets
10.1 Traps of Elementary System Nets
10.2 Cotraps
10.3 The Trap/Cotrap Property
Exercises
Further Reading
11 Place Invariants of Elementary System Nets
11.1 Vector Representation for Elementary System Nets
11.2 The Matrix N
11.3 Place Invariants
11.4 Positive Place Invariants
Exercises
Further Reading
12 Combining Traps and Place Invariants of Elementary System Nets
12.1 Calculating with Equations and Inequalities
12.2 State Properties of the Mutual Exclusion System
12.3 State Properties of the Crosstalk Algorithm
12.4 Unstable Properties
Exercises
13 Traps and Place Invariants of Generic System Nets
13.1 Traps of a System Net
13.2 Sum Expressions
13.3 Multiplying Sum Expressions
13.4 Applying a Sum Expression to a Multiset
13.5 The Matrix N of a System Net N
13.6 The Place Invariants of a System Net
13.7 The Constant of a Place Invariant
13.8 The Equation of a Place Invariant
13.9 Properties of the Philosophers System
13.10 Properties of the Kindergarten Game
Exercises
Further Reading
14 Marking and Covering Graphs
14.1 Deriving Properties from the Marking Graph
14.2 The Idea of the Covering Graph
14.3 w-Markings
14.4 The Construction of the Covering Graph
14.5 The Finiteness of the Covering Graph
14.6 The Covering of Sequential Runs
14.7 Simultaneously Unbounded Places
14.8 Dead Transitions
14.9 Covering Graphs of Generic System Nets
Exercises
Further Reading
15 Reachability in Elementary System Nets
15.1 Corollaries of Place Invariants
15.2 The Marking Equation
15.3 Transition Invariants
Exercises
Further Reading
16 Run Properties
16.1 Intuitive Question
16.2 Defining Run Properties
16.3 The Deduction Rule
16.4 Proof Graphs
Exercises
Further Reading
17 Free-Choice Nets
17.1 Defining Free-Choice Nets
17.2 The Trap/Cotrap Theorem for Free-Choice Nets
17.3 Clusters
17.4 The Rank Theorem
Exercises
Further Reading
18 Marked Graphs
18.1 Defining Marked Graphs
18.2 Liveness of Marked Graphs
18.3 1-Bounded Marked Graphs
18.4 Liveness of 1-Bounded Marked Graphs
Exercises
Further Reading
19 Well-Formed System Nets
19.1 Example: Models of Business Processes
19.2 Well-Formed Elementary System Nets
19.3 Deciding Well-Formedness
Exercises
Further Reading
Part III Case Studies
20 Mutual Exclusion
20.1 The Problem
20.2 Realizability
20.3 Fairness Assumptions
20.4 Mutex with Autonomous Fairness
20.5 The Scenarios of the Algorithm
20.6 Correctness of the Algorithm
Exercises
Further Reading
21 Asynchronous Hardware
21.1 The Counterflow Pipeline Processor (CFPP): The Problem
21.2 The Solution Idea
21.3 The Synthesis Problem for the CFPP
21.4 Structural Simplification of a Module
21.5 The Model of the CFPP
21.6 Analysis of the Model
Exercises
Further Reading
22 Network Algorithms
22.1 Some Conventions for the Representation of Network Algorithms
22.2 The Echo Algorithm
22.3 Synchronization in Acyclic Networks
22.4 Consensus in the Network
Exercises
Further Reading
Part IV Conclusion
23 Closing Remarks
23.1 A Brief History of Petri Nets
23.2 Properties of the Elementary Formalisms of Petri Nets
23.3 Speculative Questions
23.4 Petri Nets in Software Engineering
23.5 Reference to Other System Models and Analysis Techniques
23.6 Other Introductory Texts
Formal Framework
Bibliography
Index