Résumé Technique : La réachabilité pour les 3-VASS est dans EXPSPACE

Énoncé du Problème

Le papier traite du problème de réachabilité pour les systèmes d'addition de vecteurs à 3 dimensions avec états (3-VASS). Un VASS est un automate à états finis équipé d'un nombre fixe de compteurs (dimensions) détenant des entiers non négatifs. Le problème de réachabilité consiste à déterminer si une configuration cible (état et valeurs des compteurs) est atteignable depuis une configuration source via une séquence de transitions valides.

Alors que le problème général de réachabilité des VASS (où la dimension fait partie de l'entrée) a été prouvé ACKERMANN-complet en 2021, la complexité exacte pour des dimensions fixes $d > 2$ demeure une question ouverte centrale. Spécifiquement pour les 3-VASS :

• Borne Inférieure : Le problème est connu pour être PSPACE-dur, hérité du cas en 2 dimensions.
• Ancienne Borne Supérieure : Jusqu'à ce travail, la meilleure borne supérieure connue était 2-EXPSPACE (espace double exponentiel), établie par Czerwiński et al. (ICALP 2025). Avant cela, les algorithmes étaient non-élémentaires.

L'objectif du papier est de combler l'écart entre la borne inférieure PSPACE et la borne supérieure 2-EXPSPACE en prouvant que la réachabilité des 3-VASS appartient à EXPSPACE (espace simple exponentiel).

Méthodologie et Stratégie de Preuve

Le cœur de la preuve consiste à établir une borne de longueur doublement exponentielle sur les parcours les plus courts entre deux configurations dans un 3-VASS. Si la longueur du parcours le plus court est bornée par $N^{2^{poly(k)}}$ (où $N$ est la taille de l'entrée et $k$ est le nombre de composantes fortement connexes), alors la réachabilité peut être décidée en EXPSPACE en devinant de manière non déterministe un chemin de cette longueur.

Les auteurs emploient une stratégie de réduction hiérarchique et une technique de preuve de séparation des préoccupations, affinant la classe des instances de 3-VASS en une séquence de sous-classes. Cette approche évite l'induction « imbriquée » qui a conduit à des bornes triple exponentielles dans les travaux précédents.

1. Classification Hiérarchique des VASS

Le papier définit une hiérarchie de sous-classes pour les 3-VASS, ordonnées par généralité croissante :
$$\text{DiagVASS}_3 \subsetneq \text{Semi-diagVASS}_3 \subsetneq \text{PumpVASS}_3 \subsetneq \text{Semi-pumpVASS}_3 \subsetneq \text{SeqVASS}_3$$

• DiagVASS : Instances où des cycles « diagonaux » tant vers l'avant que vers l'arrière existent (cycles capables de pomper tous les compteurs positivement).
• PumpVASS : Instances où des cycles « pompables » tant vers l'avant que vers l'arrière existent (cycles capables de pomper au moins un compteur positivement).
• SeqVASS : VASS séquentiels généraux, où le parcours traverse une séquence de composantes fortement connexes (SCC) connectées par des ponts.

La preuve procède en établissant la borne de longueur pour la classe la plus restrictive (DiagVASS) puis en utilisant des auto-réductions contrôlées en longueur pour transférer ces bornes aux classes plus générales.

2. Composantes Techniques Clés

A. Représentation Efficace des Ensembles de Réachabilité (Géométriquement 2D VASS)

Un outil crucial est l'analyse des VASS géométriquement 2-dimensionnels, où tous les parcours restent entre deux plans 2D parallèles. Les auteurs étendent les résultats de Czerwiński et al. pour montrer que l'ensemble de réachabilité de tels systèmes, même en partant d'un « ensemble hybride » (un vecteur de base plus un ensemble périodique restreint), peut être représenté comme une union finie d'ensembles hybrides avec des descriptions de taille polynomiale. Cela permet une manipulation efficace des ensembles de réachabilité sans induire d'explosion exponentielle de la taille de la représentation.

B. Gestion des Instances Diagonales Non-Larges

Pour DiagVASS, les auteurs distinguent les instances « larges » et « non-larges ».

• Large : Le cône séquentiel du système contient tous les vecteurs positifs. Celles-ci sont traitées par réduction aux résultats connus.
• Non-Large : Les auteurs prouvent que dans les instances diagonales non-larges, les cônes séquentiels du préfixe et du suffixe du parcours sont séparés par un hyperplan. Cette séparation géométrique implique que les valeurs des compteurs dans les composantes intermédiaires sont contraintes à l'intérieur d'une paire de plans 2D parallèles. Par conséquent, le problème peut être transformé en une séquence d'instances de VASS géométriquement 2-dimensionnels, permettant l'application des techniques de représentation efficace mentionnées ci-dessus pour dériver une borne doublement exponentielle.

C. Auto-Réduction Contrôlée en Longueur

Pour passer de PumpVASS et SeqVASS à DiagVASS, le papier introduit une auto-réduction contrôlée en longueur.

• Extraction de la Diagonalité Conjointe : Pour une instance pompable, les auteurs montrent qu'on peut extraire un préfixe « conjointement diagonal » (une séquence de cycles qui pompent collectivement tous les compteurs).
• Réduction : Ce préfixe est utilisé pour construire une nouvelle instance de VASS avec moins de composantes (ou une structure plus simple) qui est diagonale. La taille de cette nouvelle instance est contrôlée par la fonction de longueur de la classe cible.
• Éviter l'Imbrication : Contrairement aux approches précédentes qui imbricaient la fonction de borne de longueur (ex: $h_k(h_{k-1}(\dots))$), cette méthode garantit que la borne de longueur n'apparaît qu'une seule fois sur le membre de droite de la récurrence. Ce changement structurel est ce qui réduit la complexité de 2-EXPSPACE à EXPSPACE.

Contributions Principales et Résultats

1. Théorème Principal : Le problème de réachabilité des 3-VASS est dans EXPSPACE.

   • Ceci est vrai pour les encodages unaires et binaires de l'entrée.
   • La preuve repose sur la démonstration que pour tout 3-VASS à $k$ composantes, la longueur du parcours le plus court est bornée par $size(V, s, t)^{2^{poly(k)}}$.

2. Paysage de Complexité Affiné : Le papier fournit une analyse détaillée de la complexité des sous-classes de 3-VASS :

   • DiagVASS3 : Prouvé être dans EXPSPACE (améliorant la borne précédente de 2-EXPSPACE).
   • PumpVASS3 : Prouvé pour admettre des parcours doublement exponentiels courts.
   • SeqVASS3 : Prouvé pour admettre des parcours doublement exponentiels courts via auto-réduction à PumpVASS.

3. Avancement Méthodologique : Le papier introduit une analyse de pompabilité hiérarchique et une stratégie de séparation des préoccupations. En décomposant le problème en sous-problèmes géométriquement 2D et en utilisant des auto-réductions qui respectent la hiérarchie des composantes, les auteurs éliminent la croissance triple exponentielle inhérente aux preuves inductives précédentes.

Signification et Revendications

Le papier affirme faire progresser significativement la compréhension du problème de réachabilité des 3-VASS, qui est un défi de longue date en informatique théorique.

• Resserrement de la Borne : Le résultat réduit l'écart de complexité pour les 3-VASS d'une borne supérieure doublement exponentielle à une borne simple exponentielle. Bien que la borne inférieure reste PSPACE, les auteurs notent que la réduction d'un 3-VASS général vers un 3-VASS pompable ne peut probablement pas se faire en espace polynomial, suggérant que les 3-VASS pourraient effectivement être EXPSPACE-durs.
• Fondation pour des Travaux Futurs : Le papier précise explicitement que déterminer la complexité exacte (PSPACE vs EXPSPACE) reste ouvert. Il souligne qu'une preuve de dureté EXPSPACE définitive nécessiterait un exemple de 3-VASS admettant des parcours les plus courts doublement exponentiels, ce qui est actuellement inconnu.
• Implications pour les Dimensions Supérieures : Les auteurs suggèrent que leur perspective sur la limitation des parcours les plus courts pourrait être fructueuse pour l'analyse des VASS en dimensions $d \ge 4$, où les bornes supérieures actuelles sont loin d'être élémentaires.

En résumé, le papier fournit une preuve rigoureuse que la réachabilité des 3-VASS est soluble en espace exponentiel, en utilisant une combinaison novatrice d'arguments de séparation géométrique, de représentations d'ensembles de réachabilité efficaces et d'un cadre d'auto-réduction raffiné qui évite l'explosion de complexité des méthodes précédentes.