Tsinghua University, November 2nd, 4th and 6th, 2015. Jan van Eijck and Malvin Gattinger
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 malvin@w4eg.eu or use this contact form.