Linear Algebra Based Verification of Well-Behaved Properties and P- Invariants of Petri Nets Synthesized Using Knitting Technique
趙玉, Daniel Yuh Chao · 1995
The knitting technique (KT) (CHA 94a-d, WAN 94a-c) has been proved a good approach to synthesize Petri (PNs) with the well-be haved properties such as liveness, boundedness, and reversibility preserved automatically. Hence it can relieve the complexity problem of reachability analysis of PN as required by many other methods. This work proves that the PNs synthesized with KT are structurally bounded. consistent, conser vative and safe when each home place holds one token using the well-known linear algebra approach. It also provides examples and a procedure for find ing invariants for PN synthesized using KT. These examples also show that we can synthesize more general than the assymetric-clwice nets (MUR 89). dency analysis; rather, they can be obtained 1. IXl'RODUCTION with reachability analysis. The size of reacha PNs have been used for modeling and anability graph depends not only by the structure concurrent systems (PET 81, MUR 85, of the net, but also by the initial marking. In YlUR 89). The net behavior depends not only general, the larger the initial marking (i. e .• on the graphical structure, but also on the ini more tokens are involved), tht1<l~2r the tial marking of the net. Therefore they cannot reachability graph. It has been shown that the be determined by static analysis such as depencomplexity of the reachability analysis of PNs The former name of the author was Yuh Yaw.