Three Lectures on Dynamic Epistemic Model Checking

Tsinghua University, November 2nd, 4th and 6th, 2015. Jan van Eijck and Malvin Gattinger

See here for Lecture 1 and 2.

Lecture 3: The Symbolic Approach to Dynamic Epistemic Model Checking

Downloads: Lecture Slides, Exercises

Use SMCDEL online: SMCDEL web.

Software links: SMCDEL, HasCacBDD, CacBDD.

Main reference: Johan van Benthem, Jan van Eijck, Malvin Gattinger and Kaile Su, Symbolic Model Checking for Dynamic Epistemic Logic, LORI-V, 2015.

Dynamic Epistemic Logic can model complex information scenarios in a way that appeals to logicians. However, the simple minded approach to model checking from the previous lecture does not use state-of-the-art model checking techniques, and therefore does not give a good indication of how the framework really performs. To remedy this, 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. Next, we will demonstrate that we can now solve well-known benchmark problems in epistemic scenarios much faster than with the methods of the previous lecture. Finally, we show that our method is not just a matter of implementation, but that it raises significant issues about logical representation and update.

Contact Malvin Gattinger: email to or use this contact form.