In: Theoretical Computer Science, Vol. 222, No. 1-2, pages 187-194. July 1999.
Abstract: Reset Petri nets extend Petri nets by allowing transitions to empty places, in addition to the usual adding or removing of constants. A Reset Petri net is normalized if the flow function over the Petri arcs (labeled with integers) and the initial state are valuated into 0,1. In this paper, we give an efficient method to turn a general Reset Petri net into a lambda-bisimilar normalized Reset Petri net. Our normalization preserves the main usually studied properties: boundedness, reachability, t-liveness and language (through a lambda-labeling function). The main contribution is the improvement of the complexity: our algorithm takes a time in O(size(N)2), for a Reset Petri net N, while other known normalizations require an exponential space and are presented for Petri nets only.
Keywords: Concurrency, Verification, Petri nets, Equivalences.