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, one can safely analyse Petri nets with performant tools, e.g. H_YT_(ECH), originally designed for analysing automata with real-valued variables (clocks). We also investigate the use of meta-transitions (iterative applications of a transition in a single step) and give sufficient conditions ensuring an exact computation in this case. Experimental results with H_YT_(ECH) 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.
展开▼
