Cette thèse présente des méthodes et des algorithmes pour l'évaluation de performance de systèmes à grand espace d'états décrits par des formalismes de haut niveau. Parmi les différents formalismes de haut niveau normalement utilisés, nous nous sommes intéressés au formalisme des Réseaux d'Automates Stochastiques (SAN). Le formalisme SAN se caractérise par la modélisation de systèmes complexes, où un système est représenté par la composition de sous-systèmes (automates) qui interagissent entre eux. Cette interaction se réalise par l'occurrence des événements synchronisants ou des taux fonctionnels. Lorsqu'on calcule l'espace d'états atteignables de systèmes complexes, le principal problème qui surgit est l'explosion combinatoire de l'espace d'états du modèle. Dans la première partie de cette thèse, nous proposons des méthodes pour la génération de l'espace d'états atteignables de modèles compositionnels qui utilisent des taux fonctionnels. Nous utilisons les Diagrammes de Décision Multi-valués (MDD) pour représenter et manipuler les espaces d'états et le formalisme SAN pour la modélisation de systèmes. Un MDD est une structure de donnée arborescente qui permet de représenter et de manipuler de façon performante un très grand espace d'états. L'avancée par rapport à l'état de l'art a été de proposer de méthodes qui prennent en compte ces fonctions qui expriment des relations entre les composants des modèles. Des études d'exemples sont présentées afin d'illustrer les apports de ces méthodes. Dans la deuxième partie de cette thèse, nous nous sommes intéressés à la résolution d'un modèle SAN à temps discret dont la matrice de transition est représentée par une formule tensorielle (appelée descripteur discret). A cet effet, nous présentons l'Algèbre Tensorielle compleXe (ATX) adaptée à la composition parallèle des SAN à temps discret pour la représentation du descripteur et nous démontrons des propriétés qui servent de base aux méthodes itératives pour la résolution de la chaîne de Markov associée au modèle SAN. Un des avantages de représenter un modèle SAN par un descripteur est la façon compacte par laquelle on peut représenter les transitions du modèle: on remplace une description dans un espace produit par un unique produit tensoriel portant sur des facteurs qui décrivent ce qui se passe sur une seule dimension (une composante du modèle SAN). Afin de profiter de cette représentation, nous présentons une méthode de multiplication d'un vecteur de probabilité par un descripteur discret adaptée à cette algèbre. Cette méthode vise à exploiter des propriétés du produit tensoriel complexe de façon à ce que la multiplication par un opérateur sur l'espace produit soit remplacée par une suite d'opérations qui manipulent des données de la taille d'une composante (et pour toutes les composantes).

Les chaînes de Markov facilitent l'analyse des performances des systèmes dynamiques dans de nombreux domaines d'application. Cette thèse présente le formalisme des réseaux d'automates stochastiques pour représenter des systèmes markoviens. Le principal objectif des travaux consiste à améliorer les méthodes existantes pour évaluer les performances de systèmes informatiques à grand espace d'états. Pour cela, nous introduisons le concept de réseaux d'automates stochastiques avec réplication, ainsi que des techniques pour simplifier le modèle étudié en réduisant la taille de l'espace d'états. Pour rechercher des indices de performances, on propose une amélioration de l'opération de base en tenant compte du fait que dans de nombreux modèles, la proportion d'états accessibles est faible. Les méthodes et algorithmes développés au cours de la thèse ont été implémentés dans le logiciel PEPS 2003. Des exemples numériques sont présentés pour illustrer les apports de cette thèse.