Abstract FR:

Dans cette these, nous etendons la definition du graphe symbolique aux reseaux colores generaux, et nous presentons un ensemble de proprietes qui peuvent etre etudiees directement sur ce graphe. Cependant, la construction du graphe symbolique ne peut etre effectuee de maniere automatique s'il n'existe aucune contrainte dans la maniere de decrire un modele. En effet, cette construction repose sur la connaissance d'un ensemble de symetries de comportement pour differents objets composant le systeme etudie. Nous proposons les reseaux colores bien formes, une classe de reseaux colores pour laquelle les symetries sont determinees de maniere systematique, ce qui permet une construction entierement automatique du graphe symbolique. Ceci est d'autant plus interesant que nous prouvons que les reseaux bien formes ont la meme puissance d'expression que les reseaux colores. A partir des reseaux bien formes, nous derivons un modele stochastique qui peut etre analyse efficacement au moyen de l'agregation markovienne. En effet, si la temporisation introduite dans le modele respecte les symetries de comportement qui existent pour le modele qualitatif, les marquages symboliques constituent des classes d'etats au sens markovien. En prouvant que tous les etats d'une classe ont la meme probabilite, nous montrons que cette agregation s'effectue sans perte d'information. Nous illustrons sur des exemples d'architectures multiprocesseurs le gain de complexite enorme obtenu avec cette methode