smcdel: Symbolic Model Checking for Dynamic Epistemic Logic

[ gpl, library, logic, program ] [ Propose Tags ]

See and SMCDEL.pdf for references and documentation.

[Skip to Readme]
Versions [faq] 1.0.0
Dependencies ansi-terminal, array, base (>=4.8 && <5), containers, cudd (==, directory, file-embed, filepath, graphviz, HasCacBDD (==, js-jquery (>=3), lens, process, QuickCheck, scotty, smcdel, tagged, template-haskell, temporary, text, time [details]
License GPL-2.0-only
Author Malvin Gattinger
Category Logic
Home page
Source repo head: git clone
Uploaded by m4lvin at Mon Feb 26 20:53:09 UTC 2018
Distributions NixOS:1.0.0
Executables smcdel-web, smcdel
Downloads 262 total (19 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2018-02-26 [all 2 reports]


    • SMCDEL.Examples
      • SMCDEL.Examples.CoinFlip
      • SMCDEL.Examples.DiningCrypto
      • SMCDEL.Examples.DrinkLogic
      • SMCDEL.Examples.GossipKw
      • SMCDEL.Examples.GossipS5
      • SMCDEL.Examples.MuddyChildren
      • SMCDEL.Examples.Prisoners
      • SMCDEL.Examples.RussianCards
      • SMCDEL.Examples.SallyAnne
      • SMCDEL.Examples.SumAndProduct
      • SMCDEL.Examples.WhatSum
    • Explicit
      • SMCDEL.Explicit.DEMO_S5
      • SMCDEL.Explicit.K
        • SMCDEL.Explicit.K.Change
      • SMCDEL.Explicit.S5
    • Internal
      • SMCDEL.Internal.Help
      • SMCDEL.Internal.Lex
      • SMCDEL.Internal.MyHaskCUDD
      • SMCDEL.Internal.Parse
      • SMCDEL.Internal.TexDisplay
      • SMCDEL.Internal.Token
    • SMCDEL.Language
    • Other
      • SMCDEL.Other.BDD2Form
      • SMCDEL.Other.Planning
    • Symbolic
      • SMCDEL.Symbolic.K
        • SMCDEL.Symbolic.K.Change
      • SMCDEL.Symbolic.S5
        • SMCDEL.Symbolic.S5.Change
      • SMCDEL.Symbolic.S5_CUDD
    • Translations
      • SMCDEL.Translations.K
        • SMCDEL.Translations.K.Change
      • SMCDEL.Translations.S5


Maintainer's Corner

For package maintainers and hackage trustees

Readme for smcdel-1.0.0

[back to package description]


Release Build Status

A symbolic model checker for Dynamic Epistemic Logic.

You can find a complete literate Haskell documentation in the file SMCDEL.pdf.


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.


You can try SMCDEL online here:


On Debian, just do sudo apt install graphviz dot2tex.

Basic usage

  1. Use stack from
  • stack build will compile everything. This might fail if one of the BDD packages written in C and C++ is missing. In this case, install those manually and then try stack build again.

  • stack install will put two executables smcdel and smcdel-web into ~/.local/bin which should be in your PATH variable.

  1. Create a text file 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
      [ ! (1|2|3) ] alices knows whether 1
      [ ! (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)
  2. Run "smcdel textfile" resulting in:

    >> smcdel MuddyShort.smcdel.txt
    SMCDEL 1.0 by Malvin Gattinger --
    At which states is ... true?
    Is ... valid on the given structure?

More example files are in the folder Examples.

Advanced usage

To deal with more complex models and formulas, use SMCDEL as a Haskell module.

Examples can be found in Examples.hs and the Bench folder.

Used BDD packages

SMCDEL can be used with different BDD packages. To compile and run the benchmarks you will have to install all of them.

Experimental Stuff

SMCDEL.Other.NonS5 implements general knowledge structures. They are equivalent to Kripke models which are not based on equivalence relations.