In: Mazurkiewicz, A.; Winkowski, J.: Lecture Notes in Computer Science, Vol. 1243: CONCUR'97: Concurrency Theory, 8th International Conference, Warsdaw, Poland, July 1997, pages 213-227. Germany, Berlin: Springer-Verlag, July 1997.
Abstract: We present in this paper a method combining path decomposition and bottom-up computation features for characterizing the reachability sets of Petri nets within Presburger arithmetic. An application of our method is the automatic verification of safety properties of Petri nets with infinite reachability sets. Our implementation is made of a decomposition module and an arithmetic module, the latter being built upon Boudet-Comon's algorithm for solving the decision problem for Presburger arithmetic. Our approach will be illustrated on three nontrivial examples of Petri nets with unbounded places and parametric initial markings.