Petri Nets

ISBN-13: 9789811963117 / Angielski / Miękka / 2023

Guanjun Liu

Opis

This book provides essential information on Petri net theory and Petri net-based model checking methods. As for the Petri net theory, it involves the interleaving semantics and concurrency semantics of elementary net systems, some important net structures (e.g., invariant, repetitive vector, siphon, and trap), some classical net subclasses with special structures (e.g., state machine, marked graph, free-choice net,asymmetric-choice net, normal net, and weakly persistent net), and some basic properties (e.g., reachability, liveness, deadlock, and soundness). It also involves four high-level Petri nets: knowledge-oriented Petri nets, Petri nets with insecure places, time Petri nets, and plain time Petri nets with priorities, focusing on different fields of application. As for the model checking methods, this book introduces readers to computation tree logic (CTL), computation tree logic of knowledge (CTLK), and timed computation tree logic (TCTL), as well as Petri net-based methods for checking them. The basic principle of the reduced ordered binary decision diagram (ROBDD) is employed to compress the state space used in these model checking procedures. The book also covers time-soundness for time Petri nets and secure bisimulation for Petri nets with insecure places, both of which are based on the bisimulation theory. As such, it offers an introduction to basic information on bisimulation theory.

Recenzje

"This book focuses on the basic theory of Petri nets as well as the Petri-nets-based model-checking methods. ... Each Chapter ends with a set of references. ... The book is meant for beginners as well as senior researchers." (T. C. Mohan, zbMATH 1512.68001, 2023)

Spis treści

1 Elementary Net Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

  1.1 Net Diagram and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

       1.1.1 Net and Net System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

       1.1.2 Firable Transition Sequence and Interleaving Semantics . … . . 4

       1.1.3 Process and Concurrency Semantics . . . . . . . . . . . . . . . . … . . . 7

  1.2 Reachability Graph and Coverability Graph . . . . . . . . . . . . . . . . . . . . . 13

       1.2.1 Reachability and Reachability Graph . . . . . . . . . . . . . . . . . . . . 13

       1.2.2 Unboundedness and Coverability Graph . . . . . . . . . . . . .. . . . . 15

  1.3 Unfolding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

       1.3.1 Branching Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

       1.3.2 Finite Complete Prefix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

       1.3.3 Finite Prefix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . 24

  1.4 Basic Properties and Computation Complexity . . . . . . . . . . . . . . . …. . . 26

       1.4.1 Some Basic Properties . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . 26

       1.4.2 Computation Complexity of Deciding Basic Properties . … . . . 27

  1.5 Application. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  1.6 Summary and Further Reading . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . 29

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

2 Structural Characteristics of Petri Nets . . . . . . . . . . ….. . . . . . . . . . . . . . . . . 33

  2.1 Incidence Matrix and State Equation . . . . . . . . …. . . . . . . . . . . . . . . . . . 33

       2.1.1 Incidence Matrix . . . . . . . . . . . . . . ... . . . . . . . . . . . . . . . . . . . . . 33

       2.1.2 State Equation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

  2.2 Invariant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

       2.2.1 T-invariant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

       2.2.2 P-invariant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

       2.2.3 Algorithm of Computing Invariants . . . … . . . . . . . . . . . . . . . . . 41

  2.3 Repetitiveness . . . . . . . . . . . . . . . . . . . . . . . ... . . . . . . . . . . . . . . . . . . . . . 43

       2.3.1 Repetitive Vector . . . . . . . . . . . . . . ... . . . . . . . . . . . . . . . . . . . . . 43

       2.3.2 Relation between Repetitive Vector and T-invariant . . … . . . . . 45

       2.3.3 Algorithm of Computing Repetitive Vectors . . . . . . …. . . . . . . . 47

  2.4 Siphon and Trap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . …. . . . . . . . . . 50

       2.4.1 Siphon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . … . . . . . . . . . . . . 50

       2.4.2 Trap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . … . . . . . . . . . . . . . . . . 51

       2.4.3 Relation between Siphon and Repetitive Vector . . . . . ... …. . . . . 52

       2.4.4 Algorithm of Computing Siphon and Trap . . . . . . . . ...…. . . . . . . 57

  2.5 Application. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .… . . . . . . . 58

  2.6 Summary and Further Reading . . . . . . . . . …... . . . . . . . . . . . .. . . . . . . . . . 62

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . 63

