Petri Net Theory: A Survey |
From inside the book
Results 1-3 of 48
Page 9
... definition of a net's transition relation . Definition : Let M and M ' be markings of a Petri Net N = ( P , T , pre , post , Mo ) . Let AE μT be a finite multiset of transitions . The transition relation for N is defined as MAM ' iff ...
... definition of a net's transition relation . Definition : Let M and M ' be markings of a Petri Net N = ( P , T , pre , post , Mo ) . Let AE μT be a finite multiset of transitions . The transition relation for N is defined as MAM ' iff ...
Page 17
... definition is phrased for general concurrent systems , and may be adapted specifically for Petri Nets , as detailed below . In order to obtain a definition of bisimulation for Petri Nets , it is first necessary to define functions on ...
... definition is phrased for general concurrent systems , and may be adapted specifically for Petri Nets , as detailed below . In order to obtain a definition of bisimulation for Petri Nets , it is first necessary to define functions on ...
Page 31
... Definition : A P - Net is an unmarked Petri Net N = ( P , T , pre , post ) such that for all tET , t≤ 1 and t • | ≤ 1. □ < P - nets possess no synchronisation , simply because there are no ( backward ) branched transitions ; a safe ...
... Definition : A P - Net is an unmarked Petri Net N = ( P , T , pre , post ) such that for all tET , t≤ 1 and t • | ≤ 1. □ < P - nets possess no synchronisation , simply because there are no ( backward ) branched transitions ; a safe ...
Common terms and phrases
analysis arcs bisimulation called Coloured Petri Nets combinatorial components Computer Science concurrent systems conflict Coverability Tree CR-path deadlock defined Definition denoted dynamic behaviour equivalent events A₁ Example figure finite firable Free Choice Free-Choice Nets function GVASS initial marking integers invariants label Lecture Notes Lemma live and safe live iff M₁ maximal element morphism multiset N-dense net's node Notes in Computer notion occur occurrence net occurrence nets P-completion P-net P,T,pre partially ordered set Petri Net model place-invariant poset post(p pre(p Project MAC Proof properties Reachability Problem reachable marking relation restricted result safe nets sequence set of places set of transitions simple cycles Springer-Verlag strongly connected strongly connected components structure subnet synchronic distance T-nets T₂ Theorem transition relation transitive closure trap Unmarked Petri VASS Vector Addition Systems