Parameterized complexity of n-dense modal logics

1. Problème et Contexte

Contexte :
La logique modale est un domaine fondamental de la logique mathématique avec des applications en vérification de programmes, en logique épistémique et déontique. La question centrale est celle de la satisfaisabilité ($L$-sat) : existe-t-il un modèle pour une formule donnée dans une logique $L$ ? Pour la plupart des logiques modales bien connues, ce problème est PSPACE-complet.

Le problème spécifique :
Cet article se concentre sur une classe de logiques modales normales appelées logiques $n$-denses (notées $KDe(n)$), caractérisées par l'axiome $\Box^n p \to \Box p$ (avec $n > 1$). Sémantiquement, cela correspond à des cadres (frames) où la relation d'accessibilité $R$ satisfait $R \subseteq R^n$ (si deux nœuds sont connectés, il existe un chemin de longueur $n$ entre eux).

État de l'art et difficulté :

• La satisfaisabilité pour ces logiques est connue pour être dans NEXPTIME (via la technique de filtration).
• Elle est également PSPACE-dure (démontré dans des travaux antérieurs).
• La borne exacte de complexité (entre PSPACE et EXPSPACE) reste un problème ouvert difficile.
• L'objectif de l'article est d'affiner cette analyse en utilisant la complexité paramétrée. L'idée est de considérer la profondeur modale ($d(\phi)$) de la formule d'entrée comme un paramètre fixe. Si le problème devient gérable (polynomial en la taille de l'entrée) pour une profondeur fixe, il appartient à la classe para-PSPACE.

2. Méthodologie

L'auteur propose une approche basée sur les tableaux sémantiques (tableaux), une méthode de décision standard pour les logiques modales. Cependant, les tableaux pour les logiques $n$-denses peuvent être infinis en raison de la nécessité d'insérer des nœuds intermédiaires pour satisfaire la densité.

Pour contourner l'explosion combinatoire et gérer l'infini, l'article généralise une technique introduite précédemment par Balbiani et Gasquet, appelée « fenêtres » (windows), en les rendant récursives.

Concepts clés de la méthodologie :

• Fenêtres (Windows) : Une fenêtre est une structure récursive qui représente une partie finie et polynomiale d'un tableau infini. Elle capture les contraintes locales entre un nœud $u$ et son successeur $v_0$ dans le cadre de la densité.
• Fenêtres Récursives : Contrairement aux fenêtres simples, les fenêtres récursives sont définies de manière imbriquée. Une fenêtre de niveau $k$ contient des sous-fenêtres de niveau $k-1$. Cela permet de modéliser la structure hiérarchique des contraintes modales.
• Continuations et Inclusion : L'algorithme repose sur la notion de « continuation » d'une fenêtre. Si une fenêtre $W_2$ est une continuation de $W_1$ (selon une relation d'inclusion point par point $\sqsubseteq_k$), cela signifie que $W_2$ peut prolonger $W_1$ sans violer les contraintes logiques, à condition que les nœuds soient suffisamment éloignés (distance liée à la profondeur modale).
• Détection de boucle : Grâce à la borne supérieure du nombre de configurations possibles de fenêtres (qui dépend de la taille de la formule et de la profondeur modale), l'algorithme garantit qu'une répétition de fenêtres (une boucle) se produira nécessairement si le tableau est satisfaisable. Cela permet de terminer la recherche sans explorer l'infini.

3. Algorithme Proposé

L'auteur conçoit un algorithme de décision pour le cas $2$-dense ($KDe(2)$), qui est ensuite généralisé à $n$-dense.

• Fonction principale Sat(u) : Vérifie la satisfaisabilité d'un ensemble de formules $u$ (un CCS - Classically Consistent Saturation). Elle vérifie la cohérence classique et, pour chaque formule de la forme $\neg \Box \phi$, elle lance une vérification récursive via SatW.
• Fonction SatW(W, u, k, N) : Vérifie la satisfaisabilité d'une fenêtre $W$ de profondeur $k$ et de longueur $N$.
  • Elle vérifie récursivement la satisfaisabilité des sous-fenêtres.
  • Elle utilise la fonction NextW pour générer une continuation de la fenêtre.
  • Elle s'arrête si une fenêtre est trouvée satisfaisable ou si une contradiction est détectée.
  • La récursion est bornée par la profondeur modale $d(u)$ et une fonction de longueur $\chi(u)$ (exponentielle en la taille de la formule mais indépendante de la profondeur modale dans le paramètre).

4. Résultats Principaux

1. Correction et Complétude : L'article prouve que l'algorithme est correct (si l'algorithme retourne vrai, une modèle existe) et complet (si un modèle existe, l'algorithme retourne vrai). La preuve de complétude repose sur la construction explicite d'un modèle à partir des fenêtres satisfaisables.
2. Complexité Spatiale : L'analyse de l'espace mémoire requis montre que l'algorithme fonctionne dans un espace de l'ordre de :
   $$O(|u|^3 \cdot 2^{d(u)^5})$$
   où $|u|$ est la taille de la formule et $d(u)$ sa profondeur modale.
3. Classe de Complexité : Puisque la fonction $f(d(u)) = 2^{d(u)^5}$ est calculable et que le reste de la complexité est polynomial en $|u|$, le problème de satisfaisabilité pour les logiques $n$-denses appartient à la classe para-PSPACE.
   • Cela signifie que pour une profondeur modale fixée, le problème est résoluble en espace polynomial par rapport à la taille de la formule.
4. Généralisation : Bien que l'analyse détaillée soit faite pour $n=2$, l'auteur montre que la généralisation à $n$-dense ($n > 2$) est directe, en modifiant la structure des fenêtres pour inclure des $n$-uplets de nœuds intermédiaires. Le résultat final s'applique à tout $n \in \mathbb{N}$.

5. Signification et Contribution

• Affinement de la complexité : L'article résout partiellement le problème de la borne de complexité des logiques $n$-denses. Au lieu de se contenter de la fourchette large [PSPACE, EXPSPACE], il établit une classification précise via la complexité paramétrée.
• Innovation méthodologique : La généralisation des « fenêtres » en fenêtres récursives est une contribution majeure. Cette technique permet de gérer la structure infinie des modèles de manière finie et contrôlée, en exploitant la profondeur modale comme paramètre de contrôle.
• Potentiel d'application : L'auteur suggère que la notion de fenêtre récursive pourrait être appliquée à d'autres logiques modales complexes impliquant des propriétés de chemins intermédiaires (comme les logiques multimodales ou d'autres densités), offrant ainsi un nouvel outil pour l'analyse de la décidabilité et de la complexité.
• Importance pour le domaine : L'article met en lumière le fait que la complexité paramétrée est sous-étudiée dans le domaine de la logique modale, malgré son potentiel pour caractériser finement des problèmes qui semblent intrinsèquement difficiles.

En résumé, cet article démontre que la satisfaisabilité des logiques $n$-denses, bien que potentiellement très complexe, devient traitable en espace polynomial dès lors que la profondeur modale des formules est considérée comme un paramètre fixe, grâce à une ingénieuse généralisation de la technique des fenêtres.