Petri Nets, Flat Languages and Linear Arithmetic.
Laurent Fribourg · 2000
We present a method for characterizing the least fixed-points of a certain class of Datalog programs in Presburger arithmetic. The method consists in applying some rules of decomposition that transform general sets of computation paths into "flat" ones. We apply the method for expressing the reachability relation of Petri nets as a linear arithmetic formula in order to prove (or disprove) their safety properties.