Stop-transitions of Petri Nets^*

Issue title: A Mosaic of Computational Topics: from Classical to Novel, Special Issue Dedicated to Jetty Kleijn on the Occasion of Her 65th Birthday

Guest editors: Maurice ter Beek, Maciej Koutny and Grzegorz Rozenberg

Article type: Research Article

Authors: Desel, Jörg | Finthammer, Marc^{; †}

Affiliations: Fern Universität in Hagen, Hagen, Germany. joerg.desel@fernuni-hagen.de, marc.finthammer@fernuni-hagen.de

Correspondence: [†] Address for correspondence: FernUniversität in Hagen, Germany

Note: [*] This is an extended version of [1]

Abstract: A transition t stops a place/transition Petri net if each reachable marking of the net enables only finite occurrence sequences without occurrences of t (i.e., every infinite occurrence sequence enabled at this marking contains occurrences of t). Roughly speaking, when t is stopped then all transitions of the net stop eventually. This contribution shows how to identify stoptransitions of unbounded nets using the coverability graph. Furthermore, the developed technique is adapted to a more general question considering a set of stop-transitions and focussing on a certain part of the net to be stopped. Finally, an implementation of the developed algorithm is presented.

Keywords: unbounded Petri nets, coverability graphs, termination of Petri nets, stop-transitions, minimal coverability sets

DOI: 10.3233/FI-2020-1951

Journal: Fundamenta Informaticae, vol. 175, no. 1-4, pp. 143-172, 2020