La logique épistémique modale est une branche de la logique modale qui formalise le raisonnement sur la connaissance et la croyance. Elle étend la logique propositionnelle avec des opérateurs modaux qui expriment ce que des agents individuels savent ou croient, permettant une analyse précise d'énoncés tels que « l'agent A sait que la proposition P » ou « l'agent B croit que l'agent A sait P ». Ce cadre trouve son origine en philosophie, mais est devenu un outil central en informatique, en économie et en intelligence artificielle pour modéliser les systèmes multi-agents, les protocoles distribués et les scénarios de théorie des jeux.
Le langage formel de la logique épistémique modale inclut généralement un ensemble de variables propositionnelles, des connecteurs booléens et des opérateurs modaux K_i pour chaque agent i, où K_i φ se lit « l'agent i sait que φ ». Dans les systèmes multi-agents, on ajoute souvent des opérateurs pour la connaissance commune (C_G φ) et la connaissance distribuée (D_G φ) pour un groupe G. La sémantique standard, introduite par Saul Kripke à la fin des années 1950 et raffinée par Robert Aumann en 1976, utilise des cadres de Kripke composés d'un ensemble de mondes possibles et d'une relation d'équivalence pour chaque agent. Une formule K_i φ est vraie dans un monde w si φ est vraie dans tous les mondes que l'agent i considère possibles à partir de w.
Systèmes axiomatiques
La logique épistémique la plus courante, connue sous le nom de S5, est caractérisée par les axiomes et règles suivants. L'axiome K stipule que si un agent connaît une implication et connaît son antécédent, alors l'agent connaît le conséquent : K_i(φ → ψ) → (K_i φ → K_i ψ). L'axiome T stipule que la connaissance implique la vérité : K_i φ → φ. L'axiome 4 (introspection positive) stipule que si un agent sait φ, alors l'agent sait qu'il sait φ : K_i φ → K_i K_i φ. L'axiome 5 (introspection négative) stipule que si un agent ne sait pas φ, alors l'agent sait qu'il ne sait pas φ : ¬K_i φ → K_i ¬K_i φ. La règle de nécessitation permet de dériver K_i φ à partir d'un théorème φ.
Des systèmes plus faibles assouplissent ces axiomes. La logique KT (également appelée T) abandonne les axiomes 4 et 5, permettant aux agents de manquer d'introspection. La logique S4 conserve l'axiome 4 mais abandonne l'axiome 5, souvent utilisée pour la croyance plutôt que pour la connaissance. Pour la croyance, l'axiome T est remplacé par l'axiome D : B_i φ → ¬B_i ¬φ, qui stipule que les croyances sont cohérentes mais pas nécessairement vraies. Ces distinctions importent dans les applications où les agents disposent d'informations incomplètes ou incorrectes.
Sémantique et mondes possibles
La sémantique des mondes possibles interprète la connaissance comme la vérité dans tous les mondes épistémiquement accessibles. Un modèle épistémique M = (W, R_1, ..., R_n, V) consiste en un ensemble de mondes W, une relation d'accessibilité R_i pour chaque agent et une valuation V attribuant des valeurs de vérité aux variables propositionnelles dans chaque monde. Pour la connaissance, chaque R_i est une relation d'équivalence (réflexive, symétrique, transitive), reflétant que les agents ne peuvent pas distinguer les mondes qui leur sont épistémiquement identiques. La condition de vérité pour K_i φ dans le monde w est : pour tout v tel que w R_i v, M, v ⊨ φ.
La connaissance commune, formalisée par David Lewis en 1969 et Robert Aumann en 1976, est définie comme la conjonction infinie de « tout le monde sait que tout le monde sait... ». Pour un groupe G, C_G φ est vraie si φ est vraie dans tous les mondes accessibles par toute séquence finie de relations d'accessibilité pour les membres de G. Ce concept est crucial pour l'action coordonnée dans les systèmes distribués et pour analyser les accords et les conventions.
Applications en informatique et en IA
La logique épistémique est devenue une pierre angulaire de la recherche sur les systèmes multi-agents dans les années 1980 et 1990. En 1985, Joseph Halpern et Yoram Moses ont publié des travaux fondateurs sur la connaissance et la connaissance commune dans les systèmes distribués, montrant comment les conditions épistémiques caractérisent la résolubilité de problèmes de coordination tels que le problème de l'attaque coordonnée. Le puzzle des enfants boueux, un exemple classique, démontre comment des annonces publiques d'ignorance peuvent générer une connaissance commune et permettre un raisonnement sur la connaissance d'ordre supérieur.
En intelligence artificielle, la logique épistémique fournit une base formelle pour la représentation et le raisonnement sur les connaissances. Elle a été appliquée pour modéliser des programmes basés sur la connaissance, où les actions des agents dépendent de leurs états de connaissance. Le cadre sous-tend également la planification épistémique, où les agents raisonnent sur ce que les autres savent pour atteindre des objectifs. En théorie des jeux, le résultat d'Aumann de 1976 sur l'accord pour être en désaccord a montré que si les agents ont une connaissance commune des croyances a posteriori de chacun, ils ne peuvent pas convenir d'être en désaccord, reliant la logique épistémique au raisonnement économique.
Logique épistémique dynamique
La logique épistémique dynamique (DEL), développée par Jan Plaza en 1989 puis étendue par Hans van Ditmarsch, Wiebe van der Hoek et Barteld Kooi, ajoute des opérateurs pour le changement de connaissance par des annonces publiques ou des communications privées. Une annonce publique de φ transforme le modèle en supprimant tous les mondes où φ est faux, et l'opérateur d'annonce [φ!]ψ stipule que ψ est vraie après l'annonce. Ce cadre capture des phénomènes tels que les effets de la révélation d'informations, du mensonge et de la tromperie dans des contextes multi-agents.
La DEL a été appliquée pour modéliser les protocoles de communication, les protocoles de sécurité et les interactions sociales. Par exemple, la logique des annonces publiques peut exprimer qu'après une annonce véridique de φ, les agents mettent à jour leurs connaissances en conséquence, créant potentiellement une nouvelle connaissance commune. Le cadre gère également des actions plus complexes comme les messages privés et les annonces simultanées, ce qui en fait un outil riche pour analyser le flux d'informations.
Développements récents et défis
La logique épistémique continue d'évoluer avec des connexions à la théorie des jeux, à la causalité et à l'apprentissage automatique. Les chercheurs ont exploré les conditions épistémiques pour le partage équitable, la confidentialité et la sécurité dans les systèmes multi-agents. La combinaison de la logique épistémique avec la probabilité, comme dans la logique épistémique probabiliste, permet de raisonner sur les degrés de croyance et de connaissance sous incertitude. Cela a des applications en théorie de la décision et dans la modélisation de systèmes d'IA qui maintiennent des croyances probabilistes sur leur environnement.
Un défi ouvert est la complexité computationnelle de la vérification de modèles et de la satisfiabilité dans les logiques épistémiques. Pour S5 avec plusieurs agents, la satisfiabilité est PSPACE-complète, tandis que la vérification de modèles peut être effectuée en temps polynomial pour des formules fixes. Les logiques épistémiques dynamiques ont souvent une complexité plus élevée, certaines variantes étant indécidables. Ces résultats de complexité guident la conception d'outils de raisonnement pratiques et limitent l'évolutivité de la vérification formelle dans les grands systèmes multi-agents.
Dans le contexte de l'IA moderne, la logique épistémique offre un langage formel pour spécifier ce qu'un système d'IA sait ou ne sait pas, ce qui est pertinent pour la transparence et la robustesse. Les chercheurs d'institutions telles que Stanford AI Lab et BAIR (Berkeley AI Research) ont exploré des connexions entre la logique épistémique et les modèles de Machine learning, en particulier dans des tâches impliquant le raisonnement des Large language model sur la connaissance et l'incertitude. Cependant, ces applications restent un domaine de recherche actif, et l'intégration directe de la logique épistémique dans les systèmes d'apprentissage profond est encore naissante en 2025.
Voir aussi
- Multi-agent system
- représentation des connaissances
- logique modale
- théorie des jeux
- vérification formelle