MENÜ MENÜ  

cover

Categorical Net Transformations for Petri Net Technology

Milan Urbasek

ISBN 978-3-8325-0327-7
215 pages, year of publication: 2003
price: 40.50 €
The aim of this thesis is elaboration of net transformations used in the Petri net technology called "Petri Net Baukasten". The application oriented Petri net technology "Petri Net Baukasten" provides a collection of different Petri net techniques and principles for their combination. In general, the techniques are independent of each other. Their actual use is usually given by needs of real applications and projects they operate on. Petri net technology helps to reduce the gap between academia and practice on the field of Petri nets. The role of net transformations is crucial for establishing the formal framework of Petri net technology.

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.

Keywords:
  • Petri net
  • net transformation
  • software engineering
  • high-level replacement system
  • category theory

BUYING OPTIONS

40.50 €
in stock