For a systematic study of Petri net transformations we distinguish two levels of transformations, namely net model transformations and net class transformations. The net model transformations provide a foundation for refinement of Petri net based models. Generally, they employ the rule based approach known from graph transformations, which is applied on Petri nets. They operate on a given Petri net changing its structure and/or other aspects yielding new Petri net. A series of net model transformations is a base for stepwise development of models based on Petri nets.
In order to support formal verification of Petri net based models the preservation of certain system properties during the stepwise development is of interest. One of main contributions of this thesis is the development of liveness preserving net model transformations. Several such transformations have been investigated, and formal conditions for each are supplied. Net model transformations preserving safety properties and liveness, and the possibility of building new property preserving net model transformations from other ones are presented as well.
Net class transformations allow a model developer to change the underlying Petri net class during the modeling step. The formalization of this concept is another important question in Petri net technology. The explosion of net class transformations when a new aspect of a Petri net is introduced has shown the need for a generic concept. In this thesis the generic concept based on comma categories is investigated. It is another important contribution of this thesis. This concept has been applied on classes of marked and open preserving place/transition nets, and algebraic high-level nets. The compatibility of both types of net transformations is shown as well.
The presented work includes several simple case studies which proclaim the suitability of net transformations for applications.