In: Lecture Notes in Computer Science : Petri Nets and Other Models of Concurrency - ICATPN 2006, Volume 4024, 2006, pages 322-341. 2006. URL: http://dx.doi.org/10.1007/1176758918.
Abstract: This paper proposes an analytical method for the synthesis of reversibility-enforcing supervisors for bounded Petri nets. The proposed me-thod builds upon recent developments from (i) the theory of regions, that enables the design of Petri nets with pre-specified behavioral requirements, and (ii) the theory concerning the imposition of generalized mutual exclusion constraints on the net behavior through monitor places. The derived methodology takes the form of a Mixed Integer Programming formulation, which is readily solvable through canned optimization software. The last part of the paper discusses extensions of the presented method so that it accommodates uncontrollable behavior and any potential complications arising from the large-scale nature of the underlying plant nets and their behavioral spaces. Finally, the relevance and the efficacy of the proposed approach is demonstrated through its application in the synthesis of liveness-enforcing supervisors for process-resource nets.