Les systèmes informatiques massivement parallèles et distribués posent le problème de la synchronisation complexe et nécessitent de développer des formalismes adaptés pour représenter les attentes dans l’exécution des programmes et les vérifier.
Pour cela, une sémantique par la mise en réseau d’automates probabilistes a été proposée : les réseaux d’automates stochastiques. La méthode part de spécifications formelles et utilise les algèbres de Kronecker pour construire automatiquement le graphe des états des chaînes de Markov. Ce formalisme permet à la fois de déduire le comportement dynamique du système massivement parallèle et d’en calculer les performances d’exécution, même s’il présente des interactions complexes entre les éléments (communications, synchronisations, etc). L’idée de base est que les composants d’un système parallèle ou distribué ne peuvent être très dépendants, sous peine d’inefficacité, une hypothèse le plus souvent vérifiée en pratique. Un tel système peut être vu comme une correction d’un système parallèle « pur » au sens où les composants seraient entièrement indépendants. Une extension d’un produit tensoriel d’opérateurs permet d’exprimer cette correction, prenant des formes extrêmement diverses, pourvu que soient conservées les propriétés algébriques indispensables aux calculs algorithmiques. L’algorithmique numérique pour la résolution des grands systèmes linéaires issus de ces opérateurs produits a été développée.