La concurrence joue un rôle important dans les systèmes et la programmation modernes. Il révèle le phénomène selon lequel plusieurs calculs s'exécutent simultanément. Ces exécutions entrelacées entraînent une croissance exponentielle du nombre d'états, ce que l'on appelle le « problème d'explosion d'états ».
Dans cette thèse, nous visons à construire un cadre probabiliste sur les exécutions de systèmes concurrents à des fins de vérification de modèles. Étant donné que tous les états causés par l'entrelacement ne sont pas significatifs, nous adoptons la sémantique de l'ordre partiel, qui ne garde qu'un seul ordre pour chaque ensemble d'actions concurrentes.
La mesure uniforme des exécutions s'inspire des monoïdes de traces définis sur des traces infinies. La théorie des traces a une solide base combinatoire autour du polynôme de Möbius. L'irréductibilité des monoïdes de traces implique la forte connectivité du digraphe des cliques. Par conséquent, une valeur propre dominante existe et détermine le taux de croissance des monoïdes de traces. Ceci complète la théorie probabiliste et prouve que les distributions finies sur les monoïdes de traces convergent faiblement vers la mesure uniforme définie sur les traces infinies.
Cependant, il est plus approprié de prendre en compte à la fois les états et la concurrence dans les systèmes réalistes. Dans notre travail, nous considérons les systèmes concurrents abstraits comme des actions de monoïdes sur un ensemble fini d'états. Ce paramètre englobe les réseaux de Petri à 1-bornés. Nous donnons deux interprétations à la mesure uniforme des exécutions pour les systèmes concurrents. La première interprétation donne la valeur de la measure uniforme sur les cylindres élémentaires du point de vue algébrique sur le monoïde de traces. Cette mesure uniforme est réalisée par une chaîne de Markov d'états-et-cliques. L'autre interprétation s'intéresse au processus des cliques qui apparaissent dans la forme normale d'une exécution infinie tirée suivant la measure uniforme. Dans notre contexte, nous l'avons appelé le digraphe des états-et-cliques. Nous voulons définir la mesure de Parry sur ce graphe.
La structure des systèmes concurrents conserve des propriétés combinatoires similaires aux monoïdes de traces, mais c'est plus compliqué. La difficulté à étendre aux systèmes concurrents est que le théorème de Perron-Frobenius n'est pas applicable. Pour résoudre ce problème, nous avons trouvé la propriété spectrale des systèmes concurrents irréductibles. Cela nous permet de distinguer les principaux composants qui déterminent la racine caractéristique du système. Nous prouvons également l'unicité de cette mesure uniforme. La matrice de transition peut être obtenue soit à partir de la chaîne de Markov d'états-et-cliques avec l'outil algorithmique, soit à partir de la mesure de Parry avec le rayon spectral des composantes dominantes. Cela remplit le but de la génération aléatoire.