Symbolic model checking for Dynamic Epistemic Logic — S5 and beyond

Johan Van Benthem, Jan Van Eijck, Malvin Gattinger, Kaile Su

Research output: Contribution to journalArticleAcademicpeer-review

19 Citations (Scopus)
94 Downloads (Pure)


Dynamic Epistemic Logic (DEL) can model complex information scenarios in a way that appeals to logicians. However, existing DEL implementations are ad-hoc, so we do not know how the framework really performs. For this purpose, we want to hook up with the best available model checking and SAT techniques in computational logic. We do this by first providing a bridge: a new faithful representation of DEL models as so-called knowledge structures that allow for symbolic model checking. For more complex epistemic change we introduce knowledge transformers analogous to action models. Next, we show that we can now solve well-known benchmark problems in epistemic scenarios much faster than with existing methods for DEL. We also compare our approach to model checking for temporal logics. Finally, we show that our method is not just a matter of implementation, but that it raises significant issues about logical representation and update.
Original languageEnglish
Pages (from-to)367-402
Number of pages36
JournalJournal of Logic and Computation
Issue number2
Publication statusPublished - Mar-2018
Externally publishedYes




Dive into the research topics of 'Symbolic model checking for Dynamic Epistemic Logic — S5 and beyond'. Together they form a unique fingerprint.

Cite this