On Quantitative Properties Preservation in Reconfigurable Generalized Stochastic Petri Nets

Generalized stochastic Petri nets (GSPNs) have been extended to several dynamic-structure formalisms providing suitable tools for the modeling and verification of reconfigurable discrete-event systems (R-DESs). However, analyzing the performance of large-complex R-DESs remains a big challenging issue. Indeed, dynamic-structure GSPNs still rely on old-fashioned techniques often causing the state-space explosion problem. In this article, we present a new technique for the quantitative analysis of a dynamic-structure formalism called reconfigurable GSPNs without computing the whole state space. This work describes new reconfiguration forms used to preserve desired quantitative properties of parts of interest after each reconfiguration. Therefore, it is only required to verify the examined properties at an initial configuration. The proposed technique is proven to effectively reduce the state space and shorten the computation time in such cases. Finally, some experimental results are provided to illustrate that, from a computational perspective, the developed approach outperforms the existing tools.