Proving safety properties of infinite state systems by compilation into presburger arithmetic

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.