In: Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, pages 682-701. Volume 2772 of Lecture Notes in Computer Science / Nachum Dershowitz (Ed.) --- Springer-Verlag, February 2004.
Abstract: Petri nets have been widely used to model and analyze concurrent systems. Their wide-spread use in this domain is, on one hand, facilitated by their simplicity and expressiveness. On the other hand, the analysis of Petri nets for questions like reachability, boundedness and deadlock freedom can be surprisingly hard. In this paper, we model Petri nets as transition systems. We exploit the special structure in these transition systems to provide an exact and closed-form characterization of all its inductive linear invariants. We then exploit this characterization to provide an invariant generation technique that we demonstrate to be efficient and powerful in practice. We compare our work with those in the literature and discuss extensions.