Résumé technique : La complexité de la définition et de la séparation des formules de point fixe en logique modale

1. Énoncé du problème

L'article étudie le problème de la séparabilité modale du $\mu$-calcul modal ($\mu$ML) par rapport à la logique modale propositionnelle (ML). Étant donné deux formules de $\mu$ML incohérentes $\phi$ et $\phi'$, le problème consiste à déterminer s'il existe une formule de ML $\psi$ (un « séparateur ») telle que $\phi \models \psi$ et $\psi \models \neg \phi'$.

Ce problème généralise la définissabilité modale : déterminer si une formule de $\mu$ML spécifique est équivalente à une formule de ML. La définissabilité est le cas particulier où $\phi' = \neg \phi$. L'étude est menée sur diverses classes de modèles pertinentes pour l'informatique :

• Modèles arbitraires (degré de sortie non restreint).
• Mots (modèles de degré de sortie $\le 1$, notés $T_1$).
• Arbres binaires (degré de sortie $\le 2$, notés $T_2$).
• Arbres de degré de sortie borné $d \ge 3$ (notés $T_d$).
• Modèles finis et mots infinis.

Les auteurs étudient également le problème de l'existence de l'interpolant de Craig (un cas particulier de la séparabilité où le séparateur ne doit utiliser que les symboles communs à $\phi$ et $\phi'$) ainsi que la construction effective des séparateurs.

2. Méthodologie

Les auteurs emploient une combinaison de caractérisations model-théoriques et de techniques de théorie des automates :

• Caractérisations model-théoriques : Le cœur de la procédure de décision repose sur la co-consistance. Deux formules ne sont pas séparables si et seulement si elles sont « conjointement cohérentes » par rapport à des relations de bisimulation spécifiques. Plus précisément, $\phi$ et $\phi'$ ne sont pas séparables en ML sur une classe $\mathcal{C}$ s'ils sont conjointement cohérents par rapport aux $(\sigma, n)$-bisimulations pour tout $n$.

  • Pour les mots ($T_1$) et les arbres binaires ($T_2$), les auteurs exploitent le fait que la bisimilitude implique l'isomorphisme (ou peut s'y réduire) pour équivaloir la cohérence de la bisimilitude conjointe à la cohérence de l'isomorphisme conjoint.
  • Pour $d \ge 3$, cette équivalence échoue, nécessitant une analyse plus complexe impliquant des quotients de bisimulation.

• Théorie des automates : L'article utilise la correspondance bien connue entre le $\mu$ML et les automates d'arbres parité non déterministes (NPTA).

  • Les formules de $\mu$ML sont traduites en NPTA.
  • Le problème de la vérification de la co-consistance est réduit à la vérification de l'intersection des langages acceptés par ces automates.
  • Un outil technique clé est la construction d'automates qui reconnaissent des quotients de bisimulation des langages acceptés par les automates originaux. Cela permet aux auteurs de décider la séparabilité sur les arbres de degré de sortie borné en la réduisant à la vérification d'isomorphisme de ces quotients.

• Construction de séparateurs : Lorsque la séparabilité est établie, les auteurs fournissent des algorithmes pour construire la formule séparatrice. Ces constructions impliquent souvent la génération de conséquences uniformes en ML des formules d'entrée, qui sont des disjonctions de types cohérents avec l'entrée.

3. Contributions clés et résultats

3.1. Complexité de la séparabilité et de la définissabilité

L'article établit un paysage de complexité précis pour la séparabilité et la définissabilité en ML des formules de $\mu$ML, résumé dans le Tableau 1 de l'article :

Classe de modèles	Définissabilité en ML	Séparabilité en ML	Taille de la construction du séparateur
Mots ($T_1$)	PSpace-complet	PSpace-complet	Exponentielle simple
Arbres binaires ($T_2$)	ExpTime-complet	ExpTime-complet	Double exponentielle
Modèles non restreints	ExpTime-complet	ExpTime-complet	Double exponentielle
Arbres ($T_d, d \ge 3$)	ExpTime-complet	2-ExpTime-complet	Triple exponentielle

