Toward efficient algorithms for generating compact Petri nets from labeled transition systems

Compositional methods for Petri-net-based verification of concurrent systems are appealing because they allow the analysis of a complex system to be carried out in a piece-by-piece manner. An issue in compositional Petri-net analysis is the generation of a compact net from a labeled transition system (LTS) isomorphic to the reachability graph of the net. Several existing approaches for Petri-net generation use the concept of region, a subset of the original LTS; however, the computation of the regions in an LTS appears to be quite expensive. We report preliminary results on the generation of a Petri net from an LTS isomorphic to the net´s reachability graph without requiring the computation of regions. We specifically introduce two algorithms for generating the place set and flow relation of a safe and live ordinary Petri net. The most complex of the two algorithms is nearly linear in the size of the input LTS