Titre : | Reconfiguration in stochastic petri nets |
Auteurs : | Samir Tigane, Auteur ; Laïd Kahloul, Directeur de thèse ; Souheib Baarir, Directeur de thèse |
Type de document : | Thése doctorat |
Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2020 |
Format : | 1 vol. (146 p.) / 30 cm |
Langues: | Anglais |
Mots-clés: | Generalized stochastic Petri nets ; Dynamic model and structure ; Graph transformation systems ; Formal modeling and verification ; Performance evaluation. |
Résumé : |
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. |
Sommaire : |
1 Introduction 1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Motivation and Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 I State-of-the-Art 9 2 Stochastic Petri Nets 10 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2 Modeling with Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 Petri Net Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.4 Dynamic Behavior of Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.5 Petri Net Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.5.1 Petri Net Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.5.2 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.5.3 Analysis Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.6 Stochastic Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.6.1 Stochastic Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.6.2 Markov Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.6.3 Stochastic Petri Nets having Exponential Law . . . . . . . . . . . . . 27 2.6.4 Quantitative Properties . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.7 Generalized Stochastic Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . 31 2.7.1 Embedded Markov Chain . . . . . . . . . . . . . . . . . . . . . . . . 33 2.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3 Reconfiguration in Petri Nets 37 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.2 Graph Transformation Systems . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.3 Double-Pushout Approach for Petri Nets . . . . . . . . . . . . . . . . . . . . 39 3.4 Net Rewriting Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.5 Self-Modifying Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 3.6 Reconfigurable Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.7 Improved Net Rewriting Systems . . . . . . . . . . . . . . . . . . . . . . . . 49 3.8 Other Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.9 Trade-off between Expressiveness and Calculability . . . . . . . . . . . . . . 52 3.10 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 II Contributions 55 4 GSPNs with Rewritable Topology 56 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.2 GSPNs with rewritable topology . . . . . . . . . . . . . . . . . . . . . . . . 57 4.2.1 Formal definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 4.3 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 4.4 Illustrative Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 4.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 5 Dynamic Generalized Stochastic Petri Nets 68 5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 5.2 Dynamic GSPNs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.2.1 Formal definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5.3 D-GSPNs transformation towards GSPNs . . . . . . . . . . . . . . . . . . . 71 5.4 Qualitative/Quantitative Analysis of D-GSPNs . . . . . . . . . . . . . . . . 75 5.5 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 5.6 Illustrative example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 6 Reconfigurable Generalized Stochastic Petri Nets 85 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 6.2 Reconfigurable Generalized Stochastic Petri Nets . . . . . . . . . . . . . . . 87 6.2.1 Definition of RecGSPNs . . . . . . . . . . . . . . . . . . . . . . . . . 87 6.2.2 Properties Preserving Nets . . . . . . . . . . . . . . . . . . . . . . . . 92 6.3 Preservation of properties in RecGSPNs . . . . . . . . . . . . . . . . . . . . 93 6.3.1 Preservation of LBR, home state, and deadlock-free . . . . . . . . . . 93 6.3.2 Preservation of linear temporal properties . . . . . . . . . . . . . . . 98 6.4 Quantitative Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 6.5 Using RecGSPNs in Practice . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 6.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 7 Discussion 110 7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 7.2 Qualitative Aspects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 7.3 Quantitative Aspects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 7.3.1 Factor 1: Model size . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 7.3.2 Factor 2: Markov chain spatial complexity . . . . . . . . . . . . . . . 118 7.3.3 Factor 3: Markov chain time complexity . . . . . . . . . . . . . . . . 119 7.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 8 Conclusion 122 Appendices 126 A A Prototype for RecGSPNs 126 A.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 A.2 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 A.2.1 Place . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 A.2.2 Transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 A.2.3 Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 A.2.4 GSPN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 A.2.5 RecGSPN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 A.3 Demonstration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 A.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 List of Publications 137 Bibliography 138 |
En ligne : | http://thesis.univ-biskra.dz/4770/1/Th%C3%A8se.pdf |
Disponibilité (1)
Cote | Support | Localisation | Statut |
---|---|---|---|
TINF/144 | Théses de doctorat | bibliothèque sciences exactes | Consultable |