Terminaison en temps moyen fini de systèmes de règles probabilistes, Termination within a finite mean time of probabilistic rules based systems

Florent Garnier

Description

Sous la direction de Claude Kirchner, Olivier Bournez
Thèse soutenue le 17 septembre 2007: INPL
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.
-Réécriture
-Stratégies
-Terminaison
-Terminaison en temps moyen fini
-Terminaison presque sûre
-Terminaison presque sûre positive
-Choix non-déterministes
-Choix aléatoires
-Réécriture probabiliste
-Méthodes formelles
In this thesis we define a new formalism that allows to model transition systems where transitions can be either probabilistic or non deterministic. We choose to extend the rewriting formalism because it allows to simply express non-deterministic behavior. Latter, we study the termination of such systems and we give some criteria that imply the termination within a finite mean number of rewrite steps. We also study the termination of such systems when the firing of probabilistic rules are controlled by strategies. In this document, we use our techniques to model the \WIFI~ protocol and show that a pool of stations successfully emits all its messages within a finite mean time.
-Rewriting
-Strategies
-Termination
-Bounded mean time termination
-Positive almost sure termination
-Non-determinism
-Random choices
-Probabilistic rewriting
-Formal methods
Source: http://www.theses.fr/2007INPL055N/document

Sujets

• Réécriture
• Stratégies
• Désinence
• Méthode formelle (informatique)

Informations

• Publié par: Thesee
• Nombre de lectures: 74
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

AVERTISSEMENT



Ce document est le fruit d’un long travail approuvé par le jury de
soutenance et mis à disposition de l’ensemble de la communauté
universitaire élargie.
Il est soumis à la propriété intellectuelle de l’auteur au même titre que sa
version papier. Ceci implique une obligation de citation et de
référencement lors de l’utilisation de ce document.
D’autre part, toute contrefaçon, plagiat, reproduction illicite entraîne une
poursuite pénale.

Contact SCD INPL : [e-mail]




LIENS




