09
May

Model Checking Logic Puzzles

Authors: Hans van Ditmarsch and Ji Ruan

Résumé :
Dans les puzzles épistémiques les annonces d’ignorance, ou des séquences de tels annonces, souvent résultent en connaissances. Nous présentons le puzzle ‘Quelle Somme ?’, et le modèlisent dans la logique des annonces publiques – un langage logique avec des opérateurs dynamiques et épistémiques. La solution du puzzle est controlée avec la programme de vérification DEMO.
Mots-clés : communications multi-agent, vérification des modèles, logique dynamique épistémique, annonce publique

Abstract:
A common theme in logic puzzles involving knowledge and ignorance is that announcements of ignorance may eventually result in knowledge. We present the ‘What Sum’ riddle. It is modelled in public announcement logic, a modal logic with both dynamic and epistemic operators. We then solve the riddle in the model checker DEMO.
Keywords: agent communication, model checking, dynamic epistemic logic, public announcement

Download: this paper in pdf.

BibTex:

@inproceedings{hvd.jr:2007,
author = “Hans van Ditmarsch and Ji Ruan”,
title = {Model Checking Logic Puzzles},
booktitle = “Proceedings of MFI07 (Quatriemes Journees Francophones MODELES FORMELS de l’INTERACTION)”,
pages = {139-150},
address = {Annales du Lamsade, Université Paris Dauphine},
year = 2007
}

No related posts.

Related posts brought to you by Yet Another Related Posts Plugin.

No Comments

(Required)
(Required, will not be published)