Abstract

This paper introduces DEMO, a Dynamic Epistemic Modelling tool. DEMO allows modelling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, translation of dynamic epistemic formulas to PDL formulas, and so on. The paper implements the reduction of dynamic epistemic logic [16, 2, 3, 1] to PDL given in [12]. The reduction of dynamic epistemic logic to automata PDL from [24] is also discussed and implemented. Epistemic models are minimized under bisimulation, and update action models are minimized under action emulation (the appropriate structural notion for having the same update effect, cf. [13]). The paper is an exemplar of tool building for epistemic update logic. It contains the full code of an implementation in Haskell [22], in ‘literate programming’ style [23], of DEMO.