smcdel: Symbolic Model Checking for Dynamic Epistemic Logic

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

See README.md and SMCDEL.pdf for references and documentation.


[Skip to Readme]
Versions [faq] 1.0.0, 1.1.0
Change log CHANGELOG.md
Dependencies ansi-terminal, array, base (>=4.8 && <5), containers, cudd (==0.1.0.0), directory, file-embed, filepath, graphviz, HasCacBDD (>=0.1.0.1 && <0.2), js-jquery (>=3), process, QuickCheck, scotty, smcdel, tagged, template-haskell, temporary, text, time [details]
License GPL-2.0-only
Author
Maintainer Malvin Gattinger <malvin@w4eg.eu>
Category Logic
Home page https://github.com/jrclogic/SMCDEL#readme
Bug tracker https://github.com/jrclogic/SMCDEL/issues
Source repo head: git clone https://github.com/jrclogic/SMCDEL
Uploaded by m4lvin at 2019-12-09T19:53:20Z
Distributions NixOS:1.1.0
Executables smcdel-web, smcdel
Downloads 732 total (8 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2019-12-10 [all 2 reports]

Modules

  • SMCDEL
    • SMCDEL.Examples
      • SMCDEL.Examples.Cheryl
      • SMCDEL.Examples.CherylDemo
      • SMCDEL.Examples.CoinFlip
      • SMCDEL.Examples.DiningCrypto
      • SMCDEL.Examples.DoorMat
      • SMCDEL.Examples.DrinkLogic
      • SMCDEL.Examples.GossipKw
      • SMCDEL.Examples.GossipS5
      • SMCDEL.Examples.LetterPassing
      • SMCDEL.Examples.MuddyChildren
      • SMCDEL.Examples.MuddyPlanning
      • SMCDEL.Examples.Prisoners
      • SMCDEL.Examples.RussianCards
      • SMCDEL.Examples.SallyAnne
      • SMCDEL.Examples.SimpleK
      • SMCDEL.Examples.SimpleS5
      • SMCDEL.Examples.SumAndProduct
      • SMCDEL.Examples.WhatSum
    • Explicit
      • SMCDEL.Explicit.DEMO_S5
      • SMCDEL.Explicit.K
      • SMCDEL.Explicit.S5
    • Internal
      • SMCDEL.Internal.Help
      • SMCDEL.Internal.Lex
      • SMCDEL.Internal.MyHaskCUDD
      • SMCDEL.Internal.Parse
      • SMCDEL.Internal.TaggedBDD
      • SMCDEL.Internal.TexDisplay
      • SMCDEL.Internal.Token
    • SMCDEL.Language
    • Other
      • SMCDEL.Other.BDD2Form
      • SMCDEL.Other.MCTRIANGLE
      • SMCDEL.Other.Planning
    • Symbolic
      • SMCDEL.Symbolic.K
      • SMCDEL.Symbolic.S5
      • SMCDEL.Symbolic.S5_CUDD
    • Translations
      • SMCDEL.Translations.Convert
      • SMCDEL.Translations.K
      • SMCDEL.Translations.S5

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for smcdel-1.1.0

[back to package description]

SMCDEL

Release Hackage Build Status DOI

A symbolic model checker for Dynamic Epistemic Logic.

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

References

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.

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

Online

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

Dependencies

On Debian, just do sudo apt install graphviz dot2tex.

Basic usage

  1. Use stack from https://www.stackage.org
  • 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 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)
    
  2. 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.

Advanced usage

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

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

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.