In: Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, pages 471-490. Volume 2885 of Lecture Notes in Computer Science --- Springer-Verlag, November 2003.
Abstract: Petri nets are useful for modelling complex concurrent systems. While modelling using Petri nets focusses on local states and actions, the analysis methods are concerned with global states and their transitions. Unfortunately generation of the complete state space suffers from the well-known state space explosion problem. This paper presents a method to overcome the state-space explosion problem for a class of Generalised Stochastic Petri Nets (GSPNs). Large complex GSPN models are transformed into smaller, less complex ones with smaller state spaces than the original models. This transformation is called aggregation. The aim of aggregation is to reduce the state space while preserving the desired behaviour of the original model. In this paper we investigate the aggregation of GSPNs preserving time dependent behaviour by using recent and newly developed transformation rules. These rules are used to merge several single timed transitions into one merged transition. The firing rate of the merged transition turns out to be dependent on the marking of the net. Beside the introduction of a new method for the aggregation of exponential transitions with fixed firing rates, new formulae to aggregate transitions with marking-dependent firing rates are presented. Successive aggregation becomes possible to transform very complex models into models in which either a closed-form computation of the stationary state distribution is available or which has a very small state space. A prototype implementation is used to demonstrate both the drastically reduced state space for suitable models and the general limits of the method.