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. Next, we show that we can now solve well-known benchmark problems in epistemic scenarios much faster than with existing DEL methods. Finally, we show that our method is not just a matter of implementation, but that it raises significant issues about logical representation and update.
Null option (theme 11)
W. van der Hoek (Wiebe) , W.H. Holliday , W.-F. Wang
Lecture Notes in Computer Science
Logic, Rationality and Interaction
Software Analysis and Transformation

van Benthem, J. F. A. K, van Eijck, D.J.N, Gattinger, M, & Su, K. (2015). Symbolic Model Checking for Dynamic Epistemic Logic. In W van der Hoek, W.H Holliday, & W.-F Wang (Eds.), Logic, Rationality, and Interaction; 5th International Workshop, {LORI} 2015 (pp. 366–378). Springer.