Désambiguïsabilité et Minimisation des Registres des Modèles Min-Plus

Informations Fondamentales

• ID de l'article : 2512.09484
• Titre : Désambiguïsabilité et Minimisation des Registres des Modèles Min-Plus
• Auteurs : Shaull Almagor, Guy Arbel, Sarai Sheinvald (Technion – Institut Israélien de Technologie)
• Classification : cs.FL (Théorie des Langages Formels et Automates)
• Date de publication : Décembre 2025 (prépublication arXiv)
• Lien de l'article : https://arxiv.org/abs/2512.09484

Résumé

Cet article étudie le problème de désambiguïsabilité des automates finis pondérés (WFAs) min-plus (tropicaux), ainsi que le problème de minimisation des compteurs des automates à registres de coûts (CRAs) tropicaux, qui sont équivalents en pouvoir expressif aux WFAs. Ces deux problèmes interrogent la possibilité de réduire le « degré de non-déterminisme » dans le modèle. Les auteurs démontrent que le problème de désambiguïsabilité des WFAs est décidable, résolvant ainsi une question ouverte de longue date. La méthode de preuve repose sur une réduction au problème de déterminisation des WFAs (récemment prouvé décidable). Concernant les résultats négatifs, les auteurs démontrent que le problème de minimisation des compteurs des CRAs est indécidable, même pour un nombre fixe de registres (spécifiquement sept registres).

Contexte de Recherche et Motivation

1. Problèmes de Recherche

Cet article étudie deux problèmes fondamentaux :

• Problème de désambiguïsabilité : Étant donné un automate pondéré A, existe-t-il un automate non ambigu équivalent ?
• Problème de minimisation des registres : Étant donné un automate à registres de coûts k-registres, existe-t-il un automate équivalent à (k-1)-registres ?

2. Importance du Problème

• Signification théorique : Les automates finis pondérés constituent un modèle important de calcul quantitatif, définissant des fonctions des mots vers les valeurs. Les WFAs sur le semi-anneau tropical (Z∪{∞}, min, +) ont des applications larges dans la modélisation de systèmes, permettant de raisonner sur les moyens optimaux d'utiliser les ressources (comme la consommation d'énergie).
• Valeur pratique : L'existence du non-déterminisme rend le raisonnement sur les WFAs plus difficile. Par exemple, le problème d'équivalence des WFAs tropicaux est indécidable pour les automates non-déterministes, mais décidable pour les automates déterministes.
• Statut historique : Les WFAs tropicaux ont joué un rôle clé dans la résolution de la conjecture de la hauteur d'étoile.

3. Limitations des Approches Existantes

• Le problème de déterminisation n'a été prouvé décidable que récemment (2025)
• Pour les automates tropicaux avec ambiguïté polynomiale, le problème de désambiguïsabilité a été prouvé décidable, mais le cas général reste ouvert
• Le problème de désambiguïsabilité sur le corps des nombres rationnels est décidable, mais la situation sur le semi-anneau tropical n'a pas été résolue
• Dans la plupart des modèles, les problèmes de déterminisation et de désambiguïsabilité sont généralement résolus simultanément, mais les WFAs tropicaux constituent un cas particulier

4. Motivation de la Recherche

• Les WFAs non ambigus sont strictement plus expressifs que les WFAs déterministes, tout en conservant certaines bonnes propriétés de fermeture et algorithmiques
• Le non-déterminisme peut être mesuré de plusieurs façons : l'ambiguïté et la largeur fournissent des perspectives différentes
• Le nombre de registres correspond à la largeur du WFA, fournissant une autre méthode pour mesurer le non-déterminisme

Contributions Principales

Les contributions principales de cet article incluent :

1. Résolution d'une question ouverte de longue date : Preuve que le problème de désambiguïsabilité des WFAs tropicaux est décidable, ce qui était une question non résolue depuis longtemps.
2. Méthode de réduction innovante : Résolution du problème de désambiguïsabilité par réduction au problème de déterminisation. Ceci est en quelque sorte contre-intuitif, car généralement on résout d'abord la désambiguïsabilité, puis la déterminisation.
3. Nouvelle caractérisation des lacunes : Introduction du concept de témoin de lacune de type U (U-type gap witness), fournissant une caractérisation complète de la désambiguïsabilité.
4. Résultats négatifs : Preuve que le problème de minimisation des registres des CRAs est indécidable, même avec un nombre fixe de registres égal à sept.
5. Résultats d'équivalence : Raffinement des relations d'équivalence entre les k-CRAs et les WFAs de largeur k.

