Characterisation of the state spaces of marked graph Petri nets

The structure of the reachability graph of a marked graph Petri net is fully characterised. Exact structural conditions are given for a given labelled transition system to be generated by a marked graph. Two cases are distinguished, corresponding to the boundedness or the unboundedness of the net, and, respectively, to the finiteness or the infiniteness of the transition system. Dedicated synthesis procedures are presented for both cases, and it is shown that there is always a unique minimal solution. The synthesis procedures allow this minimal net, its initial marking, and the marking bounds of its places to be computed from the labelled transition system.