Evgeny Erofeev: Reversing Transitions in Bounded Petri Nets

Reversible computation deals with mechanisms for undoing the effects of actions executed by a dynamic system. This paper is con- cerned with reversibility in the context of Petri nets which are a general formal model of concurrent systems. A key construction we investigate amounts to adding ‘reverse’ versions of selected net transitions. Such a static modification can severely impact on the behaviour of the sys- tem, e.g., the problem of establishing whether the modified net has the same states as the original one is undecidable. We therefore concentrate on nets with finite state spaces and show, in particular, that every tran- sition in such nets can be reversed using a suitable set of new transitions.