Note: [*] Research partially funded by the German Research Foundation (DFG) under grant agreement GRK 1651
Note: [†] Research partially funded by the German Research Foundation (DFG) under grant agreement WE 4891/1-1. Address for correspondence: Department of Computer Science, Humboldt-Universität zu Berlin, Germany
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.
Keywords: Petri net analysis, inductive invariants, linear inequalities, stable properties, traps, co-traps, invariants
