Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

Résumé technique : Automates ensemblistes et limites de la décidabilité de la logique à deux variables sur les mots de données

Énoncé du problème
L'article traite de la décidabilité du problème de satisfaisabilité pour des extensions de la logique du premier ordre à deux variables ($FO_2$) sur les mots de données. Un mot de données est une séquence finie de paires $(a_i, d_i)$ où $a_i$ provient d'un alphabet fini $\Sigma$ et $d_i$ d'un domaine infini $D$, l'égalité étant la seule propriété testable sur $D$. Alors que la logique $FO_2$ standard sur les mots de données (avec ordre, successeur et égalité de données) est connue pour être décidable (spécifiquement, $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1]$), les auteurs examinent les limites de la décidabilité lors de l'extension de cette logique par des prédicats réguliers gardés.

Ces prédicats, notés $eL(x, y)$, sont vrais si les positions $x$ et $y$ appartiennent à la même classe de données (c'est-à-dire $x \sim y$) et si le facteur de la chaîne strictement situé entre elles appartient à un langage régulier $L$. La question centrale est : pour quelles classes de monoïdes (ou de semi-groupes) $M$ qui reconnaissent la famille des langages réguliers utilisés dans ces prédicats le problème de satisfaisabilité est-il décidable ?

Méthodologie
Les auteurs emploient une combinaison de la théorie des automates et de la théorie algébrique des semi-groupes pour caractériser la frontière de la décidabilité.

1. Automates ensemblistes : Les auteurs introduisent un nouveau formalisme d'automates appelé automates ensemblistes. Ce sont des automates à états finis équipés d'un nombre fixe d'ensembles capables de stocker des valeurs de données. Les transitions permettent :

   • Des mises à jour locales : Ajouter ou retirer la valeur de données courante d'ensembles spécifiques.
   • Des mises à jour globales : Appliquer une relation (ou une transformation) au contenu de tous les ensembles simultanément (par exemple, déplacer des données de l'ensemble $X_i$ vers $X_j$).
     Les auteurs établissent que les automates ensemblistes sont expressivement équivalents aux automates de classes (introduits par Bojańczyk et Lasota), un modèle dont le problème de vide est connu pour être indécidable.

2. Sous-classes et décidabilité : Pour retrouver la décidabilité, les auteurs définissent une sous-classe appelée automates ensemblistes quasi-normaux ordonnés.

   • Quasi-normaux : Garantit que les valeurs de données sont présentes dans au plus un ensemble parmi un sous-ensemble spécifique d'ensembles « non stables ».
   • Ordonnés : Impose un ordre linéaire sur les ensembles non stables tel que les mises à jour globales vident le contenu d'un préfixe de ces ensembles et les déplacent vers des ensembles situés plus haut dans l'ordre.
     Le problème de vide pour les automates ensemblistes quasi-normaux ordonnés est démontré décidable par réduction au problème de vide des automates multicompteurs ordonnés, un problème décidable connu.

3. Traduction logique-automates : L'article fournit des traductions entre les formules logiques et les automates :

   • Tout automate ensembliste peut être exprimé comme une formule $EMSO_2$ avec des prédicats réguliers gardés.
   • Inversement, les formules utilisant des prédicats reconnus par un monoïde $M$ peuvent être traduites en automates ensemblistes à stockage de suffixes (un type spécifique d'automate quasi-normal).

4. Caractérisation algébrique : Les auteurs analysent la structure algébrique des monoïdes $M$. Ils définissent les bandes linéaires comme des monoïdes idempotents où les idéaux bilatères sont linéairement ordonnés (c'est-à-dire que pour deux idéaux quelconques $I, J$, soit $I \subseteq J$, soit $J \subseteq I$).

Contributions et résultats clés

• Théorème principal (Théorème 6) : La satisfaisabilité des formules $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1, \tilde{F}_M]$ sur les mots de données est décidable si et seulement si le monoïde $M$ est une bande linéaire.

  • Direction décidabilité : Si $M$ est une bande linéaire, les auteurs construisent un automate ensembliste quasi-normal ordonné équivalent. Puisque le vide de tels automates est décidable, la logique est décidable.
  • Direction indécidabilité : Si $M$ n'est pas une bande linéaire, il doit contenir une sous-structure isomorphe soit à $U_1^2$ (le produit direct de deux monoïdes à deux éléments avec zéro), soit à $N_2$ (un monoïde nul spécifique). Les auteurs montrent que les prédicats réguliers gardés reconnus par ces monoïdes spécifiques permettent l'encodage du problème de l'arrêt des machines à deux compteurs, rendant la logique indécidable.

• Équivalence expressive : L'article démontre que les automates ensemblistes sont expressivement équivalents à $EMSO_2$ avec des prédicats réguliers gardés. De plus, il montre que toute formule avec des prédicats réguliers reconnus par un monoïde $M$ peut être réécrite de manière équivalente en utilisant des prédicats réguliers gardés reconnus par un autre monoïde $M'$ (spécifiquement, le monoïde des parties $P(M)$).

• Extension stricte : Le fragment décidable identifié est une extension stricte de la logique $FO_2$ originale de [4]. Par exemple, le langage $L_2$ (exigeant aucun test de zéro entre les incréments et les décréments de la même classe), qui n'est pas définissable dans la $FO_2$ standard ou les automates de données, devient définissable dans cette logique étendue lorsque le monoïde sous-jacent est une bande linéaire.

Signification et affirmations
L'article prétend fournir une caractérisation précise de la frontière de la décidabilité pour la logique à deux variables sur les mots de données étendue par des prédicats réguliers gardés. En reliant la décidabilité logique à la propriété algébrique du monoïde de reconnaissance étant une « bande linéaire », ce travail comble le fossé entre l'expressivité logique et la structure algébrique.

Les auteurs notent que, bien que la décidabilité pour les bandes linéaires soit établie, la caractérisation pour les semi-groupes généraux reste ouverte. Ils soulignent également que la classe des langages réguliers reconnus par les bandes linéaires n'a pas été étudiée de manière approfondie dans la littérature, suggérant un besoin d'exploration supplémentaire dans ce domaine algébrique. La complexité des procédures de décision reste non élémentaire, héritée des résultats sous-jacents sur la $FO_2$ et les automates de données.

Ce travail se distingue des logiques temporelles (comme freeze-LTL) en offrant une extension décidable de la logique du premier ordre qui capture des propriétés régulières spécifiques au sein des classes de données, qui étaient auparavant indécidables ou nécessitaient des cadres logiques différents.