New Directions in Model Checking Dynamic Epistemic Logic

Dynamic Epistemic Logic (DEL) can model complex information scenarios in a way that appeals to logicians. However, its existing implementations are based on explicit model checking which can only deal with small models, so we do not know how DEL performs for larger and real-world problems.

For temporal logics, in contrast, symbolic model checking has been developed and successfully applied, for example in protocol and hardware verification. Symbolic model checkers for temporal logics are very efficient and can deal with very large models.

In this thesis we build a bridge: new faithful representations of DEL models as so-called knowledge and belief structures that allow for symbolic model checking. For complex epistemic and factual change we introduce knowledge and belief transformers, a symbolic replacement for action models.

Besides a detailed explanation of the theory, the thesis presents SMCDEL: a Haskell implementation of symbolic model checking for DEL using Binary Decision Diagrams.

Our new methods can solve well-known benchmark problems in epistemic scenarios much faster than existing methods for DEL. We also compare the performance of the implementation to existing model checkers for temporal logics and show that DEL can compete with the established frameworks.

We zoom in on two specific variants of DEL for concrete applications. First, we introduce Public Inspection Logic (PIL), a new framework for the knowledge of variables and its dynamics. Second, we study the dynamic gossip problem and how it can be analyzed with epistemic logic. We show that existing gossip protocols can be improved, but also prove that no perfect strengthening of the "Learn New Secrets" protocol exists.

This research allows DEL to join the club of efficiently implemented and applicable logics. It opens up new directions, both towards real-world applications and further development of the theory of symbolic representation.