💻 computer science

A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

Cet article présente une axiomatisation diagrammatique correcte et complète de la distance comportementale pour les processus non déterministes en utilisant les diagrammes de Milner et les diagrammes de chaînes, offrant un cadre sans variables et compositionnel qui déplace l'accent de l'équivalence langagière vers la bisimilarité.

Auteurs originaux : Wojciech Różowski, Robin Piedeleu, Alexandra Silva, Fabio Zanasi

Publié 2026-05-01

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Wojciech Różowski, Robin Piedeleu, Alexandra Silva, Fabio Zanasi

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

La Vue d'Ensemble : Mesurer à quel point deux machines sont « différentes »

Imaginez que vous avez deux robots. Dans les anciens jours de l'informatique, nous ne posions qu'une question simple : « Ces deux robots sont-ils exactement les mêmes ? » S'ils l'étaient, tant mieux. Sinon, ils étaient considérés comme complètement différents. C'était une réponse du type « oui ou non ».

Mais dans le monde réel, les choses sont rarement parfaites. Peut-être que le Robot A fait un pas de plus pour tourner à gauche, ou que le Robot B fait une pause d'un instant avant de parler. Ils ne sont pas exactement les mêmes, mais ils ne sont pas non plus totalement différents. Ils sont proches.

Ce papier introduit un moyen de mesurer à quel point deux processus informatiques complexes et imprévisibles sont proches. Au lieu d'un simple interrupteur « même/différent », les auteurs créent une règle qui mesure la « distance » entre eux.

Le Problème : Le Livre dont vous êtes le Héros

Le type spécifique de processus informatique que les auteurs étudient s'appelle un Processus Non Déterministe. Pensez-y comme à un livre « dont vous êtes le héros » où l'histoire peut se diviser dans de nombreuses directions à la fois.

Déterministe : Vous lisez une page, et il n'y a qu'une seule page suivante.
Non Déterministe : Vous lisez une page, et il y a trois pages suivantes possibles, et l'histoire pourrait suivre n'importe laquelle d'entre elles.

Lorsque vous avez deux de ces livres d'histoire à embranchements, les comparer est difficile. Si ils ont tous les deux une « impasse » (un endroit où l'histoire s'arrête) à des moments différents, à quelle distance sont-ils l'un de l'autre ?

La Solution : Les Diagrammes à Cordes (Le Langage des « Organigrammes »)

Pour résoudre cela, les auteurs utilisent un langage spécial appelé Diagrammes à Cordes.

