Daniel Y. Chao
Department of Management Information Systems
National Cheng Chi University
Taipei, Taiwan 116, R.O.C.
The knitting technique provides a set of simple synthesis rules to construct a large Petri net (PN) while 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 a temporal matrix, which records the relationships (concurrent, exclusive, sequential etc.) among processes in the PN. Upon each generation, the algorithm will consult and update the matrix. The complexity of the algorithm is O(2), where is the total number of processes. This algorithm has been incorporated into our X-Window based tool for the design, analysis, simulation, testing, and synthesis of communication protocols and others.
Keywords: Petri net, concurrent system, automated manufacturing system, liveness, boundedness, deadlock, synthesis, processes, local concurrent set, local exclusive set, structural relationship, temporal matrix, algorithm, rules, X-Window, CAD tool
Received December 14, 1995; revised September 26, 1997.
Communicated by Jhing-Fa Wang.