Tham khảo tài liệu 'petri net part 14', kỹ thuật - công nghệ, cơ khí - chế tạo máy phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả | Augmented Marked Graphs and the Analysis of Shared Resource Systems 381 For clarity in presentation P y and T y can be written as P y and T y to denote the set of places in a cycle y and the set of transitions generated by y respectively. Definition . For a PT-net N an elementary path p x1 X2 . xn is said to be conflict-free if and only if for any transition xi in p j i -1 Xj Ể Xi Barkaoui 1995 . Lemma . Let S be a minimal siphon of a PT-net. For any p p e S there exists in S a conflict-free path from p to p Barkaoui 1995 . Property . For a minimal siphon S of an augmented marked graph N Mo R there exists a set of cycles Y c Dn such that P Y S. Proof. Let S p1 p2 . pn . For each pi it follows from the definition of augmented marked graphs that pi 0. Then there exists pj e S where pj pi such that pj n pi 0. According to Lemma pi connects to pj via a conflict-free path in S. Since pj connects to pi this forms a cycle yi in S where pi e P yi c S. Let Y y1 y2 . yn . We have P Y P y1 u P y2 u . u P yn c S. On the other hand S c P y1 u P y2 u . u P yn P Y since S p1 p2 . pn . Hence P Y S. Property . Every cycle in an augmented marked graph is marked. Proof. by contradiction Let N Mo R be an augmented marked graph. Suppose there exists a cycle y in N Mo R such that y is not marked. Then y does not contain any place in R. Hence y also exists in the net N Mo obtained from N Mo R after removing the places in R and their associated arcs. However by definition of augmented marked graphs every cycle in N Mo is marked. Property . Every siphon in an augmented marked graph is marked. Proof. For an augmented marked graph according to Properties and every minimal siphon contains cycles and is marked. Hence every siphon which contains at least one minimal siphon is marked. Property . Let N Mo R be an augmented marked graph. For every r e R there exists a minimal siphon which contains only one marked place r. Proof. Let Dr ts1 th1 ts2 th2 . tsn thn where