Détails de la Méthode

Définition des Tâches

Problème de désambiguïsabilité (Problème 2) :

• Entrée : Un WFA A
• Sortie : Déterminer s'il existe un WFA non ambigu équivalent
• Définition : Un WFA A est non ambigu si et seulement si chaque mot possède au plus une exécution acceptante

Problème de minimisation des registres :

• Entrée : Un CRA à k-registres
• Sortie : Déterminer s'il existe un CRA équivalent à (k-1)-registres

Architecture de la Méthode Principale

1. Caractérisation des Lacunes de Type U (Section 3)

Définition 5 (Témoin de Lacune B de Type U) : Pour B ∈ ℕ, un témoin de lacune B de type U est constitué de paires de mots x, y ∈ Σ* et d'états p₁, q₁ ∈ Q, p₂, q₂ ∈ F, avec des exécutions :

• ρ: q₀ →^x p₁ →^y p₂
• χ: q₀ →^x q₁ →^y q₂

satisfaisant :

1. mwt(q₀ →^x Q) = wt(χx) (χ est l'exécution de poids minimal sur le préfixe x)
2. mwt(q₀ →^xy F) = wt(ρ) (ρ est l'exécution acceptante de poids minimal sur xy)
3. wt(ρx) - wt(χx) > B (après avoir lu x, ρ est supérieur d'au moins B à l'exécution minimale)

Théorème 6 : Un WFA A peut être désambiguïsé si et seulement s'il existe B ∈ ℕ tel que la lacune de A soit bornée par B.

2. Construction de la Désambiguïsabilité (Section 3.2)

Étant donné un WFA A dont la lacune est bornée par B, construction d'un WFA non ambigu équivalent U :

Espace d'états : S = Q × B-Win, où B-Win = {-∞, -B, ..., B, ∞}^Q

Idée clé :

• Suivi de l'exécution minimale canonique
• Utilisation d'une fenêtre B pour enregistrer les décalages de poids de chaque état par rapport à l'état actuellement suivi
• Sélection d'une exécution minimale unique et canonique parmi plusieurs exécutions minimales via un ordre de priorité (ordre linéaire ⪯)

Définition de la relation de transition Λ : Pour un état (q, f_q) et une lettre σ, considérant la transition (q, σ, c, p) :

1. Calcul de la fonction intermédiaire g(p) = min{f_q(r) + mwt(r →^σ p) - c | r ∈ Q}
2. Vérification de cohérence :
   • Si g(p) < 0, ne pas ajouter la transition (il existe une exécution de poids plus faible)
   • S'il existe r ≠ q et q ⪯ r tel que f_q(r) + mwt(r →^σ p) - c = g(p), ne pas ajouter la transition (il existe une exécution de priorité plus élevée)
3. Troncature de g à -B, B pour obtenir f_p

États acceptants : G = {(q, f_q) | q ∈ F ∧ ∀p ∈ F, (f_q(p) > 0 ∨ (f_q(p) = 0 ∧ p ⪯ q))}

3. Réduction à la Déterminisation (Section 4)

Idée centrale : Construction d'un WFA B tel que A peut être désambiguïsé si et seulement si B peut être déterminisé.

Détails de construction :

• États : S = Q × Com, où Com = {⊥, ↛, →}^Q (fonctions d'engagement)
• Alphabet : Γ = Σ × Updt, où Updt = {⊥, ↛, →}^(Q×Q) (fonctions de mise à jour)
• Sémantique d'engagement :
  • →: l'état est accessible et sur une exécution acceptante
  • ↛: l'état est accessible mais pas sur une exécution acceptante
  • ⊥: l'état n'est pas accessible

Conditions de cohérence :

1. Cohérence Δ : la projection sur A est une transition valide
2. Cohérence de mise à jour : α reflète correctement les transitions disponibles sur σ
3. Cohérence des arêtes sortantes : f(r) = → si et seulement s'il existe r' tel que r → r' ∈ α
4. Cohérence des arêtes entrantes : g(r') = → si et seulement s'il existe r tel que r → r' ∈ α

Lemmes clés :

• Lemme 15 : S'il existe un témoin de lacune B de type U dans A, alors il existe un témoin de lacune B de type D dans B
• Lemme 16 : S'il existe un témoin de lacune B de type D dans B, alors il existe un témoin de lacune B de type U dans A

Points d'Innovation Technique

1. Innovation dans la caractérisation des lacunes :
   • Introduction des témoins de lacune de type U, distincts des témoins de type D connus
   • Le type U exige que l'« exécution basse » puisse également continuer vers un état acceptant, ce qui est la différence clé avec le type D
2. Construction d'exécutions canoniques :
   • Filtrage progressif des exécutions minimales de l'arrière vers l'avant via un ordre linéaire ⪯
   • Garantie d'unicité tout en maintenant la propriété de poids minimal
3. Conception astucieuse de la réduction :
   • Utilisation de mécanismes d'engagement et de mise à jour pour forcer les témoins de type D de B à être aussi des témoins de type U de A
   • Vérification de cohérence pour assurer l'extensibilité des exécutions basses
4. Équivalence entre largeur et registres :
   • Établissement précis de conversions bidirectionnelles entre k-CRAs et WFAs de largeur k
   • Dans la direction WFA→CRA, l'innovation clé est la réutilisation des registres plutôt que l'allocation de registres indépendants pour chaque état

Configuration Expérimentale

Cet article est un travail purement théorique et ne contient pas d'évaluation expérimentale. Tous les résultats sont obtenus par des preuves mathématiques rigoureuses.

Structure de la Preuve

1. Décidabilité de la désambiguïsabilité (Sections 3-4) :
   • Section 3 : Preuve de la nécessité et suffisance de la caractérisation des lacunes
   • Section 4 : Réduction au problème de déterminisation
2. Indécidabilité de la minimisation des registres (Section 5) :
   • Réduction du problème d'arrêt à zéro des machines à deux compteurs
   • Utilisation de la construction du théorème 22 (de 2)
   • Construction d'un WFA de largeur 7, preuve de l'impossibilité de réduction à la largeur 6

Outils Théoriques

• Technique des témoins de lacune : Issue de la recherche sur le problème de déterminisation
• Construction par sous-ensemble : Utilisée pour la conversion CRA vers WFA
• Représentation matricielle : Utilisée pour la sémantique des CRAs
• Technique de réduction : À partir de problèmes indécidables (machines à deux compteurs) vers le problème cible

Résultats Expérimentaux

Résultats Théoriques Principaux

1. Décidabilité de la Désambiguïsabilité (Théorème 13 + Corollaire 17)

Théorème 13 : Le problème de désambiguïsabilité se réduit au problème de déterminisation.

Corollaire 17 : Le problème de désambiguïsabilité des WFAs est décidable.

Points clés de la preuve :

• Direction positive : Si B peut être déterminisé, alors A peut être désambiguïsé
  • Utilisation du lemme 16 : les témoins de type D de B impliquent les témoins de type U de A
  • Via le mécanisme d'engagement, la cohérence des arêtes entrantes garantit que les exécutions basses s'étendent aux états acceptants
• Direction négative : Si A peut être désambiguïsé, alors B peut être déterminisé
  • Utilisation du lemme 15 : les témoins de type U de A sont automatiquement des témoins de type D de B
  • La projection préserve le poids et la minimalité

2. Indécidabilité de la Minimisation des Registres (Théorème 20)

Théorème 20 : Le problème suivant est indécidable, même pour k=7 : Étant donné un WFA de largeur k, déterminer s'il existe un WFA équivalent de largeur k-1.

Corollaire 21 : Le problème suivant est indécidable, même pour k=7 : Étant donné un k-CRA, déterminer s'il existe un (k-1)-CRA équivalent.

Stratégie de preuve :

1. Construction d'un WFA A de largeur 6 à partir d'une machine à deux compteurs M (théorème 22)
2. Extension de A pour obtenir un WFA A' de largeur 7, en ajoutant :
   • États q_a et q_i (i∈6)
   • Lettres $, i, a, ī_i
3. Si la limite supérieure de A est bornée, alors q_a est redondant, permettant d'obtenir un WFA équivalent de largeur 6
4. Si A est non borné, alors il existe ζ=x@ tel que q₀ →^ζ q₀ ait un poids de 1
5. Utilisation du mot w = ζ^(6m) 1^(5m) 2^(4m) ... 5^m et du suffixe x = a ī₁ī₂...ī₅ pour construire une contradiction :
   • 7 préfixes x₀,...,x₆ tels que A'(wx_i) = im
   • Principe des tiroirs : au moins deux préfixes i<j atteignent le même état t
   • Différence de poids (j-i)m ≤ 12||B||, contredisant m > 12||B||

Analyse de Complexité

Problème de désambiguïsabilité :

• Borne inférieure : PSPACE-difficile (héritée de la borne inférieure du problème de déterminisation)
• Borne supérieure : Inconnue (la borne supérieure de complexité du problème de déterminisation n'a pas encore été établie)
• Complexité de réduction : Expansion exponentielle simple de l'espace d'états

Problème de minimisation des registres :

• Pour k fixe ≥7 : indécidable
• Pour k<7 : problème ouvert
• Pour les CRAs sur le corps des nombres rationnels : décidable (6)

Intuitions Techniques Clés

1. Essence de la limitation des lacunes :
   • La caractérisation des lacunes de type U capture le « degré de séparation » de deux exécutions acceptantes
   • Les lacunes limitées garantissent la possibilité de suivi avec une fenêtre finie de tous les exécutions pertinentes
2. Déterminisation vs Désambiguïsabilité :
   • Généralement, on résout d'abord la désambiguïsabilité, puis la déterminisation
   • Sur le semi-anneau tropical, on procède à l'inverse : résolution d'abord de la déterminisation, puis réduction de la désambiguïsabilité
   • Raison : le mécanisme d'engagement peut « forcer » les témoins de type D à devenir des témoins de type U
3. Incompressibilité de la largeur :
   • Les 7 composants (q_a et q_1,...,q_6) produisent via des mots et des lettres de suppression soigneusement conçus des configurations de poids non fusionnables
   • Chaque composant atteint son minimum à des moments différents, ne pouvant pas être simulé avec 6 registres

Travaux Connexes

1. Recherche sur le Problème de Déterminisation

• Historique : Remonte aux années 1990 19, 20
• Corps des nombres rationnels : Récemment prouvé décidable 5, 14
• Semi-anneau tropical : Prouvé décidable en 2025 1 (travaux antérieurs des auteurs de cet article)
• Caractérisation des lacunes : Filiot et al. 11 ont introduit le concept de lacune de type D

2. Recherche sur l'Ambiguïté

• Classification : k-ambiguïté, ambiguïté finie, ambiguïté polynomiale 7
• Ambiguïté polynomiale : Kirsten et Lombardy 16 ont prouvé la décidabilité de la désambiguïsabilité pour les automates tropicaux
• Corps des nombres rationnels : Bell et Smertnig 5 ont prouvé la décidabilité
• Contribution de cet article : Résolution du cas général (ambiguïté arbitraire)

3. Automates à Registres de Coûts

• Introduction : Alur et al. 4 ont défini le modèle CRA
• Pouvoir expressif : Équivalent aux WFAs 4
• Minimisation des registres :
  • Corps des nombres rationnels : décidable 6
  • Semi-anneau tropical : cet article prouve l'indécidabilité
• CRA faible : Almagor et al. 3 étudient les CRAs sans copie

4. Applications du Semi-anneau Tropical

• Problème de la hauteur d'étoile : Travaux de Hashiguchi 12, 13, Kirsten 15
• Problème de restriction : Leung et Podolskiy 18
• Limitation supérieure : Almagor et al. 2 prouvent l'indécidabilité (base de la réduction de minimisation des registres de cet article)

Contributions Uniques de Cet Article

1. Première résolution du problème général de désambiguïsabilité des WFAs tropicaux
2. Direction innovante : Résolution via réduction à la déterminisation plutôt que construction directe
3. Tableau complet : Résultats positifs (décidabilité de la désambiguïsabilité) et négatifs (indécidabilité de la minimisation des registres) simultanément
4. Caractérisation fine : Établissement de la correspondance précise entre k-CRAs et WFAs de largeur k

Conclusion et Discussion

Conclusions Principales

1. Résultat de décidabilité : Le problème de désambiguïsabilité des WFAs tropicaux est décidable, résolvant une question ouverte de longue date.
2. Résultat d'indécidabilité : Le problème de minimisation des registres des CRAs est indécidable, même pour un nombre fixe de 7 registres.
3. Contribution méthodologique : Résolution du problème de désambiguïsabilité via réduction au problème de déterminisation, révélant les connexions profondes entre les problèmes.
4. Raffinement d'équivalence : Équivalence précise entre k-CRAs et WFAs de largeur k.

Limitations

1. Complexité inconnue :
   • La complexité précise du problème de désambiguïsabilité n'est pas déterminée
   • Seule la borne inférieure PSPACE-difficile est connue
   • La réduction a une expansion exponentielle simple, dont la nécessité est inconnue
2. Lacune dans la minimisation des registres :
   • Indécidable pour k=7
   • La décidabilité pour k<7 reste un problème ouvert
   • Pour k=1 (déterminisation), c'est décidable
3. Ambiguïté relâchée :
   • La décidabilité générale de la 2-désambiguïsabilité, désambiguïsabilité finie, désambiguïsabilité polynomiale n'est pas résolue
   • Absence de caractérisation des lacunes correspondantes
4. Fragments spéciaux :
   • La décidabilité de la minimisation des registres pour les CRAs sans copie est inconnue
   • Les cas sous d'autres restrictions structurelles n'ont pas été explorés

Directions Futures

Les problèmes ouverts explicitement proposés par les auteurs :

1. Ambiguïté relâchée :
   • Peut-on déterminer si un WFA donné possède un WFA équivalent 2-ambigu/finiment ambigu/polynomialement ambigu ?
   • Le problème de 2-désambiguïsabilité semble extrêmement difficile, sans critère de lacune correspondant actuellement
2. Complétion du tableau de minimisation des registres :
   • La minimisation des registres est-elle décidable pour k<7 ?
   • Bien que moins importante, une caractérisation complète reste de valeur
3. Fragments structurels :
   • Minimisation des registres pour les CRAs sans copie
   • Propriétés d'autres classes de CRAs restreintes
4. Délimitation de complexité :
   • Détermination de la complexité précise du problème de désambiguïsabilité
   • Une fois la complexité du problème de déterminisation délimitée, étude de l'amélioration possible de la réduction (temps polynomial ou espace logarithmique)

Évaluation Approfondie

Points Forts

1. Percée théorique majeure :
   • Résolution de la question ouverte de longue date sur la désambiguïsabilité
   • Approche novatrice : utilisation inverse de la déterminisation pour résoudre la désambiguïsabilité
   • Techniques de preuve profondes et élégantes
2. Tableau théorique complet :
   • Coexistence de résultats positifs (décidabilité) et négatifs (indécidabilité)
   • Établissement de connexions entre différents modèles (WFAs et CRAs) et différentes mesures (ambiguïté et largeur)
3. Innovations techniques significatives :
   • Caractérisation des lacunes de type U : capture précise de l'essence de la non-ambiguïté
   • Construction d'exécutions canoniques : réalisation de l'unicité via tri par priorité
   • Mécanisme d'engagement : transformation astucieuse des témoins de type D en témoins de type U
   • Réutilisation des registres : évitement de l'expansion exponentielle dans la conversion WFA→CRA
4. Preuve rigoureuse et complète :
   • Tous les théorèmes possèdent des preuves détaillées
   • Logique claire entre les lemmes
   • Argumentation suffisante pour les points techniques clés (comme les lemmes 8, 9)
5. Qualité de rédaction élevée :
   • Structure claire, progression logique de la motivation aux résultats
   • Bonne combinaison d'explications intuitives et de définitions formelles
   • Les illustrations (figures 1-5) facilitent la compréhension

Insuffisances

1. Limites de complexité manquantes :
   • Borne supérieure inconnue pour le problème de désambiguïsabilité
   • Analyse manquante de la nécessité de l'expansion de la réduction
   • Absence d'évaluation de la calculabilité pratique
2. Lacune dans la minimisation des registres :
   • La limite k=7 est-elle serrée ?
   • Les cas k∈{2,3,4,5,6} restent complètement ouverts
   • Le point de basculement de k=1 (décidable) à k=7 (indécidable) n'est pas déterminé
3. Problèmes d'ambiguïté relâchée non abordés :
   • Les problèmes de 2-désambiguïsabilité, etc., ne sont mentionnés que dans la discussion
   • Aucun indice technique ou résultat partiel fourni
4. Absence de considérations pratiques :
   • Travail purement théorique, sans implémentation algorithmique
   • Absence d'analyse de complexité ou de discussion de faisabilité
   • Guidance limitée pour les applications pratiques
5. Généralisabilité des techniques de preuve :
   • Non discuté si la méthode s'applique à d'autres semi-anneaux
   • Relation insuffisamment analysée avec les résultats connus sur le corps des nombres rationnels

Évaluation de l'Impact

1. Signification théorique majeure :
   • Résolution d'une question ouverte de longue date, attendue pour devenir un jalon du domaine
   • Fourniture de nouveaux outils pour la recherche ultérieure (lacunes de type U, mécanisme d'engagement)
   • Révélation des connexions profondes entre déterminisation et désambiguïsabilité
2. Contribution méthodologique :
   • Les techniques de réduction pourraient inspirer la résolution d'autres problèmes
   • La méthode de caractérisation des lacunes pourrait s'étendre à d'autres modèles
3. Inspiration des problèmes ouverts :
   • Identification claire des directions de recherche importantes ultérieures
   • Établissement de points de référence pour la minimisation des registres avec k<7
4. Limitation de l'impact par les insuffisances :
   • L'absence de limites de complexité restreint les applications pratiques
   • L'algorithmisation et l'implémentation nécessitent des travaux supplémentaires

Scénarios d'Application

1. Recherche théorique :
   • Théorie des langages formels et automates
   • Théorie de la décidabilité et de la complexité
   • Modèles de calcul sur les semi-anneaux
2. Vérification de systèmes :
   • Systèmes nécessitant le raisonnement sur la consommation de ressources (énergie, temps)
   • Simplification d'automates en vérification quantitative
3. Conception d'algorithmes :
   • Optimisation et transformation d'automates pondérés
   • Mesure et contrôle du non-déterminisme
4. Valeur pédagogique :
   • Démonstration de la puissance des techniques de réduction
   • Illustration de la subtilité des frontières de décidabilité

Résumé des Points Forts Techniques

1. Caractérisation précise des lacunes de type U : Capture parfaite de l'essence combinatoire de la non-ambiguïté
2. Construction d'exécutions canoniques : Résolution du problème d'unicité via un simple mécanisme de priorité
3. Conception du mécanisme d'engagement : Codage explicite du DAG d'exécution dans l'alphabet, forçant la cohérence
4. Stratégie de réutilisation des registres : Réalisation de la correspondance précise de largeur tout en préservant l'équivalence
5. Élégance de la preuve d'indécidabilité : Arrangement minutieux de 7 composants démontrant l'incompressibilité

Références (Références Clés)

1 Almagor, Arbel, Sheinvald (2025). Determinization of min-plus weighted automata is decidable. SODA 2025.

2 Almagor, Boker, Kupferman (2020). What's decidable about weighted automata? Information and Computation.

4 Alur et al. (2013). Regular functions and cost register automata. LICS 2013.

5 Bell, Smertnig (2023). Computing the linear hull: Deciding determinizable and unambiguous for weighted automata over fields. LICS 2023.

11 Filiot et al. (2017). On delay and regret determinization of max-plus automata. LICS 2017.

16 Kirsten, Lombardy (2009). Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. STACS 2009.

Évaluation Générale : Cet article constitue une contribution théorique importante au domaine de la théorie des langages formels et des automates, résolvant la question ouverte de longue date sur la désambiguïsabilité et révélant l'indécidabilité de la minimisation des registres. Les techniques de preuve sont profondes et innovantes, en particulier l'approche inverse utilisant la déterminisation pour résoudre la désambiguïsabilité. Bien que des limites de complexité et des algorithmes pratiques fassent défaut, la valeur théorique et les contributions méthodologiques en font un progrès important dans le domaine. Pour les chercheurs en informatique théorique, cet article est une lecture incontournable.