Sufficient conditions for the marked graph realisability of labelled transition systems (Q1623288)

Let a system be described by a persistent (once two different labels are both enabled, neither can disable the other, and executing both, in any order, leads to the same state) Petri net which is plain (without multiple edges), bounded (there are limits on a number of tokens in every place), reversible (initial state is always reachable), and has an initial \(k\)-marking (a number of tokens in every place is divided by \(k\)) with \(k \geq 2\). It is proven that there exists a marked graph Petri net (every place has exactly one incoming edge and exactly one outgoing arc) with an isomorphic state space. Let a system be described by a persistent Petri net which is plain, safe (maximum one token in every place), reversible, and has, in its reachability graph, a cycle containing each transition once. It is proven that there exists a marked graph Petri net with an isomorphic state space.