The Guarded Fragment with Nested Equivalences

Résumé technique : Le fragment gardé avec équivalences imbriquées

Énoncé du problème
Le fragment gardé (GF) est un fragment décidable bien connu de la logique du premier ordre (FOL) qui généralise la logique modale et sert de fondement aux logiques de description. Bien que GF soit connu pour posséder la propriété du modèle fini et un problème de satisfaisabilité décidable, son comportement lorsqu'il est étendu par des relations d'équivalence nécessite une analyse rigoureuse. Plus précisément, cet article examine l'extension de GF par une famille de relations d'équivalence imbriquées ($E_1, E_2, \dots$), où $E_{k+1}$ est plus grossière que $E_k$ (c'est-à-dire $E_k \subseteq E_{k+1}$).

L'étude aborde deux défis principaux :

1. Décidabilité et complexité : Déterminer si le problème de satisfaisabilité pour GF avec équivalences imbriquées est décidable et établir des bornes de complexité serrées.
2. Limites de la décidabilité : Identifier exactement quelles conditions (telles que la contrainte d'imbrication ou l'exclusion de l'égalité) sont nécessaires pour maintenir la décidabilité.

Les travaux antérieurs se sont largement concentrés sur le fragment à deux variables (FO2) avec équivalences imbriquées ou sur des cadres restreints au sein de GF (par exemple, des gardes d'équivalence). Le cas de GF complet avec équivalences imbriquées, même avec une seule relation d'équivalence, était resté ouvert.

Méthodologie
L'article utilise une combinaison de constructions model-théoriques et de réductions de la théorie de la complexité :

1. Construction de la borne inférieure (Difficulté) :

   • Les auteurs construisent des « compteurs imbriqués » en utilisant les relations d'équivalence imbriquées pour simuler de grands nombres. En traitant les classes d'équivalence comme des bits, ils peuvent représenter des nombres jusqu'à une tour d'exponentielles ($t(K, n)$) en utilisant une formule de longueur polynomiale.
   • Ces compteurs sont utilisés pour encoder les exécutions acceptantes de machines de Turing alternantes (ATM) opérant dans un espace exponentiel.
   • Pour le fragment avec un nombre fixe de variables ($GF_3$) et $K$ relations d'équivalence, ils prouvent la dureté $(K+1)$-ExpTime.
   • En introduisant des constantes et des variables non bornées, ils élèvent cela à une dureté $(K+2)$-ExpTime.
   • Dans le cas général ($K$ non borné), le problème est montré comme étant Tower-dur (non élémentaire).

2. Construction de la borne supérieure (Décidabilité) :

   • Propriété du modèle fini (PMF) : Les auteurs prouvent que le fragment sans égalité jouit de la PMF. Ils établissent une « propriété d'imbrication à indice fini », montrant que si une phrase est satisfaisable, elle possède un modèle où chaque classe $E_{k+1}$ se décompose en un nombre fini de classes $E_k$.
   • Réduction de modèle : Ils démontrent que la relation d'équivalence la plus fine $E_1$ peut être éliminée en la remplaçant par un ensemble fini de prédicats unaires qui distinguent le nombre fini de classes $E_1$ au sein d'une classe $E_2$. Cela réduit $GF[K\text{-}EQ^\subseteq]$ à $GF[(K-1)\text{-}EQ^\subseteq]$.
   • Procédure de décision : Pour le cas de base ($K=1$), ils conçoivent une procédure de décision basée sur des « types étiquetés ». Cela implique de construire un ensemble de types satisfaisant des conditions spécifiques de fermeture et de témoin (Lemme 15), permettant d'effectuer la vérification de satisfaisabilité en temps déterministe.

Contributions et résultats clés

1. Décidabilité et bornes de complexité :

   • Cas général : Le problème de satisfaisabilité pour $GF[EQ^\subseteq]$ sans égalité est Tower-complet.
   • $K$ fixe : Pour un nombre fixe de prédicats distingués $K$, le problème de satisfaisabilité pour $GF[K\text{-}EQ^\subseteq]$ est $(K+2)$-ExpTime-complet.
   • Bornes affinées : Si les constantes sont interdites ou si le nombre de variables est fixé à $m \ge 3$, la complexité chute à $(K+1)$-ExpTime-complet.
   • L'article établit que la taille minimale des modèles pour ces fragments croît comme une tour d'exponentielles, correspondant aux bornes inférieures de complexité.

2. Résultats d'indécidabilité :

   • Égalité : L'inclusion de l'égalité rend le problème indécidable. Plus précisément, $GF_3$ avec une seule relation d'équivalence et l'égalité est indécidable (Proposition 2).
   • Équivalences non imbriquées : Si la condition d'imbrication est abandonnée, la décidabilité est perdue. $GF_3$ étendu par seulement deux relations d'équivalence indépendantes (non imbriquées) est indécidable (Théorème 6). Cela contraste avec $GF_2$, qui reste décidable avec deux équivalences indépendantes mais devient indécidable avec trois.

3. Propriété du modèle fini :

   • Les fragments sans égalité $GF[EQ^\subseteq]$ et $GF[K\text{-}EQ^\subseteq]$ possèdent la propriété du modèle fini. La taille des modèles minimaux est bornée par une fonction exponentielle $(K+2)$ (diminuant à une fonction exponentielle $(K+1)$ sous les restrictions de l'absence de constantes ou de variables fixes).

4. Application aux langages d'ontologie :

   • L'article propose une extension décidable de la logique de description ALCHI (désignée comme $ALCHI + \text{rôles d'équivalence imbriqués}$). Cette extension permet des « dépendances existentielles par paires » et des rôles d'équivalence imbriqués, capturant des politiques de contrôle d'accès (par exemple, utilisateurs et administrateurs au sein d'organisations et de départements) qui sont expressibles en GF mais pas en FO2 ou SHI standard.

Signification et affirmations
L'article prétend résoudre le problème ouvert de la décidabilité de GF avec des relations d'équivalence imbriquées. Sa signification réside dans :

• Compléter le paysage : Il comble le fossé entre le FO2 bien étudié avec équivalences imbriquées et le GF plus expressif, montrant que GF conserve la décidabilité sous la contrainte d'imbrication mais la perd immédiatement si l'égalité ou des relations non imbriquées sont introduites.
• Complexité serrée : Il fournit des bornes de complexité précises et serrées (Tower et $(K+2)$-ExpTime), démontrant que l'imbrication des équivalences induit une explosion non élémentaire de la taille des modèles et de la complexité computationnelle.
• Pertinence pratique : En reliant la logique aux politiques de contrôle d'accès et en étendant les logiques de description, ce travail suggère une fondation théorique pour le raisonnement sur des données structurées hiérarchiquement (par exemple, systèmes de fichiers, topologies de réseaux, structures organisationnelles) où les niveaux de granularité sont naturellement imbriqués.

Les auteurs déclarent explicitement que leurs résultats ne s'étendent pas au fragment faiblement gardé (LGF) ni aux requêtes conjonctives, et ils notent que l'inclusion de l'égalité conduit immédiatement à l'indécidabilité, même avec une seule relation d'équivalence.