Overview

Full Product Details

Author:   Guanjun Liu
Publisher:   Springer Verlag, Singapore
Imprint:   Springer Verlag, Singapore
Edition:   1st ed. 2022
Weight:   0.606kg
ISBN:  

9789811963087

ISBN 10:   9811963088
Pages:   279
Publication Date:   04 November 2022
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Hardback
Publisher's Status:   Active
Availability:   Manufactured on demand  
We will order this item for you from a manufactured on demand supplier.

Table of Contents

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

Reviews

“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)

Author Information

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.

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions