Efcient lumpability check in partially symmetric systems

State space based performance analysis of stochastic models may be impaired by the state space explosion but such problem can be mitigated in symmetrical behaving sys-tems by aggregating equivalent states and transitions. An effective way of exploiting symmetries when the sys-tem is modeled using the Stochastic Well-Formed Net (SWN) formalism, is to generate the Symbolic Reachability Graph (SRG) and automatically derive a lumped Continuous Time Markov Chain (CTMC) of the same size as the SRG from it. For partially symmetric systems, the Extended SRG (ESRG) can be used instead, but the derivation of a lumped CTMC in this case is not as direct as in the SRG case: in fact the ESRG structure might need a renement to satisfy the lumpability conditions. In this paper a new efcient algorithm to derive a lumped CTMC from the ESRG is presented, and the results obtained by experimenting its implementation within the GreatSPN environment are discussed. The algorithm combines the Paige and Tarjan’s partition renement algorithm (extended to work with weighted arcs) and a previously proposed lumpability check algorithm (built specically for the use with the ESRG) and outperforms both of them. The im-plementation of the algorithm within the GreatSPN envi-ronment will allow the several users that have chosen this package to apply the proposed technique.