Authors: H.P. van Ditmarsch, J. Ruan, and W. van der Hoek
Abstract: We give a relation between a logic of knowledge and change, with a semantics on Kripke models, and a logic of knowledge and time, with a semantics on interpreted systems. More in particular, given an epistemic state (pointed multi-agent Kripke model where all accessibility relations are equivalence relations) and a formula in action model logic (a logic describing the consequences of epistemic events), we construct an interpreted system relative to that epistemic state and that formula that satisfies the translation of the formula into branching temporal epistemic logic. The construction involves that the protocol that is implicit in the dynamic epistemic formula, i.e. the set of sequences of events being executed to evaluate the formula, is made explicit. For presentation reasons, we focus on the logic of knowledge and change that is known as public announcement logic, which can be seen as a specific action model logic. The interpreted system that is constructed in the process is minimal in the sense that it precisely contains all the event structure present in the dynamic epistemic formula. Different approaches to this correspondence can be considered syntactic or semantic sugar. That observation brings applications of our insights closer, because some such approaches originate in the model checking community.
Keywords: modal logic, interpreted system, model checking, action logic, protocol, temporal logic
Download this paper in pdf.
BibTex:
@inproceedings{hvd.jr.wvdh.2007,
author = {H. van Ditmarsch and J. Ruan and W. van der Hoek},
title = {Model Checking Dynamic Epistemics in Branching Time},
booktitle = {Proceedings of Workshop on Formal Approaches to Multi-Agent Systems},
address = {Durham, UK},
month= September,
year = 2007}
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
}
Authors: H. van Ditmarsch, J. Ruan, and L.C. Verbrugge
Abstract: We model the well-known Sum-and-Product problem in a modal logic, and verify its solution in a model checker. The modal logic is public announcement logic. The riddle is then implemented and its solution verified in the epistemic model checker DEMO.
Download: this paper in pdf.
BibTex (from DBLP):
@inproceedings{DBLP:conf/ausai/DitmarschRV05,
author = {Hans P. van Ditmarsch and
Ji Ruan and
L. C. Verbrugge},
title = {Model Checking Sum and Product},
booktitle = {Australian Conference on Artificial Intelligence},
year = {2005},
pages = {790-795},
ee = {http://dx.doi.org/10.1007/11589990_82},
crossref = {DBLP:conf/ausai/2005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ausai/2005,
editor = {Shichao Zhang and
Ray Jarvis},
title = {AI 2005: Advances in Artificial Intelligence, 18th Australian
Joint Conference on Artificial Intelligence, Sydney, Australia,
December 5-9, 2005, Proceedings},
booktitle = {Australian Conference on Artificial Intelligence},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3809},
year = {2005},
isbn = {3-540-30462-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
Authors: Hans P. van Ditmarsch, Wiebe van der Hoek, Ron van der Meyden and Ji Ruan
Abstract: We implement a specific protocol for bit exchange among card-playing agents in three different state-of-the-art epistemic model checkers and compare the results.
Keywords: Cryptography, unconditional security, model checking, information-based protocols, epistemic logic.
Download: this paper in pdf.
BibTex: from DBLP
@article{DBLP:journals/entcs/DitmarschHMR06,
author = {Hans P. van Ditmarsch and
Wiebe van der Hoek and
Ron van der Meyden and
Ji Ruan},
title = {Model Checking Russian Cards},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {149},
number = {2},
year = {2006},
pages = {105-123},
ee = {http://dx.doi.org/10.1016/j.entcs.2005.07.029},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
This is my master thesis completed in the ILLC (Insitute for Logic Language and Computation) in October 2004.
Supervisors: Professor Johan van Benthem, and Professor Jan van Eijck
Abstract: In this thesis, I showed how BMS framework (the state-of-the-art Dynamic Epistemic Logic) models the cases of message passing, and proposed a logical axiomatisation called Logic CC. I then studied the sufficient and necessary conditions for two action models to have the same update effects, and proposed a structural relation between action models, named action emulation, to capture the same update effects for the propositional case. Finally, I discussed the problem of update evolution and showed a sufficient condition for the stabilization of update evolution.
Download: pdf from the ILLC website or from here.
BibTex:
@mastersthesis{jiruan2004,
author = “Ji Ruan”,
title = “Exploring the Update Universe”,
school = “ILLC Publications, Master of Logic Thesis Series”,
year = 2004
}
