Characterizing Stable and Deriving Valid Inequalities of Petri Nets

Abstract

One way to express correctness of a Petri net N is to specify a linear inequality U, requiring each reachable marking of N to satisfy U. A linear inequality U is stable if it is preserved along steps. If U is stable, then verifying correctness reduces to checking U in the initial marking of N. In this paper, we characterize classes of stable linear inequalities of a given Petri net by means of structural properties. We generalize classical results on traps, co-traps, and invariants. We show how to decide stability of a given inequality. For a certain class of inequalities, we present a polynomial time decision procedure. Furthermore, we show that stability is a local property and exploit this for the analysis of asynchronously interacting open net structures. Finally, we study the summation of inequalities as means of deriving valid inequalities.