A reversibility enforcement approach for Petri nets using invariants

Abstract

Petri net model which is one of the most common modelling method of discrete event systems, is considered to enforce reversibility in this work. Reversibility guarantees that the intial state is reachable from any state in the reachability set of given Petri net. An approach, enforcing reversibility, is presented in this work. In this approach, the minimal T-invariants and the firing sequences coressponding to the determined T-invariants are determined. Then, a set of markings, which is a subset of reachability set, is constructed by using those firing sequences. In this set, any state can reach to the initial state. Furthemore, the algorithms are developed for the presented enforcement approach and implemented by using Matlab.