Réseaux d'Automates Stochastiques : Génération de l'espace d'états atteignables et Multiplication vecteur-descripteur pour une sémantique en temps discret

This thesis presents methods and algorithms for the performance evaluation of large state space models described by high-level formalisms. Among the various formalisms we use Stochastic Automata Networks (SAN) formalism. SAN formalism is dedicated to modeling very large systems by the composition of its subsystems (automata), where these automata interact with each other by synchronizing events or functional rates and probabilities. The state space explosion of a model is a common problem when computing the reachable state space of complex systems. In the first part of this thesis, we propose reachable state space generation methods of structured models which use functional rates (general state dependant rates) and probabilities. We use Multi-valued Decision Diagrams (MDD) to store sets of reachable spaces and SAN formalism to describe structured models. MDD is a multilevel data structure which efficiently manipulates a extremely large state spaces. Regarding state-of-the-art generation methods, our methods allow to construct a huge reachable state space of a model which uses functional rates and probabilities. The methods are tested on some models in order to illustrate this contribution. In the second part, we are interested in the solution of a discrete time SAN model whose transition matrix is represented by a tensor formula (called discrete descriptor). For this purpose, we present the Complex Tensor Algebra (XTA) adapted to the parallel composition of the discrete time SANs in order to represent the discrete descriptor and we prove some properties that are the basis for iterative methods for solving the Markov chain associated to the SAN model. Representing a SAN model by a descriptor is a compact way to describe the transitions among global states of the model: we replace a description in a product space by a single tensor product on factors that describe what happens on a single dimension (one automaton of the SAN model). In order to take advantage of this representation, we present a vector-descriptor product method which performs the multiplication of a probability vector and the discrete descriptor. This method aims at exploiting the properties of the complex tensor product so that the multiplication by an operator on the product space is replaced by a series of operations that manipulate data on the size of an automaton (and for all automata).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)