Reconfiguration in Stochastic Petri Nets

Abstract

Nowadays, many discrete event systems (DESs) are becoming increasingly complex, structurally dynamic and variably interconnected. These systems are designed to be able to change their structure and/or topology, at run-time, to accommodate new circumstances/requirements. As a formal tool, the use of Petri nets (PNs) in the study of such systems attracts many researchers. Although PNs (low or high) are a powerful and expressive tool, they are unable to specify/ verify, in a natural way, advanced systems having dynamic structures. Indeed, systems supporting volatile environments, continuous variations, and reconfigurable structures are expected to be extremely complex. To overcome this issue, researchers enrich PNs with reconfigurability. Nevertheless, increasing the modeling power of a formalism decreases its decision power. In fact, several properties become undecidable. Therefore, extensions proposed in the literature introducing reconfigurability to PNs try to find a compromise between the modeling and the verification levels. In this thesis, we describe three approaches – incrementally developed – for the modeling and verification of reconfiguration in generalized stochastic Petri nets (GSPNs), while maintaining verifiability of several properties with reduced complexity. First, we propose a formalism, called GSPNs with rewritable topology (GSPNs-RT), that extends GSPNs by allowing modeling dynamic topologies and transforming GSPNs- RT to equivalent GSPNs, to take full advantages of off-the-shelf tools proposed for GSPNs verification. Then, we propose another formalism, called dynamic GSPNs (D-GSPNs), that allows modeling and verifying dynamic structures (sets of places and transitions are dynamic) and transforms D-GSPNs to equivalent GSPNs. This transformation can take place when the original model disposes of a finite number of configurations. Finally, GSPNs are extended to a reconfigurable formalism, called reconfigurable GSPNs (RecGSPNs), that supports a wider range of possible structural changes than allowed in existing approaches, as well as, allows to any RecGSPN to have an infinite number of configurations while preserving the decidability of several important properties.