thesis

Vérification approchée de systèmes probabilistes

Defense date:

Jan. 1, 2010

Edit

Institution:

Paris 11

Disciplines:

Authors:

Abstract EN:

Pas de résumé disponible.

Abstract FR:

Dans cette thèse, nous considérons plusieurs types de Systèmes Probabilistes, qui modélisent le comportement de processus réels dans un environnement randomisé. De tels systèmes peuvent être des Protocoles de Communication, des Algorithmes exécutés sur des ordinateurs, des Systèmes Hybrides. . . Notre but est d'étudier leur évolution. Nous concentrons notre étude sur la comparaison quantitative de Systèmes Probabilistes, et sur l'analyse de leurs propriétés. Notre étude s'appuie sur les questions suivantes d'évaluation et de comparaison : *Étant donné le modèle d'un système réel, peut-on décider efficacement comment le système se comporte ? *Étant donnés deux modèles, comment peut-on les comparer ? Nous essayons de montrer que des algorithmes d'approximation peuvent être utiles pour l'étude de Systèmes Probabilistes. En particulier, nous montrons que des problèmes dont la solution exacte n'est pas calculable efficacement peuvent être résolus approximativement de manière efficace. Dans notre travail, nous utilisons quatres modèles de systèmes probabilistes : le modèle d'Automate Probabiliste Fini, que nous étendons au domaine des mots infinis, le modèle des Processus Markoviens avec Labels, le modèle des Processus de Décision Markoviens (MDP), et un modèle particulier de réseaux de MDPs. Nos résultats principaux concernent des méthodes de comparaison quantitatives entre systèmes, et des méthodes d'approximation de systèmes complexes.