Equivalence and aggregation of GSPNs with labeled transitions

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. 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 has also been introduced for superposed generalized stochastic Petri nets (SGSPNs). We describe 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 is 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, then 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