A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes

Résumé Technique : Une approche basée sur l'invariance par bisimulation pour la séparation des classes de complexité polynomiale

1. Énoncé du problème
Le papier traite du problème ouvert fondamental de savoir si $P = NP$ (et, par extension, $P = PSPACE$). Bien que la théorie de la complexité descriptive ait caractérisé avec succès des classes de complexité comme $NP$, $PSPACE$ et $ExpTime$ en utilisant des formalismes logiques (par exemple, $NP = \exists SO$, $PSPACE = FO + PFP$), la caractérisation de la classe $P$ sur des structures générales et non ordonnées reste insaisissable. Cette difficulté est connue sous le nom de « problème de l'ordre » : les caractérisations logiques de $P$ nécessitent généralement un ordre total explicite sur la structure d'entrée, alors que les problèmes computationnels de $P$ ne possèdent pas intrinsèquement un tel ordre.

Les auteurs étudient si la séparation des fragments invariants par bisimulation de ces classes de complexité ($P/\sim$ vs $NP/\sim$ et $P/\sim$ vs $PSPACE/\sim$) offre une voie viable pour résoudre la question générale $P=NP$. Ils postulent que prouver $P \neq NP$ est équivalent à prouver $P/\sim \neq NP/\sim$, à condition que les classes en question contiennent des problèmes difficiles qui sont invariants par bisimulation.

2. Méthodologie et cadre théorique
Le papier s'appuie sur deux résultats établis de la littérature :

1. Le théorème d'Otto [28] : La classe des requêtes invariantes par bisimulation calculables en temps polynomial ($P/\sim$) est exactement capturée par le $\mu$-calcul polyadique ($L^\omega_\mu$).
2. Réduction du Model Checking [4, 23] : Le problème de model checking pour le $\mu$-calcul polyadique peut être réduit à celui du $\mu$-calcul ordinaire (monadique) ($L_\mu$) via une construction de produit spécifique appelée « graphes de puissance » (power graphs).

Les auteurs combinent ces éléments pour développer un cadre basé sur la régularité relative :

• Réduction aux langages d'arbres : Puisque les graphes et leurs dépliages en arbres sont bisimilaires, la définissabilité dans une logique invariante par bisimulation se réduit à la définissabilité de langages d'arbres.
• Graphes de puissance : Pour un graphe $G$, la $d$-ième puissance $G^d$ est le produit asynchrone de $d$ copies de $G$, enrichi de transitions de « réinitialisation » (reset) qui ramènent un composant à la racine.
• Monofication : Une transformation syntaxique convertit une formule du $\mu$-calcul polyadique (sur $G$) en une formule du $\mu$-calcul ordinaire (sur $G^d$).
• Régularité relative : Un langage d'arbres $L$ est dit régulier relativement à un langage de contexte $R$ s'il existe une formule $L_\mu$ qui distingue correctement les membres de $L$ des non-membres au sein de $R$, tout en faisant des affirmations arbitraires sur les arbres en dehors de $R$.

3. Contributions clés et caractérisations
Le papier établit que la séparation des classes de complexité peut être réduite à la preuve de la non-régularité relative de familles spécifiques de langages d'arbres.

• Équivalence de la séparation (Théorème 1) : Le papier prouve que $P = NP$ si et seulement si $P/\sim = NP/\sim$, et de même pour $PSPACE$. Cela repose sur l'existence de problèmes difficiles invariants par bisimulation, spécifiquement les problèmes de non-universalité des automates finis non-déterministes (NFA) sur un alphabet de un lettre ($1NonUnivNFA$) et deux lettres ($2NonUnivNFA$).
• Caractérisation des graphes de puissance (Section 4) : Les auteurs fournissent deux caractérisations de graphes qui sont bisimilaires à des puissances de $d$ :
  1. Algébrique : Via une bisimulation asynchrone de dimension $d$ qui satisfait la « persistance » (les actions dans un composant n'affectent pas les autres) et la « propriété de réinitialisation » (reset property).
  2. Logique : Via la définissabilité dans le $\mu$-calcul dyadique ($L^2_\mu$) en utilisant des formules spécifiques ($\phi_{per}$, $\phi_{rst}$, $\phi_{pow}$).
• Lemme de pompage relatif (Lemme 13) : Les auteurs adaptent le lemme de pompage standard pour les langages d'arbres réguliers au contexte de la régularité relative. Ils montrent que si un langage $L$ est régulier relativement à $R$, alors pour tout arbre dans $L \cap R$, on peut pomper un segment de chemin de telle sorte que l'arbre résultant reste dans $L$ si il reste dans $R$. Cela rend la preuve de non-régularité nettement plus difficile, car le pompage doit être confiné dans les contraintes structurelles de $R$ (les graphes de puissance).

4. Résultats principaux
Les résultats centraux lient la séparation de la complexité à la non-régularité de langages d'arbres dérivés des problèmes de non-universalité des NFA :

• Théorème 26 : $P \neq NP$ si et seulement si pour tout $d \ge 1$, le langage $1NonUnivNFA_d$ (dépliages en arbres de $d$-puissances de graphes dans $1NonUnivNFA$) est non-régulier relativement à $Power_d$ (le langage des arbres bisimilaires à des $d$-puissances).
• Théorème 30 : $P \neq PSPACE$ si et seulement si pour tout $d \ge 1$, le langage $2NonUnivNFA_d$ est non-régulier relativement à $Power_d$.

Les auteurs construisent ces langages explicitement. Par exemple, $1NonUnivNFA_d$ consiste en des arbres où, pour chaque chemin, la séquence d'actions dans un composant spécifique (en ignorant les réinitialisations) mène finalement à un état sans la couleur acceptante $f$.

5. Signification et affirmations
Le papier affirme modestement offrir une nouvelle ligne d'attaque sur le problème $P=NP$, plutôt qu'une solution. Sa signification réside dans le fait que :

• Atténuation du problème de l'ordre : En déplaçant l'attention vers les requêtes invariantes par bisimulation, l'approche contourne la nécessité d'ordres totaux sur les structures, un obstacle majeur dans les tentatives précédentes de caractérisation de $P$ par la complexité descriptive.
• Expressivité logique : Elle reformule la séparation des classes de complexité comme une question d'inexpressivité logique (spécifiquement, l'incapacité du $\mu$-calcul ordinaire à définir certains langages d'arbres relativement aux graphes de puissance).
• Faisabilité et défis : Les auteurs reconnaissent que bien que la réduction théorique soit établie, la preuve réelle de la non-régularité relative implique une « complexité combinatoire élevée ». Ils notent que les preuves de non-régularité standard sont insuffisantes ; il faut construire des arguments de pompage qui préservent strictement les propriétés structurelles des graphes de puissance.

Le papier conclut que bien que le chemin soit difficile, la caractérisation des graphes de puissance (à la fois algébriquement et logiquement) fournit les outils nécessaires pour tenter de telles preuves. Il souligne également une lacune ouverte dans la littérature : contrairement à d'autres classes de complexité majeures, une caractérisation logique pour $NP/\sim$ est actuellement inconnue, ce qui reste un obstacle pour exploiter pleinement cette approche basée sur la bisimulation.