Efficient Reachability Graph Representation of Petri Nets With Unbounded Counters
Franck Pommereau, Raymond Devillers, Hanna Klaudel · Electronic Notes in Theoretical Computer Science · 2009
In this paper, we define a class of Petri nets, called Petri nets with counters, that can be seen as place/transition Petri nets enriched with a vector of integer variables on which linear operations may be applied. Their semantics usually leads to huge or infinite reachability graphs. Then, a more compact representation for this semantics is defined as a symbolic state graph whose nodes possibly encode infinitely many values for the variables. Both representations are shown behaviourally equivalent.