Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

1. Énoncé du problème

L'article aborde le défi de modéliser la communication asynchrone dans les systèmes multi-agents en utilisant la Logique Épistémique Dynamique (DEL).

• Le Vide : La DEL standard (par exemple, la Logique de l'Annonce Publique) traite la communication comme instantanée et synchronisée : un message est envoyé et reçu par tous les agents simultanément. Cela échoue à capturer les systèmes distribués réels où l'envoi et la réception sont des événements distincts se produisant à des moments différents.
• Le Défi Spécifique : Les auteurs visent à formaliser une logique où :
  1. Les agents ont une incertitude temporelle concernant l'historique des messages (ils ne savent pas combien de messages les autres ont reçus).
  2. Les agents ont une incertitude épistémique concernant l'état du monde.
  3. La logique doit distinguer l'envoi d'un message (diffusion) de la réception d'un message (action individuelle).
  4. Le système doit gérer la validité dans deux contextes :
     • Validité $\epsilon$ : Vérité dans l'état initial (historique vide).
     • Validité $\ast$ (Validité-toujours) : Vérité dans tout état étant donné n'importe quel historique antérieur d'envoi et de réception.

Des travaux antérieurs (spécifiquement la référence [4]) ont fourni une axiomatisation ($AA$) pour les validités $\epsilon$ en utilisant un système de réduction (réduisant les modalités dynamiques aux modalités épistémiques statiques). Cependant, cette approche de réduction échoue pour les validités $\ast$ car les propriétés du système changent fondamentalement dès qu'un historique existe (par exemple, les agents peuvent avoir reçu un nombre différent de messages).

2. Méthodologie

2.1 Langage et Syntaxe

Les auteurs définissent un langage $\mathcal{L}$ étendant la logique modale multi-agents avec deux types de modalités dynamiques :

• Diffusion : $\langle \varphi \rangle \psi$ (La formule $\varphi$ est annoncée/diffusée ; par la suite $\psi$ est vrai).
• Réception : $\langle a \rangle \psi$ (L'agent $a$ reçoit le prochain message dans sa file d'attente ; par la suite $\psi$ est vrai).
• Mots d'Histoire : Des séquences d'agents et de formules (par exemple, $p.a.q$) représentent la séquence d'événements. Une histoire est un mot où, pour chaque agent, le nombre de messages reçus ne dépasse jamais le nombre de messages envoyés (contrainte FIFO).

2.2 Sémantique

La sémantique est définie sur des paires $(s, \alpha)$, où $s$ est un état dans un modèle de Kripke et $\alpha$ est un mot d'histoire.

• Exécutabilité ($\triangleright\triangleleft$) : Une relation déterminant si une histoire $\alpha$ peut être exécutée dans l'état $s$. Cela garantit que :
  1. L'histoire est une séquence valide (FIFO).
  2. Toutes les formules annoncées étaient vraies au moment de leur diffusion.
  3. Les agents ne considèrent exécutable que les histoires dans les états qu'ils jugent possibles.
• Relation de Vue ($\triangleright_a$) : Définit ce que l'agent $a$ considère comme possible. L'agent $a$ considère une histoire $\beta$ possible par rapport à l'histoire réelle $\alpha$ si la séquence de messages que $a$ a reçus dans $\beta$ correspond exactement à ce qu'il a reçu dans $\alpha$. Crucialement, les agents n'imaginent pas d'histoires contenant des messages qu'ils n'ont pas encore reçus.
• Saveur Trivalente : La sémantique se comporte quelque peu comme une logique trivalente. Si une histoire n'est pas exécutable dans un état ($s \not\triangleright\triangleleft \alpha$), les formules ne sont ni vraies ni fausses dans cette paire, bien que la logique conserve les validités standards.

2.3 La Formule « Vide »

Une innovation technique centrale est la définition d'une formule empty :
$$\text{empty} := \bigwedge_{a \in A} [a]\bot \land \bigwedge_{a,b \in A} K_a [b]\bot$$
Cette formule caractérise l'état où l'historique est vide ($\alpha = \epsilon$). Elle affirme qu'aucun message n'a été reçu par personne, et que tout le monde le sait. Cela n'est possible que dans un contexte multi-agent ($|A| \ge 2$).

3. Contributions Clés

3.1 Axiomatisation $AA^*$

La contribution principale est la proposition de $AA^*$, une axiomatisation pour les validités $\ast$ (validités-toujours).

• Nature Infinie : Contrairement au système précédent basé sur la réduction $AA$, $AA^*$ est infinie. Elle ne peut pas réduire les modalités dynamiques aux modalités statiques car la vérité des formules dépend de l'historique spécifique.
• La Règle $(R^*)$ : Le système inclut une règle infinie :
  • Prémisse : Pour tous les mots $\alpha$, $\text{empty} \to [\alpha]\varphi$ est dérivable.
  • Conclusion : $\varphi$ est dérivable.
    Cette règle réduit efficacement la validité $\ast$ à la validité $\epsilon$ en « réinitialisant » l'historique à vide via la formule empty.
• Axiomes : Le système inclut des axiomes pour :
  • La distribution de la connaissance et des modalités dynamiques.
  • Les conditions d'exécutabilité (par exemple, un message ne peut être reçu que s'il a été envoyé).
  • La permanence atomique (les valeurs de vérité des atomes ne changent pas).
  • Un axiome spécifique pour la connaissance dans les contextes asynchrones : $\text{empty} \to (K_a \varphi \leftrightarrow ([\alpha]\bot \lor \bigvee_{\alpha \triangleright_a \beta} K_a [\beta]\varphi))$.