3 Petri Nets with Special Structures  . . . . . . . . . . . . . . . . . …. . . . . . .. . . . . . . . . 65

  3.1 Single Input and Single Output . . . . . . . . . . . . . . …... . . . . . . . . .. . . . . . . . 65

       3.1.1 State Machine . . . . . . . . . . . . . . . . . . . . …. . . . . . . . . . . .. . . . . . . . 65

       3.1.2 Marked Graph . . . . . . . . . . . . . . . . . . …. . . . . . . . . . . . . .. . . . . . . . 68

  3.2 Choice Structures . . . . . . . . . . . . . . . . . . . …… . . . . . . . . . . . . . . . . . . . . . . 72

       3.2.1 Free-Choice Net . . . . . . . . . …… . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

       3.2.2 Asymmetric-Choice Net . . ……. . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

  3.3 Circuit Structure . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78

       3.3.1 Normal Net . . . . . . . . . …... . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78

       3.3.2 Weakly Persistent Net . . . . . ……. . . . . . . . . . . . . . . . . . . . . . . . . . . 83

  3.4 Application. . . . . . . . . . . . . . . . . . . . …… . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

  3.5 Summary and Further Reading . . . …….. . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . … . . . . . . . . . . . . . . . . . . 91

4 Petri Nets Modeling Massage Passing and Resource Sharing  . . . . . ………. . . 93

  4.1 Workflow Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . …... . . . 93

       4.1.1 Soundness and Weak Soundness of Workflow nets . . . . . ……... . . 93

       4.1.2 Equivalence between Soundness and Weak Soundness in

            Free-choice Workflow nets . . . . . . . . . . . . . . . . . . …… . . . . . . . . . 96

       4.1.3 Equivalence between Soundness and Weak Soundness in

            Acyclic Asymmetric-choice Workflow nets . . . . . …… . . . . . . . . . 97

       4.1.4 k -soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……. . . . . . . . . . . . 98

  4.2 Inter-organisational Workflow Nets . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . 100

       4.2.1 Compatibility . . . . . . . . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . . . 100

       4.2.2 Collaborative-ness . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . . . . . . 102

  4.3 Resource Allocation Nets . . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . . . . . . 104

  4.4 Application. . . . . . . . . . . . . . . . . . . . . . . . …… . . . . . . . . . . . . . . . . . . . . . . . 107

  4.5 Summery and Further Reading . . . . . ……… . . . . . . . . . . . . . . . . . . . . . . . . . 112

  References . . . . . . . . . . . . . . . . . . . . . ….. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112

5 Verifying Computation Tree Logic Based on Petri Nets  . . . …….. . . . . . . .. . . 115

  5.1 Computation Tree Logic and Verification Based on Petri Nets . ………. . . . 115

       5.1.1 Syntax and Semantics of CTL. . . . . . . . . . . . . . . . …….. . . . . . . . . . 115

       5.1.2 Logical Equivalence of Formulae . . . . . . . . . . . . . . . . . …….. . . . . . 120

       5.1.3 Verification Algorithms Based on Reachability Graphs . . . . ………. 122

  5.2 Reduced Ordered Binary Decision Diagrams . . . . . . . ……….. . . . . . . . . . . . 125

       5.2.1 Reduced Ordered Binary Decision Diagram for Encoding

            Boolean Function . . . . . . . . . . . . . . . . . …….. . . . . . . . . . . . . . . . . . . 125

       5.2.2 Constructing the ROBDD of a Boolean Function . . . . . . ………. . . . 129

       5.2.3 Operations of Boolean Functions by Manipulating ROBDDs ……….135

  5.3 Verifying CTL with the ROBDD Technique . . . . . . . . . . . . . . . ………. . . . . 140

       5.3.1 Encoding Reachability Graphs of Safe Petri Nets Using

            ROBDDs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……. . . 140

       5.3.2 CTL Verification Based on All Reachable Markings

            Encoded by an ROBDD . . . . . . . . . . . . . . . . …….. . . . . . . . . . . . . . . 148

  5.4 Application. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……… . . . . . . . . . . . . . . . . 152

  5.5 Summery and Further Reading . . . . . . . . . . . ……….. . . . . . . . . . . . . . . . . . . . 154

  References . . . . . . . . . . . . . . . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . . . . . . . . . . 154

6 Knowledge-oriented Petri Nets and Computation Tree Logic of

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . …… . . . . . . . . . . . . . . . . . . . . . 157

  6.1 Knowledge-oriented Petri Nets Modelling Privacy-critical

     Multi-agent Systems . . . . . . . . . . . . . . ……….. . . . . . . . . . . . . . . . . . . . . . . . . . 157

       6.1.1 Knowledge-oriented Petri Nets . . . . . . . . . ……….. . . . . . . . . . . . . . . . 157

       6.1.2 Reachability Graph with Equivalence Relations . . . ………… . . . . . . . 159

  6.2 Computation Tree Logic of Knowledge . . . . . . . . . . . . ………… . . . . . . . . . . . 163

       6.2.1 Syntax and Semantics of CTLK . . . . . . . . . ………... . . . . . . . . . . . . . . 163

       6.2.2 Verifying CTLK Based on Reachability Graph with

            Equivalence Relations . . . . . . . . . . . . . . ………. . . . . . . . . . . . . . . . . . 167

       6.2.3 Verifying CTLK Based on ROBDD . . . . . . . . . . . . . . . ……….. . . . . . 170

  6.3 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……… . . . . . . . . 173

       6.3.1 Key Transport Protocol with Attacking . . . . . . . ………... . . . . . . . . . . 173

       6.3.2 Dining Cryptographers Protocol . . . . . . . . . . . . ……….. . . . . . . . . . . . 174

  6.4 Summery and Further Reading . . . . . . . . . . . . . . ………… . . . . . . . . . . . . . . . . 176

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . . . . . . . . 176

