The Model Checking Problem for Distributed Knowing How is $\Delta^p_2$-Complete

Résumé Technique : La complexité du problème de la vérification de modèle pour le "Distributed Knowing How" est $\Delta^p_2$-complète

Définition du Problème
Cet article étudie la complexité computationnelle du problème de la vérification de modèle (model checking) pour la logique du Distributed Knowing How (DKH). Le DKH est une logique modale conçue pour formaliser les capacités des agents à atteindre des objectifs par des actions appropriées. Elle généralise deux cadres existants :

1. Les cadres basés sur la planification (ex: [5, 6]), qui traitent le « savoir comment » comme l'existence d'un plan multi-étapes qui s'exécute, se termine et garantit un objectif.
2. Les cadres basés sur les coalitions (ex: [3, 4]), qui traitent le « savoir comment » de groupe comme l'existence d'une action conjointe en une seule étape assurant un objectif.

La logique DKH introduit une modalité $Kh_G \phi$, signifiant qu'un groupe d'agents $G$ possède une stratégie pour garantir que $\phi$ soit vérifié. La question centrale abordée est la suivante : Étant donné un modèle fini $M$, un état $s$ et une formule $\phi$, l'assertion $M, s \models \phi$ est-elle vraie ?

Méthodologie
Les auteurs établissent la complexité de ce problème en prouvant à la fois une borne supérieure et une borne inférieure, en utilisant un algorithme de vérification de modèle spécifique et une réduction à partir d'un problème connu de haute complexité.

1. Borne Supérieure ($\Delta^p_2$) :
   Les auteurs proposent une procédure de vérification de modèle, CHECKERDKH, qui évalue les formules de manière ascendante (bottom-up).

   • Cas Booléens et $K_G$ : Ils sont traités via des opérations d'ensembles polynomiales standards sur les états et les classes d'équivalence.
   • Le cas $Kh_G$ : C'est la composante non triviale. Au lieu de construire explicitement l'ensemble potentiellement exponentiel d'actions distribuées $A^*_G$, l'algorithme calcule l'ensemble de satisfaction de la formule intérieure $\psi$, puis effectue une construction de point fixe monotone sur l'ensemble quotient $S/\sim_G$ (l'ensemble des classes d'équivalence sous la relation d'indistinguabilité distribuée).
   • Utilisation d'Oracle : À chaque itération du point fixe, l'algorithme vérifie si une action distribuée « gagnante » existe pour une classe d'équivalence spécifique. Cette vérification (HASWINDISTRIBUTION) est effectuée par une procédure non déterministe qui devine un tuple d'actions atomiques et vérifie leur validité et leur exécutabilité. Cette étape de vérification est démontrée comme appartenant à NP.
   • Puisque l'itération du point fixe implique un nombre polynomial d'étapes, chacune appelant un oracle NP, la procédure globale réside dans $\Delta^p_2$ (problèmes décidables en temps polynomial avec un nombre polynomial d'appels à un oracle NP).

2. Borne Inférieure ($\Delta^p_2$-Dureté) :
   Pour prouver la dureté, les auteurs réduisent le problème SNSAT (un problème connu comme étant $\Delta^p_2$-complet) au problème de vérification de modèle DKH.

   • Instance SNSAT : Une instance consiste en une séquence de variables booléennes $x_1, \dots, x_n$ où chaque $x_i$ est définie par une équivalence $x_i \iff \exists Z_i F_i(x_1, \dots, x_{i-1}, Z_i)$. Le but est de déterminer la valeur de vérité de $x_n$.
   • Construction de la Réduction : Les auteurs construisent un modèle DKH $M$ et une formule $\Psi_n$ tels que $M, s_n \models \Psi_n$ si et seulement si $x_n$ est vrai dans l'instance SNSAT.
     • Le modèle contient des « états d'entrée » $s_i$ pour chaque couche et des « états mauvais » $b^i_r$ représentant des clauses non satisfaites.
     • Les agents sont assignés à des variables locales et à des occurrences précédentes de variables.
     • La formule $\Psi_k$ est définie récursivement : $\Psi_1 = Kh_{G_1} q$ et $\Psi_k = Kh_{G_k} (q \lor (r_k \land \neg \Psi_{k-1}))$.
     • La logique garantit qu'un groupe $G_k$ peut « savoir comment » atteindre l'état de succès $q$ (ou un état de vérification négative $n^k_{x_j}$) uniquement si la formule booléenne correspondante $F_k$ est satisfaisable compte tenu des valeurs de vérité des variables précédentes déterminées par les couches inférieures.
   • La réduction repose sur le fait que les actions distribuées dans cette construction spécifique peuvent être aplaties en tuples d'actions singulières, permettant à la stratégie d'encoder directement les assignations de vérité.

Contributions Clés et Résultats

• Classification de la Complexité : L'article prouve que le problème de la vérification de modèle pour le Distributed Knowing How est $\Delta^p_2$-complet. Cela fournit une borne de complexité serrée pour le problème.
• Innovation Algorithmique : Les auteurs introduisent un algorithme de vérification de modèle qui évite la construction explicite de l'ensemble d'actions distribuées $A^*_G$. Au lieu de cela, il utilise un algorithme de point fixe sur l'ensemble quotient $S/\sim_G$, déléguant l'existence d'actions distribuées valides à un oracle NP.
• Preuve de Dureté : La réduction de SNSAT démontre que l'interaction entre les quantificateurs imbriqués dans la logique (via la définition récursive de $Kh_G$) et la nature distribuée des actions capture toute la puissance de $\Delta^p_2$.

Signification
L'article affirme que l'établissement de cette borne serrée est la contribution principale. En caractérisant la complexité comme étant $\Delta^p_2$-complète, ce travail délimite les limites computationnelles de la vérification des capacités distribuées dans les systèmes multi-agents au sein de ce cadre logique. Les auteurs notent qu'une prochaine étape naturelle, basée sur ce résultat, est d'étudier le problème de la satisfaisabilité pour la logique du Distributed Knowing How.