Affiliations: [a] Department of Computing Science, Carl von Ossietzky Universität Oldenburg, D-26111 Oldenburg, Germany. [email protected] | [b] IBISC, Université d’Evry-Val-D’Essonne, 91025, Evry, France. [email protected] | [c] LIP6, Sorbonne Universités, UPMC Paris 06, UMR 7606, F-75005, Paris, France. [email protected]
Correspondence:
[†]
Address for correspondence: Department of Computing Science, Carl von Ossietzky Universität Oldenburg, D-26111 Oldenburg, Germany
Note: [*] The work of this author has been partially supported by Digiteo / Project TATAMI
Abstract: Weighted Petri nets provide convenient models of many man-made systems. Real applications are often required to possess the fundamental Petri net properties of liveness and reversibility, as liveness preserves all the functionalities (fireability of all transitions) of the system and reversibility lets the system return to its initial state (marking) using only internal operations. Characterizations of both behavioral properties, liveness and reversibility, are known for well-formed weighted Choice-Free and ordinary Free-Choice Petri nets, which are special cases of Equal-Conflict Petri nets. However, reversibility is not well understood for this larger class, where choices must share equivalent preconditions, although characterizations of liveness are known. In this paper, we provide the first characterization of reversibility for all live Equal-Conflict Petri nets by extending, in a weaker form, a known condition that applies to the Choice-Free and Free-Choice subclasses. We deduce the monotonicity of reversibility in the live Equal-Conflict class. We also give counter-examples for other classes where the characterization does not hold. Finally, we focus on well-formed Equal-Conflict Petri nets, for which we offer the first polynomial sufficient conditions for liveness and reversibility, contrasting with the previous exponential time conditions.
Keywords: Reversibility, liveness, Equal-Conflict, Petri net, characterization, polynomial time sufficient condition, polynomial markings
