Vérification symbolique de modèles pour la logique épistémique dynamique probabiliste - GREYC mad Access content directly
Conference Papers Year : 2021

Symbolic model checking for probabilistic dynamic epistemic logic

Vérification symbolique de modèles pour la logique épistémique dynamique probabiliste

Abstract

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.
Fichier principal
Vignette du fichier
article_jfpda.pdf (428.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03664513 , version 1 (11-05-2022)

Identifiers

  • HAL Id : hal-03664513 , version 1

Cite

Sébastien Gamblin, Alexandre Niveau, Maroua Bouzid. Vérification symbolique de modèles pour la logique épistémique dynamique probabiliste. Journées Francophones Planification, Décision et Apprentissage (PFIA) 2021, Jun 2021, Bordeaux, France. ⟨hal-03664513⟩
25 View
20 Download

Share

Gmail Facebook X LinkedIn More