Dependency Analysis—A Petri Net Based Technique for Synthesizing Large Concurrent Systems

Petri nets (PN’s) are frequently used in modeling, designing, and analyzing concurrent systems. A problem with PN’s, in the general case, is that they require high computational complexity to analyze their properties such as reachability, liveness, and boundedness. To avoid this problem, synthesis techniques have been suggested for constructing large PN’s. Using these techniques, the behavior of the constructed PN can be determined by local analysis which makes use of known properties of the given nets. Thus, the high computational complexity of global analysis is bypassed. This paper presents a new synthesis technique by exploring dependency relations in PN’s. It synthesizes large PN’s by combining smaller PN’s of arbitrary topology structures, and the combination can be verified efficiently by dependency analysis. A large system based on PN can be built up by repeated applications of the technique.