A non-uniform view of Craig interpolation in modal logics with linear frames

Résumé technique : Une vision non uniforme de l'interpolation de Craig dans les logiques modales à cadres linéaires

Énoncé du problème
La propriété d'interpolation de Craig (CIP) est une propriété fondamentale en logique stipulant que pour toute implication valide $\phi \to \psi$, il existe un interpolant $\iota$ utilisant uniquement le vocabulaire partagé de $\phi$ et $\psi$ tel que $\phi \to \iota$ et $\iota \to \psi$ soient également valides. Il est établi comme un fait « négatif » que de nombreuses logiques modales normales étendant K4.3 (la logique des cadres transitifs linéaires) ne possèdent pas la CIP, particulièrement celles avec des cadres de profondeur non bornée. Traditionnellement, l'absence de la CIP a mis fin à la recherche d'interpolants pour une logique donnée.

Cet article recadre l'absence de la CIP comme une question de recherche en investiguant le Problème de l'Existence de l'Interpolant (IEP) : étant donné deux formules $\phi$ et $\psi$ telles que $\phi \to \psi$ est valide dans une logique $L$, existe-t-il un interpolant de Craig dans $L$ ? Contrairement à la CIP uniforme, l'IEP ne se réduit pas à une simple vérification de validité car la validité de l'implication ne garantit pas l'existence d'un interpolant. La question centrale abordée est de savoir si l'IEP est computationnellement plus difficile que le problème de validité (l'implication) pour ces logiques. Des résultats antérieurs sur d'autres logiques (par exemple, les logiques modales avec des nominaux, les fragments de la logique du premier ordre) ont suggéré que l'IEP pourrait être nettement plus difficile (par exemple, 3ExpTime). Cet article examine si cela est le cas pour les logiques modales propositionnelles contenant K4.3.

Méthodologie
Les auteurs emploient une approche non uniforme et modèle-théorique basée sur les bisimulations et les cadres descriptifs.

1. Caractérisation par bisimulation : L'article utilise un critère connu (Théorème 3.2) stipulant que $\phi \to \psi$ manque d'un interpolant dans $L$ si et seulement s'il existe deux modèles, $M_1$ et $M_2$, basés sur des cadres descriptifs pour $L$, tels que $M_1$ satisfait $\phi$, $M_2$ satisfait $\neg\psi$, et les points racines de ces modèles sont $\sigma$-bisimilaires (où $\sigma$ est la signature partagée).
2. Cadres descriptifs : L'analyse repose lourdement sur la structure des cadres descriptifs (cadres équipés d'une algèbre spécifique d'ensembles internes satisfaisant des conditions de différenciation, de compacité et de densité/tightness). Ceci est crucial car, pour des logiques comme GL.3 et Log{(N, <)}, les contre-exemples à la CIP ne peuvent pas être manifestés par des cadres de Kripke standards mais nécessitent des cadres descriptifs infinis.
3. Décomposition structurelle : L'innovation technique centrale implique l'analyse de la structure de ces modèles bisimilaires. Les auteurs partitionnent les modèles en $\sigma$-blocs (intervalles de points ayant des propriétés de bisimulation spécifiques) et montrent que toute paire de modèles bisimilaires manifestant l'absence d'un interpolant peut être transformée en une paire de modèles « quasi-finis ». Ces modèles sont construits comme des sommes ordonnées de modèles simples basés sur des cadres atomiques spécifiques (chaînes finies, clusters finis, ou structures en « tadpole » comme $C(\bigcirc_k, \bullet)$).
4. Propriété Quasi-Polynômiale : Pour les logiques fini-axiomatisables, les auteurs prouvent que ces modèles manifestant l'absence d'interpolant peuvent être bornés en taille par un polynôme de la taille des formules d'entrée et des axiomes de la logique. Cela est nommé la propriété de modèle bisimilaire quasi-polynomiale.

Contributions clés et résultats

• Décidabilité et Complexité : L'article prouve que pour toutes les logiques modales normales fini-axiomatisables contenant K4.3, l'IEP est décidable et coNP-complet.

  • Ce résultat est significatif car il montre que l'IEP n'est pas plus difficile que le problème de validité (qui est également dans coNP pour ces logiques). Cela contraste fortement avec les récents résultats de non-uniformité d'interpolation dans d'autres cadres logiques où l'IEP est strictement plus difficile.
  • La preuve implique un algorithme non déterministe qui devine des modèles de taille polynomiale satisfaisant le critère de bisimulation et vérifie les axiomes de la logique.

• Propriété de Modèle Bisimilaire Quasi-Polynômiale : Les auteurs établissent que toutes les extensions de K4.3 fini-axiomatisables possèdent la « propriété de modèle bisimilaire quasi-polynômiale ». Cela signifie que si un interpolant n'existe pas, il existe une paire de modèles bisimilaires témoignant de ce fait où les modèles sont des sommes ordonnées d'un nombre polynomial de modèles simples basés sur des cadres atomiques de taille polynomiale.

  • Pour les logiques de sous-cadres cofinaux d-persistants (une sous-classe), la propriété est encore plus forte : elles possèdent la propriété de modèle bisimilaire polynomiale, où les modèles sont des cadres de Kripke standards de taille polynomiale.

• Extension aux logiques temporelles prioraines : La méthodologie est étendue aux logiques temporelles prioraines (contenant à la fois des modalités de futur et de passé) sur des flux temporels standards :

  • Lin (tous les cadres linéaires), LinQ (rationnels) et LinR (réels) : Ces logiques sont montrées comme possédant la proprierté de modèle bisimilaire polynomiale, et leur IEP est coNP-complet.
  • Lin<ω (ordres linéaires stricts finis) et LinZ (entiers) : Ces logiques ne possèdent pas la propriété polynomiale mais possèdent la propriété de modèle bisimilaire quasi-polynômiale. Leur IEP est également prouvé comme étant coNP-complet.
  • La preuve pour les logiques temporelles nécessite de gérer des chaînes bidirectionnelles et des clusters limites dans les deux directions, nécessitant de nouvelles constructions de cadres (par exemple, des cadres « tadpole » symétriques $C(\bullet, \bigcirc_k, \bullet)$).

Signification et Revendications
L'article affirme fournir le premier résultat général sur l'existence de l'interpolant de Craig couvrant une large famille de logiques modales (extensions de K4.3) qui ne possèdent pas la CIP. En démontrant que l'IEP est coNP-complet pour ces logiques, les auteurs contestent l'intuition selon laquelle l'absence de la CIP mène nécessairement à une classe de complexité supérieure pour le problème d'existence.

Le travail suggère que la complexité de l'IEP n'est pas intrinsèquement liée à l'échec de la CIP mais dépend plutôt des propriétés structurelles des modèles requis pour témoigner de cet échec. Les auteurs positionnent cela comme une étape vers une classification des logiques modales basée sur la complexité de leur IEP.

L'article note explicitement que sa preuve n'est pas constructive concernant le calcul des interpolants ; elle fournit une procédure de décision pour l'existence mais ne produit pas d'algorithme efficace pour calculer l'interpolant lui-même ou des bornes supérieures sur sa taille. Les auteurs soulignent également que les cadres descriptifs sont essentiels pour leurs preuves, soulevant la question ouverte de savoir si les cadres de Kripke suffisent pour l'IEP dans les logiques qui ne sont pas d-persistantes mais qui sont fortement complètes pour Kripke (comme LinR).