SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.

Online

You can try SMCDEL online here: https://w4eg.de/malvin/illc/smcdelweb/

Basic usage

1) Use stack from https://www.stackage.org

• stack install will build and install an executable smcdel into ~/.local/bin which should be in your PATH variable.

2) Create a text file MuddyShort.smcdel.txt which describes the knowledge structure and the formulas you want to check for truth or validity:

```
-- Three Muddy Children in SMCDEL
VARS 1,2,3
LAW  Top
OBS  alice: 2,3
     bob:   1,3
     carol: 1,2
WHERE?
  [ ! (1|2|3) ] alice knows whether 1
VALID?
  [ ! (1|2|3) ]
  [ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ]
  [ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ]
  (alice,bob,carol) comknow that (1 & 2 & 3)
```

3) Run smcdel MuddyShort.smcdel.txt resulting in:

```
>> smcdel MuddyShort.smcdel.txt
SMCDEL 1.0 by Malvin Gattinger -- https://github.com/jrclogic/SMCDEL

At which states is ... true?
[]
[1]

Is ... valid on the given structure?
True
```

More example files are in the folder [Examples](https://github.com/jrclogic/SMCDEL/tree/master/Examples).

4) To also build and install the web interface, run stack install --flag smcdel:web Then you can run smcdel-web and open http://localhost:3000.

Advanced usage

The executables only provide model checking for S5 with public announcements. For K and to define more complex models and updates, SMCDEL should be used as a Haskell library. Please refer to the Haddock documentation for each module.

Examples can be found in the folders src/SMCDEL/Examples and bench.

Dependencies: To get all visualisation functions working, graphviz, dot2tex and some LaTeX packages should be installed. On Debian, please do sudo apt install graphviz dot2tex libtinfo5 texlive-latex-base poppler-utils preview-latex-style texlive-pstricks.

Used BDD packages

SMCDEL uses different BDD packages.

• Data.HasCacBDD which runs CacBDD from http://kailesu.net/CacBDD/. This is the default choice used by the executables and the modules Symbolic.S5 and Symbolic.K.

• The pure Haskell library decision-diagrams. It is used by the module Symbolic.S5_DD.

• Optionally, Cudd (with some patches) which uses the CUDD library. To obtain the modules SMCDEL.Symbolic.S5_CUDD, SMCDEL.Symbolic.S5_K, SMCDEL.Symbolic.S5_Ki you should compile with stack build --flag smcdel:with-cudd.

References

Main reference for the theory behind the implementation, also containing benchmarks:

• Malvin Gattinger: New Directions in Model Checking Dynamic Epistemic Logic. PhD thesis, ILLC, Amsterdam, 2018.

Additional publications:

• Johan van Benthem, Jan van Eijck, Malvin Gattinger, and Kaile Su: Symbolic Model Checking for Dynamic Epistemic Logic. In: Proceedings of The Fifth International Conference on Logic, Rationality and Interaction (LORI-V), 2015.

• Johan van Benthem, Jan van Eijck, Malvin Gattinger, and Kaile Su: Symbolic Model Checking for Dynamic Epistemic Logic --- S5 and Beyond. Journal of Logic and Computation, 2017.

• Malvin Gattinger: Towards Symbolic Factual Change in DEL. ESSLLI 2017 student session, 2017.

• Daniel Miedema, Malvin Gattinger: Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic, TARK 2023, 2023