Sciweavers

Share
BIRTHDAY
2003
Springer

Petri Net Analysis Using Invariant Generation

10 years 9 months ago
Petri Net Analysis Using Invariant Generation
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.
Sriram Sankaranarayanan, Henny Sipma, Zohar Manna
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where BIRTHDAY
Authors Sriram Sankaranarayanan, Henny Sipma, Zohar Manna
Comments (0)
books