Jan van Eijck and Malvin Gattinger

Preparation：

To prepare for these lectures, students are advised to bring their own laptop. It would be nice if you manage to install the Haskell platform. You can find it at haskell.org/downloads, with instructions on how to install it for your operating system;

If you don't want to program you can forget about this, but then you will miss an opportunity to speed up your learning.

Abstracts:

Lecture 1: Logic, (Functional) Programming, Model Checking

2 Nov (Monday): 1:30-4:20 pm (Jan van Eijck), 新斋346

This lecture will set the stage by combining the topics of the title in various ways. First I will remind you that logic is part of every programming language, in the form of boolean expressions. Next, we will do a computational analysis of the language of boolean expressions, looking both at syntax and semantics. If the language of boolean expressions is enriched with quantifiers, we move from propositional logic to predicate logic. We will discuss how the expressions of that language can describe the ways things are, and we will look at model checking, and at the reverse side of the expressive power of predicate logic. The lecture ends with a brief sketch of epistemic model checking. In the course of the lecture we will connect everything with (functional) programming, and you will be able to pick up some Haskell as we go along.

Lecture 2: Dynamic Epistemic Model Checking With DEMO-S5 and PRO-DEMO

4 Nov (Wednesday): 1:30-4:20 pm (Jan van Eijck), 新斋346

This lecture introduces and discusses a tiny program for epistemic model checking with S5 models in Haskell. The model update operations are public announcement and publicly observable factual change. The implementation is much more efficient than the earlier implementation of DEMO (Van Eijck 2007), but less efficient than a symbolic model checker for DEL (Lecture 3). Still, because the approach is so simple, it gives a useful idea of what goes on in model checking DEL. As examples, we implement the sum and product riddle, which is solved in a few seconds, and the parametrized muddy children problems, where the cases with up to ten children run in a matter of seconds. Next, we look at PRODEMO, a program for probabilistic epistemic model checking, and use it for solving some probabilistic epistemic model checking problems.

Lecture 3: The Symbolic Approach to Dynamic Epistemic Model Checking

6 Nov (Friday): 1:30-4:20 pm (Malvin Gattinger), 6教6B111

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.

References:

Kees Doets and Jan van Eijck, The Haskell Road to Logic, Maths and Programming, Second Edition, College Publications, London, 2012. Also look here.

Jan van Eijck, DEMO-S5, CWI, Amsterdam, 2014.

Jan van Eijck and Malvin Gattinger, Towards Model Checking Cryptographic Protocols with Dynamic Epistemic Logic, Proceedings LAMAS (LAMAS 2015).

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

Malvin Gattinger, SMCDEL, Symbolic Model Checking for DEL Software.