Nous avons dans cette thèse cherché à définir un formalisme simple pour pouvoir modéliser des systèmes où se combinent des phénomènes non-déterministes et des comportements aléatoires. Nous avons choisi d'étendre le formalisme de la réécriture pour lui permettre d'exprimer des phénomènes probabilistes, puis nous avons étudié la terminaison en temps moyen fini de ce modèle. Nous avons également présenté une notion de stratégie pour contrôler l'application des règles de réécriture probabilistes et nous présentons des critères généraux permettant d'identifier des classes de stratégies sous lesquelles les systèmes de réécriture probabilistes terminent en temps moyen fini. Afin de mettre en valeur notre formalisme et les méthodes de preuve de terminaison en temps moyen fini, nous avons modélisé un réseau de stations WIFI et nous montrons que toutes les stations parviennent à émettre leurs messages dans un temps moyen fini.
Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00186774 |
Date | 17 September 2007 |
Creators | Garnier, Florent |
Publisher | Institut National Polytechnique de Lorraine - INPL |
Source Sets | CCSD theses-EN-ligne, France |
Language | French |
Detected Language | French |
Type | PhD thesis |
Page generated in 0.105 seconds