Reversing Unbounded Petri Nets

Lukasz Mikulski (1) , Ivan Lanese (2, 3)

1 Nicolaus Copernicus University [Toruń]
2 FOCUS - Foundations of Component-based Ubiquitous Systems
3 UNIBO - Alma Mater Studiorum Università di Bologna = University of Bologna

In Petri nets, computation is performed by executing transitions. An effect-reverse of a given transition b is a transition that, when executed, undoes the effect of b. A transition b is reversible if it is possible to add enough effect-reverses of b so to always being able to undo its effect, without changing the set of reachable markings. This paper studies the transition reversibility problem: in a given Petri net, is a given transition b reversible? We show that, contrarily to what happens for the subclass of bounded Petri nets, the transition reversibility problem is in general undecidable. We show, however, that the same problem is decidable in relevant subclasses beyond bounded Petri nets, notably including all Petri nets which are cyclic, that is where the initial marking is reachable from any reachable marking. We finally show that some non-reversible Petri nets can be restructured, in particular by adding new places, so to make them reversible, while preserving their behaviour.

Mots clés: Reverse transition; Petri Nets; Reversibility

Domaines: Théorie et langage formel [cs.FL]

Lukasz Mikulski, Ivan Lanese. Reversing Unbounded Petri Nets. PETRI NETS 2019 - Applications and Theory of Petri Nets, Jun 2019, Aachen, Germany. ⟨10.1007/978-3-030-21571-2_13⟩. ⟨hal-02376158⟩