Dependency analysis-a Petri-net-based technique for synthesizing large concurrent systems

Petri nets (PNs) are frequently used in modeling, designing, and analyzing concurrent systems. A problem with PNs, 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 for constructing large PNs are presented. Using these techniques, the behavior of the constructed PN can be determined by local analysis that uses known properties of the given nets. Thus, the high computational complexity of global analysis is bypassed. A synthesis technique that explores dependency relations in PNs is presented. It synthesizes large PNs by combining smaller PNs of arbitrary topology structures, and the combination is verified efficiently by dependency analysis. A large system based on a PN can be built up by repeated applications of the technique