Reversible computation vs. reversibility in Petri nets

Adding reverses can severely impact on the behaviour of a Petri net. Therefore it is important, in particular, to be able to determine whether the modified net has a similar set of states as the initial one. We first prove that the problem of establishing whether the initial and modified nets have the same reachable markings is undecidable, even in the restricted case considered in this paper. We then show that the problem of checking whether the reachability sets of the two nets cover the same markings is decidable.