TY - GEN
T1 - Efficient lumpability check in partially symmetric systems
AU - Beccuti, M.
AU - Franceschinis, G.
AU - Baarir, S.
AU - Ilié, J. M.
PY - 2006
Y1 - 2006
N2 - 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 systems by aggregating equivalent states and transitions. An effective way of exploiting symmetries when the system 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 refinement to satisfy the lumpability conditions. In this paper a new efficient 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 refinement algorithm (extended to work with weighted arcs) and a previously proposed lumpability check algorithm (built specifically for the use with the ESRG) and outperforms both of them. The implementation of the algorithm within the GreatSPN environment will allow the several users that have chosen this package to apply the proposed technique.
AB - 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 systems by aggregating equivalent states and transitions. An effective way of exploiting symmetries when the system 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 refinement to satisfy the lumpability conditions. In this paper a new efficient 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 refinement algorithm (extended to work with weighted arcs) and a previously proposed lumpability check algorithm (built specifically for the use with the ESRG) and outperforms both of them. The implementation of the algorithm within the GreatSPN environment will allow the several users that have chosen this package to apply the proposed technique.
UR - http://www.scopus.com/inward/record.url?scp=41149158111&partnerID=8YFLogxK
U2 - 10.1109/QEST.2006.17
DO - 10.1109/QEST.2006.17
M3 - Conference contribution
AN - SCOPUS:41149158111
SN - 0769526659
SN - 9780769526652
T3 - Third International Conference on the Quantitative Evaluation of Systems, QEST 2006
SP - 211
EP - 220
BT - Third International Conference on the Quantitative Evaluation of Systems, QEST 2006
T2 - 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006
Y2 - 11 September 2006 through 14 September 2006
ER -