In: Baeten, Jos C.M.; Mauw, Sjouke: Lectures Notes in Computer Science, Vol. 1664: Proceedings of 10th International Conference on Concurrency Theory, Eindhoven, pages 178-193. Springer-Verlag, August 1999.
Abstract: In this paper, we address the issue of reachability analysis for Petri nets, viewed as automata with counters. We show that exact reachability analysis can be achieved by treating Petri nets integer variables (counters) as real-valued variables, and using Fourier-Motzkin procedure instead of Presburger elimination procedure. As a consequence, on can safely analyse Petri nets with performant tools, e.g. HYTECH, originally designed for analysing automata with real-valued variables (clocks). We also investigate the use of meta-transitions (iterative application of a transition in a single step) and give sufficient conditions ensuring an exact computation in this case. Experimental results with HYTECH show an impressive speed-up with respect to previous experiences performed with a Presburger arithmetic solver. The method extends for analysing Petri nets with inhibitors and with timing constraints, but difficulties arise for the treatment of meta-transitions in the latter case.