ABSTRACT
The knitting technique provides a set of simple synthesis rules to construct a large Petri net (PN), thus avoiding time-consuming verification. We show that the synthesized nets are well behaved and form a new class called synchronized choice nets. In order to determine the applicable rules and detect rule violations, we present the concept of temporal matrix that records relationship (concurrent, exclusive, sequential, … etc.) among processes in the PN. Upon each generation, the algorithm will consult and update the matrix. The complexity for the algorithm is
O
where
is the total number of processes. This algorithm has been incorporated into our X-Window-based tool for design, analysis, simulation, testing, and synthesis of communication protocols, etc. The rules and algorithm have been extended to
include the once forbidden generations between exclusive transitions and arcs with multiple-weights, i.e., general Petri nets (GPNs).
