Preface
Purpose
Prerequisites
Content
Acknowledgements
Contents
1 Elementary Net Systems
1.1 Net Diagram and Semantics
1.1.1 Net and Net System
1.1.2 Firable Transition Sequence and Interleaving Semantics
1.1.3 Process and Concurrency Semantics
1.2 Reachability Graph and Coverability Graph
1.2.1 Reachability and Reachability Graph
1.2.2 Unboundedness and Coverability Graph
1.3 Unfolding
1.3.1 Branching Process
1.3.2 Finite Complete Prefix
1.3.3 Finite Prefix
1.4 Basic Properties and Computation Complexity
1.4.1 Some Basic Properties
1.4.2 Computation Complexity of Deciding Basic Properties
1.5 Application
1.6 Summary and Further Reading
References
2 Structural Characteristics of Petri Nets
2.1 Incidence Matrix and State Equation
2.1.1 Incidence Matrix
2.1.2 State Equation
2.2 Invariant
2.2.1 T-Invariant
2.2.2 P-Invariant
2.2.3 Algorithm of Computing Invariants
2.3 Repetitiveness
2.3.1 Repetitive Vector
2.3.2 Relation Between Repetitive Vector and T-Invariant
2.3.3 Algorithm of Computing Repetitive Vectors
2.4 Siphon and Trap
2.4.1 Siphon
2.4.2 Trap
2.4.3 Relation Between Siphon and Repetitive Vector
2.4.4 Algorithm of Computing Siphon and Trap
2.5 Application
2.6 Summary and Further Reading
References
3 Petri Nets with Special Structures
3.1 Single Input and Single Output
3.1.1 State Machine
3.1.2 Marked Graph
3.2 Choice Structures
3.2.1 Free-Choice Net
3.2.2 Asymmetric-Choice Net
3.3 Circuit Structure
3.3.1 Normal Net
3.3.2 Weakly Persistent Net
3.4 Application
3.5 Summary and Further Reading
References
4 Petri Nets Modeling Message Passing and Resource Sharing
4.1 Workflow Nets
4.1.1 Soundness and Weak Soundness of Workflow Nets
4.1.2 Equivalence Between Soundness and Weak Soundness in Free-choice Workflow Nets
4.1.3 Equivalence Between Soundness and Weak Soundness in Acyclic Asymmetric-Choice Workflow Nets
4.1.4 k-Soundness
4.2 Inter-organisational Workflow Nets
4.2.1 Compatibility
4.2.2 Collaborative-ness
4.3 Resource Allocation Nets
4.4 Application
4.5 Summery and Further Reading
References
5 Verifying Computation Tree Logic Based on Petri Nets
5.1 Computation Tree Logic and Verification Based on Petri Nets
5.1.1 Syntax and Semantics of CTL
5.1.2 Logical Equivalence of Formulae
5.1.3 Verification Algorithms Based on Reachability Graphs
5.2 Reduced Ordered Binary Decision Diagrams
5.2.1 Reduced Ordered Binary Decision Diagrams for Encoding Boolean Functions
5.2.2 Constructing the ROBDD of a Boolean Function
5.2.3 Operations of Boolean Functions by Manipulating ROBDDs
5.3 Verifying CTL with the ROBDD Technique
5.3.1 Encoding Reachability Graphs of Safe Petri Nets Using ROBDDs
5.3.2 CTL Verification Based on All Reachable Markings Encoded by an ROBDD
5.4 Application
5.5 Summery and Further Reading
References
6 Knowledge-Oriented Petri Nets and Computation Tree Logic of Knowledge
6.1 Knowledge-Oriented Petri Nets Modelling Privacy-Critical Multi-agent Systems
6.1.1 Knowledge-Oriented Petri Nets
6.1.2 Reachability Graph with Equivalence Relations
6.2 Computation Tree Logic of Knowledge
6.2.1 Syntax and Semantics of CTLK
6.2.2 Verifying CTLK Based on Reachability Graph with Equivalence Relations
6.2.3 Verifying CTLK Based on ROBDD
6.3 Applications
6.3.1 Key Transport Protocol with Attacking
6.3.2 Dining Cryptographers Protocol
6.4 Summery and Further Reading
References
7 Petri Nets with Insecure Places and Secure Bisimulation
7.1 Bisimulation and Weak Bisimulation
7.2 Petri Nets with Insecure Places and Secure Bisimulation
7.2.1 Petri Nets with Insecure Places
7.2.2 Secure Bisimulation
7.3 Summery and Further Reading
References
8 Time Petri Nets and Time-Soundness
8.1 Time Petri Nets
8.1.1 Formal Definition and Firing Rules
8.1.2 Generation of State Class Graph
8.1.3 Completeness of State Class Graph
8.2 Time-Soundness
8.2.1 Time-Soundness Based on Bisimulation
8.2.2 Deciding Time-Soundness
8.3 Application
8.4 Discussion of CTL over Time Petri Nets
8.5 Summery and Further Reading
References
9 Verifying Timed Computation Tree Logic Based on Time Petri Nets
9.1 Syntax and Semantics of TCTL
9.1.1 Syntax of TCTL
9.1.2 Semantics of TCTL
9.2 Verifying TCTL Based on State Class Graphs of Time Petri Nets
9.2.1 Recursively Computing Satisfiable State Sets of TCTL Formulae
9.2.2 Computing Satisfiable State Set for EUI Based on Forward Exploration
9.2.3 Computing Satisfiable State Set of AUI Based on Forward Exploration
9.3 Summery and Further Reading
References
10 Plain Time Petri Nets with Priorities
10.1 Plain Time Petri Net with Priorities
10.1.1 Definition of Plain Time Petri Net with Priorities
10.1.2 Firing Rules and State Class Graph of Plain Time Petri Nets with Priorities
10.2 Properties of State Class Graphs of Plain Time Petri Nets with Priorities
10.3 Verifying TCTL Based on State Class Graphs of Plain Time Petri Nets with Priorities
10.3.1 Computing Satisfiable State Set for EUI Based on Backward Exploration
10.3.2 Computing Satisfiable State Set for AUI Based on Backward Exploration
10.4 Application
10.5 Summery and Further Reading
References
Index