Symbolic model checking for probabilistic dynamic epistemic logic
Vérification symbolique de modèles pour la logique épistémique dynamique probabiliste
Résumé
Probabilistic Dynamic Epistemic Logic (PDEL) allows reasoning about the nested probabilistic knowledge of agents and the knowledge changes induced by the occurrence of events. Although PDEL has been studied theoretically, it has only been applied to toy examples: indeed, the combinatorial explosion of Kripke structures does not allow the formalism to be used directly for real applications, such as card games. The present paper is a first step towards the use of PDEL in practice: in the continuity of recent works on (non-probabilistic) DEL model checking, we propose a "symbolic" representation of probabilistic Kripke structures with pseudo-Boolean functions, which can be represented by data structures from the family of decision diagrams, in particular algebraic decision diagrams (ADDs). We show that ADDs scale better than explicit Kripke structures, and allow for efficient symbolic model checking, even on a realistic example of the Hanabi card game, thus paving the way for the practical application of epistemic planning techniques.
La logique épistémique dynamique probabiliste (PDEL) permet de raisonner sur les connaissances probabilistes imbriquées des agents et sur les changements de connaissances induits par l'occurrence d'événements. Bien que PDEL a été étudiée de manière théorique, elle n'a été appliquée qu'à des exemples jouets : en effet, l'explosion combinatoire des structures de Kripke ne permet pas d'utiliser directement le formalisme pour des applications réelles, comme des jeux de cartes. Le présent article constitue un premier pas vers l'utilisation de PDEL en pratique : dans la continuité des récents travaux sur la vérification de modèles de DEL (non probabiliste), nous proposons une représentation "symbolique" des structures de Kripke probabilistes avec des fonctions pseudo-booléennes, représentables par des structures de données de la famille des diagrammes de décision, en particulier les diagrammes de décisions algébriques (ADDs). Nous montrons que les ADDs passent mieux à l'échelle que les structures de Kripke explicites, et permettent une vérification symbolique de modèles efficace, même sur un exemple réaliste du jeu de carte Hanabi, ouvrant ainsi la voie à l'application pratique de techniques de planification épistémique.
Origine : Fichiers produits par l'(les) auteur(s)