7 Petri Nets with Insecure Places and Secure Bisimulation  . . . …………. . . . . . . . . 179

  7.1 Bisimulation and Weak Bisimulation . . . . . . . . . . . . . . …………. . . . . . . . . . . . 179

  7.2 Petri Nets with Insecure Places and Secure Bisimulation . . . . . . ………….. . . . 182

       7.2.1 Petri Nets with Insecure Places . . . . . . . . . . . . . . . ………... . . . . . . . . . 182

       7.2.2 Secure Bisimulation . . . . . . . . . . . . . . . . . . . . . ……….. . . . . . . . . . . . . 185

  7.3 Summery and Further Reading . . . . . . . . . . . . . . . . . ………… . . . . . . . . . . . . . 189

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . …….. . . . . . . . . . . . . . . . . . . . . . 189

8 Time Petri Nets and Time-soundness  . . . . . . . . . . . . . . . . . . . ….……. . . . . . . . . . 191

  8.1 Time Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……….. . . . . . . . . . . . . . . . 191

       8.1.1 Formal Definition and Firing Rules . . ………… . . . . . . . . . . . . . . . . . . 191

       8.1.2 State Class Graph . . . . . . . . . . . . . ……….. . . . . . . . . . . . . . . . . . . . . . . 196

  8.2 Time-soundness . . . . . . . . . . . . . . . . . . ……… . . . . . . . . . . . . . . . . . . . . . . . . . . 205

       8.2.1 Time-soundness Based on Bisimulation . . . . . . . . . . …………. . . . . . . 205

       8.2.2 Deciding Time-soundness . . . . . . . . . . . . . . . ……..…. . . . . . . . . . . . . . 211

  8.3 Application. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……….. . . . . . . . . . . 213

  8.4 Summery and Further Reading . . . . . . . . . . . . . . . . . ……….. . . . . . . . . . . . . . . 219

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . …… . . . . . . . . . . . . . . . . . . 219

9 Timed Computation Tree Logic and Plain Time Petri Nets with

  Priorities  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ……. . . . . . . . . . . . . . . . . . 221

  9.1 Timed Computation Tree Logic . . . . . . . . . . . . . . . ……… . . . . . . . . . . . . . . . . 221

       9.1.1 CTL Verification over State Class Graphs . . . …..……. . . . . . . . . . . . . 221

       9.1.2 Syntax and Semantics of TCTL . . . . . . . . . . . ………... . . . . . . . . . . . . 224

       9.1.3 Model Checking Algorithms of TCTL Based on State

            Class Graphs of Time Petri Nets . . . . . . . . . ………. . . . . . . . . . . . . . . 227

  9.2 Plain Time Petri Net with Priorities . . . . . . . . . . . . ……….. . . . . . . . . . . . . . . . 240

       9.2.1 Definition of Plain Time Petri Net with Priorities . . ……….... . . . . . . . 241

       9.2.2 Firing Rules and State Class Graph of Plain Time Petri

            Nets with Priorities . . . . . . . . . . . . . . . . . ……… . . . . . . . . . . . . . . . . . . 243

       9.2.3 Properties of State Class Graphs of Plain Time Petri Nets

            with Priorities . . . . . . . . . . . . . . . . . . . . ……..…. . . . . . . . . . . . . . . . . . . 247

       9.2.4 Verifying TCTL over the State Class Graphs of Plain Time

            Petri Nets with Priorities . . . . . . . . . . ……..… . . . . . . . . . . . . . . . . . . . . 248

  9.3 Application. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . …..…… . . . . . . . . . . . . . . 252

  9.4 Summery and Further Reading . . . . . . . . . . . . . . ……..……. . . . . . . . . . . . . . . . . 256

  References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ………. . . . . . . . . . . . . . . . . . . . . . 256

Index  . . . . . . . . . . . . . . . . . . . . . . . . . . . . …… . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259

O autorze

Dr. Guanjun Liu received his Ph.D. in Computer Software and Theory from Tongji University, China, in 2011. He was Post-Doctoral Research Fellow with the Singapore University of Technology and Design from 2011 to 2013 and Post-Doctoral Research Fellow with the Humboldt University of Berlin, Germany, from 2013 to 2014 (supported by the Alexander von Humboldt Foundation). He is currently Professor at the Department of Computer Science, Tongji University, China. He has authored over 120 articles and three monographs (two in Chinese and one in English). His research interests include Petri net theory, model checking, machine learning, information security, credit card fraud detection, real-time concurrent systems, and multi-agent systems.