Characterization of Admissible Marking Sets in Petri Nets With Conflicts and Synchronizations

In this paper we study the problem of constraint transformation for Petri nets with uncontrollable transitions and containing both conflicts and synchronizations. We show that given an arbitrary net and a set of legal markings, the admissible marking set cannot always be represented by a finite number of disjunctions of GMECs. Moreover, we characterize the GMEC inflation phenomenon, that is, the case in which the representation of the admissible marking set may be too complex to be efficiently implemented in a closed-loop net. To rule out the possibility of GMEC inflation we consider a subclass of constraints called singular GMECs with an acyclic backward-conflict-free uncontrollable subnet. By these assumptions we propose an algorithm to transform a given singular GMEC into a controllable OR-GMEC which precisely characterizes its admissible marking set.