loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Ugo Buy, University of Illinois at Chicago
Gaurav Singal, University of Illinois at Chicago
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.