• Mots ($T_1$) : La séparabilité est PSpace-complète. C'est le cas le plus simple, correspondant à la complexité de la satisfaisabilité du $\mu$ML sur les mots.
• Arbres binaires ($T_2$) et Modèles non restreints : La séparabilité est ExpTime-complète. Les auteurs montrent que les propriétés structurelles des arbres binaires (où la bisimilitude implique l'isomorphisme) permettent un traitement algorithmique commun avec les modèles non restreints.
• Arbres avec $d \ge 3$ : C'est la découverte la plus significative. Alors que la définissabilité en ML reste ExpTime-complète, la séparabilité en ML bondit à 2-ExpTime-complète.
  • Les auteurs démontrent que cette augmentation de complexité n'est pas simplement due à l'encodage de degrés de sortie plus élevés dans les arbres binaires (ce qui préserverait la complexité).
  • La difficulté provient du fait que la ML ne possède pas la propriété d'interpolation de Craig (CIP) sur $T_d$ pour $d \ge 3$.

3.2. Interpolation de Craig et existence de l'interpolant

• Échec de la CIP : L'article prouve que la ML jouit de la propriété d'interpolation de Craig sur tous les modèles, mots et arbres binaires, mais qu'elle échoue sur les arbres de degré de sortie $d \ge 3$.
• Existence de l'interpolant : Motivés par l'échec de la CIP, les auteurs étudient le problème de l'existence de l'interpolant de Craig (un séparateur existe-t-il en utilisant uniquement les symboles communs ?) pour la ML sur $T_d$ ($d \ge 3$). Ils montrent que ce problème est coNExpTime-complet, ce qui est strictement plus difficile que le problème de validité pour la ML (qui est PSpace-complet sur ces classes).

3.3. Construction effective

L'article fournit des algorithmes pour construire des séparateurs lorsqu'ils existent :

• Mots : La construction est possible en temps exponentiel (optimal, car le $\mu$ML est exponentiellement plus succinct que la ML sur les mots).
• Binaires/Non restreints : La construction est possible en temps double exponentiel.
• $d \ge 3$ : La construction est possible en temps triple exponentiel.
• Les auteurs notent que pour $d \ge 3$, les séparateurs construits sont conjecturés comme étant optimaux en taille, bien qu'une borne inférieure formelle pour la taille de la construction reste ouverte.

3.4. Modalités graduées (Étude de cas)

Les auteurs étendent leurs résultats à la logique modale graduée (grML) et au $\mu$-calcul gradué (gr$\mu$ML), qui incluent des modalités comptant le nombre de successeurs (ex: « au moins $k$ enfants satisfont... »).

• Avec des grades dans le séparateur : La définissabilité et la séparabilité restent toutes deux ExpTime-complètes.
• Sans grades dans le séparateur :
  • Définissabilité : La définissabilité en ML des formules de gr$\mu$ML est ExpTime-complète.
  • Séparabilité : La séparabilité en ML des formules de gr$\mu$ML est 2-ExpTime-complète.
  • Les auteurs attribuent la complexité plus élevée de la séparabilité (comparée à la définissabilité) au fait que les arbres de degré de sortie borné sont définissables dans le gr$\mu$ML, permettant la réduction du cas général $d \ge 3$ au cadre gradué.

4. Signification et affirmations

L'article affirme fournir une « image assez complète et intéressante » de la complexité de la définissabilité et de la séparabilité pour les logiques de point fixe. Sa principale importance réside dans :

1. Identification d'un écart de complexité : C'est le premier cas connu dans le domaine de la logique où la séparabilité est prouvée plus difficile que la définissabilité (spécifiquement 2-ExpTime contre ExpTime) pour une logique naturelle sur une classe standard de modèles. Cela contraste avec les résultats précédents où la séparabilité était soit égale, soit plus facile que la définissabilité.
2. Connexion entre interpolation et complexité : Le travail établit un lien direct entre l'échec de la propriété d'interpolation de Craig et l'augmentation de la complexité computationnelle du problème de séparabilité. L'absence de CIP sur les arbres $d \ge 3$ est montrée comme la cause racine de la dureté 2-ExpTime.
3. Affinement du paysage de la logique modale : Les résultats clarifient que le raisonnement modal n'est pas uniforme à travers les structures d'arbres ; la transition des arbres binaires aux arbres ternaires modifie fondamentalement les propriétés logiques (spécifiquement l'interpolation) et le coût computationnel des tâches de raisonnement comme la séparabilité.
4. Résultats constructifs : Au-delà des procédures de décision, l'article propose des constructions effectives de séparateurs, fournissant des bornes sur la taille de ces séparateurs (ex: double exponentielle pour les arbres binaires, triple exponentielle pour $d \ge 3$).

Les auteurs concluent que leurs découvertes mettent en lumière l'interaction subtile entre les propriétés structurelles des modèles (degré de sortie), les propriétés logiques du langage (interpolation) et la complexité computationnelle des problèmes de raisonnement. Ils laissent ouvertes des questions concernant l'optimalité de la taille des séparateurs pour $d \ge 3$ et l'extension de ces résultats à d'autres fragments ou opérateurs.