Author : Karsten Schmidt Title: as above Language: German Publisher : Dieter Bertz Verlag, Berlin ISBN : 3--929470--54--3
The text of this book is a dissertation, submitted to Humboldt--University in Berlin. It deals with symbolic analysis methods for algebraic Petri nets. For this kind of high--level nets algebraic specifications are used to describe the individuality of tokens. Though it is possible to specify infinite data types and therefore many standard properties are undecidable for this net class there should be a computer aid for the analysis of algebraic nets.
The formalism of algebraic specifications provides a syntactic framework for symbolic calculations, in particular rewriting techniques for deciding equivalence of descriptions and solving equations. We study how these techniques can be involved in well known Petri net analysis methods, namely invariant calculus and reachability graph construction.
Chapter I introduces the main concepts used in the remaining chapters. It contains a short introduction of algebraic specifications, the definition of algebraic Petri nets and their interpretation.
In chapter II we compare invariant definitions for place transition nets, coloured nets and algebraic nets. Then we investigate the structure of place invariants and transition invariants for algebraic nets and end up in the characterization of small generator sets. We develop an algorithm to enumerate such a generator set. Thereby the calculations are traced back to unification problems. We prove that an algorithm which computes a generator set for all transition invariants cannot always terminate since it is undecidable whether an algebraic net has non--trivial transition invariants or not. We propose simplifications of the analysis problems which allow to circumvent the major computational problems.
In chapter III we take up the idea of parameterized reachability graphs which have been introduced for predicate/transition nets. We translate this method to the formalism of algebraic nets. Thereby we apply several improvements which allow stronger implications between the graph and the behavior of the underlying nets. We present ideas how the stubborn set method can be used to reduce the size of a parametrized reachability graph.
Chapter IV contains examples where we demonstrate our methods and general conclusions.
Karsten Schmidt