26th Annual International Computer Software and Applications Conference Toward Efficient Algorithms for Generating Compact Petri Nets from Labeled Transition Systems Oxford, England August 26-August 29 ISBN: 0-7695-1727-7
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.
Index Terms:
Petri nets, transition systems, concurrency, automatic verification, Petri net generation, reachability graph
Citation:
Ugo Buy, Gaurav Singal, "Toward Efficient Algorithms for Generating Compact Petri Nets from Labeled Transition Systems," compsac, pp.717, 26th Annual International Computer Software and Applications Conference, 2002 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||