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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Sankaranarayanan, S., Sipma, H., & Manna, Z. (2004). Petri net analysis using invariant generation. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2772, 682–701. https://doi.org/10.1007/978-3-540-39910-0_29
Mendeley helps you to discover research relevant for your work.