Dynamic Epistemic Model Checking
Jan van Eijck · 2015
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. Abstract 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. Update of the abstract: the slides give a full implementation of public announcement updates for S5 models and for S5 weight models.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. Update of the abstract: the slides give a full implementation of public announcement updates for S5 models and for S5 weight models. Who in Modal and Epistemic Logic? Who in Modal and Epistemic Logic? Saul Kripke (born 1940) Jaakko Hintikka (1929–2015)