Equivalence of temporal and structural relationships of synthesized nets using knitting technique

摘要

The knitting technique provides a set of simple synthesis rules to construct a large Petri net (PN) avoiding time-consuming verification. The linear-algebra technique is useful to show the synthesized nets (SC) are bounded and conservative, but unable to prove that they are live. This paper shows that the SC are live by showing the equivalence of temporal and structure relationships. We also show that they belong to a special class of nets called synchronized choice (SC) nets.