Authors:   Juan Ignacio Latorre, Emilio Jimenez

Abstract

Petri net is a modelling paradigm used for discrete event systems (David and Alla 2005), (Cassandras et al. 2008). Their transformations are a powerful tool for the validation and verification of Petri nets as models of discrete event systems. If a simplified Petri net verifies a certain set of properties, the original Petri net will verify them if the applied net transformation preserves these properties. On the other hand, the control of Petri nets may also improve with the application of Petri net transformations. If the unobservable transitions are removed by the application of transformation rules, then the state of the simplified net evolves under the firing of the observable transitions. In this paper, the transformation of nets will be applied to modify the formalism that represents a disjunctive constraint of a decision problem stated on a Petri net model. Some formalisms may be more suitable for the modelling process than others (alternative Petri nets), while others are more compact and suitable for the development of optimization processes in an efficient way (compound Petri nets, alternatives aggregation Petri nets or disjunctive coloured Petri nets). A set of transformation rules that preserve the structure of the associated graph or reachable markings are provided in this paper, as well as an example of application in a net transformation between two formalisms. As a consequence of the application of these rules, both the original and resulting formalisms will show an equivalent behaviour. Hence, any of them can be used to state a decision problem but the efficiency of the algorithm to solve the problem may be different when considering the required computer resources and the quality of the obtained solution.