Universiteit van Amsterdam

Archives

Institute for Logic, Language and Computation

Please note that this newsitem has been archived, and may contain outdated information or links.

13 October 2015, Logic Tea, Malvin Gattinger

Speaker: Malvin Gattinger
Title: From Muddy Children to Sum and Product in a few seconds -- Symbolic Model Checking for Dynamic Epistemic Logic.
Date: Tuesday 13 October 2015
Time: 17:00-18:00
Location: Room F1.13, Science Park 107, Amsterdam

Abstract

Dynamic Epistemic Logic (DEL) can model puzzles and complex information scenarios in a way that appeals to logicians. However, not much work on efficient implementations has been done and we do not know how the DEL framework performs in practice. In contrast, much progress has been made in
model checking for temporal logics. To use these ideas and move from explicit to symbolic model checking we provide a truth-preserving representation of Kripke models as knowledge structures with observational variables. On these structures we can translate every DEL formula to a boolean equivalent represented as a binary decision diagram (BDD).

The talk will first introduce a few logic puzzles and then give an introduction to DEL and symbolic model checking with BDDs. Finally, we show how large instances of the puzzles can be solved in a few seconds with our software.

For more information, please visit the website http://www.illc.uva.nl/logic_tea/ or contact Thomas Brochhagen (), Johannes Marti (), Masa Mocnik () or Julian Schloder ().

Please note that this newsitem has been archived, and may contain outdated information or links.