Muddy Children drawing by Sarah Vollert

New Directions in Model Checking Dynamic Epistemic Logic

PhD thesis by Malvin Gattinger at ILLC, University of Amsterdam, 2018.

Full text: gattinger-thesis.pdf

Abstract: gattinger-thesis-abstract.txt

Samenvatting: gattinger-thesis-samenvatting.txt

BibTex file: gattinger-thesis.bib

Mistakes and corrections: gattinger-thesis-errata.pdf

Abstract

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.

Links

SMCDEL:

Other mentioned and related work:

For other PhD candidates at ILLC:
ILLC Dissertation Style with some adjustments and scripts.

Defense

2018-06-13 at 11:00
in the Aula of the University of Amsterdam, Singel 411

Joint Workshop with Chenwei Shi

2018-06-12 from 9:30 to 16:30
Details can be found here on the LIRa website.

MoL project

In June 2018 there was a MoL project related to the topics of this thesis: Functional Programming for Logicians.

CC-BY-SA 2018 Malvin Gattinger