A Formal Framework for Petri Net Class Transformations

A formalization of transformations of Petri Nets is presented in a categorical framework. It uses rule based modifications for the transformation of models within one Petri net class (replacement of one subnet by another one) and functors for the enrichment of the models to a different class (addition of features previously ignored). Net class transformations are defined between elementary nets, place/transition nets and algebraic high level nets. These class transformations preserve the rules and the derivation sequences. This compatibility guarantees that the order of application of a net class transformation and a model transformation does not affect the result. The net class transformations are then shown to ”lift” providing a form of stepwise enrichment of net classes.