3.2 Complétude et Correction

• Correction : Les auteurs prouvent que chaque théorème de $AA^*$ est $\ast$-valide.
• Complétude : Ils prouvent que chaque formule $\ast$-valide est un théorème de $AA^*$. La preuve utilise une construction de modèle canonique basée sur des théories maximales cohérentes. Un obstacle technique majeur a été la définition des relations d'accessibilité sur le modèle canonique pour garantir qu'elles forment des relations d'équivalence uniquement lorsqu'elles sont restreintes aux théories contenant empty.

3.3 La Limitation à un Agent Seul

L'article démontre rigoureusement que la méthode proposée échoue pour un agent seul.

• Dans un système à agent unique, un agent sait toujours qu'il a reçu tous les messages qu'il a vus. Il n'existe aucune formule équivalente à empty capable de distinguer un historique vide d'un historique non vide où l'agent a tout reçu.
• Par conséquent, la réduction de la validité $\ast$ à la validité $\epsilon$ via empty est impossible dans le cas d'un agent unique. Les auteurs laissent l'axiomatisation pour le cas d'un agent unique comme un problème ouvert.

4. Résultats

1. Système Formel : Une axiomatisation infinie complète et correcte ($AA^*$) pour la logique épistémique asynchrone avec des modalités d'envoi/réception séparées.
2. Mécanisme de Réduction : Une méthode novatrice pour gérer la « validité-toujours » en utilisant la formule empty pour ancrer la logique à l'état initial, contournant ainsi le besoin d'un système de réduction fini.
3. Distinction par rapport à S5 : La logique ne satisfait pas l'axiome de vérité standard de S5 ($K_a \varphi \to \varphi$) globalement. La connaissance n'est factuelle que si l'agent sait que l'historique est vide. Sinon, la modalité se comporte davantage comme une « croyance cohérente ».
4. Comparaison avec l'Informatique Distribuée : La sémantique s'aligne sur le concept de coupes cohérentes dans les systèmes distribués, mais la raffine en intégrant directement les conditions de vérité (exécutabilité) dans la logique, empêchant ainsi les états incohérents (par exemple, recevoir un message avant qu'il ne soit envoyé, ou recevoir une annonce fausse).

5. Signification

• Avancement Théorique : Ce travail comble le fossé entre la Logique Épistémique Dynamique standard (qui suppose la synchronie) et les réalités de l'informatique distribuée (asynchronie). Il fournit le premier cadre logique rigoureux traitant l'envoi et la réception comme des événements distincts et asynchrones avec des modalités séparées.
• Gestion de l'Incertitude Temporelle : Il modélise avec succès le type spécifique d'incertitude où les agents sont incertains de la longueur de l'historique de communication par rapport aux autres, un scénario courant dans les protocoles de commérages et le consensus distribué.
• Innovation Méthodologique : L'utilisation d'une règle infinie ($R^*$) combinée à une formule de « réinitialisation » spécifique (empty) offre un nouveau modèle pour axiomatiser des logiques où les propriétés dynamiques ne peuvent pas être réduites à des propriétés statiques via une réécriture finie.
• Voies Futures : L'article identifie des pistes claires pour la recherche future, notamment l'extension de la logique à la connaissance de groupe (connaissance distribuée), à la communication non publique, et à la résolution du problème de l'axiomatisation pour un agent unique.

En résumé, l'article établit une fondation logique robuste pour le raisonnement sur la connaissance dans des environnements asynchrones, prouvant que bien que les techniques de réduction standards échouent, un système infini soigneusement construit peut capturer toute la complexité du passage de messages asynchrone.