Characterisation of the state spaces of marked graph Petri nets (Q515678)

A marked graph Petri net is a Petri net where each place has exactly one ingoing and exactly one outgoing arc, and hence no choices, i.e., alternative routings of tokens. The paper shows that this structural property of a Petri net results in a structural property of its behaviour, given by its reachability graph.\par Moreover, the authors are able to characterize all reachability graphs that result from marked graph Petri nets by structural means. The result is obtained by a distinction of cases: bounded marked graph Petri nets with finitely many reachable states and unbounded ones with infinitely many reachable states. For each of these two cases, it is shown how to obtain a reachability graph which satisfies the structural property. The converse direction is much more involved, to synthesise a marked graph Petri net from a graph with the above property. The synthesis procedure constructs a unique minimal net and moreover allows to compute its initial marking and all maximal token counts on places of this net.