In: Proceedings of 9th International Workshop on Petri Nets and Performance Models, PNPM'01 Aachen, Sept. 11-14, 2001, Reinhard German and Boudewijn Haverkort (eds.), IEEE, pages 187-196. 2001.
Abstract: Equivalence is a basic concept in many modeling formalisms to compare different realizations of a system or to compute for a given system a minimal equivalent representation. In this paper we present two different equivalence relations for a class of Generalized Stochastic Petri Nets (GSPNs), with labeled transitions (LGSPNs), namely trace equivalence and bisimulation equivalence. In contrast to most other approaches we allow labeling of timed and immediate transitions and thus have to define equivalence for a stochastic process with exponentially timed and immediate transitions. For this class of GSPNs it is possible to compose nets via timed and immediate transitions which hag recently also been introduced for Superposed Generalized Stochastic Petri Nets (SGSPNs). In the second part of the paper it is described under which conditions the proposed equivalences are congruences according to the composition of nets. The congruence condition is easily to achieve for timed transitions but it will be shown that some additional restrictions are necessary to obtain a congruence relation which is preserved under composition via immediate transitions. However, if such a congruence is defined, the component state spaces can be reduced by aggregation before composition. This aggregation includes an elimination of some immediate transitions in LGSPNs composed via immediate transitions which has not been considered yet.