L'Analogie : Imaginez un organigramme ou une carte de circuit imprimé. Vous avez des fils qui entrent, des boîtes au milieu (qui font des choses), et des fils qui sortent.
Pourquoi les utiliser ? Les mathématiques traditionnelles pour ces processus utilisent des variables et du texte complexe (comme l'algèbre). Les diagrammes à cordes sont visuels. Ils ressemblent au flux réel du processus.
- Une boîte est une action (comme « appuyer sur un bouton »).
- Un fil est le flux d'information.
- Les fils qui se croisent signifient échanger des choses.
- Les boucles signifient que le processus se répète lui-même (récursivité).

Les auteurs soutiennent que dessiner ces diagrammes est beaucoup plus facile et plus intuitif que d'écrire des équations complexes, surtout lorsque l'on veut prouver des choses à leur sujet.

L'Innovation Centrale : La « Règle de Distance »

La principale réalisation du papier est de créer un ensemble de règles (axiomes) qui permettent de calculer la distance entre deux diagrammes sans réellement exécuter les ordinateurs.

Pensez-y comme à une recette mathématique pour mesurer la différence :

Le Point Zéro : Si deux diagrammes sont identiques (ou se comportent exactement de la même manière), leur distance est 0.
Le Point Max : S'ils sont complètement sans rapport, la distance est 1.
La Règle de la Moitié : C'est la partie astucieuse. Si deux processus sont différents, mais que vous pouvez les faire ressembler de la même manière en ajoutant une seule « étape » de plus (comme appuyer sur un bouton) aux deux, la distance entre eux est la moitié de la distance de ce qui suit.
- Analogie : Imaginez deux coureurs. S'ils sont actuellement au même endroit, la distance est 0. Si l'un est en avance d'un pas, ils sont « proches ». Si l'un est en avance de deux pas, ils sont « moins proches ». Les mathématiques du papier disent : À chaque fois que vous ajoutez une étape au début du processus, la « distance » entre les deux processus est divisée par deux.

Comment Ils Ont Prouvé Que Cela Fonctionne

Les auteurs n'ont pas simplement deviné ces règles ; ils ont prouvé deux choses critiques :

La Correction (Les Règles ne Mentent Pas) : Si leurs règles disent que deux diagrammes sont séparés par une « distance de 0,25 », ils le sont réellement de 0,25. Les mathématiques tiennent la route.
La Complétude (Les Règles Attrapent Tout) : Si deux diagrammes sont réellement séparés de 0,25, les règles peuvent trouver ce nombre. Il n'y a pas de distances cachées que les règles manqueraient.

Ils ont fait cela en montrant que n'importe quel diagramme complexe peut être décomposé en une « forme normale » standard (comme simplifier une fraction). Une fois simplifié, ils ont pu utiliser une technique mathématique appelée points fixes (répéter un calcul jusqu'à ce qu'il cesse de changer) pour mesurer la distance exacte.

L'Astuce du « Dépliement »

L'une des métaphores clés du papier est le dépliement.
Imaginez une pelote de laine emmêlée (un processus complexe avec des boucles). Les auteurs montrent que vous pouvez « déplier » cette pelote en une longue ligne droite (une structure arborescente).

Une fois dépliée, vous pouvez voir exactement où les deux processus divergent.
S'ils divergent après 2 étapes, la distance est de $1/4$ (car $1/2 \times 1/2$ ).
S'ils divergent après 3 étapes, la distance est de $1/8$ .

Le papier prouve que vous pouvez faire ce « dépliement » et cette mesure entièrement dans le langage visuel des diagrammes à cordes, sans avoir besoin de les traduire d'abord en code texte désordonné.

Résumé

En bref, ce papier offre aux informaticiens une boîte à outils visuelle pour mesurer à quel point deux programmes informatiques imprévisibles sont similaires ou différents.

Ancienne méthode : « Sont-ils les mêmes ? Oui/Non. »
Nouvelle méthode : « À quelle distance sont-ils ? Voici une règle, et voici les règles pour la mesurer en utilisant des images. »

C'est une étape fondamentale. Cela ne construit pas une application spécifique ni ne corrige un bug aujourd'hui, mais cela fournit le fondement mathématique (la règle et les règles) que les ingénieurs futurs pourront utiliser pour construire de meilleurs systèmes, plus fiables, qui gèrent l'incertitude et les erreurs avec grâce.

1. Énoncé du problème

L'article aborde le défi de la comparaison quantitative des comportements des processus non déterministes.

Contexte : L'algèbre des processus traditionnelle et la théorie des automates reposent sur des notions booléennes d'équivalence (par exemple, la bisimulation, l'équivalence langagière). Bien qu'utiles, ces notions sont souvent trop rigides pour les systèmes modernes impliquant des aspects probabilistes ou quantitatifs, où il faut mesurer à quel point deux comportements sont éloignés plutôt que simplement s'ils sont identiques.
Lacune spécifique : Bien que les distances comportementales aient été étudiées pour les systèmes probabilistes et les automates déterministes (DFA), il manque un cadre axiomatique solide et complet pour les processus non déterministes (spécifiquement les graphes de Milner).
Défi : Le non-déterminisme déplace l'accent sémantique de l'équivalence langagière vers la bisimulation. Les syntaxes algébriques existantes (comme les expressions régulières avec des lieurs) peinent à capturer ces comportements de manière compositionnelle sans mécanismes de substitution complexes. De plus, étendre le raisonnement quantitatif aux systèmes non déterministes nécessite de gérer le « relèvement de Hausdorff » des métriques, ce qui est techniquement difficile à axiomatiser.

2. Méthodologie

Les auteurs adoptent une approche diagrammatique utilisant les diagrammes de cordes (le langage graphique des catégories monoïdales symétriques) pour représenter et raisonner sur les comportements des processus.

Modèle sémantique (Graphes) : L'article se concentre sur les graphes de Milner, qui généralisent les automates non déterministes à états finis (NFA) en remplaçant les états d'acceptation par des sorties variables. La sémantique est définie sur une catégorie de comportements réguliers ( $\Omega$ ), équipée d'une structure de pseudométrie.
Définition de la métrique : La distance comportementale est définie via un cadre coalgébrique. Elle utilise :
1. Relèvement des transitions : Relèvement d'une métrique sur les états vers une métrique sur les transitions (arêtes étiquetées et sorties variables).
2. Relèvement de Hausdorff : Relèvement de la métrique vers des ensembles de transitions (pour gérer le non-déterminisme).
3. Caractérisation par point fixe : La distance est le plus petit point fixe d'un opérateur monotone sur le treillis des pseudométries. Elle est concrètement caractérisée par la stratification de la bisimulation (logique de Hennessy-Milner), où la distance est $2^{-n}$ si deux processus sont bisimilaires jusqu'à la profondeur $n$ mais pas $n+1$ .
Syntaxe (Diagrammes de cordes) : Les auteurs utilisent les diagrammes de cordes comme syntaxe. Ce choix offre :
- Représentation sans variables : La récursion est gérée via des boucles de rétroaction (traces) plutôt que par des lieurs explicites et une substitution.
- Sémantique compositionnelle : Les diagrammes correspondent naturellement à la structure catégorielle des comportements réguliers.
- Construction Int : Pour gérer le flux de données bidirectionnel (entrées/sorties) et les boucles de rétroaction, les auteurs utilisent la construction Int pour transformer la catégorie monoïdale tracée des comportements en une catégorie compacte fermée, permettant des courbures locales de fils.

3. Contributions clés

A. Un système d'inférence quantitatif

L'article propose un ensemble de règles d'équations quantitatives (système d'inférence) pour dériver des bornes sur les distances comportementales ( $s \equiv_\epsilon t$ ).

Règles métriques standards : Réflexivité, Symétrie, Inégalité triangulaire, et une règle de « Continuité » (si $s \equiv_{\epsilon'} t$ pour tout $\epsilon' > \epsilon$ , alors $s \equiv_\epsilon t$ ).
Règles compositionnelles : Règles pour la composition séquentielle et la composition parallèle (tenseur) qui préservent la non-expansion.
Règles spécifiques au domaine :
- (Pref) : Le préfixage par une action $a$ divise la distance par deux ( $d(a.s, a.t) = \frac{1}{2}d(s, t)$ ). Cela capture l'intuition que distinguer deux processus nécessite une étape supplémentaire.
- (Codel) : Un diagramme sans état initial (blocage) est à une distance de 0 du graphe vide.
- Axiomes équationnels : Un ensemble d'axiomes (A1-B11) capturant la bisimulation forte (distance 0), incluant des lois pour le choix non déterministe, la fusion de variables et la récursion (axiomes de la théorie de Conway).

B. Adéquation et complétude

La réalisation technique centrale est la preuve que le système d'inférence est à la fois adéquat et complet.

Adéquation (Théorème 16) : Toute équation quantitative dérivable $f \equiv_\epsilon g$ est valide (c'est-à-dire que la distance comportementale réelle $d(\llbracket f \rrbracket, \llbracket g \rrbracket) \leq \epsilon$ ).
Complétude (Théorème 31) : Si la distance comportementale entre deux diagrammes est $\leq \epsilon$ $\leq ϵ$ , alors l'équation $f \equiv_\epsilon g$ $f \equiv_{ϵ} g$ est dérivable en utilisant les règles proposées.
- Stratégie de preuve : La preuve de complétude implique la transformation de diagrammes arbitraires en une forme normale (représentant un prégraphe fini). Elle simule ensuite le calcul du relèvement de Hausdorff et l'itération de point fixe (théorème de Kleene) de manière syntaxique en utilisant les règles d'inférence. La règle de Continuité (Cont) est cruciale pour combler l'écart entre l'approximation syntaxique et la limite exacte.

C. Structure catégorielle

L'article établit que la catégorie des comportements réguliers ( $\text{RegBeh}$ ) est une Théorie de Conway (un type spécifique de catégorie monoïdale tracée) et que la structure de pseudométrie en fait une catégorie enrichie sur la catégorie des espaces de pseudométrie ( $\text{PMet}$ ). Cela garantit que toutes les opérations catégorielles (composition, tenseur, trace/dagger) sont non expansives.

4. Résultats

Caractérisation formelle : L'article fournit la première axiomatisation complète de la distance comportementale pour les graphes de Milner (processus non déterministes avec sorties).
Simulation syntaxique des métriques : Les auteurs démontrent que des calculs métriques complexes, tels que la distance de Hausdorff entre des ensembles de transitions, peuvent être simulés purement par manipulation syntaxique des diagrammes de cordes.
Exemple d'application : L'article inclut une dérivation détaillée montrant comment prouver que deux graphes spécifiques (l'un avec un blocage après deux 'a', l'autre avec une suite infinie de 'a') sont à une distance exactement égale à $1/4$ . Cela est obtenu en déroulant la récursion et en appliquant la règle (Pref) deux fois.

5. Importance

Pont entre théorie et pratique : En passant de l'équivalence booléenne à la distance quantitative, ce travail permet une analyse plus nuancée des systèmes où « presque équivalent » est un concept significatif (par exemple, dans la vérification de systèmes approximatifs ou probabilistes).
Cadre diagrammatique unifié : L'utilisation des diagrammes de cordes évite la complexité du liage de variables et de la substitution trouvée dans les algèbres de processus traditionnelles. Cela suggère une voie vers un cadre unifié pour axiomatiser les équivalences et les distances à travers divers modèles de calcul (déterministes, non déterministes, probabilistes, pondérés).
Fondement pour les travaux futurs : L'article pose les bases pour étendre ces résultats aux systèmes de transitions pondérés et aux automates probabilistes, où les distances comportementales sont encore plus critiques. Il suggère également des applications potentielles dans le raisonnement sur les algorithmes de décompilation et l'Algèbre de Kleene Gardée avec Tests (GKAT).
Avancement théorique : Il relie les métriques comportementales coalgébriques, la logique équationnelle quantitative et l'algèbre diagrammatique, montrant comment ces domaines peuvent être intégrés pour résoudre des problèmes de longue date en théorie des processus.

En résumé, cet article traduit avec succès la définition abstraite et coalgébrique de la distance comportementale pour les processus non déterministes en un calcul concret, diagrammatique et entièrement axiomatisé, prouvant que le raisonnement quantitatif sur le comportement des processus peut être effectué entièrement par manipulation syntaxique des diagrammes de cordes.