Cette thèse présente des méthodes et des algorithmes pour l'évaluation de performance de modèles avec très grands espace d'états décrits par des formalismes de haut niveau. Parmi les différents formalismes couramment utilisés, on se place dans le cadre des Réseaux d'Automates Stochastiques (SAN). Le formalisme SAN se caractérise par la représentation de très grands systèmes par la composition de sous-systèmes (automates), où ces automates interagissent entre eux par des événements synchronisants ou des taux et des probabilités fonctionnels. <br /><br />La première partie de cette thèse s'intéresse au calcul des indices de performances transitoires pour des grands modèles. Lorsqu'on calcule des indices de performances transitoires, tel que la disponibilité ponctuelle, la méthode d'uniformisation est la plus souvent utilisée. Cependant le nombre d'itérations vecteur-matrice peut être très grand ce qui devient critique pour de très grands modèles. Des méthodes de détection du régime stationnaire peuvent réduire le coût de calcul en arrêtant les itérations lorsque le régime stationnaire est atteint. Dans cette thèse, nous proposons une adaptation et une comparaison de différentes méthodes de détection du régime stationnaire lorsque la matrice est stockée sous un format tensoriel. Les méthodes sont comparées selon deux critères : nombre d'itérations et précision des résultats.<br /><br />Dans la deuxième partie, nous présentons le formalisme SAN à temps discret. La définition formelle du formalisme SAN présentée dans cette thèse nous permet de définir la sémantique des modèles en temps discret que nous souhaitons exploiter. Nous définissons une nouvelle algèbre tensorielle (appelée Algèbre Tensorielle compleXe - ATX) capable d'exprimer cette sémantique. Pour cela, trois opérateurs sont définis afin de décrire différents comportement d'un système, tels que la simultanéité, la concurrence et le choix. Enfin, le principal apport de cette thèse réside dans la définition d'une formule tensorielle (appelée Descripteur discret) qui utilise cette nouvelle algèbre pour représenter un modèle SAN à temps discret de façon compacte. Nous montrons que ce descripteur discret permet aisément de générer la chaîne de Markov représentée par le modèle SAN.

Cette thèse propose des techniques numériques visant à optimiser les méthodes itératives d'évaluation de performances de modèles Markoviens. Ces techniques s'appliquent à des modèles où la matrice de transition de la chaîne de Markov associée est stockée sous un format tensoriel. Particulièrement, le formalisme des réseaux d'automates stochastiques est employé pour la description des modèles. L'évaluation de performances cherchée est la détermination de l'état stationnaire de la chaîne de Markov (\emph(résolution)). De ce fait, les propriétés de l'algèbre tensorielle généralisée sont proposées et démontrées de façon à établir la base nécessaire aux algorithmes de résolution introduits. Le principal apport de cette thèse réside dans l'efficacité des ces algorithmes, qui est obtenue avec l'accélération des méthodes itératives. Ceci est fait à deux niveaux: la réduction du coût de chaque itération; et la réduction du nombre d'itérations nécessaire à la convergence. La multiplication d'un vecteur par une matrice sous format tensoriel (produit vecteur-descripteur) est l'opération de base des itérations. L'efficacité de cette opération est le premier objectif à atteindre. Le deuxième objectif est l'implémentation des méthodes de la puissance, d'Arnoldi et GMRES dans ses versions standards et pré-conditionnées de façon a minimiser le nombre d'itérations sans trop augmenter le coût de chaque itération. La totalité des concepts introduits est alors utilisée dans le logiciel PEPS 2.0. Plusieurs exemples pratiques de modèles en réseaux d'automates stochastiques ont été mesurés sur PEPS 2.0 pour illustrer les résultats de cette thèse.