Vous êtes ici : UVSQ RechercheDoctoratSoutenances de thèse

Model checkting stochastique par les méthodes de comparaison stochastique

le 9 décembre 2008

Le mardi 9 décembre 2008 à 10h00

à l'Université de Versailles Saint-Quentin-en-Yvelines UFR des Sciences Bâtiment Descartes - Salle 301 45 avenue des Etas-Unis78035 Versailles cedex

Par Madame Sana YOUNES Discipline : Informatique Laboratoire : PRISM

Nous proposons dans cette thèse une nouvelle méthode de vérification des chaînes de Markov. La vérification de ces modèles est effectuée à partir des distributions transitoires ou stationnaires de la chaîne de Markov considérée. Nous utilisons les méthodes de comparaison stochastique pour obtenir des mesures bornantes afin de vérifier la chaîne considérée. Ces mesures sont obtenues par la construction d'une chaîne bornante à la chaîne initiale qui est en générale de très grande taille. Les chaînes bornantes construites doivent être plus simples à analyser permettant de construire des bornes pour les modèles dont la résolution numérique est difficile voire impossible. Nous avons exploré certains schémas pour construire des chaînes bornantes comme la lumpabilité et la classe C. Nous avons développé également d'autres schémas de construction de chaînes bornantes sur les chaînes de Markov censurées. Il est évident que les mesures bornantes ne permettent pas toujours de conclure. Dans ce cas il faut affiner le modèle bornant si le schéma de borne le permet. Nous avons montré que les méthodes de bornes que nous proposons sont pertinentes pour la vérification de chaînes de Markov et permettent de réduire remarquablement le temps de vérification.

 

Abstract :

We propose in this work a new method to verify Markov chains. The verification is performed by transient or steady-state distributions of the considered chain. We use stochastic comparison techniques to obtain bounding measures in order to verify the considered chain. These measures are obtained by the construction of a bounding chain to the initial chain that can be very large. Bounding models have to be easier to analyze that let to consider models for which numerical analysis are difficult or impossible. We have explored some schemes of construction of bounding chains as lumpability and class C matrices. We have also developed other methods of construction of bounding chains for censored Markov chains. Clearly, bounding measures can not always lead to a conclusion. In this case, the bounding model must be refined if it is possible. We have showed that bounding techniques that we propose are appropriate for the verification of Markov chains and they may reduce drastically the verification time.

Informations complémentaires

Kamel BARKAOUI, Professeur des Universités, au Conservatoire National des Arts et Métiers, Paris - Rapporteur Serge HADDAD, Professeur des Universités, à l'Ecole Nationale Supérieure de Cachan - Rapporteur Hind CASTEL, Maître de Conférences, à l'Institut National des Télécommunications - Examinateur Riah ROBBANA, Professeur des Universités, à l'Ecole Polytechnique de Tunisie - Examinateur Susanna DONATELLI, Professeur des Universités, à l'Université de Torino, Italie - Examinateur Jean-Michel FOURNEAU, Professeur des Universités à l'Université de Versailles Saint-Quentin-en-Yvelines - Examinateur Nihal PEKERGIN, Professeur des Universités à l'Université de Versailles Saint-Quentin-en-Yvelines - Directrice de Thèse