Cet ouvrage et des milliers d'autres font partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour les lire en ligne
En savoir plus

Partagez cette publication


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 : scdinpl@inpl-nancy.fr




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. . . . . . . . . . . . . . 113
6.3 Produit synchronis´e d’automates avec variables . . . . . . . . . . 117
6.3.1 Automates temporis´es avec variables . . . . . . . . . . . . 118
6.3.2 Produit synchronis´e via une ressource de synchronisation . 120
vii