Code de la propriété intellectuelle. Articles L 122.4
Code de la propriété intellectuelle. Articles L 335.2 – L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm
D´epartement de formation doctorale en informatique
´Ecole doctorale IAEM Lorraine
Terminaison en temps moyen fini de
syst`emes de r`egles probabilistes
`THESE
pr´esent´ee et soutenue publiquement le 17 Septembre 2007
pour l’obtention du
Doctorat de l’Institut National Polytechnique de Lorraine
(sp´ecialit´e informatique)
par
Florent Garnier
Composition du jury
Pr´esident : Jean-Franc¸ois Monin Professeur, Universit´e Joseph Fourier Grenoble I
Rapporteurs : Catuscia Palamidessi Directeur de Recherche, INRIA
Laurent Fribourg Directeur de Recherche, CNRS
Examinateurs : Ye Qiong Song Professeur, Institut National Polytechnique de Lorraine
Claude Kirchner Directeur de Recherche, INRIA
Olivier Bournez Charg´e de Recherche, INRIA
Francis Klay Ing´enieur de Recherche, Orange France T´el´ecom R&D
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Mis en page avec la classe thloria.Remerciements
Je tiens `a remercier en premier lieu mon encadrant Olivier Bournez qui en plus
de m’avoir propos´e ce sujet de th`ese, s’est toujours montr´e disponible pour me venir
en aide et m’apporter ses conseils pr´ecieux. Je remercie ´egalement mon directeur de
th`ese Claude Kirchner pour sa patience, ses grandes qualit´es p´edagogiques ainsi que
sa gentillesse.
Jeremerciechaleureusement lespersonnesquiontaccept´ed’ˆetremembresdemon
jury, en particulier Catuscia Palamidessi et Laurent Fribourg qui ont accept´e d’ˆetre
mes rapporteurs.
Je ne remercierais jamais assez mes amis et coll`egues, Emmanuel, Germain, An-
toine qui ont facilit´e mon arriv´ee `a Nancy et qui m’ont appuy´e moralement et parfois
mat´eriellement durant toute la dur´ee de ma th`ese. Je remercie ´egalement tous le
membres de l’´equipe PROTHEO avec qui j’ai pass´e des moments forts agr´eables
dans le cadre de la recherche et parfois en dehors.
Merci `a mes parents ainsi et `a mes deux fr`eres Sylvain et Ghislain pour leur
appui moral. Je remercie aussi G´erˆome pour m’avoir transmis la passion du cyclisme
`a la montagne. Et merci encore `a tous mes amis que je n’ai pas cit´e ici, mais qui
m´eriteraient de l’ˆetre.
iiiJ’ai rarement eu des
journ´ees aussi longues
que durant ma th`ese.
En effet, `a chaque fois
que j’ai promis quelque chose
pour le lendemain, il m’a
fallu six mois pour le faire.
iiiivTable des mati`eres
Introduction 1
Partie I Notions pr´eliminaires 7
Chapitre 1
Pr´esentation de la r´e´ecriture et de la r´e´ecriture sous strat´egie
1.1 Relations binaires et syst`emes de r´eduction abstraits . . . . . . . 9
1.2 Le principe de l’induction bien fond´ee. . . . . . . . . . . . . . . . 11
1.3 Terminaison des syst`emes abstraits de r´eduction . . . . . . . . . . 12
1.4 Les alg`ebres de termes . . . . . . . . . . . . . . . . . . . . . . . . 14
1.4.1 Substitutions et relation de r´eduction sur les termes . . . . 16
1.4.2 Σ-identit´es et relations de r´eduction associ´ees . . . . . . . 17
1.5 Les syst`emes de r´e´ecriture . . . . . . . . . . . . . . . . . . . . . . 18
1.6 Terminaison des syst`emes de r´e´ecriture . . . . . . . . . . . . . . . 19
1.6.1 Les ordres de r´eduction . . . . . . . . . . . . . . . . . . . 20
1.6.2 M´ethode d’interpr´etation . . . . . . . . . . . . . . . . . . 21
1.6.3 Les ordres de simplification . . . . . . . . . . . . . . . . . 24
1.7 Les strat´egies de r´e´ecriture . . . . . . . . . . . . . . . . . . . . . . 24
1.7.1 Pr´esentation de la notion de strat´egie de r´e´ecriture . . . . 24
Chapitre 2
Les mod`eles de syst`emes probabilistes
2.1 Rappels sur la th´eorie des probabilit´es . . . . . . . . . . . . . . . 27
2.1.1 Ph´enom`enes al´eatoires . . . . . . . . . . . . . . . . . . . . 27
2.1.2 Propri´et´es importantes des probabilit´es . . . . . . . . . . . 29
2.1.3 Esp´erance d’une variable al´eatoire. . . . . . . . . . . . . . 30
vTable des mati`eres
2.1.4 Convergence d’une suite de variables al´eatoires . . . . . . 31
2.1.5 Probabilit´e conditionnelle et esp´erance conditionnelle . . . 33
2.2 Martingales, surmatingales et sous martingales. . . . . . . . . . . 35
2.2.1 Martingales . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2.3 Chaˆınes de Markov . . . . . . . . . . . . . . . . . . . . . . . . . . 37
2.3.1 Chaˆınes de Markov `a espace discret et `a temps discret . . 37
2.3.2 Comportement asymptotique des chaˆınes de Markov . . . 38
2.3.3 R´ecurrence et transience . . . . . . . . . . . . . . . . . . . 40
2.3.4 Convergence en loi des chaˆınes de Markov . . . . . . . . . 42
2.3.5 Exemples d’applications . . . . . . . . . . . . . . . . . . . 42
2.3.6 Tempsmoyend’atteinted’unintervallepourunesur-martingale 43
2.4 Processus de d´ecision Markovien . . . . . . . . . . . . . . . . . . 44
2.4.1 Ex´ecutions . . . . . . . . . . . . . . . . . . . . . . . . . . 45
2.4.2 Ensembles mesurables d’ex´ecutions . . . . . . . . . . . . . 46
2.4.3 Politiques . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
2.5 Probl`emes classiques . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.5.1 Le probl`eme du plus court chemin stochastique (SSP). . . 47
2.5.2 M´ethode de r´esolution de SSP . . . . . . . . . . . . . . . . 48
2.6 V´erification de propri´et´es sur des mod`eles probabilistes . . . . . . 49
2.6.1 M´ethodes formelles . . . . . . . . . . . . . . . . . . . . . . 49
2.6.2 La v´erification dans le cas g´en´eral . . . . . . . . . . . . . . 50
2.6.3 Quelques propri´et´es importantes . . . . . . . . . . . . . . 50
2.6.4 Aperc¸us des m´ethodes de v´erifications de propri´et´es sur les
Processus de d´ecision Markoviens . . . . . . . . . . . . . . 51
2.6.5 Logique probabiliste arborescente . . . . . . . . . . . . . . 52
2.6.6 Model checking de pCTL . . . . . . . . . . . . . . . . . . 53
2.7 Logiciels de model-checking probabiliste . . . . . . . . . . . . . . 53
Partie II R´e´ecriture probabiliste 55
Chapitre 3
Les Syst`emes Abstraits de R´eduction Probabilistes
3.1 Pr´esentation du mod`ele . . . . . . . . . . . . . . . . . . . . . . . 57
3.2 Terminaison des Syst`emes Abstraits de R´eduction Probabiliste . . 61
vi3.3 Prouver la terminaison presque suˆre positive . . . . . . . . . . . . 63
3.4 En r´esum´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
Chapitre 4
Les syst`emes de r´e´ecriture probabilistes
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
4.2 D´efinition du mod`ele . . . . . . . . . . . . . . . . . . . . . . . . . 71
4.3 Terminaison des syst`emes de r´e´ecriture probabilistes . . . . . . . 78
4.4 Crit`eres de terminaison presque suˆre positive . . . . . . . . . . . . 80
4.5 Application `a quelques exemples simples . . . . . . . . . . . . . . 81
4.6 Preuve de terminaison grˆace `a une m´ethode d’interpr´etation poly-
nomiale. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
4.7 R´esum´e du chapitre . . . . . . . . . . . . . . . . . . . . . . . . . 85
Chapitre 5
La terminaison presque suˆre positive sous strat´egies
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
5.2 Strat´egies et terminaison sous strat´egie . . . . . . . . . . . . . . . 87
5.3 Terminaison presque suˆre sous strat´egie. . . . . . . . . . . . . . . 92
5.3.1 G´en´eralisation . . . . . . . . . . . . . . . . . . . . . . . . 93
5.4 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
Partie III Exemple d’application 101
Chapitre 6
Produit synchronis´e d’automates temporis´es
6.1 Les Automates temporis´es `a la Alur et Dill . . . . . . . . . . . . . 103
6.1.1 S´equence temporelle . . . . . . . . . . . . . . . . . . . . . 103
6.1.2 Contraintes et op´erations sur les horloges. . . . . . . . . . 104
6.2 Composition parall`ele. . . . . . . . . . . . . . . . . . . . . . . . . 107
6.2.1 Comportements non d´eterministes. . .